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

[Harvey Friedman]

Please give an example in a common real world mathematica situation,
without resorting to any technical notions from proof theory, of what
exactly you are flagging and what you are not. Actual real world
mathematical activity more or less correlates in various senses with
various proof systems. But for the kind of fine structure you are concerned
with, I do not believe that there is any one way of formalizing actual
mathematical proofs. The robustness that is truly there is very
significant, and fully adequate for most foundational purposes. But I don't
believe that this robustness - how to exactly formalize an already clearly
rigorous and convincing proof - is really there.

So in the absence of this robustness, it is not possible for me to really
see just what kind of feature you are flagging that has or might have
significance for real mathematical proofs - without looking at some real
world examples. Actual text would be highly preferable.

Another way to clarify the situation is to take one of the standard ways
that people enter formal proofs of mathematics, such as Mizar. In this
approach, there is no question about what formal description is appropriate
for the mathematics. The mere fact that one is using Mizar or something
like it, already fixes the nature of the formal descriptions of the
underlying mathematical proofs.

So can you state what you are flagging by simply stating what Mizar steps
you want to flag? I.e., conform your setup to an existing setup already in
use for formalizing actual mathematical proofs.

After you do that, we can ask an expert in Mizar or related systems whether
they have seen people actually do these flagged things, or not.

Harvey Friedman

On Sun, Aug 30, 2015 at 10:20 PM, Tennant, Neil <tennant.9 at osu.edu> wrote:

> 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/20150830/e2214bb7/attachment.html>