Explosion and Cut Required

[Mario Carneiro]

On Thu, Jun 16, 2022 at 6:56 AM Joseph Vidal-Rosset <joseph at vidal-rosset.net>
wrote:

> Le 16/06/2022 à 06:20, Mario Carneiro a écrit :
> > You have not established this (specifically, the reverse direction
> >
> > X, (A -> B) -> B  |- B
> > ----------------------------- anti-DNS.1
> >            X, A |- B
> >
> > ).
>
> Again I guess that you meant DNS.1 (because it makes no sense both to
> talk about a rule on anti-sequents and to write only sequents in this
> rule).


I'm talking about the rule I wrote. Your naming system does not help here,
but I will also accept "reversed-DNS.1" for the name of this rule. I am
certainly not talking about DNS.1 (the forward direction), which is easily
provable.


> But note that the so-called restricted Cut for Core logic leads to
> conclude:
>
>                 ------- Ax.
>                  A |- A
>              ----------  L~
>              ~A, A |-
> ----------------------- DNS.3
> ~A, (A -> B) -> B |- B
>   ----------------------- reversed-DNS.3  (i.e. restricted Cut)
>               ~A,A |-
>

The final line is a derivable theorem, but the proof of it does not have
any of that stuff above it. Core logic proofs are Cut-free. (Not entirely
sure what this has to do with anything, but I don't see anything
immediately wrong here.)

But this equivalence suddenly disappears for the Core
> logician in the following derivations that are no longer valid in
> minimal logic, but that are provable in Core logic:
>
>
>                  A |- bot
> ========================
>      (A -> B) -> B |- B
>

The provable theorems in Core logic are a subset of classically provable
theorems. The reverse direction of this derivation is not classically valid
and so it would not be provable in Core logic either.


>                  A |- bot
> ========================
> (A -> bot) -> bot |- B
>

The forward direction here is obviously not provable because it fails
relevance. The reverse direction is also not provable because it's
classically not a tautology.


> Slaney's prover can prove these derivations with the -i option to get
> the intuitionistic logic system:
>
>   SEQUENT 2:  ~a -> (((a -> F) -> F) -> b)
>   |- ~a -> (~~a -> b)
>
>   | ~a   ASSUMPTION
>   |  | ~~a   ASSUMPTION
>   |  | F   arrow_E
>   |  | b   Bot_E
>   | ~~a -> b   arrow_I
> ~a -> (~~a -> b)   arrow_I
>
> It's easy to get the Core logic version of these proofs: just delete the
> line Bot_E, copy and paste the same proofs.
>

The theorem you proved here is not the same as the one you just quoted.
Core logic proves |- ~A -> (~~A -> B) but it doesn't prove ~A, ~~A |- B.


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

Mario
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20220616/3401ad17/attachment-0001.html>