D
Journal of Mathematics and System Science 5 (2015) 60-71 doi: 10.17265/2159-5291/2015.02.002
DAVID PUBLISHING
Atomic Entailment and Atomic Inconsistency and Classical Entailment T. J. Stepień, L. T. Stepień The Pedagogical University of Cracow, ul. Podchorazych 2, 30 - 084 Krakow, Poland Received: December 01, 2014 / Accepted: December 24, 2014 / Published: February 25, 2015. Abstract: In this paper we put forward a new solution of the well-known problem of relevant logics,i.e., we construct an atomic entailment. Hence, we construct a system of predicate calculus based on the atomic entailment. Next, we establish the definition of atomic inconsistency. The atomic inconsistency establishes an infinite class of inconsistent, but non-trivial systems. In this paper we construct the new definition of the classical entailment, into the bargain. Key words: Atomic entailment, atomic inconsistency, classical entailment, relevance
1. Introduction In a number of publications, (see [1] - [7], [9] - [18], [21], [22], [24] - [35], [39] - [45], [53] - [59]), their authors have offered many notions of relevance. Of course, in some publications of these mentioned above, their authors have established the basic properties of the well-known relevant logics. On the other hand, in [14]one can read that although the essence of entailment has been studied from 400 B.C., the problem of establishing such a logic of entailment, which solves the problem of relevance, is still open until now. Thus, the essential aim is to create such a notion of relevance, which generates a system S of logic, which satisfies the following condition: this system S is generated by this notion of relevance, which is defined by a necessary and sufficient condition. Therefore in this paper we at first construct a new definition of entailment, i.e. the definition of atomic entailment. Then we construct the definition of the system based on the atomic entailment. Next, we build Corresponding author:L. T. Stepień, The Pedagogical University of Cracow, Kraków, Poland. E-mail:
[email protected] , www.ltstepien.up.krakow.pl ⊓
² In the next paper we will show that the system 𝑆𝑆 can be used for the formalization of The Arithmetic System (see [20]).
a system 𝑆𝑆 of propositional calculus (see [47], [48]) ⊓
and a system 𝑆𝑆 of predicate calculus, which are based
on the atomic entailment (see [49], [51], [52])². Besides, in this paper, we give also the new definition of the classical entailment.
2. Notational Preliminaries Let →, ~,∨,∧, ≡ denote the connectives of implication, negation, disjunction, conjunction and equivalence, respectively. We use ⇒, ¬, ⇔, &, 𝕍𝕍, ∀, ∃ as metalogical symbols. Next 𝐴𝐴𝐴𝐴0 = {𝑝𝑝, 𝑝𝑝1 , 𝑝𝑝2 , … , 𝑞𝑞, 𝑞𝑞1 , 𝑞𝑞2 , … , 𝑠𝑠, 𝑠𝑠1 , 𝑠𝑠2 , … 𝑡𝑡, … } denotes the set of all propositional variables. 𝑆𝑆0 is the set of all well-formed formulas, which are built in the usual manner from propositional variables and by means of logical connectives. 𝑃𝑃0 (𝜙𝜙) denotes the set of all propositional variables occuring in 𝜙𝜙(𝜙𝜙 ∈ 𝑆𝑆0 ). 𝑅𝑅𝑆𝑆0 denotes the set of all rules over 𝑆𝑆0 . Hence, for every 𝑟𝑟 ∈ 𝑅𝑅𝑆𝑆0 , 〈Π, 𝜙𝜙〉 ∈ 𝑟𝑟 , where Π ⊆ 𝑆𝑆0 and
𝜙𝜙 ∈ 𝑆𝑆0 and Π is a set of premisses and 𝜙𝜙 is a conclusion. Hence, 𝑟𝑟∗0 denotes here the rule of simultaneous substitution for propositional 0 𝑒𝑒 (𝜙𝜙) = 𝜓𝜓], where ℎ𝑒𝑒 is variables.〈{𝜙𝜙}, 𝜓𝜓〉 ∈ 𝑟𝑟∗ ⇔ [ℎ the extension of the mapping 𝑒𝑒: 𝐴𝐴𝐴𝐴0 ⟶ 𝑆𝑆0 (𝑒𝑒 ∈ 𝜀𝜀∗0 )
Atomic Entailment and Atomic Inconsistency and Classical Entailment
to endomorphism ℎ𝑒𝑒 : 𝑆𝑆0 ⟶ 𝑆𝑆0 , where ℎ𝑒𝑒 (𝜙𝜙) = 𝑒𝑒(𝜙𝜙), for 𝜙𝜙 ∈ 𝐴𝐴𝐴𝐴0 ℎ𝑒𝑒 (~𝜙𝜙) = ~ℎ𝑒𝑒 (𝜙𝜙) ℎ𝑒𝑒 (𝜙𝜙𝜙𝜙𝜙𝜙) = ℎ𝑒𝑒 (𝜙𝜙)𝐹𝐹ℎ𝑒𝑒 (𝜓𝜓),
for 𝐹𝐹 ∈ {→,∨,∧, ≡} and for every 𝜙𝜙, 𝜓𝜓 ∈ 𝑆𝑆0 . Thus, 𝜀𝜀∗0 is a class of functions 𝑒𝑒: 𝐴𝐴𝐴𝐴0 ⟶ 𝑆𝑆0 (for details, see [36]) (cf. [19]). 𝑟𝑟00 denotes here the Modus Ponens rule in propositional calculus. 𝑅𝑅0∗ = {𝑟𝑟00 , 𝑟𝑟∗0 } (for details, see [19], [36]). A logical matrix is a pair 𝔐𝔐 = {𝑈𝑈, 𝑈𝑈 ′ } , 𝑈𝑈 is an abstract algebra and 𝑈𝑈′ is a subset of the universe 𝑈𝑈, i.e. 𝑈𝑈 ′ ⊆ 𝑈𝑈. Any 𝑎𝑎 ∈ 𝑈𝑈′ is called a distinguished element of the matrix 𝔐𝔐. 𝐸𝐸(𝔐𝔐) is the set of all formulas valid in the matrix 𝔐𝔐. 𝔐𝔐2 denotes the classical two-valued matrix. Hence, 𝑍𝑍2 is the set of all formulas valid in the classical matrix 𝔐𝔐2 (see [19], [36]). The symbols 𝑥𝑥1 , 𝑥𝑥2 , … are individual variables. 𝑎𝑎1 , 𝑎𝑎2 , … are individual constants. 𝑉𝑉 is the set of all individual variables. 𝑃𝑃𝑖𝑖𝑛𝑛 (𝑖𝑖, 𝑛𝑛 ∈ 𝒩𝒩 = {1, 2, … } ) are 𝑛𝑛 -ary predicate letters. The symbols 𝑓𝑓𝑖𝑖𝑛𝑛 (𝑖𝑖, 𝑛𝑛 ∈ 𝒩𝒩) are n-ary function letters. The symbols ⋀ 𝑥𝑥𝑘𝑘 , ⋁ 𝑥𝑥𝑘𝑘 are quantifiers. ⋀ 𝑥𝑥𝑘𝑘 is the universal quantifier and ⋁ 𝑥𝑥𝑘𝑘 is the existential quantifier. The function letters, applied to the individual variables and individual constants, generate terms. The symbols 𝑡𝑡1 , 𝑡𝑡2, … areterms. 𝑇𝑇 is the set of all terms. The predicate letters, applied to terms, yield simple formulas, i.e. if
𝑃𝑃𝑖𝑖𝑘𝑘 is a predicate letter and 𝑡𝑡1 , … , 𝑡𝑡𝑘𝑘 are terms, then 𝑃𝑃𝑖𝑖𝑘𝑘 (𝑡𝑡1 , … , 𝑡𝑡𝑛𝑛 ) is a simple formula. 𝑆𝑆𝑆𝑆𝑆𝑆 is the set of all simple formulas. Next, 𝐴𝐴𝐴𝐴1 is the set of all atomic formulas, where 𝐴𝐴𝐴𝐴1 = {𝑃𝑃𝑖𝑖𝑘𝑘 �𝑥𝑥𝑗𝑗 1 , … , 𝑥𝑥𝑗𝑗 𝑘𝑘 � ∶ 𝑘𝑘, 𝑖𝑖, 𝑗𝑗1 , … , 𝑗𝑗𝑘𝑘 ∈ 𝒩𝒩} . At last 𝑆𝑆1 is the set of all well-formed formulas. 𝐹𝐹𝐹𝐹(𝜙𝜙) denotes the set of all free variables occuring in 𝜙𝜙 , where 𝜙𝜙 ∈ 𝑆𝑆1 . 𝑥𝑥𝑘𝑘 ∈ 𝐹𝐹𝐹𝐹(𝑡𝑡𝑚𝑚 , 𝜙𝜙) expresses that 𝑥𝑥𝑘𝑘 is free for term 𝑡𝑡𝑚𝑚 in 𝜙𝜙. By 𝑥𝑥𝑘𝑘 /𝑡𝑡𝑚𝑚 we denote the substitution of the term 𝑡𝑡𝑚𝑚 for the individual variable 𝑥𝑥𝑘𝑘 . 𝑃𝑃1 (𝜙𝜙) denotes the set of all predicate letters occuring in 𝜙𝜙(𝜙𝜙 ∈ 𝑆𝑆1 ) . If 𝐹𝐹𝐹𝐹(𝜙𝜙) = {𝑥𝑥1 , … , 𝑥𝑥𝑘𝑘 } , then ⋀ 𝜙𝜙 = ⋀ 𝑥𝑥1 … ⋀ 𝑥𝑥𝑘𝑘 𝜙𝜙. 𝑅𝑅𝑆𝑆1 denotes the set of all rules over 𝑆𝑆1 . Hence, for
61
every 𝑟𝑟 ∈ 𝑅𝑅𝑆𝑆1 , 〈Π, 𝜙𝜙〉 ∈ 𝑟𝑟 , where Π ⊆ 𝑆𝑆1 and
𝜙𝜙 ∈ 𝑆𝑆1 and Π is a set of premisses and 𝜙𝜙 is a conclusion. Hence, 𝑟𝑟∗1 denotes here the rule of simultaneous substitution for predicate letters. 〈{𝜙𝜙}, 𝜓𝜓〉 ∈ 𝑟𝑟∗1 ⇔ [ℎ𝑒𝑒 (𝜙𝜙) = 𝜓𝜓] , where ℎ𝑒𝑒 is the extension of the mapping 𝑒𝑒: 𝑆𝑆𝑆𝑆𝑆𝑆 ⟶ 𝑆𝑆1 (𝑒𝑒 ∈ 𝜀𝜀∗1 ) to endomorphism ℎ𝑒𝑒 : 𝑆𝑆1 ⟶ 𝑆𝑆1 , where ℎ𝑒𝑒 (𝜙𝜙) = 𝑒𝑒(𝜙𝜙),for 𝜙𝜙 ∈ 𝑆𝑆𝑆𝑆𝑆𝑆 ℎ𝑒𝑒 (~𝜙𝜙) = ~ℎ𝑒𝑒 (𝜙𝜙) ℎ𝑒𝑒 (𝜙𝜙𝜙𝜙𝜙𝜙) = ℎ𝑒𝑒 (𝜙𝜙)𝐹𝐹ℎ𝑒𝑒 (𝜓𝜓),
for 𝐹𝐹 ∈ {→,∨,∧, ≡} ℎ 𝑥𝑥𝑘𝑘 𝜙𝜙) = ⋀𝑥𝑥𝑘𝑘 ℎ𝑒𝑒 (𝜙𝜙) 𝑒𝑒 (⋁ ℎ 𝑥𝑥𝑘𝑘 𝜙𝜙) = ⋁𝑥𝑥𝑘𝑘 ℎ𝑒𝑒 (𝜙𝜙), for every 𝜙𝜙, 𝜓𝜓 ∈ 𝑆𝑆1 and 𝑘𝑘 ∈ 𝒩𝒩 (for details, see [37], [38]). Next, 𝑟𝑟01 denotes the Modus Ponens rule in predicate calculus, 𝑟𝑟+1 denotes the generalization rule. 𝑅𝑅0+ = {𝑟𝑟01 , 𝑟𝑟+1 }, 𝑅𝑅0∗+ = {𝑟𝑟01 , 𝑟𝑟∗1 , 𝑟𝑟+1 }. We write 𝑋𝑋 ⊂ 𝑌𝑌, if 𝑋𝑋 ⊆ 𝑌𝑌 and 𝑋𝑋 ≠ 𝑌𝑌. We assume here that for every 𝛼𝛼 ∈ 𝑆𝑆1 , if 𝐹𝐹𝐹𝐹(𝛼𝛼) = {𝑥𝑥1 , . . . , 𝑥𝑥𝑛𝑛 } , then 𝛼𝛼 ∗ = ⋁ 𝑥𝑥1 … ⋁ 𝑥𝑥𝑛𝑛 ∼ 𝛼𝛼 . Hence, for every 𝛼𝛼 ∈ 𝑆𝑆1 , if 𝐹𝐹𝐹𝐹(𝛼𝛼) = ∅ , then 𝛼𝛼 ∗ = ∼ 𝛼𝛼. Analogically, for every 𝛼𝛼 ∈ 𝑆𝑆0 , 𝛼𝛼 ∗ = ∼ 𝛼𝛼. Finally, for any 𝑋𝑋 ⊆ 𝑆𝑆𝑖𝑖 and 𝑅𝑅 ⊆ 𝑅𝑅𝑆𝑆𝑖𝑖 , 𝐶𝐶𝐶𝐶𝑖𝑖 (𝑅𝑅, 𝑋𝑋) 𝑒𝑒 (⋀
is the smallest subset of 𝑆𝑆𝑖𝑖 containing 𝑋𝑋 and closed under the rules 𝑅𝑅 ⊆ 𝑅𝑅𝑆𝑆𝑖𝑖 , where 𝑖𝑖 ∈ {0,1}. The couple 〈𝑅𝑅, 𝑋𝑋〉 is called a system, whenever 𝑅𝑅 ⊆ 𝑅𝑅𝑆𝑆𝑖𝑖 and 𝑋𝑋 ⊆ 𝑆𝑆𝑖𝑖 and 𝑖𝑖 ∈ {0,1}. 𝑆𝑆𝑆𝑆𝑆𝑆𝑆𝑆 ∩ 𝐴𝐴0 denotes here the class of all systems 〈𝑅𝑅, 𝑋𝑋〉, which are based on an atomic entailment, where 𝑅𝑅 ⊆ 𝑅𝑅𝑆𝑆0 and 𝑋𝑋 ⊆
𝑆𝑆0 . 𝑆𝑆𝑆𝑆𝑆𝑆𝑆𝑆 ∩ 𝐴𝐴1 denotes here the class of all systems 〈𝑅𝑅, 𝑋𝑋〉, which are based on an atomic entailment, where 𝑅𝑅 ⊆ 𝑅𝑅𝑆𝑆1 and 𝑋𝑋 ⊆ 𝑆𝑆1 . 𝑆𝑆𝑆𝑆𝑆𝑆𝑆𝑆 ∩ 𝐶𝐶1 denotes
here the class of all systems 〈𝑅𝑅, 𝑋𝑋〉, which are based on a classical entailment, where 𝑅𝑅 ⊆ 𝑅𝑅𝑆𝑆1 and 𝑋𝑋 ⊆ 𝑆𝑆1 . 𝐴𝐴
𝜙𝜙 �𝑅𝑅,𝑋𝑋0 𝜓𝜓 denotes that 𝜓𝜓 results atomically from 𝜙𝜙
on the ground of the system 〈𝑅𝑅, 𝑋𝑋〉, where 𝑅𝑅 ⊆ 𝑅𝑅𝑆𝑆0 𝐴𝐴
and 𝑋𝑋 ⊆ 𝑆𝑆0 . Next, 𝜙𝜙 �𝑅𝑅,𝑋𝑋1 𝜓𝜓 denotes that 𝜓𝜓 results
atomically from 𝜙𝜙 on the ground of the system
Atomic Entailment and Atomic Inconsistency and Classical Entailment
62
𝐶𝐶
〈𝑅𝑅, 𝑋𝑋〉, where 𝑅𝑅 ⊆ 𝑅𝑅𝑆𝑆1 and 𝑋𝑋 ⊆ 𝑆𝑆1 . At last, 𝜙𝜙 � 1 𝜓𝜓 𝑅𝑅,𝑋𝑋
denotes that 𝜓𝜓 results classically from 𝜙𝜙 on the ground of the system 〈𝑅𝑅, 𝑋𝑋〉 , where 𝑅𝑅 ⊆ 𝑅𝑅𝑆𝑆1 and
𝑋𝑋 ⊆ 𝑆𝑆1 . 𝑆𝑆1 = {𝜙𝜙 ∈ 𝑆𝑆1 : 𝐹𝐹𝐹𝐹(𝜙𝜙) = ∅}, 𝑆𝑆1∗ denotes the set of all formulas, which are in normal form (see [19] pp. 35 - 42 and 130 - 132, [20] pp. 214 - 222 and [37] pp. 146 - 149). Definition 2.1. The function 𝑗𝑗: 𝑆𝑆1 ⟶ 𝑆𝑆0 , is defined, as follows: 𝑗𝑗�𝑃𝑃𝑘𝑘𝑛𝑛 (𝑡𝑡1 , … , 𝑡𝑡𝑛𝑛 )� = 𝑝𝑝𝑘𝑘 (𝑝𝑝𝑘𝑘 ∈ 𝐴𝐴𝐴𝐴0 )
𝑗𝑗(~𝜙𝜙) = ~ 𝑗𝑗(𝜙𝜙) 𝑗𝑗(𝜙𝜙𝜙𝜙𝜙𝜙) = 𝑗𝑗(𝜙𝜙)𝐹𝐹𝐹𝐹(𝜓𝜓), for 𝐹𝐹 ∈ {→,∨,∧, ≡} 𝑗𝑗(⋀ 𝑥𝑥𝑘𝑘 𝜙𝜙) = 𝑗𝑗(⋁ 𝑥𝑥𝑛𝑛 𝜙𝜙) = 𝑗𝑗(𝜙𝜙). By 〈𝑅𝑅, 𝑋𝑋〉 ∈ 𝐶𝐶𝐶𝐶𝐶𝐶 𝐴𝐴 we denote here the well-known notion of the absolute consistency (see [36] and [37]). Thus, Definition 2.2. 〈𝑅𝑅, 𝑋𝑋〉 ∈ 𝐶𝐶𝐶𝐶𝐶𝐶 𝐴𝐴 ⟺ 𝐶𝐶𝐶𝐶(𝑅𝑅, 𝑋𝑋) ≠ 𝑆𝑆𝑖𝑖 , where 𝑅𝑅 ⊆ 𝑅𝑅𝑆𝑆𝑖𝑖 , 𝑋𝑋 ⊆ 𝑆𝑆𝑖𝑖 and 𝑖𝑖 ∈ {0,1}.
3. Classical Entailment Definition
3.1.
Let 𝐶𝐶
𝐶𝐶𝐶𝐶1 (𝑅𝑅, 𝑋𝑋) = 𝐿𝐿 ≠ ∅
and
1 𝜓𝜓 iff the following conditions 𝜙𝜙, 𝜓𝜓 ∈ 𝑆𝑆1 . Then 𝜙𝜙 �𝑅𝑅,𝑋𝑋
are satisfied (1) (∀𝑒𝑒 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒 (⋀ 𝜙𝜙) ∈ 𝐿𝐿 ⇒ ℎ𝑒𝑒 (𝜓𝜓) ∈ 𝐿𝐿] (2) (∀𝑒𝑒 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒 �(𝜓𝜓 ∗ → 𝜙𝜙 ∗ ) → 𝜙𝜙 ∗ � ∈ 𝐿𝐿 ⇒ ℎ𝑒𝑒 (𝜙𝜙 ∗ ) ∈ 𝐿𝐿 ]. Definition 3.2. 〈𝑅𝑅, 𝑋𝑋〉 ∈ 𝑆𝑆𝑆𝑆𝑆𝑆𝑆𝑆 ∩ 𝐶𝐶1 iff the following condition is satisfied: (∀𝜙𝜙, 𝜓𝜓 ∈ 𝑆𝑆1 )[⋀ 𝜙𝜙 → 𝜓𝜓 ∈ 𝐶𝐶𝐶𝐶1 (𝑅𝑅, 𝑋𝑋) ⇔ 𝜙𝜙 �
4. The classical predicate logic
𝐶𝐶1
𝑅𝑅,𝑋𝑋
𝜓𝜓].
Let 𝐴𝐴2 denote the set of axioms of the classical
predicate
logic.
Hence,
〈𝑅𝑅0+ , 𝐴𝐴2 〉
denotes
the
classical predicate calculus, where 𝐶𝐶𝐶𝐶(𝑅𝑅0+, 𝐴𝐴2 ) = 𝐿𝐿2
(see [20] and [37]).
Thus, (see [37] p.57, p.71):
Theorem 4.1. 𝐶𝐶𝐶𝐶1 (𝑅𝑅0∗+, 𝐿𝐿2 ) = 𝐿𝐿2 .
Now we notice that on the ground of the classical
predicate calculus, the following theorem is valid (cf. [20] pp. 222 - 223): Theorem 4.2. (on the extensionality of logical expressions). Let 𝑥𝑥1 , … , 𝑥𝑥𝑛𝑛 , 𝑦𝑦1 , … , 𝑦𝑦𝑙𝑙 be all the free variables, which occur in the expressions 𝛼𝛼 and 𝛽𝛽, and let 𝐶𝐶 𝛼𝛼 be any expression that contains 𝛼𝛼 or an expression obtained from 𝛼𝛼 by the substitution for the variables 𝑥𝑥1 , … , 𝑥𝑥𝑛𝑛 of some other variables different from the bound variables occurring in the expressions 𝛼𝛼 or 𝛽𝛽 , and let 𝐶𝐶𝛽𝛽 differ from 𝐶𝐶 𝛼𝛼 only in that in certain places (unnecessarily in all these places) in which in 𝐶𝐶 𝛼𝛼 there occurs 𝛼𝛼 or an expression obtained from 𝛼𝛼 by a substitution for the variables 𝑥𝑥1 , … , 𝑥𝑥𝑛𝑛 , in the corresponding places in
𝐶𝐶𝛽𝛽 there occurs 𝛽𝛽 or an expression obtained from 𝛽𝛽 by an appropriate substitution, while the variables 𝑦𝑦1 , … , 𝑦𝑦𝑙𝑙 are all the free variables in 𝐶𝐶 𝛼𝛼 and 𝐶𝐶𝛽𝛽 . Then the sentence: ⋀ … 𝑦𝑦1 , … , 𝑦𝑦𝑙𝑙 �⋀𝑥𝑥1 , … , 𝑥𝑥𝑛𝑛 (𝛼𝛼 ≡ 𝛽𝛽) → �𝐶𝐶 𝛼𝛼 ≡ 𝐶𝐶𝛽𝛽 ��
is a theorem in 𝐿𝐿2 .
5. Atomic Entailment In [57] one can read that Lewis told that from his very first contact with the logic of “Principia Mathematica”, he had been bothered by the paradoxes of material implication. As Whitehead and Russell have it written, a true proposition is implied by arbitrary (true or false) proposition, while a false proposition implies arbitrary (true or false) proposition. Aiming at avoiding these consequences of the material conditional, Lewis wrote his first paper devoted to logic (in this current paper, the Lewis' paper is as [25]). At first, it ought to be noticed here that the results contained in [1] - [7], [9] - [18], [21], [22], [24] - [35], [39] - [45], [53] - [59], and in the other papers, have essentially contributed to the better understanding of the problem of relevance. Thus (see [47], [48], [49], [51], [52]): Definition 5.1. Let 𝐶𝐶𝐶𝐶0 (𝑅𝑅, 𝑋𝑋) = 𝐿𝐿 ≠ ∅ and 𝐴𝐴
𝜙𝜙, 𝜓𝜓 ∈ 𝑆𝑆0 . Then 𝜙𝜙 �𝑅𝑅,𝑋𝑋0 𝜓𝜓 iff the following conditions
Atomic Entailment and Atomic Inconsistency and Classical Entailment
are satisfied: (1) (∀𝑒𝑒 ∈ 𝜀𝜀∗0 )[ℎ𝑒𝑒 (𝜙𝜙) ∈ 𝐿𝐿 ⇒ ℎ𝑒𝑒 (𝜓𝜓) ∈ 𝐿𝐿 & 𝑃𝑃0 �ℎ𝑒𝑒 (𝜙𝜙)� ⊆ 𝑃𝑃0 �ℎ𝑒𝑒 (𝜓𝜓)�] (2) (∀𝑒𝑒 ∈ 𝜀𝜀∗0 )[ℎ𝑒𝑒 ((𝜓𝜓∗ → 𝜙𝜙 ∗ ) → 𝜙𝜙 ∗ ) ∈ 𝐿𝐿 ⇒ ℎ𝑒𝑒 (𝜙𝜙 ∗ ) ∈ 𝐿𝐿 & 𝑃𝑃0 �ℎ𝑒𝑒 (𝜓𝜓∗ )� ⊆ 𝑃𝑃0 �ℎ𝑒𝑒 (𝜙𝜙 ∗ )�].
Definition 5.2. 〈𝑅𝑅, 𝑋𝑋〉 ∈ 𝑆𝑆𝑆𝑆𝑆𝑆𝑆𝑆 ∩ 𝐴𝐴0 iff the following condition is satisfied: (∀𝜓𝜓, 𝜙𝜙 ∈ 𝑆𝑆0 )[𝜙𝜙 → 𝜓𝜓 ∈ 𝐶𝐶𝐶𝐶0 (𝑅𝑅, 𝑋𝑋) ⇔ 𝜙𝜙 �
Definition
5.3.
Let
𝐴𝐴 1
𝐴𝐴 0
𝑅𝑅,𝑋𝑋
𝜓𝜓].
𝐶𝐶𝐶𝐶1 (𝑅𝑅, 𝑋𝑋) = 𝐿𝐿 ≠ ∅
and
𝜙𝜙, 𝜓𝜓 ∈ 𝑆𝑆1 . Then 𝜙𝜙 �𝑅𝑅,𝑋𝑋 𝜓𝜓 iff the following conditions
are satisfied: (1) (∀𝑒𝑒 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒 (⋀ 𝜙𝜙) ∈ 𝐿𝐿 ⇒ ℎ𝑒𝑒 (𝜓𝜓) ∈ 𝐿𝐿 & 𝑃𝑃1 (ℎ𝑒𝑒 (⋀𝜙𝜙)) ⊆ 𝑃𝑃1 (ℎ𝑒𝑒 (𝜓𝜓))] (2) (∀𝑒𝑒 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒 ((𝜓𝜓 ∗ → 𝜙𝜙 ∗ ) → 𝜙𝜙 ∗ ) ∈ 𝐿𝐿 ⇒ ℎ𝑒𝑒 (𝜙𝜙 ∗ ) ∈ 𝐿𝐿 & 𝑃𝑃1 �ℎ𝑒𝑒 (𝜓𝜓∗ )� ⊆ 𝑃𝑃1 �ℎ𝑒𝑒 (𝜙𝜙 ∗ )��. Definition 5.4. 〈𝑅𝑅, 𝑋𝑋〉 ∈ 𝑆𝑆𝑆𝑆𝑆𝑆𝑆𝑆 ∩ 𝐴𝐴1 iff the following condition is satisfied:
(∀𝜓𝜓, 𝜙𝜙 ∈ 𝑆𝑆1 )[⋀ 𝜙𝜙 → 𝜓𝜓 ∈ 𝐶𝐶𝐶𝐶1 (𝑅𝑅, 𝑋𝑋) ⇔ 𝜙𝜙 �
6. Atomic Inconsistency
𝐴𝐴 1
𝑅𝑅,𝑋𝑋
𝜓𝜓].
By 𝑆𝑆𝑆𝑆𝑆𝑆𝑆𝑆 ∩ 𝐴𝐴𝐴𝐴𝐴𝐴𝐴𝐴 we denote here the class of all systems 〈𝑅𝑅, 𝑋𝑋〉, which have the property of atomic inconsistency (see also [8], [23], [60]), where 𝑅𝑅 ⊆ 𝑅𝑅𝑆𝑆𝑖𝑖
and 𝑋𝑋 ⊆ 𝑆𝑆𝑖𝑖 and 𝑖𝑖 ∈ {0,1}. Definition 6.1. Let 𝑖𝑖 ∈ {0,1} and 𝛼𝛼 ∈ 𝑆𝑆𝑖𝑖 . Then 𝑆𝑆𝑖𝑖𝑖𝑖 = {𝜙𝜙 ∈ 𝑆𝑆𝑖𝑖 ∶ 𝑃𝑃𝑖𝑖 (𝜙𝜙) ⊆ 𝑃𝑃𝑖𝑖 (𝛼𝛼)}. Definition 6.2. Let 𝑅𝑅 ⊆ 𝑅𝑅𝑆𝑆𝑖𝑖 and 𝑋𝑋 ⊆ 𝑆𝑆𝑖𝑖 and 𝑖𝑖 ∈ {0,1}. Then 〈𝑅𝑅, 𝑋𝑋〉 ∈ 𝑆𝑆𝑆𝑆𝑆𝑆𝑆𝑆 ∩ 𝐴𝐴𝐴𝐴𝐴𝐴𝐴𝐴 ⇔ (∀𝛼𝛼 ∈ 𝑆𝑆𝑖𝑖 ){[𝑆𝑆𝑖𝑖𝑖𝑖 ⊆ 𝐶𝐶𝐶𝐶(𝑅𝑅, 𝑋𝑋 ∪ {𝛼𝛼, ~𝛼𝛼})]& (∀𝛽𝛽 ∈ 𝑆𝑆𝑖𝑖 )[𝑃𝑃𝑖𝑖 (𝛽𝛽) ⊈ 𝑃𝑃𝑖𝑖 (𝛼𝛼) ⇒ 𝛽𝛽 ∉ 𝐶𝐶𝐶𝐶(𝑅𝑅, 𝑋𝑋 ∪ {𝛼𝛼, ~𝛼𝛼})𝕍𝕍 ~𝛽𝛽 ∉ 𝐶𝐶𝐶𝐶(𝑅𝑅, 𝑋𝑋 ∪ {𝛼𝛼, ~𝛼𝛼})]}.
7. System 𝑺𝑺
Let us take the matrix 𝔐𝔐𝐷𝐷 = 〈{0,1,2}, {1,2}, 𝑓𝑓𝐷𝐷→ , 𝑓𝑓𝐷𝐷≡ , 𝑓𝑓𝐷𝐷∨ , 𝑓𝑓𝐷𝐷∧ , 𝑓𝑓𝐷𝐷∼ 〉, where:
63
𝑓𝑓𝐷𝐷→ 0 1 2
0 1 0 0
1 1 1 1
2 1 0 2
𝑓𝑓𝐷𝐷≡ 0 1 2
0 1 0 0
1 0 1 0
2 0 0 2
𝑓𝑓𝐷𝐷∨ 0 1 2
0 0 1 0
1 1 1 1
2 0 1 2
𝑓𝑓𝐷𝐷∧ 0 1 2
0 0 0 0
1 0 1 1
2 0 1 2
𝑓𝑓𝐷𝐷∼ 0 1 2
1 0 2
In [47] (see [48]) we have defined the system 𝑆𝑆 as follows:
Definition 7.1. 𝑆𝑆 = 〈𝑅𝑅0∗ , 𝑇𝑇𝐷𝐷 〉, where 𝑇𝑇𝐷𝐷 = 𝐸𝐸(𝔐𝔐𝐷𝐷 ). Thus, the system 𝑆𝑆 is the logic that is obtained from the set of valid formulas in the matrix 𝔐𝔐𝐷𝐷 , by the rules of substitution and detachment. It should be noticed here that the matrix 𝔐𝔐′𝐷𝐷 = 〈{0,1,2}, {1,2}, 𝑓𝑓𝐷𝐷→ , 𝑓𝑓𝐷𝐷∼ 〉 was investigated by B. Sobocinski (see [46], [47]). Next, in [47] we have proved the following: Theorem 7.2. Let 𝜙𝜙, 𝜓𝜓 ∈ 𝑆𝑆0 and (∃𝑒𝑒 ∈ 𝜀𝜀∗0 )[ℎ𝑒𝑒 (𝜙𝜙) ∈ 𝑇𝑇𝐷𝐷 ]. Then 𝜙𝜙 → 𝜓𝜓 ∈ 𝐶𝐶𝐶𝐶0 (𝑅𝑅0∗ , 𝑇𝑇𝐷𝐷 ) iff (∀𝑒𝑒 ∈ 𝜀𝜀∗0 )[ℎ𝑒𝑒 (𝜙𝜙) ∈ 𝑇𝑇𝐷𝐷 ⇒ ℎ𝑒𝑒 (𝜓𝜓) ∈ 𝑇𝑇𝐷𝐷 & 𝑃𝑃0 �ℎ𝑒𝑒 (𝜙𝜙)� ⊆ 𝑃𝑃0 �ℎ𝑒𝑒 (𝜓𝜓)�].
Theorem 7.3. The system 𝑆𝑆 is axiomatizable. ⊓
8. System 𝑺𝑺
At first we define the set 𝐿𝐿𝐷𝐷 , putting: Definition 8.1. 𝐿𝐿𝐷𝐷 = {𝜙𝜙 ∈ 𝑆𝑆1 : 𝑗𝑗(𝜙𝜙) ∈ 𝑇𝑇𝐷𝐷 & 𝜙𝜙 ∈ 𝐿𝐿2 }. ⊓
Next, we define the system 𝑆𝑆, as follows: ⊓
Definition 8.2. 𝑆𝑆 = 〈𝑅𝑅0+ , 𝐿𝐿𝐷𝐷 〉.
By Theorem 4.1 and by Definition 8.1, one obtains: Corollary 8.3. 𝐶𝐶𝐶𝐶1 (𝑅𝑅0∗+ , 𝐿𝐿𝐷𝐷 ) = 𝐿𝐿𝐷𝐷 . By Definition 8.1 and by Corollary 8.3, we get
64
Atomic Entailment and Atomic Inconsistency and Classical Entailment
Corollary 8.4. Let 𝛼𝛼, 𝛽𝛽, 𝛾𝛾, 𝜙𝜙, 𝜓𝜓, 𝛿𝛿 ∈ 𝑆𝑆1 and 𝑄𝑄𝑖𝑖 ∈ {⋀ 𝑥𝑥𝑖𝑖 , ⋁ 𝑥𝑥𝑖𝑖 } and 𝑖𝑖, 𝑘𝑘, 𝑠𝑠 ∈ 𝒩𝒩. Then the following formulas belong to 𝐿𝐿𝐷𝐷 : (1) 𝛼𝛼 → 𝛼𝛼 (2) 𝛼𝛼 → [(𝛼𝛼 → 𝛽𝛽) → 𝛽𝛽] (3) (𝛼𝛼 → 𝛽𝛽) → [(𝛽𝛽 → 𝛾𝛾) → (𝛼𝛼 → 𝛾𝛾)] (4) [𝛼𝛼 → (𝛽𝛽 → 𝛾𝛾)] → [𝛽𝛽 → (𝛼𝛼 → 𝛾𝛾)] (5) [𝛼𝛼 → (𝛼𝛼 → 𝛽𝛽)] → (𝛼𝛼 → 𝛽𝛽) (6) {[(𝛽𝛽 → 𝛾𝛾) → (𝛼𝛼 → 𝛾𝛾)] → 𝛿𝛿} → [(𝛼𝛼 → 𝛽𝛽) → 𝛿𝛿] (7) [𝛼𝛼 → (𝛽𝛽 → 𝛾𝛾)] → {(𝛿𝛿 → 𝛽𝛽) → [𝛼𝛼 → (𝛿𝛿 → 𝛾𝛾)]} (8) [𝛼𝛼 → (𝛽𝛽 → 𝛾𝛾)] → [(𝛼𝛼 → 𝛽𝛽) → (𝛼𝛼 → 𝛾𝛾)] (9) (𝛽𝛽 → 𝛾𝛾) → [(𝛼𝛼 → 𝛽𝛽) → (𝛼𝛼 → 𝛾𝛾)] (10) (𝛽𝛽 → 𝛾𝛾) → {(𝛼𝛼 → 𝛽𝛽) → [(𝛾𝛾 → 𝛿𝛿) → (𝛼𝛼 → 𝛿𝛿)]} (11) ~~ 𝛼𝛼 → 𝛼𝛼 (12) 𝛼𝛼 → ~~𝛼𝛼 (13)(~𝛼𝛼 → 𝛼𝛼) → 𝛼𝛼 (14) (𝛼𝛼 → ~ 𝛼𝛼) → ~𝛼𝛼 (15) ( ~~𝛼𝛼 → ~~𝛽𝛽) → (𝛼𝛼 → 𝛽𝛽) (16) (𝛼𝛼 → ~𝛽𝛽 ) → (~~𝛼𝛼 → ~𝛽𝛽) (17) (𝛼𝛼 → 𝛽𝛽 ) → (𝛼𝛼 → ~~𝛽𝛽) (18) (𝛼𝛼 → ~ 𝛽𝛽 ) → (𝛽𝛽 → ~ 𝛼𝛼) (19) (~𝛽𝛽 → ~~ 𝛼𝛼) → (~𝛽𝛽 → 𝛼𝛼) (20) (~ 𝛼𝛼 → 𝛽𝛽) → ( ~𝛽𝛽 → 𝛼𝛼) (21) 𝛼𝛼 → ~(𝛼𝛼 → ~ 𝛼𝛼) (22) (~ 𝛼𝛼 → ~~ 𝛼𝛼) → 𝛼𝛼 (23) (𝛼𝛼 → 𝛽𝛽) → (~ 𝛽𝛽 → ~ 𝛼𝛼) (24) (𝛼𝛼 → 𝛽𝛽) → [(𝛼𝛼 → ~ 𝛽𝛽) → ~𝛼𝛼] (25) ( ~𝛼𝛼 → 𝛽𝛽) → [( ~𝛽𝛽 → ~ 𝛼𝛼) → ~~𝛽𝛽] (26) ( ~𝛼𝛼 → 𝛽𝛽) → [(𝛼𝛼 → 𝛽𝛽) → 𝛽𝛽] (27) 𝛼𝛼 → [𝛽𝛽 → ~(𝛼𝛼 → ~ 𝛽𝛽)] (28) 𝛼𝛼 ≡ 𝛼𝛼 (29) 𝛼𝛼 ≡ ~~𝛼𝛼 (30) ~~𝛼𝛼 ≡ 𝛼𝛼 (31) (𝛼𝛼 → 𝛽𝛽) → [(𝛽𝛽 ≡ 𝛾𝛾) → (𝛼𝛼 → 𝛾𝛾)] (32) (𝛼𝛼 ≡ 𝛽𝛽) → [(𝛽𝛽 ≡ 𝛾𝛾) → (𝛼𝛼 → 𝛾𝛾)] (33) (𝛽𝛽 → 𝛼𝛼) → [(𝛽𝛽 ≡ 𝛾𝛾) → (𝛾𝛾 → 𝛼𝛼)] (34) (𝛼𝛼 ≡ 𝛽𝛽) → (𝛼𝛼 → 𝛽𝛽) (35) (𝛼𝛼 ≡ 𝛽𝛽) → (𝛽𝛽 → 𝛼𝛼) (36) (𝛼𝛼 → 𝛽𝛽) → [(𝛽𝛽 → 𝛼𝛼) → (𝛼𝛼 ≡ 𝛽𝛽)] (37) (𝛼𝛼 ≡ 𝛽𝛽) → [(𝛼𝛼 → 𝛾𝛾) ≡ (𝛽𝛽 → 𝛾𝛾)]
(38) (𝛼𝛼 ≡ 𝛽𝛽) → [(𝛾𝛾 ≡ 𝛼𝛼) ≡ (𝛾𝛾 ≡ 𝛽𝛽)] (39) (𝛼𝛼 ≡ 𝛽𝛽) → (𝛽𝛽 ≡ 𝛼𝛼) (40) 𝛼𝛼 → (𝛼𝛼 ∨ 𝛽𝛽), if 𝑃𝑃1 (𝛼𝛼) = 𝑃𝑃1 (𝛼𝛼 ∨ 𝛽𝛽) (41) 𝛼𝛼 → (𝛽𝛽 ∨ 𝛼𝛼), if 𝑃𝑃1 (𝛼𝛼) = 𝑃𝑃1 (𝛽𝛽 ∨ 𝛼𝛼) (42) (𝛼𝛼 ∨ 𝛽𝛽) → [(𝛼𝛼 → 𝛽𝛽) → 𝛽𝛽] (43) (𝛼𝛼 → 𝛽𝛽) → [(𝛼𝛼 ∨ 𝛾𝛾) → (𝛾𝛾 ∨ 𝛽𝛽)] (44) (𝛼𝛼 → 𝛽𝛽) → [(𝛼𝛼 ∨ 𝛾𝛾) → (𝛽𝛽 ∨ 𝛾𝛾)] (45) (𝛼𝛼 → 𝛽𝛽) → [(𝛾𝛾 ∨ 𝛼𝛼) → (𝛾𝛾 ∨ 𝛽𝛽)] (46) [𝛼𝛼 ∨ (𝛽𝛽 ∨ 𝛾𝛾)] → [(𝛼𝛼 ∨ 𝛽𝛽) ∨ 𝛾𝛾] (47) [𝛼𝛼 ∨ (𝛽𝛽 ∨ 𝛾𝛾)] → [𝛼𝛼 ∨ (𝛾𝛾 ∨ 𝛽𝛽)] (48) [𝛼𝛼 ∨ (𝛾𝛾 ∨ 𝛽𝛽)] → [(𝛼𝛼 ∨ 𝛽𝛽) ∨ 𝛾𝛾] (49) [𝛼𝛼 ∨ (𝛽𝛽 ∨ 𝛾𝛾)] → [𝛽𝛽 ∨ (𝛼𝛼 ∨ 𝛾𝛾)] (50) [𝛾𝛾 ∨ (𝛼𝛼 ∨ 𝛽𝛽)] → [𝛽𝛽 ∨ (𝛾𝛾 ∨ 𝛼𝛼)] (51) [𝛽𝛽 ∨ (𝛾𝛾 ∨ 𝛼𝛼)] → [𝛽𝛽 ∨ (𝛼𝛼 ∨ 𝛾𝛾)] (52) [(𝛽𝛽 ∨ 𝛼𝛼) ∨ 𝛾𝛾] → [𝛽𝛽 ∨ (𝛼𝛼 ∨ 𝛾𝛾)] (53) (𝛼𝛼 → 𝛽𝛽) ∨ (𝛽𝛽 → 𝛼𝛼) (54) (𝛼𝛼 → 𝛽𝛽) → {(𝛾𝛾 → 𝛽𝛽) → [(𝛼𝛼 ∨ 𝛾𝛾) → 𝛽𝛽]} (55) ~𝛼𝛼 ∨ 𝛼𝛼 (56) 𝛼𝛼 ∨ ~𝛼𝛼 (57) (𝛼𝛼 ∨ 𝛽𝛽) → (~𝛽𝛽 → 𝛼𝛼) (58) (𝛼𝛼 ∨ 𝛽𝛽) → (~𝛼𝛼 → 𝛽𝛽) (59) (~𝛼𝛼 ∨ 𝛽𝛽) → (𝛼𝛼 → 𝛽𝛽) (60) 𝛼𝛼 → (𝛼𝛼 ∧ 𝛼𝛼) (61) (𝛼𝛼 ∧ 𝛽𝛽) → (𝛽𝛽 ∧ 𝛼𝛼) (62) 𝛼𝛼 → [𝛽𝛽 → (𝛼𝛼 ∧ 𝛽𝛽)] (63) [(𝛼𝛼 ∧ 𝛽𝛽) → (𝛽𝛽 → 𝛾𝛾)] → [(𝛼𝛼 ∧ 𝛽𝛽) → 𝛾𝛾] (64) [𝛼𝛼 → (𝛽𝛽 → 𝛾𝛾)] → [(𝛼𝛼 ∧ 𝛽𝛽) → 𝛾𝛾] (65) [(𝛼𝛼 ∧ 𝛽𝛽) → 𝛾𝛾] → [𝛼𝛼 → (𝛽𝛽 → 𝛾𝛾)] (66) [(𝛼𝛼 → 𝛽𝛽) ∧ 𝛼𝛼] → 𝛽𝛽 (67) [(𝛼𝛼 ∧ 𝛾𝛾) → 𝛽𝛽] → [(𝛼𝛼 ∧ 𝛾𝛾) → (𝛽𝛽 ∧ 𝛾𝛾)] (68) (𝛼𝛼 → 𝛽𝛽) → [(𝛾𝛾 ∧ 𝛼𝛼) → (𝛾𝛾 ∧ 𝛽𝛽)] (69) (𝛼𝛼 → 𝛽𝛽) → {(𝛼𝛼 → 𝛾𝛾) → [𝛼𝛼 → (𝛽𝛽 ∧ 𝛾𝛾)]} (70) [(𝛼𝛼 → 𝛾𝛾) ∧ (𝛽𝛽 → 𝛿𝛿)] → [(𝛼𝛼 ∧ 𝛽𝛽) → (𝛾𝛾 ∧ 𝛿𝛿)] (71) [(𝛼𝛼 → 𝛾𝛾) ∧ (𝛽𝛽 → 𝛿𝛿)] → [(𝛽𝛽 ∧ 𝛼𝛼) → (𝛿𝛿 ∧ 𝛾𝛾)] (72) [(𝛼𝛼 → 𝛽𝛽) ∧ (𝛼𝛼 → 𝛾𝛾)] → [α → (𝛽𝛽 ∧ 𝛾𝛾)] (73) [(𝛼𝛼 ∧ 𝛽𝛽)∧ 𝛾𝛾] →{[(𝛼𝛼 ∧ 𝛽𝛽)∧ 𝛾𝛾]∧ 𝛽𝛽} (74) {[(𝛼𝛼 ∧ 𝛽𝛽)∧ 𝛾𝛾]∧ 𝛽𝛽}→[(𝛼𝛼 ∧ 𝛾𝛾) ∧ 𝛽𝛽] (75) ~(𝛼𝛼 ∧ ~𝛼𝛼) (76) ~(~𝛼𝛼 ∧ 𝛼𝛼) (77) ~(𝛼𝛼 → 𝛽𝛽) →(𝛼𝛼 ∧ ~𝛽𝛽) (78) [~(𝛼𝛼 ∧ ~𝛽𝛽) ∧ 𝛼𝛼] → 𝛽𝛽
Atomic Entailment and Atomic Inconsistency and Classical Entailment
(79) [𝛼𝛼 ∧ ~( 𝛼𝛼 ∧ ~𝛽𝛽)] → 𝛽𝛽 (80) (𝛼𝛼 ∧ 𝛽𝛽)→ (~~𝛼𝛼 ∧ ~~𝛽𝛽) (81) (𝛼𝛼 ∧ 𝛽𝛽)→ ~(𝛼𝛼 → ~𝛽𝛽) (82) (𝛼𝛼 ∧ ~~𝛽𝛽) → (𝛼𝛼 ∧ 𝛽𝛽) (83) ~(𝛼𝛼 → ~𝛽𝛽) → (𝛼𝛼 ∧ 𝛽𝛽) (84) (𝛼𝛼 → ~~𝛽𝛽) → ~ ( 𝛼𝛼 ∧ ~𝛽𝛽) (85) (𝛼𝛼 → ~𝛽𝛽) → ~ ( 𝛼𝛼 ∧ 𝛽𝛽) (86) (𝛼𝛼 → 𝛽𝛽) ≡ (~𝛽𝛽 → ~𝛼𝛼) (87) (𝛼𝛼 ≡ 𝛽𝛽)≡ (~𝛼𝛼 ≡ ~𝛽𝛽) (88) (𝛼𝛼 ∧ 𝛽𝛽) ≡ ( 𝛽𝛽 ∧ 𝛼𝛼) (89) [𝛼𝛼 ∧ (𝛽𝛽 ∧ 𝛾𝛾)] ≡[(𝛼𝛼 ∧ 𝛽𝛽)∧ 𝛾𝛾] (90) [(𝛼𝛼 ≡ 𝛽𝛽)∧ (𝛾𝛾 ≡ 𝛿𝛿)] → [(𝛼𝛼 → 𝛾𝛾)≡ ( 𝛽𝛽 → 𝛿𝛿)] (91) (𝛼𝛼 ≡ 𝛽𝛽) → [(𝛽𝛽 → 𝛼𝛼) ∧ (𝛼𝛼 → 𝛽𝛽)] (92) (𝛼𝛼 ≡ 𝛽𝛽) → [(𝛼𝛼 → 𝛽𝛽) ∧ (𝛽𝛽 → 𝛼𝛼)] (93)(𝛼𝛼 ∧ 𝛼𝛼) ≡ 𝛼𝛼 (94) (𝛼𝛼 ≡ 𝛽𝛽) → [(𝛼𝛼 ∧ 𝛾𝛾) ≡ (𝛽𝛽 ∧ 𝛾𝛾)] (95) (𝛼𝛼 ≡ 𝛽𝛽) → [(𝛾𝛾 ∧ 𝛼𝛼) ≡ (𝛾𝛾 ∧ 𝛽𝛽)] (96) [(𝛼𝛼 ≡ 𝛽𝛽) ∧ (𝛾𝛾 ≡ 𝛿𝛿)] → [(𝛼𝛼 ≡ 𝛾𝛾) ≡ (𝛽𝛽 ≡ 𝛿𝛿)] (97) [(𝛼𝛼 → 𝛾𝛾) ∧ (𝛾𝛾 → 𝛼𝛼)] → (𝛼𝛼 ≡ 𝛾𝛾) (98) [(𝛼𝛼 ≡ 𝛽𝛽) ∧ (𝛾𝛾 ≡ 𝛿𝛿)] → [(𝛼𝛼 ∧ 𝛾𝛾) ≡ (𝛽𝛽 ∧ 𝛿𝛿)] (99) [(𝛼𝛼 ≡ 𝛽𝛽) ∧ (𝛽𝛽 ≡ 𝛾𝛾)] →[(𝛼𝛼 → 𝛾𝛾) ∧ (𝛾𝛾 → 𝛼𝛼)]
(100) (𝛼𝛼 ∨ 𝛼𝛼) ≡ 𝛼𝛼 (101) (𝛼𝛼 ∨ 𝛽𝛽) ≡ (𝛽𝛽 ∨ 𝛼𝛼) (102) (𝛼𝛼 ≡ 𝛽𝛽) → [(𝛾𝛾 ∨ 𝛼𝛼) ≡ (𝛾𝛾 ∨ 𝛽𝛽)] (103) (𝛼𝛼 ∨ 𝛽𝛽) ≡ (~𝛼𝛼 → 𝛽𝛽) (104) (𝛼𝛼 → 𝛽𝛽) ≡ (~𝛼𝛼 ∨ 𝛽𝛽) (105) [(𝛼𝛼 ≡ 𝛽𝛽) ∧ (𝛾𝛾 ≡ 𝛿𝛿)] →[(𝛼𝛼 ∨ 𝛾𝛾) ≡ (𝛽𝛽 ∨ 𝛿𝛿)] (106) ~(𝛼𝛼 ∧ 𝛽𝛽) ≡ (𝛼𝛼 → ~𝛽𝛽) (107) ~(𝛼𝛼 ∧ 𝛽𝛽) ≡ (𝛽𝛽 → ~𝛼𝛼) (108) (𝛼𝛼 ∨ 𝛽𝛽) → ~(~𝛼𝛼 ∧ ~𝛽𝛽) (109) (~𝛼𝛼 ∧ ~𝛽𝛽) → ~ (𝛼𝛼 ∨ 𝛽𝛽) (110) ~(~𝛼𝛼 ∨ ~𝛽𝛽) → (𝛼𝛼 ∧ 𝛽𝛽) (111) ~(𝛼𝛼 ∧ 𝛽𝛽) → (~𝛼𝛼 ∨ ~ 𝛽𝛽) (112) ~(𝛼𝛼 ∨ 𝛽𝛽) → (~𝛼𝛼 ∧ ~𝛽𝛽) (113) ~(~𝛼𝛼 ∧ ~𝛽𝛽) → (𝛼𝛼 ∨ 𝛽𝛽) (114) (𝛼𝛼 ∧ 𝛽𝛽) → ~(~𝛼𝛼 ∨ ~ 𝛽𝛽) (115) (~𝛼𝛼 ∨ ~𝛽𝛽) → ~(𝛼𝛼 ∧ 𝛽𝛽) (116) (𝛼𝛼 ∨ 𝛽𝛽) ≡ ~(~𝛼𝛼 ∧ ~𝛽𝛽) (117) (𝛼𝛼 ∧ 𝛽𝛽) ≡ ~(~𝛼𝛼 ∨ ~ 𝛽𝛽) (118) (𝛼𝛼 ∧ 𝛽𝛽) ≡ ~(𝛼𝛼 → ~ 𝛽𝛽) (119) (𝛼𝛼 → 𝛽𝛽) ≡ ~(𝛼𝛼 ∧ ~ 𝛽𝛽)
65
(i)⋀ 𝜙𝜙 → 𝜙𝜙 (ii) ⋀ 𝑥𝑥𝑘𝑘 𝜙𝜙 → ⋁ 𝑥𝑥𝑘𝑘 𝜙𝜙 (iii) ⋀ 𝑥𝑥𝑘𝑘 𝜙𝜙 ≡ 𝜙𝜙, if 𝑥𝑥𝑘𝑘 ∉ 𝐹𝐹𝐹𝐹(𝜙𝜙) (iv) ⋁ 𝑥𝑥𝑘𝑘 𝜙𝜙 ≡ 𝜙𝜙, if 𝑥𝑥𝑘𝑘 ∉ 𝐹𝐹𝐹𝐹(𝜙𝜙) (v) ⋀ 𝑥𝑥𝑘𝑘 (𝜙𝜙 → 𝜓𝜓) ≡ (𝜙𝜙 → ⋀𝑥𝑥𝑘𝑘 𝜓𝜓), if𝑥𝑥𝑘𝑘 ∉ 𝐹𝐹𝐹𝐹(𝜙𝜙) (vi) ⋁ 𝑥𝑥𝑘𝑘 (𝜙𝜙 → 𝜓𝜓) ≡ (𝜙𝜙 → ⋁ 𝑥𝑥𝑘𝑘 𝜓𝜓), if 𝑥𝑥𝑘𝑘 ∉ 𝐹𝐹𝐹𝐹(𝜙𝜙) (vii)⋀ 𝑥𝑥𝑘𝑘 (𝜙𝜙 → 𝜓𝜓) ≡ (⋁𝑥𝑥𝑘𝑘 𝜙𝜙 → 𝜓𝜓), if 𝑥𝑥𝑘𝑘 ∉ 𝐹𝐹𝐹𝐹(𝜓𝜓) (viii) ⋁ 𝑥𝑥𝑘𝑘 ~𝜙𝜙 ≡ ~ ⋀ 𝑥𝑥𝑘𝑘 𝜙𝜙 (ix) 𝛼𝛼 → ⋁ 𝑥𝑥𝑘𝑘 𝛼𝛼 (x) (𝜙𝜙 → ⋀ 𝑥𝑥𝑘𝑘 𝜓𝜓 ) → [(⋀ 𝑥𝑥𝑘𝑘 𝜓𝜓 → 𝜙𝜙) → (𝜙𝜙 → 𝜓𝜓)] (xi) (⋁ 𝑥𝑥𝑘𝑘 𝜙𝜙 → 𝜓𝜓) → [(𝜓𝜓 → ⋁ 𝑥𝑥𝑘𝑘 𝜙𝜙) → (𝜙𝜙 → 𝜓𝜓)] (xii) 𝜙𝜙𝑥𝑥𝑘𝑘 /𝑡𝑡𝑠𝑠 → ⋁ 𝑥𝑥𝑘𝑘 𝜙𝜙, if 𝑥𝑥𝑘𝑘 ∈ 𝐹𝐹𝐹𝐹(𝑡𝑡𝑠𝑠 , 𝜙𝜙) (xiii) ⋀ 𝑥𝑥𝑘𝑘 ( 𝜙𝜙 → 𝜓𝜓) → (⋀ 𝑥𝑥𝑘𝑘 𝜙𝜙 → ⋀ 𝑥𝑥𝑘𝑘 𝜓𝜓) (xiv) ⋀ 𝑥𝑥𝑘𝑘 ( 𝜙𝜙 → 𝜓𝜓) → ( ⋁ 𝑥𝑥𝑘𝑘 𝜙𝜙 → ⋁ 𝑥𝑥𝑘𝑘 𝜓𝜓) (xv) ⋀ 𝑥𝑥𝑘𝑘 (𝛼𝛼 ≡ 𝛽𝛽) → ( ⋀ 𝑥𝑥𝑘𝑘 𝛼𝛼 ≡ ⋀ 𝑥𝑥𝑘𝑘 𝛽𝛽) (xvi) ⋀ 𝑥𝑥𝑘𝑘 (𝛼𝛼 ≡ 𝛽𝛽) → ( ⋁ 𝑥𝑥𝑘𝑘 𝛼𝛼 ≡ ⋁ 𝑥𝑥𝑘𝑘 𝛽𝛽) (xvii) ~ ⋁ 𝑥𝑥𝑘𝑘 ~(𝜙𝜙 → 𝜓𝜓) ≡ (⋁𝑥𝑥𝑘𝑘 𝜙𝜙 → 𝜓𝜓),if 𝑥𝑥𝑘𝑘 ∉ 𝐹𝐹𝐹𝐹(𝜓𝜓) (xviii) ⋀ 𝑥𝑥𝑘𝑘 (𝜙𝜙 ∧ 𝜓𝜓) ≡ (⋀ 𝑥𝑥𝑘𝑘 𝜙𝜙 ∧ ⋀ 𝑥𝑥𝑘𝑘 𝜓𝜓) (xix) (⋀ 𝑥𝑥𝑘𝑘 𝜙𝜙 ∨ ⋀ 𝑥𝑥𝑘𝑘 𝜓𝜓) → ⋀ 𝑥𝑥𝑘𝑘 (𝜙𝜙 ∨ 𝜓𝜓) (xx) ⋁ 𝑥𝑥𝑘𝑘 (𝜙𝜙 → 𝜓𝜓) ≡ (⋀ 𝑥𝑥𝑘𝑘 𝜙𝜙 → ⋁ 𝑥𝑥𝑘𝑘 𝜓𝜓) (xxi) ⋁ 𝑥𝑥𝑘𝑘 (𝜙𝜙 ∧ 𝜓𝜓) → ( ⋁ 𝑥𝑥𝑘𝑘 𝜙𝜙 ∧ ⋁ 𝑥𝑥𝑘𝑘 𝜓𝜓) (xxii) ⋁ 𝑥𝑥𝑘𝑘 (𝜙𝜙 ∨ 𝜓𝜓) ≡ ( ⋁ 𝑥𝑥𝑘𝑘 𝜙𝜙 ∨ ⋁ 𝑥𝑥𝑘𝑘 𝜓𝜓) (xxiii) ⋀ 𝑥𝑥𝑘𝑘 (𝜙𝜙 ∨ 𝜓𝜓) ≡ ( 𝜙𝜙 ∨ ⋀ 𝑥𝑥𝑘𝑘 𝜓𝜓), if 𝑥𝑥𝑘𝑘 ∉ 𝐹𝐹𝐹𝐹(𝜙𝜙) (xxiv) ⋀ 𝑥𝑥𝑘𝑘 (𝜙𝜙 → 𝜓𝜓) ≡ (⋁ 𝑥𝑥𝑘𝑘 𝜙𝜙 → 𝜓𝜓), if 𝑥𝑥𝑘𝑘 ∉ 𝐹𝐹𝐹𝐹(𝜓𝜓) (xxv) ⋁ 𝑥𝑥𝑘𝑘 (𝜙𝜙 ∧ 𝜓𝜓) ≡ (𝜙𝜙 ∧ ⋁ 𝑥𝑥𝑘𝑘 𝜓𝜓), if 𝑥𝑥𝑘𝑘 ∉ 𝐹𝐹𝐹𝐹(𝜙𝜙) (xxvi) ⋀ 𝑥𝑥𝑘𝑘 ⋀ 𝑥𝑥𝑠𝑠 𝜙𝜙 ≡ ⋀ 𝑥𝑥𝑠𝑠 ⋀ 𝑥𝑥𝑘𝑘 𝜙𝜙 (xxvii) ⋁ 𝑥𝑥𝑘𝑘 ⋁ 𝑥𝑥𝑠𝑠 𝜙𝜙 ≡ ⋁ 𝑥𝑥𝑠𝑠 ⋁ 𝑥𝑥𝑘𝑘 𝜙𝜙 (xxviii) ⋁ 𝑥𝑥𝑘𝑘 ⋀ 𝑥𝑥𝑠𝑠 𝜙𝜙 → ⋀ 𝑥𝑥𝑠𝑠 ⋁ 𝑥𝑥𝑘𝑘 𝜙𝜙 (xxix) ~ ⋁ 𝑥𝑥𝑘𝑘 𝜙𝜙 ≡ ⋀ 𝑥𝑥𝑘𝑘 ~𝜙𝜙 (xxx) ~ ⋁ 𝑥𝑥𝑘𝑘 ~𝜙𝜙 ≡ ⋀ 𝑥𝑥𝑘𝑘 𝜙𝜙 (xxxi) ~ ⋀ 𝑥𝑥𝑘𝑘 ~𝜙𝜙 ≡ ⋁ 𝑥𝑥𝑘𝑘 𝜙𝜙 (xxxii) {[(𝜓𝜓 ∗ → 𝜙𝜙 ∗ ) → 𝜙𝜙 ∗ ] → 𝜙𝜙 ∗ } → (⋀ 𝜙𝜙 → 𝜓𝜓) (xxxiii) ∼ 𝑄𝑄𝑖𝑖 (⋀ 𝜙𝜙 ∧ 𝜓𝜓) ≡ (⋀ 𝜙𝜙 → ∼ 𝑄𝑄𝑖𝑖 𝜓𝜓) (xxxiv) ⋀𝑥𝑥𝑘𝑘 (𝜙𝜙 ≡ 𝜓𝜓) → [⋀𝑥𝑥𝑘𝑘 (𝜙𝜙 → 𝜓𝜓) ∧ ⋀𝑥𝑥𝑘𝑘 (𝜓𝜓 → 𝜙𝜙)]. Using Definition 8.1, Corollary 8.3, Corollary 8.4 and using the proof of Theorem 4.2 (see [20], pp.222 -
66
Atomic Entailment and Atomic Inconsistency and Classical Entailment
224), one can obtain Corollary 8.5 (on the extensionality of logical expressions). Let 𝑥𝑥1 , … , 𝑥𝑥𝑛𝑛 , 𝑦𝑦1 , … , 𝑦𝑦𝑙𝑙 be all the free variables, which occur in the expressions 𝛼𝛼 and 𝛽𝛽, and let 𝐶𝐶 𝛼𝛼 be any expression that contains 𝛼𝛼 or an expression obtained from 𝛼𝛼 by the substitution for the variables 𝑥𝑥1 , … , 𝑥𝑥𝑛𝑛 of some other variables different from the bound variables occurring in the
expressions 𝛼𝛼 or 𝛽𝛽 , and let 𝐶𝐶𝛽𝛽 differ from 𝐶𝐶 𝛼𝛼 only in that in certain places (unnecessarily in all these places) in which in 𝐶𝐶 𝛼𝛼 there occurs 𝛼𝛼 or an expression obtained from 𝛼𝛼 by a substitution for the variables 𝑥𝑥1 , … , 𝑥𝑥𝑛𝑛 , in the corresponding places in
𝐶𝐶𝛽𝛽 there occurs 𝛽𝛽 or an expression obtained from 𝛽𝛽 by an appropriate substitution, while the variables
𝑦𝑦1 , … , 𝑦𝑦𝑙𝑙 are all the free variables in 𝐶𝐶 𝛼𝛼 and 𝐶𝐶𝛽𝛽 . Then the sentence: ⋀ … 𝑦𝑦1 , … , 𝑦𝑦𝑙𝑙 (⋀𝑥𝑥1 , … , 𝑥𝑥𝑛𝑛 (𝛼𝛼 ≡ 𝛽𝛽) → �𝐶𝐶 𝛼𝛼 ≡ 𝐶𝐶𝛽𝛽 �) is a theorem in 𝐿𝐿𝐷𝐷 . Definition 8.6. Let 𝜙𝜙 ∈ 𝑆𝑆1 and 𝛼𝛼 ∈ 𝑆𝑆𝑆𝑆𝑆𝑆. Next let 𝑣𝑣: 𝐴𝐴𝐴𝐴0 ⟶ |𝔐𝔐2 | be an arbitrary, but fixed valuation in the matrix 𝔐𝔐2 such that ℎ𝑣𝑣 �𝑗𝑗(𝜙𝜙)� = 1. Then ⋀ 𝜙𝜙 ∧ 𝛼𝛼, if 𝑒𝑒𝜙𝜙 (𝛼𝛼) = �⋀ 𝜙𝜙 → 𝛼𝛼, if
𝑣𝑣(𝔦𝔦(𝛼𝛼)) = 0 𝑣𝑣(𝔦𝔦(𝛼𝛼)) = 1.
By the definition of the formulas 𝜙𝜙 ∗ , 𝜓𝜓 ∗ , one can easily obtain right away Corollary 8.7. (∀𝜙𝜙, 𝜓𝜓 ∈ 𝑆𝑆1 )(∃𝑒𝑒 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒 (⋀ 𝜙𝜙) ∈ 𝐿𝐿𝐷𝐷 𝕍𝕍 ℎ𝑒𝑒 ((𝜓𝜓 ∗ → 𝜙𝜙 ∗)→ 𝜙𝜙 ∗ ) ∈ 𝐿𝐿𝐷𝐷 ]. Lemma 8.8. If ⋀ 𝜙𝜙 → 𝜓𝜓 ∈ 𝐿𝐿𝐷𝐷 , then (∀𝑒𝑒 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒 (⋀𝜙𝜙) ∈ 𝐿𝐿𝐷𝐷 ⇒ ℎ𝑒𝑒 (𝜓𝜓) ∈ 𝐿𝐿𝐷𝐷 & 𝑃𝑃1 (ℎ𝑒𝑒 (⋀𝜙𝜙)) ⊆ 𝑃𝑃1 (ℎ𝑒𝑒 (𝜓𝜓))] and (∀𝑒𝑒 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒 ((𝜓𝜓 ∗ → 𝜙𝜙 ∗)→ 𝜙𝜙 ∗ ) ∈ 𝐿𝐿𝐷𝐷 ⇒ ℎ𝑒𝑒 (𝜙𝜙 ∗) ∈ 𝐿𝐿𝐷𝐷 & 𝑃𝑃1 (ℎ𝑒𝑒 (𝜓𝜓 ∗ )) ⊆ 𝑃𝑃1 (ℎ𝑒𝑒 (𝜙𝜙 ∗ ))].
Proof. Let (1) ⋀ 𝜙𝜙 → 𝜓𝜓 ∈ 𝐿𝐿𝐷𝐷 . Hence, by Corollary 8.3, we obtain that (2) (∀𝑒𝑒 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒 (⋀𝜙𝜙) ∈ 𝐿𝐿𝐷𝐷 ⇒ ℎ𝑒𝑒 (𝜓𝜓) ∈ 𝐿𝐿𝐷𝐷 ]. Hence, by the definition of the set 𝐿𝐿𝐷𝐷 and by the definition of the matrix 𝔐𝔐𝐷𝐷 , it follows that (3) (∀𝑒𝑒 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒 (⋀𝜙𝜙) ∈ 𝐿𝐿𝐷𝐷 ⇒ ℎ𝑒𝑒 (𝜓𝜓) ∈ 𝐿𝐿𝐷𝐷 & 𝑃𝑃1 (ℎ𝑒𝑒 (⋀𝜙𝜙)) ⊆ 𝑃𝑃1 (ℎ𝑒𝑒 (𝜓𝜓))]. Let (4) 𝐹𝐹𝐹𝐹(𝜙𝜙) =
{𝑥𝑥1 , … , 𝑥𝑥𝑛𝑛 } and (5) 𝐹𝐹𝐹𝐹(𝜓𝜓) = {𝑦𝑦1 , … , 𝑦𝑦𝑚𝑚 }. Hence, by the definition of the formulas 𝜙𝜙 ∗ , 𝜓𝜓 ∗, it follows that (6) 𝜙𝜙 ∗ = ⋁ 𝑥𝑥1 … ⋁ 𝑥𝑥𝑛𝑛 ~𝜙𝜙 and (7) 𝜓𝜓 ∗ = ⋁ 𝑦𝑦1 … ⋁ 𝑦𝑦𝑚𝑚 ~𝜓𝜓. Hence, from (1), by Definition 8.1, Corollary 8.3, Corollary 8.4 and Corollary 8.5, we obtain that (8) 𝜓𝜓 ∗ → 𝜙𝜙 ∗ ∈ 𝐿𝐿𝐷𝐷 . Hence, by Definition 8.1, Corollary 8.3, Corollary 8.4 and Corollary 8.5, we obtain that (9)(∀𝑒𝑒 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒 �(𝜓𝜓∗ → 𝜙𝜙 ∗ ) → 𝜙𝜙 ∗ � ∈ 𝐿𝐿𝐷𝐷 ⇒ ℎ𝑒𝑒 (𝜙𝜙 ∗ ) ∈ 𝐿𝐿𝐷𝐷 & 𝑃𝑃1 �ℎ𝑒𝑒 (𝜓𝜓∗ )� ⊆ 𝑃𝑃1 �ℎ𝑒𝑒 (𝜙𝜙 ∗ )�],
what together with (3) complete the proof. □ Lemma 8.9. If 𝜙𝜙 ∈ 𝑆𝑆1∗ and (∃𝑒𝑒 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒 (𝜙𝜙) ∈ 𝐿𝐿𝐷𝐷 ], then ℎ𝑒𝑒 𝜙𝜙 (𝜙𝜙) ∈ 𝐿𝐿𝐷𝐷 . Proof. Now we assume that (1) 𝑄𝑄𝑖𝑖 ∈ {⋀ 𝑥𝑥𝑖𝑖 , ⋁ 𝑥𝑥𝑖𝑖 } and (2) 𝜙𝜙 ∈ 𝑆𝑆1∗ and (3) (∃𝑒𝑒1 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒1 (𝜙𝜙) ∈ 𝐿𝐿𝐷𝐷 ]. Hence, by the definition of the set 𝐿𝐿𝐷𝐷 , it follows that (4) (∃𝑣𝑣: 𝐴𝐴𝐴𝐴0 ⟶ |𝔐𝔐2 |)[ℎ𝑣𝑣 �𝑗𝑗(𝜙𝜙)� = 1]. Let: (1.1) 𝜙𝜙 ∈ 𝑆𝑆𝑆𝑆𝑆𝑆. Hence, by (4) and Definition 8.6, one can obtain that (5) ℎ𝑒𝑒 𝜙𝜙 (𝜙𝜙) = ⋀ 𝜙𝜙 → 𝜙𝜙. Hence, by Corollary 8.4 (i), in (1.1), it follows that (6) ℎ𝑒𝑒 𝜙𝜙 (𝜙𝜙) ∈ 𝐿𝐿𝐷𝐷 . Let (1.2) 𝜙𝜙 = ~𝑃𝑃𝑘𝑘𝑛𝑛 (𝑡𝑡1 , … , 𝑡𝑡𝑛𝑛 ). Hence, from (4) and Definition 8.6, it follows that (7) ℎ𝑒𝑒𝜙𝜙 (𝜙𝜙) = ~(⋀ 𝜙𝜙 ∧ 𝑃𝑃𝑘𝑘𝑛𝑛 (𝑡𝑡1 , … , 𝑡𝑡𝑛𝑛 )). Therefore, by Corollary 8.4 (107) and (1.2), it follows that (8) ℎ𝑒𝑒 𝜙𝜙 (𝜙𝜙) ≡ (⋀ 𝜙𝜙 → 𝜙𝜙 ) ∈ 𝐿𝐿𝐷𝐷 . So, using Corollary 8.4 (i), in (1.2), one can obtain that (9) ℎ𝑒𝑒𝜙𝜙 (𝜙𝜙) ∈ 𝐿𝐿𝐷𝐷 . Let (1.3) 𝜙𝜙 = 𝜙𝜙1 ∨ 𝜙𝜙2 and assume inductively that (𝑎𝑎1 )ℎ𝑒𝑒 𝜙𝜙 (𝜙𝜙1 ) ∈ 𝐿𝐿𝐷𝐷 or (𝑎𝑎2 )ℎ𝑒𝑒 𝜙𝜙 (𝜙𝜙2 ) ∈ 𝐿𝐿𝐷𝐷 .
Atomic Entailment and Atomic Inconsistency and Classical Entailment
From Definition 8.6 it follows that (10) ℎ𝑒𝑒 𝜙𝜙 (𝜙𝜙1 ∨ 𝜙𝜙2 ) = ℎ𝑒𝑒 𝜙𝜙 (𝜙𝜙1 ) ∨ ℎ𝑒𝑒 𝜙𝜙 (𝜙𝜙2 ). Next, in (𝑎𝑎1 ) and (𝑎𝑎2 ) , from (1.3) and by Definition 8.6, it follows that (11) 𝑃𝑃1 �ℎ𝑒𝑒 𝜙𝜙 (𝜙𝜙1 )� = 𝑃𝑃1 �ℎ𝑒𝑒 𝜙𝜙 (𝜙𝜙2 )� = 𝑃𝑃1 (𝜙𝜙). Hence, from (10), by Corollary 8.4 (40) and Corollary 8.4 (41), in (𝑎𝑎1 ) and (𝑎𝑎2 ), in (1.3), it follows that (12) ℎ𝑒𝑒 𝜙𝜙 (𝜙𝜙) ∈ 𝐿𝐿𝐷𝐷 . Let (1.4) 𝜙𝜙 = 𝜙𝜙1 ∧ 𝜙𝜙2 and assume inductively that (13) ℎ𝑒𝑒 𝜙𝜙 (𝜙𝜙1 ), ℎ𝑒𝑒 𝜙𝜙 (𝜙𝜙2 ) ∈ 𝐿𝐿𝐷𝐷 . From (1.4) and (13), using Definition 8.6, by Corollary 8.4 (62), in (1.4), one can obtain that (14) ℎ𝑒𝑒 𝜙𝜙 (𝜙𝜙) ∈ 𝐿𝐿𝐷𝐷 . Let (1.5) 𝜙𝜙 = 𝑄𝑄𝑖𝑖 𝜙𝜙′ and assume inductively that (15) ℎ𝑒𝑒 𝜙𝜙 (𝜙𝜙′) ∈ 𝐿𝐿𝐷𝐷 . Hence, from (1.5), using Definition 8.6, by Corollary 8.4 (ix) and Corollary 8.3, in (1.5), one can obtain that (1.6) ℎ𝑒𝑒 𝜙𝜙 (𝜙𝜙) ∈ 𝐿𝐿𝐷𝐷 , which completes the proof. □ Lemma 8.10. If 𝜙𝜙 ∈ 𝑆𝑆1 and (∃𝑒𝑒 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒 (𝜙𝜙) ∈ 𝐿𝐿𝐷𝐷 ], then ℎ𝑒𝑒 𝜙𝜙 (𝜙𝜙) ∈ 𝐿𝐿𝐷𝐷 . Proof. By Definition 8.6, Corollary 8.4, Corollary 8.5 and Lemma 8.9 and by the well-known Theorem concerning normal form (see [19] pp. 35-42 and 130-132, [20] pp. 214 - 222, and [37] pp.146-149). □ Lemma 8.11. Let ⋀ 𝜙𝜙 → 𝜓𝜓 ∈ 𝐿𝐿2 and (∀𝑒𝑒 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒 (⋀𝜙𝜙) ∈ 𝐿𝐿𝐷𝐷 ⇒ ℎ𝑒𝑒 (𝜓𝜓) ∈ 𝐿𝐿𝐷𝐷 & 𝑃𝑃1 (ℎ𝑒𝑒 (𝜙𝜙)) ⊆ 𝑃𝑃1 (ℎ𝑒𝑒 (𝜓𝜓))] 𝑎𝑎𝑎𝑎𝑎𝑎 (∀𝑒𝑒 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒 �(𝜓𝜓∗ → 𝜙𝜙 ∗ ) → 𝜙𝜙 ∗ � ∈ 𝐿𝐿𝐷𝐷 ⇒ ℎ𝑒𝑒 (𝜙𝜙 ∗ ) ∈ 𝐿𝐿𝐷𝐷 & 𝑃𝑃1 (ℎ𝑒𝑒 (𝜓𝜓∗ )) ⊆ 𝑃𝑃1 (ℎ𝑒𝑒 (𝜙𝜙 ∗ ))]. Then ⋀ 𝜙𝜙 → 𝜓𝜓 ∈ 𝐿𝐿𝐷𝐷 . Proof. By Theorem 7.2, the Definition 8.1, Corollary 8.3, Corollary 8.4, Corollary 8.5, Definition 8.6, Corollary 8.7, Lemma 8.10 and by the definition of the matrix 𝔐𝔐𝐷𝐷 and by the definitions of the formulas
67
𝜙𝜙 ∗ , 𝜓𝜓 ∗. □ Lemma 8.12. Let 𝜙𝜙, 𝜓𝜓 ∈ 𝑆𝑆1 and (∃𝑒𝑒 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒 (𝜙𝜙) ∈ 𝐿𝐿𝐷𝐷 ] and (∀𝑒𝑒 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒 (𝜙𝜙) ∈ 𝐿𝐿𝐷𝐷 ⇒ ℎ𝑒𝑒 (𝜓𝜓) ∈ 𝐿𝐿𝐷𝐷 & 𝑃𝑃1 (ℎ𝑒𝑒 (𝜙𝜙)) ⊆ 𝑃𝑃1 (ℎ𝑒𝑒 (𝜓𝜓))].
Then (∀𝑒𝑒 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒 (𝜙𝜙) ∈ 𝐿𝐿2 ⇒ ℎ𝑒𝑒 (𝜓𝜓) ∈ 𝐿𝐿2 ]. Proof. Let (1) 𝜙𝜙, 𝜓𝜓 ∈ 𝑆𝑆1 , (2) (∃𝑒𝑒 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒 (𝜙𝜙) ∈ 𝐿𝐿𝐷𝐷 ] and (3) (∀𝑒𝑒 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒 (𝜙𝜙) ∈ 𝐿𝐿𝐷𝐷 ⇒ ℎ𝑒𝑒 (𝜓𝜓) ∈ 𝐿𝐿𝐷𝐷 & 𝑃𝑃1 �ℎ𝑒𝑒 (𝜙𝜙)� ⊆ 𝑃𝑃1 �ℎ𝑒𝑒 (𝜓𝜓)�]. From (1), (2), it follows that (4) (∃𝑒𝑒1 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒1 (𝜙𝜙) ∈ 𝐿𝐿2 ] . Now suppose that (5) (∃𝑒𝑒2 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒2 (𝜙𝜙) ∈ 𝐿𝐿2 & ℎ𝑒𝑒2 (𝜓𝜓) ∉ 𝐿𝐿2 ] . Next 𝑒𝑒2 (𝜙𝜙) 𝑒𝑒2 (𝜓𝜓) assume that (6) ℎ = 𝜙𝜙′ and (7) ℎ = 𝜓𝜓′.
From (5) – (7), it follows that (8) 𝜙𝜙′ ∈ 𝐿𝐿2 and (9) 𝜓𝜓 ′ ∉ 𝐿𝐿2 . From (8) it follows that (10)
(∃e ∈ ε *1 )[ h e (φ' ) ∈ LD ] . Hence, by Lemma 8.10, it 𝑒𝑒
follows that (11) ℎ 𝜙𝜙 ′ (𝜙𝜙′) ∈ 𝐿𝐿𝐷𝐷 . Hence, from (3) it 𝑒𝑒 follows that (12) ℎ 𝜙𝜙 ′ (𝜓𝜓 ′ ) ∈ 𝐿𝐿𝐷𝐷 . From (8) and (9) and Definition 8.6 and Theorem 4.2, it follows that 𝑒𝑒
(14) ℎ 𝜙𝜙 ′ (𝜓𝜓′ ) ∉ 𝐿𝐿2 . From (12), by the definition of 𝑒𝑒 the set 𝐿𝐿𝐷𝐷 , it follows that (15) ℎ 𝜙𝜙 ′ (𝜓𝜓′ ) ∈ 𝐿𝐿2 , what contradicts (14). □ Lemma 8.13. Let (∀𝑒𝑒 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒 �(𝜓𝜓 ∗ → 𝜙𝜙 ∗ ) → 𝜙𝜙 ∗ � ∈ 𝐿𝐿𝐷𝐷 ⇒ ℎ𝑒𝑒 (𝜙𝜙 ∗ ) ∈ 𝐿𝐿𝐷𝐷 & 𝑃𝑃1 (ℎ𝑒𝑒 (𝜓𝜓∗ )) ⊆ 𝑃𝑃1 (ℎ𝑒𝑒 (𝜙𝜙 ∗ ))] and (∃𝑒𝑒 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒 �(𝜓𝜓 ∗ → 𝜙𝜙 ∗ ) → 𝜙𝜙 ∗ � ∈ 𝐿𝐿𝐷𝐷 ]. Then (∀𝑒𝑒 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒 �(𝜓𝜓 ∗ → 𝜙𝜙 ∗ ) → 𝜙𝜙 ∗ � ∈ 𝐿𝐿2 ⇒ ℎ𝑒𝑒 (𝜙𝜙 ∗ ) ∈ 𝐿𝐿2 ]. Proof. The proof of this lemma is analogical to the proof of Lemma 8.12. □ In [50] we have proved the following Lemma: Lemma 8.14. Let 𝜙𝜙, 𝜓𝜓 ∈ 𝑆𝑆1 , 𝑋𝑋 ⊆ 𝑆𝑆1 and (∃𝑣𝑣: 𝐴𝐴𝐴𝐴0 ⟶ |𝔐𝔐2 |)�ℎ𝑣𝑣 �𝑗𝑗(𝜙𝜙)� = 1�and 𝐶𝐶𝐶𝐶1 (𝑅𝑅0+ , 𝐿𝐿2 ∪ 𝑋𝑋) = 𝑍𝑍3 and (∀𝑒𝑒 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒 (𝜙𝜙) ∈ 𝑍𝑍3 ⇒ ℎ𝑒𝑒 (𝜓𝜓) ∈ 𝑍𝑍3 ].
68
Atomic Entailment and Atomic Inconsistency and Classical Entailment
Then ⋀ 𝜙𝜙 → 𝜓𝜓 ∈ 𝑍𝑍3 . In consequence: Lemma 8.15. If (∃𝑒𝑒 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒 (𝜙𝜙) ∈ 𝐿𝐿𝐷𝐷 ] and (∀𝑒𝑒 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒 (𝜙𝜙) ∈ 𝐿𝐿𝐷𝐷 ⇒ ℎ𝑒𝑒 (𝜓𝜓) ∈ 𝐿𝐿𝐷𝐷 & 𝑃𝑃1 (ℎ𝑒𝑒 (𝜙𝜙)) ⊆ 𝑃𝑃1 (ℎ𝑒𝑒 (𝜓𝜓))], then ⋀ 𝜙𝜙 → 𝜓𝜓 ∈ 𝐿𝐿2 . Proof. By Corollary 8.4, Lemma 8.12 and Lemma 8.14. □ Lemma 8.16. Let (∀𝑒𝑒 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒 �(𝜓𝜓∗ → 𝜙𝜙 ∗ ) → 𝜙𝜙 ∗ � ∈ 𝐿𝐿𝐷𝐷 ⇒ ℎ𝑒𝑒 (𝜙𝜙 ∗) ∈ 𝐿𝐿𝐷𝐷 & 𝑃𝑃1 (ℎ𝑒𝑒 (𝜓𝜓∗ )) ⊆ 𝑃𝑃1 (ℎ𝑒𝑒 (𝜙𝜙 ∗ ))]
and (∃𝑒𝑒 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒 �(𝜓𝜓∗ → 𝜙𝜙 ∗ ) → 𝜙𝜙 ∗ � ∈ 𝐿𝐿𝐷𝐷 ]. Then 𝜓𝜓 ∗ → 𝜙𝜙 ∗ ∈ 𝐿𝐿2 . Proof. By Corollary 8.4, Lemma 8.13 and Lemma 8.14. □ Lemma 8.17. Let 𝜙𝜙 ∗ , 𝜓𝜓 ∗ ∈ 𝑆𝑆1 . If(∀𝑒𝑒 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒 �(𝜓𝜓 ∗ → 𝜙𝜙 ∗ ) → 𝜙𝜙 ∗ � ∈ 𝐿𝐿𝐷𝐷 ⇒ ℎ𝑒𝑒 (𝜙𝜙 ∗) ∈ 𝐿𝐿𝐷𝐷 & 𝑃𝑃1 (ℎ𝑒𝑒 (𝜓𝜓∗ )) ⊆ 𝑃𝑃1 (ℎ𝑒𝑒 (𝜙𝜙 ∗ ))] and (∀𝑒𝑒 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒 (𝜙𝜙) ∈ 𝐿𝐿𝐷𝐷 ⇒ ℎ𝑒𝑒 (𝜓𝜓) ∈ 𝐿𝐿𝐷𝐷 & 𝑃𝑃1 (ℎ𝑒𝑒 (𝜙𝜙)) ⊆ 𝑃𝑃1 (ℎ𝑒𝑒 (𝜓𝜓))], then ⋀ 𝜙𝜙 → 𝜓𝜓 ∈ 𝐿𝐿𝐷𝐷 . Proof. By the definitions of the formulas 𝜙𝜙 ∗ , 𝜓𝜓 ∗ andCorollary 8.7, Lemma 8.11, Lemma 8.15 and Lemma 8.16. □ Lemma 8.18. Let 𝜙𝜙 ∗ , 𝜓𝜓 ∗ ∈ 𝑆𝑆0 . If(∀𝑒𝑒 ∈ 𝜀𝜀∗0 )[ℎ𝑒𝑒 �(𝜓𝜓 ∗ → 𝜙𝜙 ∗ ) → 𝜙𝜙 ∗ � ∈ 𝑇𝑇𝐷𝐷 ⇒ ℎ𝑒𝑒 (𝜙𝜙 ∗) ∈ 𝑇𝑇𝐷𝐷 & 𝑃𝑃0 (ℎ𝑒𝑒 (𝜓𝜓∗ )) ⊆ 𝑃𝑃0 (ℎ𝑒𝑒 (𝜙𝜙 ∗ ))] and (∀𝑒𝑒 ∈ 𝜀𝜀∗0 )[ℎ𝑒𝑒 (𝜙𝜙) ∈ 𝑇𝑇𝐷𝐷 ⇒ ℎ𝑒𝑒 (𝜓𝜓) ∈ 𝑇𝑇𝐷𝐷 & 𝑃𝑃0 (ℎ𝑒𝑒 (𝜙𝜙)) ⊆ 𝑃𝑃0 (ℎ𝑒𝑒 (𝜓𝜓))], then 𝜙𝜙 → 𝜓𝜓 ∈ 𝑇𝑇𝐷𝐷 . Proof. Using the similar reasoning as in the proof of Lemma 8.17. □ Lemma 8.19.If 𝜙𝜙 → 𝜓𝜓 ∈ 𝑇𝑇𝐷𝐷 , then (∀𝑒𝑒 ∈ 𝜀𝜀∗0 )[ℎ𝑒𝑒 (𝜙𝜙) ∈ 𝑇𝑇𝐷𝐷 ⇒ ℎ𝑒𝑒 (𝜓𝜓) ∈ 𝑇𝑇𝐷𝐷 & 𝑃𝑃0 �ℎ𝑒𝑒 (𝜙𝜙)� ⊆ 𝑃𝑃0 �ℎ𝑒𝑒 (𝜓𝜓)�]
and
(∀𝑒𝑒 ∈ 𝜀𝜀∗0 )[ℎ𝑒𝑒 �(𝜓𝜓 ∗ → 𝜙𝜙 ∗ ) → 𝜙𝜙 ∗ � ∈ 𝑇𝑇𝐷𝐷 ⇒ ℎ𝑒𝑒 (𝜙𝜙 ∗) ∈ 𝑇𝑇𝐷𝐷 & 𝑃𝑃0 (ℎ𝑒𝑒 (𝜓𝜓∗ )) ⊆ 𝑃𝑃0 (ℎ𝑒𝑒 (𝜙𝜙 ∗ ))].
Proof. The proof of this Lemma is analogical to the proof of Lemma 8.8. □
9. The Main Result Theorem 9.1. 〈𝑅𝑅0 , 𝑇𝑇𝐷𝐷 〉 ∈ 𝑆𝑆𝑆𝑆𝑆𝑆𝑆𝑆 ∩ 𝐴𝐴0 .
Proof. By Lemma 8.18 and Lemma 8.19. □ Theorem 9.2. 〈𝑅𝑅0+ , 𝐿𝐿𝐷𝐷 〉 ∈ 𝑆𝑆𝑆𝑆𝑆𝑆𝑆𝑆 ∩ 𝐴𝐴1 . Proof. By Lemma 8.8 and Lemma 8.17. □ Theorem 9.3. 〈𝑅𝑅0+ , 𝐿𝐿2 〉 ∈ 𝑆𝑆𝑆𝑆𝑆𝑆𝑆𝑆 ∩ 𝐶𝐶1 . Proof. By similar reasonings as in the proofs of Lemma 8.8 and Lemma 8.17 (or by Corollary 8.7, the definition of the set 𝐿𝐿𝐷𝐷 and by Lemma 8.14). □ Theorem 9.4. 〈𝑅𝑅0 , 𝑇𝑇𝐷𝐷 〉 ∈ 𝑆𝑆𝑆𝑆𝑆𝑆𝑆𝑆 ∩ 𝐴𝐴𝐴𝐴𝐴𝐴𝐴𝐴. Proof. By the definition of the set 𝑇𝑇𝐷𝐷 and by the Definition 6.1 and the Definition 6.2. □ Theorem 9.5. 〈𝑅𝑅0+ , 𝐿𝐿𝐷𝐷 〉 ∈ 𝑆𝑆𝑆𝑆𝑆𝑆𝑆𝑆 ∩ 𝐴𝐴𝐴𝐴𝐴𝐴𝐴𝐴. Proof. Let (1) 𝛼𝛼 ∈ 𝑆𝑆1 and (2) 𝛽𝛽 ∈ 𝑆𝑆1 . Hence, by the definition of the set𝐿𝐿𝐷𝐷 , it follows that (3) 𝛼𝛼 → (~𝛼𝛼 → 𝛽𝛽) ∈ 𝐿𝐿𝐷𝐷 , where (4) 𝑃𝑃1 (𝛽𝛽) ⊆ 𝑃𝑃1 (𝛼𝛼). From (1)-(4), it follows that (5) 𝑆𝑆1𝛼𝛼 ⊆ 𝐶𝐶𝐶𝐶(𝑅𝑅0+ , 𝐿𝐿𝐷𝐷 ∪ {𝛼𝛼, ~𝛼𝛼}). Let now, (6) 𝑃𝑃1 (𝛽𝛽) ⊈ 𝑃𝑃1 (𝛼𝛼).
Next, by the definition of the set 𝐿𝐿2 , it follows that (7) (𝛼𝛼 ∧ ~𝛼𝛼) → (𝛽𝛽 ∧ ~𝛽𝛽) ∈ 𝐿𝐿2 .
Next, from (6), by the definition of the set 𝑇𝑇𝐷𝐷 , it follows that (8) 𝑗𝑗(𝛼𝛼 ∧ ~𝛼𝛼) → 𝑗𝑗(𝛽𝛽 ∧ ~𝛽𝛽) ∉ 𝑇𝑇𝐷𝐷 . Hence, from (6), (7), by the definition of the set 𝐿𝐿𝐷𝐷 , it follows that (9) 𝛽𝛽 ∉ 𝐶𝐶𝐶𝐶(𝑅𝑅0+ , 𝐿𝐿𝐷𝐷 ∪ {𝛼𝛼 ∧ ~𝛼𝛼}) or (10) ~𝛽𝛽 ∉ 𝐶𝐶𝐶𝐶(𝑅𝑅0+, 𝐿𝐿𝐷𝐷 ∪ {𝛼𝛼 ∧ ~𝛼𝛼}), what together with 5), 6) and the Definition 6.2, completes the proof. □
10. Summary Remark 10.1. Let (∀𝑒𝑒 ∈ 𝜀𝜀∗0 )[ℎ𝑒𝑒 (𝜓𝜓 ∗ ) ∈ 𝐿𝐿 ⇒ ℎ𝑒𝑒 (𝜙𝜙 ∗ ) ∈ 𝐿𝐿 & 𝑃𝑃0 �ℎ𝑒𝑒 (𝜓𝜓 ∗ )� ⊆ 𝑃𝑃0 �ℎ𝑒𝑒 (𝜙𝜙 ∗)�] = Λ 0 and (∀𝑒𝑒 ∈ 𝜀𝜀∗0 )[ℎ𝑒𝑒 �(𝜓𝜓 ∗ → 𝜙𝜙 ∗ ) → 𝜙𝜙 ∗ � ∈ 𝐿𝐿 ⇒
Atomic Entailment and Atomic Inconsistency and Classical Entailment
ℎ𝑒𝑒 (𝜙𝜙 ∗) ∈ 𝐿𝐿 & 𝑃𝑃0 �ℎ𝑒𝑒 (𝜓𝜓 ∗ )� ⊆ 𝑃𝑃0 �ℎ𝑒𝑒 (𝜙𝜙 ∗ )�] = Λ1 .
By an inspection of Definition 5.1, Definition 5.2,
Definition 7.1, Lemma 8.18 and Lemma 8.19, one can easily see that in condition (2) of Definition 5.1 one cannot put Λ 0 instead of Λ1 .
1962. [4]
entailments. Mathematische Annalen, 149:302-319, 1963. [5]
𝐿𝐿 & 𝑃𝑃1 �ℎ𝑒𝑒 (𝜓𝜓 ∗ )� ⊆ 𝑃𝑃1 �ℎ𝑒𝑒 (𝜙𝜙 ∗ )�] = Λ 0
A. R. Anderson, N. D. Belnap, and J. M. Dunn. Entailment: The Logic of Relevance and Necessity, volume II. Princeton University Press, 1992.
[7]
and
R. Barcan-Marcus. Strict implication, Deducibility and the deduction theorem. The Journal of Symbolic Logic,
(∀𝑒𝑒 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒 �(𝜓𝜓 ∗ → 𝜙𝜙 ∗ ) → 𝜙𝜙 ∗ � ∈ 𝐿𝐿 ⇒
ℎ𝑒𝑒 (𝜙𝜙 ∗ ) ∈ 𝐿𝐿 &𝑃𝑃1 �ℎ𝑒𝑒 (𝜓𝜓 ∗ )� ⊆ 𝑃𝑃1 �ℎ𝑒𝑒 (𝜙𝜙 ∗ )�] = Λ1 .
18:234-236, 1953. [8]
5.4 and Definition 8.1 and Lemma 8.8 and Lemma 8.17, one can easily see that in condition (2) of Definition 5.3 one cannot put Λ 0 instead of Λ1 .
Remark 10.3.
Let(∀𝑒𝑒 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒 (𝜓𝜓 ∗ ) ∈ 𝐿𝐿 ⇒ ℎ𝑒𝑒 (𝜙𝜙 ∗ ) ∈ 𝐿𝐿 ] = Λ 0 𝑎𝑎𝑎𝑎𝑎𝑎 (∀𝑒𝑒 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒 �(𝜓𝜓∗ → 𝜙𝜙 ∗ ) → 𝜙𝜙 ∗ � ∈ 𝐿𝐿 ⇒ ℎ𝑒𝑒 (𝜙𝜙 ∗) ∈ 𝐿𝐿] = Λ1 .
By an inspection of Definition 3.1, Definition 3.2 and by Lemma 8.14, Theorem 9.3, one can easily see that in condition (2) of Definition 3.1 one cannot put Λ 0 instead of Λ1 .
Using Definition 2.2 and Definition 6.1 and
Definition 6.2, one can obtain the following remark: Remark 10.4.
J. Beall. Truth without Detachment, 2012. A Talk delivered at Munich Center for Mathematical Philosophy, 14.03.2012.
By an inspection of Definition 5.3 and Definition [9]
K. Bimbo. Relevance Logics and Relation Algebras. In Philosophy of Logic, ed. D. Jacquette, vol. 5, pages 723-789. Elsevier/North-Holland, Amsterdam, 2007. Included in series Handbook of the Philosophy of Science (eds. D. M.Gabbay, P. Thagard and J. Woods).
[10] K. Bimbo, J. M. Dunn, and R. D. Maddux. Relevance Logics and Relation Algebras. The Review of Symbolic Logic, 2:102-131, 2009. [11] L. Borkowski.Comments on Conditional Sentences and on Material and Strict Implication, inThe Book in Honour of Kazimierz Ajdukiewicz., 102-104, Warszawa, 1964. [12] R. T. Brady. Entailment, classicality and the paradoxes, delivered to the Australasian Association of Philosophy Conference, A.N.U., Canberra, 1989. [13] Ross T. Brady. Relevant implication and the case for a weaker logic. Journal of Philosophical Logic, 25:151-183, 1996.
𝐴𝐴
〈𝑅𝑅, 𝑋𝑋〉 ∈ 𝑆𝑆𝑆𝑆𝑆𝑆𝑆𝑆 ∩ 𝐴𝐴𝐴𝐴𝐴𝐴𝐴𝐴 ⇒ 〈𝑅𝑅, 𝑋𝑋〉 ∈ 𝐶𝐶𝐶𝐶𝐶𝐶 ,
where 𝑅𝑅 ⊆ 𝑅𝑅𝑆𝑆𝑖𝑖 and 𝑋𝑋 ⊆ 𝑆𝑆𝑖𝑖 and 𝑖𝑖 ∈ {0,1}.
References
[14] Jingde Cheng. The fundamental role of entailment in knowledge representation and reasoning. Journal of Computing and Information, 2:853-873, 1996. [15] Jingde Cheng. Temporal relevant logic as the logic basis for reasoning about dynamics of concurrent systems. In
W. Ackerman. Begrundung einer strengen implication.
Proceedings of the 1998 IEEE-SMC Annual International
The Journal of Symbolic Logic, 21:113-128, 1956.
Conference on Systems, Man, and Cybernetics, San
A. R. Anderson. Completeness theorems for the system E
Diego, USA, 11-14 October 1998, 1998.
of entailment and EQ of entailment with quantification. Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 6:201-216, 1960. [3]
A. R. Anderson and N. D. Belnap. Entailment: The Logic of Relevance and Necessity, volume I. Princeton
[6]
𝐿𝐿𝐿𝐿𝐿𝐿 (∀𝑒𝑒 ∈ 𝜀𝜀∗1 )[ℎ𝑒𝑒 (𝜓𝜓∗ ) ∈ 𝐿𝐿 ⇒ ℎ𝑒𝑒 (𝜙𝜙 ∗ ) ∈
[2]
A. R. Anderson and N. D. Belnap. First degree
University Press, 1975.
Remark 10.2.
[1]
69
A. R. Anderson and N. D. Belnap. The Pure Calculus of Entailment. The Journal of Symbolic Logic, 27:19-52,
[16] Z. Czerwinski. On paradox of implication. Studia Logica, VII:264-271, 1958. [17] A. E. Duncan-Jones. Is strict implication the same as entailment ? Analysis, II:70-78, 1935. [18] J. M. Dunn. A modification of Parry's analytic
Atomic Entailment and Atomic Inconsistency and Classical Entailment
70
implication. Notre Dame Journal of Formal Logic, [19] Yu. L. Ershov and E. A. Palyutin. Mathematical Logic.
Fundamental Results and Notions Explained with All D.
Reidel
Publishing
Company,
Dordrecht-Holland/Boston-USA, PWN, Warszawa, 1974. [21] I. Hacking. what is strict implication ? The Journal of [22] R. Hirsch and Szabolc Mikulas. Positive Fragments of Relevance Logic and Algebras of Binary Relations. The
[38] W. A. Pogorzelski and T. Prucnal. The substitution rule for predicate letters in the first-order predicate calculus. Reports on Mathematical Logic, 5:77-90,1975. [39] G. Pottinger. On analysing relevance constructively. [40] G. Priest. Sense, Entailment and Modus Ponens. Journal of Philosophical Logic, 9:415-435, 1980. [41] A. N. Prior. Facts, propositions, and entailment. Mind,
Review of Symbolic Logic, 4:81-105, 2011. [23] Anthony Hunter and S. Konieczny. Approaches to measuring inconsistent information. In Inconsistency Tolerance, 191-236, Springer, 2005.
57:62-68, 1947. [42] R. Routley. The American Plan Completed: alternative classic-style semantics, without stars, for relevant and
[24] S. A. Kripke. The problem of entailment. The Journal of Symbolic Logic, 24:324, 1959.
paraconsistent logics. Studia Logica, XLIII1/2:131-158, 1984.
[25] C. I. Lewis. Implication and the algebra of logic. Mind, New Series, 21:522-531, 1912.
[43] R. Routley and R. K. Meyer. Towards a general semantical theory of implication and conditionals. I.
[26] C. Lewy. Entailment. Aristotelian Society Supplementary
Systems with normal conjunctions and disjunctions and aberrant and normal negations. Reports on Mathematical
Volume, 32:123-142, 1958. [27] S. Mccall. A new variety of implication. The Journal of Symbolic Logic, 29:151-152, 1964.
Logic, 4:67-90,1975. [44] R. Routley and R. K. Meyer. Towards a general
[28] R. K. Meyer. Entailment and relevant implication. Logique et Analyse, 11:472-479, 1968.
semantical theory of implication and conditionals. II. Systems with normal conjunctions and disjunctions and
[29] R. K. Meyer. Two questions from Anderson and Belnap.
aberrant and normal negations. Reports on Mathematical Logic, 9:47-62,1977.
Reports on Mathematical Logic, 7:71-86, 1976. [30] R. K. Meyer and J. M. Dunn. Entailment and material implication. Notices of The American Mathematical Society, 15:1021-1022, 1966.
[45] T. J. Smiley. Entailment and deducibility. Proceedings of The Aristotelian Society, 59:233-254, 1959. [46] B. Sobocinski. Axiomatization of partial system of
[31] R. K. Meyer and R. Routley. Classical relevant logics (I).
Paradoxes of Consistency and the K Rule II. A Logics
three-valued calculus of propositions. The Journal of Computing System, 1:22-55, 1952.
Studia Logica, XXXII:51-68, 1973. [32] J. M. MÉndez and G. Robles. Relevance Logics, Negation.
PWN, Warszawa, 1981.
Studia Logica, 38:171-185, 1979.
Symbolic Logic, 28:51-71, 1963.
Non-constructive
PWN, Warszawa, 1975. [37] W. A. Pogorzelski. The Classical Calculus of Quantifiers.
Mir Publishers, MOSCOW, 1984. [20] A. Grzegorczyk. An Outline of Mathematical Logic. Details,
13:224-226, 1972. [36] W. A. Pogorzelski. The Classical Propositional Calculus.
13:195-205, 1972.
and
Logical
Philosophy, 15:175-191, 2006. [33] J. M. MÉndez, Francisco Salto, and G. Robles. Anderson and Belnap's Minimal Positive Logic with Minimal Negation. Reports on Mathematical Logic, 36:117-130, 2002. [34] J. Norman and R. Sylvan, Editors. Directions in Relevant Logic. Kluwer Academic Publishers, 1989. [35] R. Z. Parks and J. R. Chidgey. Necessity and ticket entailment. Notre Dame Journal of Formal Logic,
[47] T. Stepien. System 𝑆𝑆̅. Reports on Mathematical Logic, 15:59-65, 1983.
[48] T. Stepien. System 𝑆𝑆̅. Zentralblatt für Mathematik, 471, 1983.
[49] T. Stepien. Logic based on atomic entailment. Bulletin of the Section of Logic, 14:65-71, 1985. [50] T. Stepien. Derivability. Reports on Mathematical Logic, 33:79-99, 1999. [51] T. Stepien. Logic Based On Atomic Entailment And Paraconsistency.
11th
international
Congress
Of
Logic,Methodology and Philosophy Of Science (August 1999, Krakow, Poland).
Atomic Entailment and Atomic Inconsistency and Classical Entailment [52] T. J. Stepien and L. T. Stepien. Atomic Entailment and Classical Entailment, The Bulletin of Symbolic Logic, Tennant.
Perfect
Journal of Philosophical Logic, 39:453-472, 2010. [58] Andreas Weiermann and Martin Bunder. Ackermannian lower bounds for a combinatorial problem related to the
17:317-318, 2011. [53] N.
71
validity,
entailment
and
paraconsistency. Studia Logica, XLIII:181-200, 1984. [54] A. Urquhart. Semantics for relevant logics. The Journal of Symbolic Logic, 37:159-169, 1972. [55] A. Urquhart. The Undecidability of Entailment and Relevant Implication, The Journal of Symbolic Logic, 49:1059-1073, 1984. [56] A. Urquhart. Failure of Interpolation in Relevant Logics. Journal of Philosophical Logic, 22:449-479, 1993. [57] A. Urquhart. Anderson and Belnap's Invitation to Sin.
decidability
of
certain
relevant
logics,
2005.
http://cage.ugent.be/~weierman/relevancelogic.pdf. [59] P. Weingartner. Two simple ideas of relevance. In Proceedings of the Xxxth Conference on the History of Logic, Dedicated To Roman Suszko, Cracow, 19-21 October 1984, 1984. [60] G. Xiao and Y. Ma, Inconsistency measurement based on variables in minimal unsatisfable subsets. 2012. A Talk delivered
at
European
Conference
Intelligence, ECAI’12, France (2012).
on
Artificial
