[FOM] Fwd: A request--Reply to Mario Carneiro

[Mario Carneiro]

On Sat, Sep 5, 2015 at 11:14 AM, Tennant, Neil <tennant.9 at osu.edu> wrote:

> Core Logic does not allow *Unrestricted Accumulation of Proofs*---the
> natural-deduction analog of not allowing *Unrestricted Cut* in sequent
> calculus. Whenever (in natural deduction) a would-be accumulation-of-proofs
> is proffered as a proof, the Core Logician says "Wait! Normalize the
> would-be result first, in order to determine what it is that you have
> really 'proved'. You may well find yourself making important epistemic
> gains as a result."
>

I suppose that this could then be identified as an undesirable feature of
Core: Proofs do not 'compose' or 'accumulate' upon the application of the
axiomatic inference rules, which is usually taken for granted.

To fix this, from a Core logic perspective, one could attempt to 'repair'
the core proof derivability operator by defining A |-c B if there is a
proper core proof of A' |- # or A' |- B for some subset A' of A. Then this
operator is preserved under "normalization", and your comments would
suggest that this operator can be interpreted as provability in classical
deductive logic.

This also seems a better target for proper (less prone to confusion)
naming: If A |-c B then we could say "the assumptions in A imply B", or "A
proves B classically", while if A |- B then we say "A exactly proves B" or
"there is a normalized proof of A implies B" or "A proves B in core logic".
After all, I think a core logician who can derive A |- # will respond to
"does A imply B" by "yes (and it also proves everything else)". The
classical logician will leave off the parenthetical remark, but this
doesn't change the fact that the answer to the question is still "yes".
This is also preserved by the rules of Core: despite not having an actual
proof of A |- B, we can still proceed under the assumption that it is
provable to derive more work even though an epistemologically stronger
intermediate result was used. (Or to say it another way, classical logic is
a conservative extension of core, in that any EFQ-free result is provable
in core iff it is classically provable, even if EFQ is used in an
intermediate stage in the classical proof.)

What is the complexity of a single derivation step in Core, since just
tacking the new rule at the end is apparently insufficient? Is the
normalization process proof-relevant, i.e. given two proofs of A |- B is it
possible that an application of some inference rule like B |- C may yield A
|- C for the first proof and A |- # or A' |- C for the other? Is it linear
in the number of previous steps, or is it something worse, say exponential
or super-exponential? Certainly if it is polynomial then there is a
polynomial time algorithm for normalizing entire proofs, but you seem to be
claiming that full-proof normalization is super-exponential.

Mario
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150906/a9d9a967/attachment.html>