Explosion and Cut Required

[Joseph Vidal-Rosset]

Hello Mario,

I agree on the couple of corrections you made about the last sequent
derivations: the double line must be replaced by a single line, and
sequent ~A, ~~A |- B is unprovable in Core logic. Your corrections on
these points are correct, but that does not change the main point of our
controversy.

Le 16/06/2022 à 13:21, Mario Carneiro a écrit :
> On Thu, Jun 16, 2022 at 6:56 AM Joseph Vidal-Rosset
> <joseph at vidal-rosset.net <mailto:joseph at vidal-rosset.net>> wrote:

>>     My point in this paper is that, if you do *not* presuppose the
>>     consistency or inconsistency of the set of premises in  DNS.1 rule, like
>>     you do when you're reasoning in minimal logic or in intuitionistic
>>     logic, and if you assume only that your logical system is consistent and
>>     that your propositional calculus is sound, then you have to admit that
>>     this rule is both derivable and invertible and  that it involves an
>>     invertible rule for antisequents, that is anti-DNS.1.
>
>
> Soundness and consistency (and paraconsistency for that matter, by your
> definition) are both *negative* statements about what is provable. The
> first one says that false theorems are not provable and the second one
> says that there are theorems that are not provable (and your definition
> of paraconsistency says A, ~A |- B is not provable for some A, B). The
> empty system, with no axioms or rules of inference, is obviously sound
> and consistent (and paraconsistent). I don't see how you can deduce any
> kind of positive statement about provability from these properties, like
> the invertibility of a rule or the existence of an antisequent rule. The
> only way you can deduce such things is by showing that the proof system
> can prove things by deriving them directly, according to the rules of
> the system.

On this last point, that is the main point, I disagree. The refutation
systems have been established on the ground of proof systems. It means
that from the set of logical rules of each proof system S it must be
possible to construct a set of logical consequences that is the set
anti-S of refutation rules. See Goranko's work, among others, on this
point. But nobody needs such a big machinery to understand that the rule
that Slaney intentionally called misleadingly "Double Negation" i.e.

             X, A |- B
--------------------- DNS
X, (A -> B) -> B |- B

because it is invertible, entails a refutation rule that is


             X, A |/- B
---------------------- DNS
X, (A -> B) -> B |/- B


The intuitionistic tree method helps understand this point:

In this method, the interderivability between

X, A |- B

and

X, (A -> B) -> B |- B

can be translated by the following  alternation :

              ( X, A |- B )  <->  ( X, (A -> B) -> B |- B )
                              |
                              |
X, A |- B                    |    ?(X, A |- B)
X, (A -> B) -> B |- B        |    ?(X, (A -> B) -> B |- B)

which means that if this biconditional is valid (i.e. if it is an
implication), then either both sequents are provable, or both are
unprovable (which is exactly anti-DNS.1)

I am aware of the philosophical debates on equivalence and identity, but
it is indisputable that identity relation is an equivalence relation.
Therefore, if it has been proved that G is identical to F, every
sentence that can be formulated in an extensional language (like FOL)
that is true about G is also true about F, and  reciprocally, if it is
not true about F is also not true about G. Denying this point would turn
out to deny simply the principle of Indiscernibility of Identicals and
that would be absurd. Therefore, if your logical system S is consistent,
you cannot deny that if it is provable in S that DNS is both derivable
and invertible, then anti-DNS is also involved in S. That's it. If you
persist in denying this point, I won't repeat myself and I quote
Rousseau, in French:

"Je ne sais pas l'art d'être clair, pour qui ne veut point être
attentif."  ("I don't know the art of being clear, for those who don't
want to be attentive.")

Now it is clear that only a formal sophistic can help the Core logician.
His only way out is therefore to reject the proof of the invertibilty of
DNS rule, that is to say to change  the Cut rule to make it admissible,
like he had changed the disjunction elimination rule, like he added a
second conditional introduction rule and stressed on the point that all
proofs must be in normal form. In my opinion, all these efforts are
unconvincing, because I do not believe that exist an intermediate logic
between minimal logic and intuitionistic logic, and all the difficulties
or "subtleties" of Core logic are a good clue to believe it.

All the best,

Jo.