Core Inconsistency

[Joseph Vidal-Rosset]

Sorry. The reply is no. I wanted just to test my comment engine. The page is deleted again.

Thanks !

Best wishes,

Jo.

---
https://www.vidal-rosset.net

Sent with [ProtonMail](https://protonmail.com) Secure Email.

‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐
Le jeudi 21 janvier 2021 11:59, Lukasz T. Stepien <sfstepie at cyf-kr.edu.pl> a écrit :

> Dear Prof. Vidal-Rosset
>
> As I have seen, you had deleted (on Saturday or on Sunday) the subpage on your blog: https://www.vidal-rosset.net/core_inconsistency.html , but yesterday you brought back this subpage. So, I have a question, whether you have updated your proof of inconsistency of Core Logic ?
>
> Best regards
>
> Lukasz T. Stepien
>
> On 2021-01-16 02:54:27, Joseph Vidal-Rosset wrote:
>
> Le   sam.   01/16/21  janv.   2021   à   02:54:27  ,   "Tennant,   Neil"
> <
> [tennant.9 at osu.edu](https://cs.nyu.edu/mailman/listinfo/fom)
>> 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.)"
>
> --
>
> Lukasz T. Stepien
>
> The Pedagogical University of Cracow
> Institute of Computer Science,
> ul. Podchorazych 2
> 30-084 Krakow
> Poland
>
> tel. +48 12 662-78-54, +48 12 662-78-44
>
> The URL
> http://www.ltstepien.up.krakow.pl
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20210121/f67410fa/attachment.html>