[FOM] Re:Certainty (Ideas in Proof Checking)

[William.Piper@colorado.edu]

Hello all,
    I just want to introduce myself to the group and ask a few questions of Dr.
Friedman. My name is Everett Piper and I am a third year student at CU Boulder.
I am currently interested in logic and foundational issues, hence why I joined
this group. Alright, down to it then:
    I agree with Dr. Friedman in that we should develop a standard formal
notation and that, yes, there will be great difficulties in developing a
standard informal notation, but this should be a central aim of at least some
FOMers. I am not volunteering for such a massive project at this time, but I
would be interested in the future. I don't personally believe that a primary
task of mathematicians is to verify proofs. I do however believe that there is
such a thing as certainty and that it can, in principle, be verified. This would
seem to be a secondary task for a universal or standard formalism, the primary
task being to communicate mathematical ideas and proofs. I happen to believe
that mathematicians primarily create and communicate these creations to others,
so a standard language would be of great economy to mathematicians. I am,
however, not a working mathematician but a student, so if I sound naive, please
forgive me.
    I do have a question concerning the proof program Dr. Friedman is
describing. I actually have several. One, is this a real program being developed
by you or your colleagues or is it some sort of grand idea that may come to be
in the near future? 
    Two, I like the idea of forcing predicates or functions or theorems to be
absurd and I can tell how this will be useful to the philosopher in making
arguments (formal or informal) but I am not sure this will be terribly useful
for any interesting mathematics. Correct me if I am wrong, but if we have a
formal system capable enough to express number theoretic relations, shouldn't we
arrive at statements in number theory that will not be absurd to the computer?
What I mean by this is, assuming F(A) for some number theoretic statement A does
not guarantee a tree model with "closed branches", i.e. there will be some
branches of the tree undecided and so we cannot say whether F(A) is absurd or
T(A) is absurd, and hence we can have no certainty (I'm not sure this the right
word I would like to use here) of either case. I feel like this is closely
related to the halting problem. If this doesn't make sense right now, feel free
to write me back so that I can clarify. 
    Three, in light of what I have just said, I am a little unclear as to
whether or not this ideal program of yours is intended to simply verify or
simply to construct proofs. I believe you imply that it will be useful to
construct proofs, but I can only guess that it will help in constructing only
trivial proofs. Perhaps I am being impatient, but I would like very much to know
what you mean by "TRIVIAL". I am very intrigued to see if your conception of
trivial is solely related to the complexity of a given statement A or if it
encompasses the informal notion of triviality, which to me says "little or no
effort (mental or physical) is required on the part of the mathematician in
proving A.  In either case, I would be glad to hear your reply.

Sincerely, 
Everett