Core Inconsistency
joseph.vidal.rosset at gmail.com
joseph.vidal.rosset at gmail.com
Fri Jan 15 15:03:08 EST 2021
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.
More information about the FOM
mailing list