[FOM] Theory of Actual Proofs

[Neil Tennant]

On Tue, 17 Jun 2003, Harvey Friedman wrote:
 
> My proposal of the condition to study is this. Every assertion made 
> in the first proof has a trivial proof from the set of assertions 
> made in the second proof, and every assertion made in the second 
> proof has a trivial proof from the set of assertions made in the 
> first proof.

This presupposes---does it not?---that we have a way of identifying what
counts as an "assertion" within a proof. With a Frege-Hilbert style of
proof, this is unproblematic: every line or sentence in such a proof
counts as an assertion. But with a natural-deduction style of proof, not
every sentence-at-a-node is really an assertion. There are, for example,
assumptions made for reductio ad absurdum; or for conditional proof; or
for existential elimination; or for proof by cases. The person
constructing the proof would not, in general, be committed to asserting
any of these---nor, for that matter, many of the sentences following from
them within the proof.

So my first question is: For one whose preferred style of proof is natural
deduction, how are we to understand and apply the condition quoted above?

> Now how are we going to talk about proofs, and in particular trivial 
> proofs? Or the level of triviality of a proof?
> 
> I use the Beth tableaux idea as a uniform gold standard. I am hereby 
> going to collectively call of the relevant variants of Beth tableaux 
> that are important in this approach, model trees. I say model trees 
> because they are exactly the trees you would most naturally use to 
> try to construct countermodels. Remember that a formula is valid if 
> and only if various associated model trees have no infinite path if 
> and only if various associated model trees are finite.

The same question would apply to Beth tableaux or model trees. Not every
sentence occurring in a tableaux- or tree-"proof" can be construed as an
assertion that the prover would be prepared to make. Let's illustrate this
with the trivial example of a Beth-tree-"proof" of the argument

	(x)(Ax -> Bx)
	(x)(Bx -> Cx)
    So, (x)(Ax -> Cx)

The idea behind a Beth-tree-"proof" is to take the premises, along with
the negation of the conclusion, to form the trunk of the tree (which here
we shall make branch downwards). One then applies branching-rules to
develop the branches in such a way that they all close off with explicitly
contradictory pairs of sentences on them. Here is such a tree-"proof" for
our example:

		(x)(Ax -> Bx)
		(x)(Bx -> Cx)
	       ~(x)(Ax -> Cx)  [initial trunk ends;
			       application of branching rules begins]
	       Ex~(Ax -> Cx)   ... rule turning ~(x) into Ex~
		 ~(Aa -> Ca)   ... rule for dealing with Ex (a is "new")
		      Aa    )
		     ~Ca    )... rule for dealing with negated conditional
		    Aa -> Ba   ... rule for instantiating (x)
		    Ba -> Ca   ... ditto
		     /  \
		  ~Aa   Ba     ... rule for dealing with ->
		   #   /  \
		     ~Ba   Ca  ... ditto
		      #    #   all branches now contain contradictions
		     

Clearly, only the first two lines are ones that the prover would be
willing to assert (assuming that they serve as the two "axioms" for the
derivation of the "theorem" (x)(Ax -> Cx)).

So my second question is: how does the choice of Beth tableaux as the
"gold standard" sustain the suggested criterion for equivalence of proofs?
Does my example not create any problems because of its triviality and
degeneracy? Or have I identified a difficulty in principle for the
proposed approach?

Neil Tennant