There is no inconsistency either in or about Core Logic.
Tennant, Neil
tennant.9 at osu.edu
Sat Jan 16 11:44:46 EST 2021
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>
More information about the FOM
mailing list