[FOM] Theory of Actual Proofs

[Harvey Friedman]

Reply to Tennant 7:57PM 6/17/03.

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

I cut my posting of 2PM 6/17/03 off before I could get to such 
issues, issues that I am fully aware of.

1. My proposal concerns actual mathematical proofs. In nontrivial 
actual mathematical proofs, there are all kinds of assertions that 
are made in the course of that proof. Many of these assertions are in 
the form of quoting previously obtained results. E.g., typically a 
nontrivial Theorem is preceded by a number of Lemmas. The proofs of 
each Lemma may typically quote earlier Lemmas, as well as earlier 
Theorems. The proof of the Theorem itself will generally quote 
earlier Lemmas as well as other previously obtained results.

2. I have not seriously explored the consequences of my proposal in 
the context of various formalisms. But actual mathematics rules, not 
toy examples in logically convenient formalisms.

3. The way model trees come in to the way I want to formalize 
mathematics is as follows. In order to give a proof of a Theorem, one 
first imports a handful of previously obtained results, or perhaps 
instantiations of previously obtained results, including 
instantiations of axioms of ZFC, (instantiations of free variables 
that are implicitly quantified). The importation should be sufficient 
to logically imply the Theorem being proved. Then the model tree must 
be finite. However, the model tree might be complex. One requirement 
on mathematical text with proofs is that these imports are spelled 
out, and ALL model trees are required to be simple. In particular, 
they are very feasibly computer obtainable. In other words, in this 
approach, ALL PROOFS ARE TRIVIAL LOCALLY. The nontrivial steps are 
the importations, and the constructions of suitable Lemmas.

4. A typical objection to this approach is that one might want to 
argue by reductio on a creative hypothesis. I.e., suppose we want to 
prove Theorem T. We argue inside the proof that suppose A holds. Then 
T follows. And suppose A fails. Then T follows. We have all done this 
kind of proofs. But then it would be required that we create two 
Lemmas:

LEMMA 1. Suppose A. Then T.

LEMMA 2. Suppose notA. Then T.

And then we have:

THEOREM. T.

with a completely trivial proof by importing Lemmas 1 and 2.

5. Another typical objection is that the proof of the Theorem may run 
into an existential quantifier, where the term is not right in front 
of your face. There are two ways I am thinking of handling this.

The first is to maintain, come what must, the idea that every proof 
is trivial. So what I would do here is to again force one to break 
this up into Lemmas. The nontrivial construction (i.e., term) will 
actually appear in the statement of the Lemmas. Or, if the theorem is 
itself existential, or AE, then state a stronger theorem with the 
extra information that the term works. Then there would be again a 
trivial model tree because the term is right in front of your face.

I guess I would prefer, at first, the all out attempt to make every 
proof a trivial model tree. Nontrivial proofs by cases or reductio on 
a statement, have the cases or statement appear in the Lemmas. 
Nontrivial constructions; i.e., terms, would actually appear also in 
the statement of the Lemmas.

6. One might call my model of mathematical practice, Administratively 
Broken Down Proof Development. Everything is broken down, 
administratively, into bite sizes that have trivial model trees.

7. Above and beyond all, this must be done so that it is entirely 
readable, and flows perfectly mathematically. Everything nontrivial 
is above board. What is suppressed is completely routine trivial 
model trees.

8. In fact, it may even be more readable than technical Journal 
articles! Of course, it is extremely time consuming to prepare. You 
would have to know the ins and outs of elementary things far better 
than people see any reason to know them. You would have to know them, 
say, at the level a professional pianist knows the  Piano Concertos 
he plays with Orchestra. But it is not necessary to have this extreme 
knowledge in real time, as a pianist must have.

9. But can be apply such ideas to some standard formal systems? 
Again, this is an interesting, but secondary question, as the real 
question is how we should model mathematical proofs.

10. Let's take a Hilbert style proof system for propositional logic 
first. Let us say that we have two proofs of the same propositional 
formula, with no hypotheses. We can ask about the set of lines in the 
proof, all of which are valid formulas.

11. One immediate question that comes to mind is this. Does every 
tautology have a Hilbert style proof where every line except the last 
is a trivial tautology?

12. Also, consider a sequent calculus. Here every line of the proof 
is a sequent, even if it is in tree form. Every sequent is obviously 
a formula, by conjuncting the left side, disjuncting the right side, 
and using implication for the sequent sign. So my proposal makes some 
sense in the context of sequent calculus.

13. Even in natural deduction, at every stage in a natural deduction 
proof, there is a set of working assumptions, and a statement being 
asserted. This is also a formula, by taking the conjunction of the 
working assumptions and arrowing the statement being asserted.

I'll stop here.

Harvey Friedman