There is no inconsistency either in or about Core Logic.

[joseph.vidal.rosset at gmail.com]

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://www.vidal-rosset.net/core_inconsistency.html#comments .  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