[FOM] What is a proof? Not a Hilbert-type proof!

[Arnon Avron]

> Standard Definition. 1. A proof is a sequence of propositions each of 
> which is either an axiom or follows from those earlier in the list by a 
> rule of inference.

This is a standard definition of a proof in a Hilbert-type system. It
is unquestionably the simplest type of proof, and arguably the basic
one. However, it is not the type of proofs one finds in mathematical
papers, and it is useless for the questions you raise. 
> 
>  From the standpoint of Position B, the defect of Definition 1, is that 
> there is no criteria of relevance of the steps of the proof to the 
> result.  If we interpolate a sequence of tautologies in a proof (maybe 
> many times the length of the original proof) it is still a proof by the 
> (inadequate) definition 1).
> 
> This problem could be addressed by
> Definition. 1'. A proof is a sequence of propositions each of which is 
> either an axiom or follows from those earlier in the list by a rule of 
> inference and each line is a premise of some later step.

This solves nothing. It is still possible to throw into a proof
any tautology anywhere. For example, suppose at a certain point 
in the proof C was obtained, and you want to throw the tautology D
into the proof. Well, just add the sequence C->(D->C), D->C , D, C
after the first C, and continue the proof as before...

  You might in response add another condition: that no proposition in the
proof is proved twice. In such a case all we need to do is something
a little bit more complicated. Suppose the given proof of B
is A_1,..., A_n=B. Create the sequence D->A_1, ..., D->A_n. Turn it
into a full proof of D->A_n (i.e. D->B) using the method of the standard
proof of the propositional deduction theorem. Then add D and B to the
resulting sequence, getting a proof of B in which D is "used".

Note that these problems are well known.  The problem of relevance in proof 
is n fact the main focus of what is 
known as relevance logic (see e.g. Dunn's chapter in vol. 6 of the
new edition of the handbook of Philosophical logic). In this logic
(or rather: these logics) the validity of C->(D->C) is rejected. 
This rejection allows the construction of a Hilbert-type system, R_{->},
for purely implicational logic in which A->B follows from a set
of assumptions T iff there is a proof of B from
T and A in which A is actually used the system (R_{->} was originally 
developed by Church). However, there are difficulties when conjunction 
is added.  Thus if one adds to R_{->} A->(B->A&B), A&B->A and A&B->B as 
new axioms then C->(D->C) becomes derivable, and the whole idea collapses.

 In any case it is clearly impossible to define an appropriate notion of a 
relevant proof within the framework of Hilbert-type systems
for classical (or even intuitionistic) 
logic. On the other hand (as Tate has pointed out) the technical problem
you raised is formally solved in the framework of natural deduction
by the notion of a normal proof (and the normalization theorem).
I doubt, however, if this notion helps much
in clarifying the idea of `proof as explanation'. Thus the simple
tautology A->(A->A)->A has an infinite set of different normal proofs
(corresponding to Church numerals). Are they all `explanatory'?


Arnon Avron