There is no inconsistency either in or about Core Logic.

[joseph.vidal.rosset at gmail.com]

Le   sam.   01/16/21  janv.   2021   à   02:54:27  ,   "Tennant,   Neil"
<tennant.9 at osu.edu> a envoyé ce message:
> Jo,
>
> You have claimed now that
>
> "in your system [of Core Logic] you cannot show in one proof that
> (3) ~A -> (A -> B), ~ A, A |- B
> is provable and that
> (2) ~A -> (A -> B)
> is a theorem."
>
> My response is: So what?!

Dear Neil, fair enough,  but what I claim is always  the same point: the
*occurrence* of Core theorem (2) i.e.  (~A -> (A -> B)) in the proof of
sequent (3) is unprovable in Core logic.

So what?

First,  I   believe  that  this   idiosyncrasy  of  Core  logic   is  in
contradiction with the usual definition of  what is a theorem in natural
deduction which is not based, as far as I know, on the definition of
normal proof. But  of course, "In logic, there are  no morals", to quote
the famous Carnap's word, and you are  free to define your rules and to
give your own definition of what is a Core theorem.

Nevertheless, and it is my second and last point, it seems to me that the
composition of proofs and their normalization when these proofs are not
normal  is a  basic property  of natural  deduction and  of mathematical
logic in general.  The Core  logician can prefer breaks this composition
property,  but I  am quite  convinced  that many  other logicians,  like
Bartleby the Scrivener, would prefer not to.

All the best,
Jo.

PS: Because,  I admit after  discussion that it  can be considered  as a
fallacy to call about an "inconsistency" about Core logic, I am going to
delete this  note on my  blog, as  I promised, and  I will try  maybe to
write  another text  that even  you, the  Pope of  Core logic,  will not
contest. It was yesterday the World Logic Day and I believed that it was
finally also the Core Logic Death...  I was wrong. (Sorry, I was too
proud  to  make this  bad  pun  in a  language  that  is not  my  native
language! I was only joking.)