[FOM] Reply to Harvey Friedman's embedded letter from Avigad

[Tennant, Neil]

"Most automated methods rely on classical reductions and/or rules that
presuppose EFQ."

And some don't---for example, all the proof-finders discussed in my book Autologic.

"In the constructive theorem proving community, most
people are convinced by the usual stories about the computational
interpretation of falsity, so I don't know of anyone in that community
that is keen to give that up."

Most people convinced by the usual stories tend to be attracted away from them when they finally learn of better stories. The problem is simply that of finding open minds that can absorb a new perspective and think about it.

"Of course, in higher-order systems, you can define "false" by "forall
P, P" in which case EFQ is valid. In Coq and Lean, it is defined by an
inductive definition (i.e. the empty one). So, in a sense, these
systems don't rely on EFQ, falsity is simply defined in a way that
makes it true."

# is a Bad Thing without having to imply every P.

"In short, I don't know of anyone seriously interested in avoiding EFQ.
Is there any good motivation to do so?"

Yes, very good motivation: it ensures relevance, does not sacrifice transitivity of deduction, and respects intuitions. Unfortunately, however, the suggestion that we can and should explore the benefits of avoiding EFQ gets some people really worked up!

"As far as using cut: in interactive theorem proving, of course, we
prove libraries of theorems and use them in proofs. So cut is used all
the time."

Note the adjective "interactive". But more importantly: we don't have to described this by saying "cut is used". That holds only if one actually applies a rule of cut in constructing a proof. One could, instead, simply refrain from cuts, and gather together all the sections of cut-free proof. It's what good writers of textbooks in mathematics actually do! That *there is* a proof of the 'overall' result is guaranteed by the cut-admissibility result.

"In resolution theorem proving, one proceeds by negating the
conclusion and trying to prove a contradiction with the resolution
rule, essentially "from 'A or B'  and 'not A' conclude B". So that is
sort of like a "cut calculus"."

I beg to differ. That is merely Disjunctive Syllogism, which holds in Core Logic. It should also be borne in mind that resolution theorem-proving falls far short of exhausting all the already extant approaches to fully automated deduction. Resolution theorem-proving derives from the pioneering book by Alan Robinson, 'Logic: Form and Function: the mechanization of deductive reasoning' (which I refereed for Edinburgh University Press).  My own approach to theorem proving, however, does not involve the resolution method. Ironically, though, since I program my proof-finders in that other great Edinburgh product, Prolog---which itself runs on the resolution method---I'm operating in resolution's shadow, so to speak. But it's really important to stress that the actual method of proof-search does not have to be a resolution method. It can instead be a method that seeks to mimic the way an expert logician searches for a proof of a given sequent. And it's amazing how much this effort benefits from judiciously formulated, completeness-conserving normal-form theorems, which provide very exigent constraints on proof-search, thereby affording great speed-up. Also, Prolog is beautifully adapted to the framing of inductive definitions (of things like sentences and proofs), which is the bread and butter of computational logic.

"As far as "guessing" lemmas or
generalizations in automated reasoning, there has been some work along
these lines, but I don't know of any striking successes."

This is fully to be expected. I have already mentioned the computational costs of determining interpolants, in an earlier posting.

Harvey, there is absolutely nothing here to worry the Core Logician---just as I predicted.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150912/0cc29234/attachment-0001.html>