EFQ
Joseph Vidal-Rosset
joseph.vidal.rosset at gmail.com
Sun May 22 08:22:16 EDT 2022
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.
More information about the FOM
mailing list