[FOM] Fwd: A request

[Mario Carneiro]

If I may add my own interpretation (not being a Core Logician but following
Tennant's explanations):

I think the key here is the difference between the deductive entailment "A
|- B" and the material implication "A => B", which are interchangable in
classical logic (by the deduction theorem) but are quite different in core
logic, from what I can tell. Given a derivation of # under the assumption
A, we are allowed to conclude A => B, that is, if A |- # then |- (A => B).
Thus "if (not P and P) then Q" is derivable, in the form "|- (P /\ ~P) =>
Q". What is *not* derivable is a derivation of Q from the assumption P /\
~P, that is "(P /\ ~P) |- Q" or "P, ~P |- Q". This is what Tennant is
calling EFQ, while others have been looking at the former as a closed-form
EFQ. The former is what is needed to prove the emptyset is a subset of
anything, which is why the proof goes through in core without issue even
though it deals with EFQ-like statements (which are not being judged as
'true' EFQ here).

The part which still confuses me is why one cannot apply modus ponens to
the implication to get true EFQ. For example:

             ___         ___(1)
              ~A           A
              __________
                       #
       ___       ____(1)
         A         A->B
       ________________
              B

Here we are taking A and ~A as assumptions, and deriving B, i.e. "A, ~A |-
B" which is EFQ if anything is. How does modus ponens / implies-elimination
interact with the lack of cut?

Mario

On Thu, Sep 3, 2015 at 7:46 PM, Martin Davis <martin at eipye.com> wrote:

> ---------- Forwarded message ----------
> From: <aa at post.tau.ac.il>
> Date: Thu, Sep 3, 2015 at 6:35 AM
> Subject: Re: [FOM] Concerning EFQ and Cut [from Arnon Avon]
>
> Quoting "Tennant, Neil" <tennant.9 at osu.edu>:
>
> "The conditional-introduction signalled by "So" in the foregoing informal
> proof would is formalized as an application of the formal rule that allows
> one to infer "if P then Q" upon refuting P. And this formal rule in turn is
> justified by the last two lines of the familiar truth table for the
> conditional, which tell one that a conditional is true if its antecedent is
> false."
>
> If upon refuting P you can infer if P then Q", then in particular
> (assuming that a logic should be structural) upon refuting
> "not P and P" (which I hope you can) you are allowed to infer
> "if (not P and P) then Q". If this move is forbidden in your system
> then you  cannot truly say that you are formalizing ordinary mathematical
> ways of proving things.
>
> In fact, "If A and B then C" and "If A then if B then C" are
> always equivalent in mathematical texts. It seems that for you
> they are not. Don't you find it strange?
>
> Arnon
>
>
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>

>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150904/887a76a3/attachment.html>