[FOM] Moderator's Comments on Harvey Friedman's "challenge"

[Martin Davis]

Here is the paragraph from Harvey Friedman's email message that Neil
Tennant has viewed as a "challenge":

"What is being offered for first order predicate calculus? I havenot
seen the Tennant turnstile in action on the FOM with quantifiers.

Here are there more things mathematicians prove normally and quickly
that do not conform, maybe well beyond, emptyset containedin A?

According to Tennant, the axioms and rules for quantifiers are
unchanged. But there may be unexpected interactions. What would a
detailed analysis of Tennantism look like for, say, the usual proofs of
n^2 = 2m^2 has no solution in nonzero integers"

Neil Tennant interprets this as a challenge to produce such a "core
logic" proof. That's not how I read it, and, I believe, not what was
intended. As I read it, without doubting that such a proof could be
developed, Harvey Friedman is suggesting that a study of a detailed
proof of a simple mathematical fact, like the irrationality of
squareroot(2), may be worthwhile because of the differences that would
show up with a proof along more usual lines because, e.g., of
"unexpected interactions".

By making the effort to produce his meticulously detailed proof, Neil
Tennant has performed a service for someone interested in initiating
such a study. But I don't see any  "challenge" that has been answered.

BTW the old thread on pro and con on "core logic" remains closed.

Martin
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20151216/0cb221ad/attachment.html>