[FOM] Fwd: A request--Reply to Arnon Avron

[Tennant, Neil]

Arnon writes:

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.

Answer: No, this move is not forbidden in Core Logic. Here is a core proof:

                (1)___     __(1)
                     ~P       P
(2)______    ________
    ~P & P           #
    _____________(1)
                 #
       ____________(2)
          (~P&P)->Q

Arnon also writes:

"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."

Answer: These are indeed equivalent in Core Logic. Proofs (using parallelized &E and ->E):

              (3)__   __(2)
                    A    B
                   ______       ___(1)
(A&B)->C      A&B           C
______________________(1)
                       C
                _______(2)
                    B->C
              _________(3)
                A->(B->C)

                                           (2)_____       __(3)    __(1)
                                                 B->C        B         C
                                  (3)___    __________________(1)
                A->(B->C)        A                       C
____(4)   ____________________________(2)
A&B            C
_______________(3)
             C
_____________(4)
(A&B)->C


Metatheorem: If X:A is provable in Intuitionistic Logic, and X is intuitionistically consistent, then for some subset X' of X we have X':A provable in Core Logic.

Metatheorem: If X:A is provable in Intuitionistic Logic, and contains no sentence in which ~ occurs, then for some subset X' of X we have X':A provable in Core Logic.

Neil Tennant
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150904/a322e11d/attachment-0001.html>