[FOM] Comment on formalization of proofs

[Harvey Friedman]

In my postings #182-185, Ideas in proof checking 1-4, 6/21/03 - 6/25/03, I
emphasized the proof style of always arguing for contradictions, in a
tableaux like setup.

I had some specific reasons for this related to user interface then, and
also now in terms of a uniform standard for writing proofs on paper that are
to be easily read (texts).

I now see clearly how to incorporate the idea of assumptions/goals into this
framework without losing the simplicity and uniformity that I had in mind,
both in the user interface and in easily readable text.

So in this modified setup, arguing for contradictions is replaced by arguing
for a specified goal statement.

I expect to take these issues up in some detail after some intensive
investigations, by late October or early November.

Harvey Friedman