[FOM] The EFQ controversy

[Peter Aczel]

I think that Neil and Harvey <may be arguing> at cross purposes.  There are
two consequence relations, standard or relevant, playing a role in the
discussion.  There is the standard consequence relation, for classical or
intuitionistic logic, that is the appropriate one in the issue of whether
or not a sentence is a theorem of an axiom system.  There is no general
concern that all the axioms have to be used in proving a theorem of an
axiom system.  So core logic is not relevant to the general concern.  But
sometimes, given a sentence of an axiom system one may have a strong
intuition that the sentence is a theorem and what the axioms are that will
be needed to prove the theorem.  Then, in searching for a proof, by hand or
by machine, it <may be more efficient> to use the relevant consequence
relation of core logic.  It seems that Neil believes that using core logic
for proof search <is significantly more efficient> while Harvey seems to be
highly skeptical.  It would be good to have an objective test!

Peter A
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150906/770f2ef1/attachment.html>