Explosion and Cut Required
Joseph Vidal-Rosset
joseph.vidal.rosset at gmail.com
Sat Jun 11 10:26:47 EDT 2022
Hello Vaughan, hello everyone
(I met a problem with my email client, I hope that this email will not
be sent twice. If it is the case, I apologize.)
Le mer. 06/08/22 juin 2022 à 11:04:01 , "Vaughan Pratt"
<pratt at cs.stanford.edu> a envoyé ce message:
> But if it is, then it would be nice to have a short proof showing that
> while CA --> can arise in Core Logic, CA |-- cannot. Or however Core
> Logic distinguishes them.
The Core logician's slogan is "relevance at the level of the turnstile"
(it is repeated many times in Tennant's book on Core logic). The
*unprovability* of sequent
¬ A, A |- B (1)
i.e. the *antisequent*
¬ A, A |/- B (2)
is undoubtedly the main claim of Core logic i.e. the "intuitionistic
relevant logic" i.e. *IR*, where all intuitionistic *theorems* are
provable, but where no irrelevant logical *sequent* like (1) is
deducible. In Tennant's book on Core logic, p. 195, formula
¬ A, A |/= B
is claimed from the Core logic's point of view. Therefore (2) is
certainly also claimed by the Core logician (because Core logic is
claimed to be sound and complete).
Now, here is my argument against the claim of (2) from the Core
logic's point of view: the claim of (2) leads Tennant's theory to a
contradiction and therefore it is false that Core logic is
paraconsistent, contrarily to what Tennant wrote (p. 156 of his book
on Core logic).
Proof:
- First, it is provable that these *invertible* rules that I call
"DNS1" and "DNS.3" are *derivable* in sequent calculus for Core
logic and therefore these rules belong to Core logic. (I do not
reproduce the Core-derivations of these rules in this email.)
X, A |- B
---------------------- DNS.1
X, (A -> B) -> B |- B
X, A |-
---------------------- DNS.3
X, (A -> B) -> B |- B
- Second, *if Core logic is consistent*, this rule for antisequents must
also be accepted as *valid* in Core logic:
X, A |/- B
---------------------- anti-DNS.1
X, (A -> B) -> B |/- B
Reason: the following sequent is provable in Core logic
A -> B, B -> A |- (¬B -> ¬A) & (¬A -> ¬B) (3)
Let us interpret A and B as the premise and conclusion of rule DNS.1
(which are provably *interderivable*), then the logical consequence of
DNS.1 must be the invertible rule for antisequents ¬A and ¬B hat I
have called "anti-DNS.1".
Note that the Core logician cannot reject such a consequence without
making Core logic inconsistent, as it is provable via the trees
method for intuitionistic logic. Indeed, once the left part of sequent
(3) is asserted ( and in our interpretation, rule DNS.1), the Core
logician cannot without contradiction refuse to assert the formula
on the right, included our interpretation i.e. anti-DNS.1. If sequent
(3) is valid for Core logic, then, by definition, *no interpretation*
of A and B is supposed to falsify this sequent, and if it were the
case, the sequent calculus for propositional Core logic could
logically prove inferences that can be false; that's clearly not an option.
3. Last, the following deduction proves that antisequent (2) cannot be
claimed by the Core logician without contradiction, because, if (2)
is claimed in Core logic, we can deduce from this theory the
following contradiction:
X, A |/- B X, A |-
--------------------- anti-DNS.1 ----------------------- DNS.3
X,(A -> B) -> B |/-B X, (A -> B) -> B |- B
------------------------------------------------------------
#
Replacing set of formulas X by ¬A, we get:
¬A, A |/- B ¬A,A |-
---------------------- anti-DNS.1 ----------------------- DNS.3
¬A,(A -> B) -> B |/-B ¬A, (A -> B) -> B |- B
------------------------------------------------------------
#
Therefore, antisequent (2) cannot be claimed in Core logic without
making Core logic inconsistent, and if Core is consistent, it
cannot be paraconsistent, contrarily to what Tennant claims.
Q.E.D.
(Remark : in minimal logic, only the premise on the left in the
deduction above is accepted, rule DNS.3 is *not* valid only in
minimal logic. By contrast, in intuitionistic logic, DNS.3 is valid,
and that's why antisequent (2) is rejected as false. The Core logician
both claim (2) and allows the derivation of rule DNS.3. It can't
work unless my argument is incorrect for some plain and simple
reason that I do not see.)
For more details, see my paper online
https://www.vidal-rosset.net/paraconsistent_tennants_logic_is_inconsistent.html
Best wishes,
Jo.
PS: I would certainly have been happy to publish this argument
elsewhere, but it was brutally rejected by a referee of a famous
international review whose name I will keep silent, without the
slightest start of discussion and with the following conclusion :
"Author appears not to understand just how exigent the notion of Core
Proof is." A very harsh conclusion for a not very exigent report. Too
bad... But since my university career is coming to an end, I no longer
need to publish in prestigious journals and I don't care. I am more
interested in open and free discussions online. Many thanks to the FOM
list editors. Is my argument flawless or not? Surprisingly, I have not
received at the moment the least objection via the comment engine of my
blog...
More information about the FOM
mailing list