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

[Michael Thayer]

At 01:38 PM 10/30/2003 +0200, Arnon Avron wrote:

>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 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'?

That is where the various types of Relevant (or Relevance) Logic natural deduction systems might come in handy.

It would be interesting to know Harvey's views on this approach to Baldwin's concerns, given that he has investigated Relevance Logics.