This is a piece of current output of a proof assistant, and a translation showing how a mathematician would write down the same information. The example shows that formal mathematics need not look like an indigestible mess of low level proof information.
The source is taken verbatim from ''Basis proofs for system C4, the pure implicational fragment of S4'' (by John Halleck), and was translated by hand.
# Proof output notation
=format cs
# ----------------- Proof: --------------------
# Produced Mon Jan 5 10:20:43 2009
# by the "shotgun" program, version 2009-01-01 0.01.002
# Input files:
# "input.c4.anderson-belnap"
# "wishlist.c4.EFHW-2base1"
# Name of this logical system.
=name C4
# Axiomatic Basis:
=basis Anderson and Belnap
# --- Axioms ---
1: p -> p # Axiom 1
2: (p -> q) -> (r -> (p -> q)) # Axiom 2
3: (p -> (q -> r)) -> ((p -> q) -> (p -> r))
# Axiom 3
# --- Wish List ---
=wishlist "p -> (q -> q)" "EFHW 2base1 Axiom 1"
=wishlist "(p -> (q -> r)) -> ((p -> q) -> (s -> (p -> r)))" "EFHW 2base1 Axiom 2"
# --- Theorems ---
# Wish list theorem: EFHW 2base1 Axiom 1
4: p -> (q -> q) # Condensed detachment, inference line 2 with line 1
5: p -> ((q -> r) -> (s -> (q -> r))) # Condensed detachment, inference line 2 with line 2
6: (p -> (q -> r)) -> (p -> (s -> (q -> r)))
# Condensed detachment, inference line 3 with line 5
7: p -> ((q -> (r -> s)) -> ((q -> r) -> (q -> s)))
# Condensed detachment, inference line 2 with line 3
8: (p -> (q -> (r -> s))) -> (p -> ((q -> r) -> (q -> s)))
# Condensed detachment, inference line 3 with line 7
9: (p -> q) -> ((r -> p) -> (r -> q)) # Condensed detachment, inference line 8 with line 2
10: ((p -> q) -> (r -> p)) -> ((p -> q) -> (r -> q))
# Condensed detachment, inference line 3 with line 9
11: (((p -> q) -> (p -> r)) -> s) -> ((p -> (q -> r)) -> s)
# Condensed detachment, inference line 10 with line 7
# Wish list theorem: EFHW 2base1 Axiom 2
12: (p -> (q -> r)) -> ((p -> q) -> (s -> (p -> r)))
# Condensed detachment, inference line 11 with line 6
# Final proof had 12 lines (9 steps)
# ------------------ End proof --------------
# Summary of 2 wish list items proven:
# (p -> (q -> r)) -> ((p -> q) -> (s -> (p -> r))) # EFHW 2base1 Axiom 2
# p -> (q -> q) # EFHW 2base1 Axiom 1
My view is that proofs intended to be read by humans should look
like proofs one reads in ordinary math textbooks or papers.
Thus in place of the original example, I'd like to see something
close to the following. (L1) is the original line 4, (L2) is the
original line 12. (1) is the original line 6 and (2) is the original
line (7).
We consider the following three axioms (I1)-(I3):
(I1) p -> p
(I2) (p -> q) -> (r -> (p -> q))
(I3) (p -> (q -> r)) -> ((p -> q) -> (p -> r))
Proposition 1.
In a system satisfying (I1)-(I3), we have
p -> (q -> q), (L1)
(p -> (q -> r)) -> ((p -> q) -> (s -> (p -> r))). (L2)
Proof.
(i) (L1) follows from (I1) and (I2) by inserting q=p.
(ii) Applying (I2) twice gives
p -> ((q -> r) -> (s -> (q -> r))),
so that
(p -> (q -> r)) -> (p -> (s -> (q -> r))) (1)
by (I3). From (I2) and (I3), we find
p -> ((q -> (r -> s)) -> ((q -> r) -> (q -> s))), (2)
which implies
(p -> (q -> (r -> s))) -> (p -> ((q -> r) -> (q -> s)))
by (I3). Therefore, by (I2),
(p -> q) -> ((r -> p) -> (r -> q)),
so that
((p -> q) -> (r -> p)) -> ((p -> q) -> (r -> q))
by (I3). Together with (2), this implies
(((p -> q) -> (p -> r)) -> s) -> ((p -> (q -> r)) -> s),
and using (1), we conclude (L2).
QED.
The above reduces the output to what humans can easily read and need to be able to check the proof without thinking. It should also be readable by an automaton: A formal proof checker should be able to figure out by itself that in each step, the method to be applied is condensed detachment. (Alternatively, one could add in the beginning the statement: ``Each individual step is proved by condensed detachment.'')
The other words in the verbal proof can be given a concise meaning so that the proof checker knows how to translate them back into its internal code, which the original current output tries to mirror faithfully but with a verbosity irritating a human reader. One could even give the translation key to make the informal looking proof really formal.
The ``translated'' proof is just the original proof, line by line. (i) indicates the start of the proof of the first statement of the wish list, (ii) the start of the second. No programming language is so stupid that it cannot easily do automatically all the changes that I made.
I just used my own (brain-wired) rewrite system to turn the original text line by line into my version, checking at the end what was referenced by my version to relabel the items. (Since the proposition is not of real interest to me, I didn't even check the correctness, relying on the output of the "shotgun" program for this.)
Proposition 1 is simply the wish list for the original first example. I gave it the name Proposition 1 to give the original claim proved a familiar form.
Note that I only removed the references to statements immediately preceding, and replaced them by words that say whether the preceding is in fact used. Thus the human reader lost no piece of information that the original version had.
Arnold Neumaier
Added July 1, 2022: For a detailed formal proof of a well-known result
that translates fairly nicely into a human-readable proof see
W. Neumaier,
Irrationality of the square root of 2.
Proofs in a universal logic calculus, Manuscript, Juni 2022.
my home page (http://arnold-neumaier.at/)
Arnold Neumaier (Arnold.Neumaier@univie.ac.at)