[FOM] 603: Removing Deep Pathology 3 Harvey Friedman Tue Aug 25 10:24:45 EDT 2015

[Tennant, Neil]

Harvey apparently misunderstands what goes on in Core Logic. He describes proofs by cases in which certain cases close off with a contradiction, and says "Superficially, this seems to be the kind of thing that people actually do and teach, and like, which you are negatively flagging."

I am NOT 'negatively flagging' it at all! In fact, one of the signal features of Core Logic is that these kinds of proof by cases are ALLOWED as PRIMITIVE. The rule of v-E is framed so as to allow one, when one of the case proofs ends with #, to bring down the conclusion of the other case proof as the main conclusion. One does NOT 'top up' the absurd case with a terminal application of EFQ to get that conclusion as the conclusion of that case proof. One simply stops at the #, and looks to the other case-proof for its conclusion. (And if the latter is also #, then it's # that gets brought down as the main conclusion.)

In Core Logic, *there is no rule of EFQ*. That's because mathematicians NEVER (NEED TO) USE IT!

Harvey's example in fact underscores just what I was emphasizing in my earlier post. Classical Core Logic  [resp., Core Logic] formalizes much more faithfully than classical logic [resp., intuitionistic logic] how mathematicians actually reason deductively.

Neil Tennant

PS Anyone interested in more details about Core Logic can find recent papers of mine in the Review of Symbolic Logic, downloadable at http://u.osu.edu/tennant.9/publications/  (articles 6, 7, 15 on the current numbering)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150831/b465c07c/attachment.html>