There is no inconsistency either in or about Core Logic.

[Tennant, Neil]

Jo,

I need to address two other things you said:
1. "my note is not based on sequent calculus, but only on natural
deduction for Core logic."
2. "I do not feel competent enough to talk about your new Cut rule."

I need to address (2) first: Core Logic has no Cut rule, new or old. There is no rule of Cut in the system.
Instead, there is a metatheorem about Core Logic, to the effect that an epsitemically gainful form of cut is admissible​.

As for (1): You seem to be missing the fact that one of the emphasized features of Core Logic is that natural deductions are (in a simply definable sense) isomorphic to the corresponding sequent proofs of the same result. In thinking about core proofs qua natural deductions, one is ipso facto thinking about them qua sequent proofs!

This is because
(i) the absence of EFQ in the natural deduction system for Core Logic is matched by there being no rule of Thinning in the sequent system for Core Logic;
(ii) the requirement of normal form for natural deductions in Core Logic is matched by the cut-freeness of sequent proofs in Core Logic (because it has no Cut rule!); and
(iii) the Introduction [resp., Elimination] rules for the logical operators in the natural-deduction system for Core Logic match their Right- [resp., Left-] rules in the sequent calculus for Core Logic.

All this is explained in Chapter 5, Section 4 of my book Core Logic.

Neil
________________________________
From: joseph.vidal.rosset at gmail.com <joseph.vidal.rosset at gmail.com>
Sent: Saturday, January 16, 2021 9:45 AM
To: Tennant, Neil <tennant.9 at osu.edu>
Cc: Foundations of Mathematics <fom at cs.nyu.edu>
Subject: Re: There is no inconsistency either in or about Core Logic.

Dear Neil, thanks  for your reply and for your  consideration to my work
on your logical  system. (I copy to  the FOM list the  discussion that we
have                              also                              here
https://urldefense.com/v3/__https://www.vidal-rosset.net/core_inconsistency.html*comments__;Iw!!KGKeukY!jHBXzJXebtmdTzBCg3d9AfPAHP2vj_Iw5FwKpgIBQxKR1vevrMOc0A8CHZh-szGI$  .  I avoid
html in emails when it possible. To  see italics in my text, please, see
this webpage.)

Neil, first, my note is not based on sequent calculus, but only on natural
deduction for Core  logic. I do not feel competent  enough to talk about
your  new Cut  rule.  I hope  sincerely that  very  soon the  scientific
community will discuss on it, and probably this community will do it via
the  FOM list.  Even if  a logician  told me  gently that  my point  was
"crystal  clear",  I  am  going  to  repeat it  to  ask  you  finally  a
question. I said that the occurrence of formula (2) i.e.

~A -> (A -> B)

taken as an assumption in sequent (3) i.e.

~A -> (A -> B), ~ A, A |- B

is unprovable because such a proof  in natural deduction is forbidden by
your claim according to which all proofs  must be in normal form. What I
mean is  that in your system  you cannot show  in one proof that  (3) is
provable and that (2) is a  theorem. Therefore, in the natural deduction
of sequent (3), formula (2) must  be considered as unprovable (it cannot
be  deduced from  any assumptions),  even if  it is  a formula  which is
provable ... in another  proof. Note that it is not  the case in Heyting
logic  where abnormal  proofs are  nevertheless proofs  that can  be put
normal form where theorems taken as assumptions disappear.

From a semantic point of view, it  is also hard for me to understand how
you can  both assert that  truth tables  are "respected" by  your system
(p.  185  of  Core  Logic)  and  deny that  the  first  formula  in  the
conjunction  of assumptions  can be  immediately deleted  without paying
attention to the rest of this conjunction.  It is not Cut, it is simpler
than Cut, it is only the first rule of Quine's algorithm: "Delete T as a
component of a conjunction. Reason:  a conjunction with a true component
is true or false according as the rest of it is true or false." (Methods
of Logic,  I, 5,  p. 34) .  Students do not  need to  understand sequent
calculus and Cut  to understand this rule, truth  tables are sufficient,
and it  is admissible  to say that  commas on the  left of  sequents are
conjunctions,  it could  be  hard to  explain why  a  theorem cannot  be
immediately deleted from  the list of assumptions,  independently of any
consideration on the rest of it.

My question now: starting from the proof of (3) in natural deduction for
Core logic, how I can deduce sequent ~A, A |- # ? I do not see.
--
Joseph
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20210116/2463be26/attachment-0001.html>