EFQ

[Joseph Vidal-Rosset]

Hello Neil, hello everyone,

Le   sam.   05/21/22   mai   2022   à   06:44:08   ,   "Tennant,   Neil"
<tennant.9 at osu.edu> a envoyé ce message:
> Jo (and all)--
>
> Let P1 be the obvious Core proof of the Core theorem ((AvB)&~A)->B.
> Note that P1 ends with ->-Introduction.
> Let P2 be the proof you have given of the conclusion B from the set
> {((AvB)&~A)->B, A, ~A} of assumptions.
> Note that  P2 has ((AvB)&~A)->B  as a  major premise for  its terminal
> step of ->-Elimination.
>
> Your mistake is to think that you now  have a Core proof of B from the
> set {A, ~A}.

No, it is not my mistake, because it is not exactly what I  wrote.
I used Prawitz's inversion principle to say that because you know that
((AvB)&~A)->B is a Core theorem (whose  proof is P1), proof P2 shows or,
more exactly,  betrays a deduction  of B by set  of premises {A,  ¬A} in
Core logic.
Our disagreement on this point is that, in my opinion, the intuitionistic
absurdity rule is *used but not mentioned* in your logical system.

> You think  that by putting P1  "on top of"  P2 you will obtain  a Core
> proof of B from the set {A, ~A}. But you will not.
> At the "grafting point" of  the two proof-trees you have ((AvB)&~A)->B
> standing as the conclusion of ->-Introduction
> and as the major premise for a step of ->-Elimination.
>
> This violates a crucial condition on Core natural deductions:
> their MPEs must "stand proud", with no non-trivial proof-work above them.
>
> In   sequent-terminology,  you   are  treating   ((AvB)&~A)->B  as   a
> Cut-formula.
> The sequent version of P1 proves the sequent
>           emptyset : ((AvB)&~A)->B
> while the sequent version of P2 proves the sequent
>           ((AvB)&~A)->B, A, ~A : B .
>
> But sequent proofs in Core Logic have to be both Cut-free and Thinning-free.
>
> So you cannot get a sequent proof of A,~A : B .

The Core logician  seems to be like  a doctor who refuses  a medical act
considered reliable  by everyone in the  world, but which he  refuses to
use  as such,  when the  result does  not please  him.  He  then invents
another procedure to  produce the result he  deems appropriate.  Indeed,
for  both semantic  and syntactic  reasons, everyone  - except  the Core
logician - accepts  that, in any logical system S  of First-Order logic,
any S-theorem T on the left of any sequent
T, X : C
can be reduced to
X : C
without changing the deductibility of C from X, because T is useless in
this deduction and therefore can be cut. But in the case of
((AvB)&~A)->B, A, ~A : B
even if the Core logician accepts  that ((AvB)&~A)->B is a theorem, he
persists in denying A,~A:B. He refuses to see  it. ("Cover up that
bosom, which  I can't endure to  look on!", more in  French: "Couvrez ce
sein,  que je  ne saurais  voir.  Par de  pareils objets  les âmes  sont
blessées,  Et  cela  fait  venir de  coupables  pensées."   Molière,  Le
Tartuffe, III,  2 v. 860-862  ") Then, in  this case, the  Core logician
cuts in this sequent not only on the left, but also on the right, to get
this, via a new Cut rule (a "Core Cut"):

A, ~A:

i.e.

A, ~A: #

> In my  RSL papers  and book  on Core  Logic it  is explained  how this
> apparent  "failure"  of  Cut  in  more than  compensated  for  by  the
> epistemic gain involved in obtaining a proof of some subsequent of the
> overall target sequent of a cut.

I deny that  Core logic provides any "epistemic gain"  in a reasonable
sense of  this  expression,  that   is  that  you  learn  something
more. Heyting agreed with Johansson on the validity of A,~A:#, but not
on the absurdity  constant on the right of this  sequent.  "The minimal
logic  approach   treats  [the  symbol  of   absurdity  constant]  as,
essentially,  a   nonlogical  constant.  The   intuitionistic  logic
approach  provides an  additional inference rule for this  [symbol],
namely that one can infer any  formula from it (Ex Falso Quodlibet)"
(D. Miller, G. Nadathur,  Programming with Higher-Order Logic, C.U.P.,
2102, pp. 89-90).  The Core logician  does not like the absurdity symbol
and wants to have a foot in  each camp: he claims that the First Lewis's
Paradox is unprovable in his system,  but in the case of sequent A,~A:#,
he treats # as a signal to
infer A -> B from ~A, i.e.
~A: A -> B
or to infer ~A -> B from A,
A: ~A -> B
sequents indeed Core provable, while they are invalid in Johansson's
logic. In  the same way,  in the liberalized rule  vE, if #  is inferred
from one the side of the disjunction,  and C by the other side, the Core
logician, can conclude directly C to  eliminate the disjunction, as if C
had been conclude  by the two sides  of the disjunction. It  leads me to
think that, in fact, rule vE  as well as  rule ->(a)I in Core  logic are
only shortcuts, where the intuitionistic absurdity rule is used but not
mentioned. But such a point that it  is difficult to prove, and that why
it is of course denied by the Core logician.

Best wishes,

Jo.