There is no inconsistency either in or about Core Logic.
joseph.vidal.rosset at gmail.com
joseph.vidal.rosset at gmail.com
Sat Jan 16 09:45:40 EST 2021
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
More information about the FOM
mailing list