[FOM] Theory of Actual Proofs

[Harvey Friedman]

Reply to Guglielmi 2:22PM 6/16/03.

>I don't believe that linear logic has a direct relevance for the 
>foundations of mathematics, and, at least as it stands now, it is 
>not foundational for computer science. So, for me linear logic is 
>different than intuitionistic logic, or relevance logic: these 
>logics come with a philosophy, they aim at being foundational. 
>Linear logic is just an algebraic theory.
>
>On the other hand, I believe that linear logic might have a 
>beneficial indirect effect on the foundations of mathematics, and 
>could be further developed to become a foundation for computer 
>science.

I think all subscribers appreciate this frank assessment. I now feel 
less guilty/stupid for having ignored linear logic.

>
>I'd say that proof theory is still seriously underdeveloped, as 
>witnessed by the fact that we are still not able to answer the 
>question: `When are two different mathematical proofs essentially 
>the same?' (it's not even clear how to define being `essentially the 
>same'); and supposing we know that: `Given two proofs, can we decide 
>that they are the same?'.
>
>One of the reasons for our inability is that proof theory is 
>currently suffocated by bureaucracy, meaning that proofs are 
>cumbersome objects, which leave us very little freedom of 
>manipulation and analysis.

Let me mention a possible approach to this problem of equivalence 
between proofs - and also the problem of bureaucracy.

First of all, one should aim for informative equivalence relations 
between proofs, without having to assert that one has really found 
THE notion of identity between proofs.

I have been working on sorting out notions of trivial proof. These 
are proofs that have no ideas, and are forced upon us by routine 
unraveling of the theorem being proved. I will be more precise later 
this later, as there are some crucial ambiguities that need to be 
clarified here. In any case, all trivial proofs will be regarded as 
the same proof - the trivial proof.

So what significant equivalence relation do we want to place on proofs?

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.

There is a problem conducting serious research on such ideas, and 
even the more elemental problem of uncovering appropriate notions of 
"trivial proof".

There is only one real source of representative proofs of varying 
depth that is appropriate for such research. It is from actual 
elementary mathematics. State of the art mathematics is much too 
unwieldy for this kind of study (at this time), and there is already 
much more than enough in actual elementary mathematics.

The trouble is that even quite elementary mathematics, when fully 
formalized, is unwieldy and unreadable unless one is casting it in a 
particularly flexible formal language.

One can try to provide the most convenient possible formal language, 
equipped with rigorous semantics, for the practicing mathematician, 
where validity is r.e., of course. This is a very worthy project, 
which is particularly vital for creating, say, a database of 
mathematical information. The problem is, of course, to do this so 
well that a mathematician can profitably search such a database. I 
believe that this can be, and will be, done so well as to be a useful 
tool for mathematicians. But that is another project.

Coming back to the matter at hand, it will be sufficient to use a 
reasonably sophisticated form of first order ZFC for this study. 
There is a happy medium that is enough so that one can study serious 
examples of actual proofs.

After the construction of this form of ZFC, which flexibly supports 
undefined terms, and abbreviations, the first issue that comes up is: 
what is a mathematical theorem?

A mathematical theorem is not simply a sentence (or formula) in the 
language of set theory that is provable in ZFC. Serious mathematical 
theorems can rarely be stated in such primitive notation.

Instead, I take it to be given by a finite sequence of formulas, 
where all entries in the sequence except the last entry, is the 
introduction of a relation, constant, or function by explicit 
definition. (Allowing undefined terms alleviates any responsibility 
for proving existence or uniqueness when making these definitions). 
The final entry in the sequence is the actual theorem, and is given 
using only the symbols previously defined in the sequence, together 
with the primitives of ZFC.

The theorem is considered valid if and only if every model of ZFC 
plus all of the entries except the last, is a model of the last entry.

If this is to be used as a model of mathematical practice, then we 
consider the  stuff above embedded in a wider structure.

Thus we come to the notion of a Mathematical Development over ZFC. A 
MD over ZFC has absolutely no proofs. Instead, it is a sequence of 
formulas, every one of which is

i) an explicit definition of a new symbol using only symbols that 
have appeared previously or are the primitives of ZFC. These are 
labeled DEFINITION. Or,

ii) a formula using only symbols that have appeared previously, and 
is labeled THEOREM.

The MD over ZFC is considered valid if and only if every statement 
labeled THEOREM holds in every model of ZFC in which all previous 
entries labeled DEFINITION hold. Inductively, this is the same as 
requiring that every statement labeled THEOREM holds in every model 
of ZFC in which all previous entries hold.

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 proper use of model trees allows us to "write" proofs with almost 
no symbols, relieving us of nearly all of the "bureaucracy" that you 
refer to. The only thing that needs to be written down is what 
corresponds to the nontrivial "idea". And to verify that the mere 
writing down of the "ideas" in proper form, results in a correct 
proof, is best done by a piece of software that generates the 
required model trees. Given the setup, one knows in advance that the 
construction of the appropriate model trees is efficient - otherwise 
an "idea" is missing.

When this is set up properly, one can then redo elementary 
mathematics in this way, where only ideas appear in the human proof. 
The rest is taken care of by the software.

Of course, the main "ideas" needed are often the citation of relevant 
previously established facts, including the specification of 
instances of schemes.

I never liked schemes here, but I think that they are just too useful 
a tool to remain unused for such research.

Enough for now. I would be interested to see if people are interested...

PS: There is one arena where these ideas may need some significant 
sharpening. That is, in the arena of algebraic manipulations. It may 
be somewhat unsatisfactory to have to quote just what algebraic facts 
(equalities and inequalities) one is using. Rather, one may wish to 
import packages into the picture. Packages are essential for normal 
automated theorem proving projects of various kinds, but that's not 
what we are talking about. We are talking about a theory of actual 
proofs without "bureaucracy", something quite different.

Harvey Friedman