[FOM] EFQ and Faithful Formalization--reply to Alan Weir

[Tennant, Neil]

Alan Weir asks

"I wonder if Neil would sign up to this, or something close to it:

All (or the overwhelming majority) of good informal proofs are such that if they admit of formalization at all, they admit of a formalization in Core Logic which competent experts would agree is faithful to the informal proof."

Yes, with "Classical" inserted, since so much mathematics is done with classical logic.

Alan says

"...two formalised proofs, each of the same conclusion from the same premisses, may differ radically in terms of faithfulness to an informal proof of that conclusion from those premisses."

Agreed. One of the proofs might faithfully regiment the informal reasoning, and the other proof not. This entails that the two formalized proofs exploit different 'lines of reasoning'. Here is a toy example--so simple it's almost silly, but it makes the point clearly.

Gottlob gives the following informal proof of (A or B) from (B and C):

                Suppose A and B. Then B follows. So, A or B.

Alfred formalizes this informal proof faithfully as follows, paying careful attention to Gottlob's text:

                A&B
                ____
                  B
                ____
                 AvB

Kurt, by contrast, knows only what Gottlob wanted to prove, and works out his own formal proof, without paying any attention to Gottlob's informal proof. Kurt's formal proof is

                A&B
                ____
                  A
                ____
                 AvB

The two formal proofs exploit different lines of reasoning. Alfred's formal proof is faithful to Gottlob's informal one; while Kurt's formal proof is not.

Matters get more interesting when we discover from the Nachlass of Gottlob's wife that her husband agonized over the original problem, and produced what he regarded as two *distinct* informal proofs. In her diary it is recorded that he was obsessed with always trying conjunction eliminations by focusing first on the right-hand conjunct. He would only ever bring down the lefthand conjunct in cases where he could not make do with the righthand one. [By the way, it is very easy to inadvertently program an automated deducer to behave like Gottlob in this regard!] The good Frau notes her deceased spouse's fixation with all that is on the right, and reports that he nevertheless thought he had found *two* distinct informal proofs in the following, both of them fixated on the righthand conjunct:

Informal Proof #1:  I want to prove the disjunction (A or B). I can do so if I can prove B. Let's try that tack ... Now, I am given (A and B). Wunderbar! we haff B.

Informal Proof #2:  I am given (A and B). So, B follows. We have to prove (A or B). Hah!--we are done!

Unfortunately, Alfred's earlier formal proof

                A&B
                ____
                  B
                ____
                 AvB

will not do justice to Gottlob's perceived difference between Informal Proof #1 and Informal Proof #2. It is not enough to say that Gottlob's Informal Proof #1 corresponds to 'reading' Alfred's formal proof upwards, and that Gottlob's Informal Proof #2 corresponds to 'reading' Alfred's formal proof downwards. Because Alfred's formal proof is presented with no particular ordering of reading indicated.

So we call in the expert consultant Gerhard, who proposes that we make explicit, in the vertical ordering of steps, the possibilities corresponding to 'reading upwards' and 'reading downwards'. We abandon serial &-Elimination, and replace it with parallelized &-Elimination. Now we can construct Formal Proof #1 and Formal Proof #2, as follows, to bring out the difference that Gottlob perceived between his Informal Proof #1 and Informal Proof #2:

              ___(1)
     A&B    B
    ________(1)                 Formal Proof #1
          B
       _____
        AvB


               ___(1)
                 B
              _____
    A&B      AvB                  Formal Proof #2
    ___________(1)
           AvB


"To take an extreme example: if there actually is a formal PA proof of Fermat’s Last Theorem there is a clear sense it will not be a faithful representation of Wiles’ proof, since the latter brings in content from branches of mathematics other than arithmetic."

Presumably this is because Wile's proof exploits axioms from those other branches of mathematics, in addition to the axioms of PA?

Neil Tennant
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150909/21fd5915/attachment-0001.html>