[FOM] Concerning EFQ and Cut

[Tennant, Neil]

Harvey judges my earlier informal proof to be too long! He offers the following revision. It is, in effect, a subproof of my own informal proof. It results by deleting from the latter its final step of explicit universal introduction, and its appeal to the definition of 'containedin'. That's just fine by me. Let those things be tacitly understood. So here is the informal prooflet we both agree on (Harvey's rendition):

    THEOREM. {x|~x=x} containedin A.

    Proof
​*​
: Let b be arbitrary. Suppose b in {x|~x=x}. Then ~b=b. But b=b.
    Contradiction. So, if b in {x|~x=x}, then b in A. QED

Harvey goes on to say

    This is obviously the same proof that I gave before (twice).

That's fine by me too. So now we both know and agree on what would need to be formalized. Schematically, what we have agreed on is a passage of reasoning like this:

      ____________(1)
       b in {x|~x=x}
       ____________    _____
           ~b=b              b=b
           __________________

                 Contradiction
        ________________________(1)

         if b in {x|~x=x}, then b in A


Thank you, Harvey. That is a Core proof.

Neil Tennant
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150902/8e6a25ab/attachment-0001.html>