[FOM] Concerning EFQ and Cut

[Tennant, Neil]

Here is an informal proof of the theorem Harvey wishes to see proved. It does not use EFQ.

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. But b was arbitrary. So for all y, if y in {x|~x=x}, then y in A. Hence by definition {x|~x=x} containedin A.

I can understand this not being publishable, but only on grounds of triviality, not on grounds of excessive complication! This informal proof was faithfully formalized, very rigorously, in my last email, using rules for the free logic of sets with the set term-forming operator primitive. The complication in that formal proof was not at all excessive, but rather, as always in the nature of these things, the inevitable price one pays for full and faithful formalization.

The conditional-introduction signalled by "So" in the foregoing informal proof would is formalized as an application of the formal rule that allows one to infer "if P then Q" upon refuting P. And this formal rule in turn is justified by the last two lines of the familiar truth table for the conditional, which tell one that a conditional is true if its antecedent is false.

Neil Tennant
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150901/6076b064/attachment.html>