Core Inconsistency

[joseph.vidal.rosset at gmail.com]

Le  ven.   01/15/21  janv.   2021  à   07:10:13  ,   "Rossberg,  Marcus"
<marcus.rossberg at uconn.edu> a envoyé ce message:
> Hello.
>
> Isn’t Core Logic a subsystem of intuitionistic logic and hence also of classical logic?
> Finding that Core Logic is inconsistent would seem to have much wider ranging consequences.
>
> Best wishes,
> Marcus

Hi Marcus,

Thanks. You sent  to me the same  reply that Neil sent to  me today, and,
before Neil, Jeffrey Ketland had the same reaction, some months ago.

Logicians can  be reassured: the  inconsistency that this note  shows is
specific to Core  logic only and it is not  a problem for intuitionistic
logic or  classical logic.  It could  also be  called (and  maybe better
called)  "meta-inconsistency" because  it is  entailed by  the meta-rule
according to which "all proofs must  be in normal form, i.e. a deduction
that  is not  in normal  form cannot  be a  proof in  Core logic."  This
meta-rule exists neither in intuitionistic  logic nor in classical logic
and it is because of this meta-rule that in sequent (3) of my note
~ A -> (A -> B), ~A , A |- B
the  first formula  on  the left  cannot be  proved  as a  Core-theorem,
because such a proof  would be abnormal, and it must  be so, because the
first formula  on the  left is  useless in  intuitionistic logic  in the
derivation  of  B, precisely  because  of  the intuitionistic  absurdity
rule.  Therefore, the paradox is only that the occurrence of
~ A -> (A-> B)
in the set of assumptions is  unprovable in Core logic, but this paradox
is the idiosyncrasy of Core logic.

>From a semantic point of view, even in Core logic this formula should be
reducible to (with T as symbol of truth constant):
T, ~A , A |- B
that is of course
~A, A |- B
But such a reduction is inadmissible only for the Core logician who
nevertheless   claims   that   his   logical   system   respects   truth
tables. That's another point which I do not understand:
~ A -> (A -> B)
is provable in Core logic, and therefore  its truth value is T, but if T
cannot be deleted  in the conjunction on the left  of this sequent, then
Core logic contradicts the first  rule of Quine's algorithm according to
which  one  can always  delete  T  in  a  conjunction (see  "Methods  of
logic"). Last,  I point out  that this rule is  of course also  valid in
intuitionistic logic. I  did not want to mention this  semantic point in
my note. Thanks  again for having given  to me the occasion  of doing it
here.

Best wishes from Nancy (France),

Jo.