Explosion and Cut Required - Inference Systems

[Joseph Vidal-Rosset]

Hello Mario,

Quickly,

Le 17/06/2022 à 08:05, Mario Carneiro a écrit :
> I appreciate the summary of the argument as it currently stands. You
> misapprehend my objection however: I have no problem at all with step 3,
> and (A <-> B) -> (~A <-> ~B) is very obviously derivable. You focus a
> lot on this step but give short shrift to the actually flawed step which
> is step 2. I have been asking for a direct proof of your claim that
> reverse-DNS.1 is derivable but I have received only a reference to a
> proof on your website that apparently proves X, A |- B ==> X, A |- B and
> does not use Core rules: in particular Cut appears and you have not used
> it correctly. If I interpret this proof charitably as a way to show X,
> (A -> B) -> B |- B ==> X, A |- B, I get:
>
> 1. X, (A -> B) -> B |- B (Hyp)
> 2. A |- A  (Ax.)
> 3. B |- B  (Ax.)
> 4. A, A -> B |- B (L-> 2,3)
> 5. A |- (A -> B) -> B (R-> 4)
> 6. X, A |- B (Cut 1,5)
>
> The last step very clearly uses Cut, which is not a rule of Core logic.
> The thing that was proven admissible is not exactly this rule but rather
>
> 6. X, A |- B/# (Cut' 1,5)
>
> where the determination of whether the consequent is B or # depends on
> details of the two derivations 1 and 5 that were used (and since 1 is an
> arbitrary hypothetical derivation we cannot evaluate it to say which it
> is). In the case of interest, X = ~A and 1. is proved by applying DNS.3
> to the trivial proof of ~A, A |- #, and for this choice of derivation
> step 6 evaluates to the trivial proof of ~A, A |- #.

I disagree, because for the Core logician, B is not # (i.e. the falsity
or absurdity constant, bot, F, etc.)


> PS: You often turn to minimal logic provers in order to make a point
> about derivability of this or that, but while doing so you ignore the
> difference between A, (B -> C) |- D ==> E |- F and (A -> ((B -> C) ->
> D)) -> (E -> F). For core logic specifically, this is not okay: core
> logic for pure formulas involving implication looks basically like
> classical logic, but there are various effects that appear only "at the
> level of the turnstile" as you well know, so you can't argue that just
> because the latter is derivable the former must also be derivable.

I always gave proofs in minimal logic that are valid in Core logic and I
do not ignore the difference between these two systems.
Most derivations in minimal logic are exactly the same derivations in
intuitionistic logic as in Core logic. The only difference between Core
logic and minimal logic (except, of course, the relaxed rule VE and rule
-> I that replaces bot E, rules that are not in minimal logic) is that
in Core logic, there is no vacuous discharge, i.e. no Weakening on the
left when there is a contradiction on the left of the turnstile. In ND
for Core logic

   B
------ -> I
A -> B

is allowed, by contrast with

   bot
--------- -> I
A -> bot

which is not allowed in Core logic. This ban allows the Core logician to
claim that the following sequent

bot |- ~B

is unprovable in Core logic, by contrast with minimal logic. I never
discussed this subtlety of Core logic, for the simple reason that it
seems to me both tricky from a syntactical point of view, and not
justified from a philosophical point of view. The only claim of the
"minimal logician" is that if you accept a contradiction in the premises
of your theory, you can prove that any sentence is false. Such a claim
does not sound so "irrelevant".

Now, I had only time this morning to check via Minlog  that DNS.1 is
provably invertible in minimal logic and here is a proof *without
detour* i.e. a normal proof that is, of course, a proof in Core logic:

  SEQUENT 1:  (((x & ((a -> b) -> b)) -> b) -> ((x & a) -> b)) & (((x &
a) -> b) -> ((x & ((a -> b) -> b)) -> b))

  |- (((x & ((a -> b) -> b)) -> b) -> ((x & a) -> b)) & (((x & a) -> b)
-> ((x & ((a -> b) -> b)) -> b))

  |  | (x & ((a -> b) -> b)) -> b   ASSUMPTION
  |  |  | x & a   ASSUMPTION
  |  |  | x   &E
  |  |  | a   &E
  |  |  |
  |  |  |  |  | a -> b   ASSUMPTION
  |  |  |  |  | b   arrow_E
  |  |  |  | (a -> b) -> b   arrow_I
  |  |  | x & ((a -> b) -> b)   &I
  |  |  | b   arrow_E
  |  | (x & a) -> b   arrow_I
  | ((x & ((a -> b) -> b)) -> b) -> ((x & a) -> b)   arrow_I

  |  | (x & a) -> b   ASSUMPTION
  |  |  | x & ((a -> b) -> b)   ASSUMPTION
  |  |  | x   &E
  |  |  | (a -> b) -> b   &E
  |  |  | a   Double_Negation
  |  |  |
  |  |  | x & a   &I
  |  |  | b   arrow_E
  |  | (x & ((a -> b) -> b)) -> b   arrow_I
  | ((x & a) -> b) -> ((x & ((a -> b) -> b)) -> b)   arrow_I
(((x & ((a -> b) -> b)) -> b) -> ((x & a) -> b)) & (((x & a) -> b) ->
((x & ((a -> b) -> b)) -> b))   &I

I do not translate this proof in Core logic's style i.e. in Gentzen's
style with parallel elimination rules. I do not have time, but there
must be no problem for such a translation.

The invertibility of DNS.1 is therefore provable in Core logic,
anti-DNS.1 is deducible from this point if Core logic is consistent.

Best wishes,

Jo.