Access the full text.
Sign up today, get DeepDyve free for 14 days.
axioms Article Joanna Golinska-Pilarek ´ and Magdalena Welle Institute of Philosophy, University of Warsaw, 00–927 Warsaw, Poland; m.welle@uw.edu.pl * Correspondence: j.golinska@uw.edu.pl Received: 5 September 2019; Accepted: 14 October 2019; Published: 17 October 2019 Abstract: We study deduction systems for the weakest, extensional and two-valued non-Fregean propositional logic SCI. The language of SCI is obtained by expanding the language of classical propositional logic with a new binary connective that expresses the identity of two statements; that is, it connects two statements and forms a new one, which is true whenever the semantic correlates of the arguments are the same. On the formal side, SCI is an extension of classical propositional logic with axioms characterizing the identity connective, postulating that identity must be an equivalence and obey an extensionality principle. First, we present and discuss two types of systems for SCI known from the literature, namely sequent calculus and a dual tableau-like system. Then, we present a new dual tableau system for SCI and prove its soundness and completeness. Finally, we discuss and compare the systems presented in the paper. Keywords: non-Fregean logic; identity connective; sentential calculus with identity; situational semantics; deduction; (dual) tableau; Gentzen system MSC: 03A05; 03B60; 03B65; 03B80; 03F99 1. Introduction One of the tasks of formal logic is to provide adequate tools for the formal analysis of certain fragments of natural language, as well as for the languages of particular ﬁelds of science. It is commonly accepted that the theory of interpretation of a language is semantics. The choice of semantics determines how we think about a given language and what meaning we assign to its components. It is often acknowledged that the ﬁrst precisely formulated semantic principles—that serves as a foundation for contemporary formal logic and have determined its development—were presented by Frege in his Begriffsschrift. According to Frege, a correct and adequate formal system of a given language should meet the following conditions: F1 All names and all sentences have meaning and denotation. Meaning is not the same as denotation. F2 A name and a sentence are the proper names of their denotations. F3 Only one logical value can be assigned to each sentence: true or false. F4 If two expressions have the same denotation, then they are exchangeable in any propositional context of a sentence without changing the logical value of that sentence. F5 If two sentences are exchangeable in any propositional context of a sentence without changing its logical value, then they have the same denotation. Note that crucial notions for Frege’s account are the following: meaning, denotation, and logical valuation. Frege admits that the meaning of a sentence is not the same as its denotation. Indeed, the same holds for names: ‘Evening Star ’ and ‘Morning Star ’ denote the same object, but they have different meanings. The meaning of a sentence should be understood as its sense that the sentence expresses. Thus, we should ask what a sentence is referring to. From the formal point Axioms 2019, 8, 115; doi:10.3390/axioms8040115 www.mdpi.com/journal/axioms Axioms 2019, 8, 115 2 of 19 of view, the answer to this question requires, in particular, to decide what the denotation of a propositional variable is. Propositional variables have an unusual character due to the fact that, at the same time, they are formulas. In classical logic, this ambiguity is removed as it identiﬁes denotations of sentences with their truth values. In other words, in classical logic, propositional variables occur only at the metalogical level (they are not treated as real variables) or, as it holds in propositional calculus, variables range over the two element set of logical values. Within such an account, only terms have a meaningful ontological reference. Thus, the advocate of classical logic, if he is also a proponent of the Fregean semantic principles, must accept that all true sentences have one and the same denotation, namely the logical value Truth, and denotation of all false sentences is the logical value False. The consequence of Frege’s semantic principles, according to which denotations of sentences are logical values, is usually called the Fregean principle, and every logical system that adopts this principle is called a Fregean system. The Fregean approach can be considered as philosophically justiﬁed in the study of mathematical languages, but it is not obvious that such an approach is justiﬁed as a foundation of a philosophically adequate semantics. The debatable cases of the applicability of the Fregean account in the formalization of any language are, for instance, theories of meaning or ontology. If we admit that the references of sentences are situations (states of affairs) that these sentences describe (in analogy with the assumption that the semantic references of terms are objects named by these terms), then the Fregean principle is not only a semantic principle, but also an ontological one which imposes a quantitative restriction on the universe of situations: there are at most two situations described by sentences. This is an extremely strong assumption. Note that the Fregean account does not impose an upper limit on the universe of objects. Roman Suszko in 1968 [1] proposed to change the Fregean paradigm and introduced the so-called non-Fregean logic (see also [2]). The basic philosophical assumption underlying non-Fregean logic is the thesis in reality to which the language is referring, and there exist semantic correlates of all expressions that are not purely syntactic. Therefore, in the non-Fregean approach, it is assumed that the semantic correlates of names are objects from the universe of objects, the semantic correlates of predicates are appropriate sets, and the semantic correlates of sentences are situations described by these sentences. Furthermore, a universe of situations cannot be quantitatively restricted, except that there are at least two situations. The construction of a propositional non-Fregean logic, which at the same time preserves all properties of classical logic with respect to the classical connectives, is relatively simple. To make it possible to express statements on situations and interactions between them, propositional calculus is extended with the additional connective, named the identity connective and denoted by. The intended interpretation of the identity connective is the following: f y is true if and only if the semantic correlates of f and y are the same, that is, sentences j and y describe the same situation (the same state of affairs). Note that, in a general case, the identity connective is different than the classical equivalence. Equivalent sentences, that is, sentences that do not have the same logical value, do not have to refer to the same situation, and so they do not have to be identical. In other words, the logical value of a sentence and the situation described by this sentence are two different things. Suszko states that the identity connective is more primitive than other non-truth functional connectives such as modal connectives of possibility and necessity. The identity connective is more primitive in the sense that it cannot be eliminated without identifying it with the equivalence connective. However, if we add the identity connective to classical logic, we do not lose two-valuedness. If a non-Fregean system of logic would be constructed based on classical logic, extending its language with the identity connective and constructing semantics in which classical connectives preserve their classical meaning, we will obtain a two-valued system, in which each sentence is either true or false. On the other hand, being logically two-valued, non-Fregean logics can be seen as systems that are ontologically (referentially) many-valued. Axioms 2019, 8, 115 3 of 19 The weakest extensional and two-valued propositional non-Fregean logic is SCI (Sentential Calculus with Identity). A detailed description of the philosophical assumptions of SCI can be found in [2]. Originally, logic SCI was deﬁned as an extension of classical propositional logic with four axioms expressing the following properties of the identity connective: (1) any sentence is identical with itself, (2) if two sentences are identical, then so are their negations, (3) identical sentences are equivalent, and (4) sentences that are identical are interchangeable in any propositional context. A sound and complete semantics for SCI was designed by Suszko and Bloom in [3]. A models for SCI is a structure that consists of a universe of situations, a distinguished subset of facts (situations that actually hold), and operations that represent all the connectives. Furthermore, it is assumed that the operations satisfy certain conditions with respect to the distinguished set of situations so that the classical connectives gain their classical meaning, and the operation corresponding to the identity connective represents the identity between situations. For details, see Section 2. It is established that SCI has the ﬁnite model property and is decidable. Moreover, as shown in [4], the class of different axiomatic extensions of SCI is uncountable. There is also some research on non-standard (deviant) modiﬁcations of SCI obtained by rejecting some of its fundamental assumptions or extending its language with additional operators. Recently, the most studied modiﬁcations of SCI are Grzegorczyk’s non-Fregean logics, which are paraconsistent non-Fregean logics ([5–7]). Some research has been also focused on ﬁrst-order non-Fregean logics, in particular SCI . In [8], it has been proved that the logic SCI , obtained by extending SCI with propositional quantiﬁers, is able to express inﬁniteness and many well-known mathematical theories (e.g., the theories of groups and ﬁelds, Peano arithmetic). Furthermore, SCI does not have the ﬁnite model property, is undecidable, satisﬁes the Löwenheim-Skolem Theorem, and is an analog of Fagin’s Theorem (the class of sets of natural numbers that are expressible in SCI is precisely the complexity class NP). The non-Fregean approach has many philosophical and logical advantages as it offers a relatively simple, natural and intuitive basis for exploring fundamental relationships between language and situations. Moreover, non-Fregean logics can be seen as a general framework for representing and comparing logics with different languages or semantics. Indeed, it turned out that many non-classical logics can be equivalently translated into some extensions of SCI. For instance, modal logics S3, S4, and S5 are equivalent to some extensions of SCI, that is, there are translations—from a non-Fregean language to a modal one and the other way round—that preserve the satisfaction of formulas with respect to the appropriate class of structures (see [9]). It has been also proved in [10] that SCI can serve as a basis for expressing many-valued logics. Furthermore, it has been shown that the weakest non-Fregean logic MGL (Minimal Grzegorczyk Logic) introduced in [11] is able to express most non-classical logics, including uncountably many extensions of SCI and paraconsistent non-Fregean Grzegorczyk’s logics. Thus, MGL can be treated as a generic non-Fregean logic. The non-Fregean approach could be relevant in cognitive science applications as well as in natural language processing. Last but not least, research on non-Fregean logics could lead to a better understanding of the capabilities and relationships of logics with mutually incompatible languages and semantics. Studies on various versions of non-Fregean logic may also shed light on which class of logics offers the most adequate account of logical symbols from point of view of natural language. In this paper, we focus on deduction systems for the logic SCI. The deduction system for SCI was originally deﬁned in a Hilbert-style. Since then, some other systems for SCI have been proposed: Gentzen sequent calculus ([12–14]) and a dual tableau system ([15,16]). The aim of the paper is to present a new dual tableau system for SCI, which is suitable for automated reasoning in SCI. The main advantage of the new system is that, contrary to previously known systems, it is more efﬁcient: it does not involve any substitution rule, its rules for the identity connective do not branch a proof tree, and it generates shorter and simpler proof trees. The paper consists of ﬁve sections: in Section 2, we present the basics of the non-Fregean propositional logic SCI, that is, its language, semantics, and axiomatization. In Sections 3 and 4, we brieﬂy survey sequent calculus and a dual tableau system for SCI, respectively. In Section 5, Axioms 2019, 8, 115 4 of 19 we present a new dual tableau system for SCI and prove its soundness and completeness. Finally, in Section 6, we discuss and compare the systems presented in the paper. 2. The Non-Fregean Propositional Logic SCI The vocabulary of the language of the non-fregean propositional logic, SCI, consists of the symbols from the following pairwise disjoint sets: V = f p , p , p , . . .g—a countable inﬁnite set of propositional variables; 2 3 f:,_,^,!,$,g—the set of propositional operations of negation :, disjunction _, conjunction ^, implication !, equivalence $, and identity . The set FOR of all SCI-formulas is the smallest set including V and closed with respect to all propositional operations. An SCI-model is a structure M = (U,,t,u,),,,, D), where U is a non-empty set referred to as a universe, D is any non-empty proper subset of U, and ,t,u,),,, are operations on U with arities 1, 2, 2, 2, 2, 2, respectively, such that, for all a, b 2 U the following hold: (SCI1) a 2 D iff (a 62 D); (SCI2) at b 2 D iff (a 2 D or b 2 D); (SCI3) au b 2 D iff (a 2 D and b 2 D); (SCI4) a ) b 2 D iff (a 62 D or b 2 D); (SCI5) a , b 2 D iff (a 2 D if and only if b 2 D); (SCI6) a b 2 D iff a = b. Let M be an SCI-model. A valuation in M is any mapping v : FOR ! U such that v( p) 2 D, for every p 2 V, and the following conditions hold for all SCI-formulas: v(:j) = v(j) v(j ! y) = v(j) ) v(y) v(j_ y) = v(j)t v(y) v(j^ y) = v(j)u v(y) v(j $ y) = v(j) , v(y) v(j y) = v(j) v(y). Given an SCI-model M and a valuation v in M, an SCI-formula j is said to be satisﬁed in M by v (in short M, v j= j) whenever v(j) 2 D. An SCI-formula j is true in M if and only if for every v in M, M, v j= j. A formula is SCI-valid if and only if it is true in all SCI-models. An SCI-formula j is said to be satisﬁable in an SCI-model M whenever there exists a valuation v on M such that M, v j= j. A model is referred to as ﬁnite if its universe is ﬁnite. The intended philosophical interpretation of an SCI-model M = (U,,t,u,),,,, D) is as follows: U is the set of situations (denotations of sentences); D is the set of facts, that is, it consists of those situations that correspond to true sentences; the operations correspond to the formation of new formulas with connectives. The logic SCI is two-valued. We may deﬁne the logical value of a formula j in a model M as: df true , if for every v in M, v(j) 2 D , val (j) = false, otherwise. The following proposition shows that SCI is extensional in the sense that any subformula y of an SCI-formula j can be replaced with another formula J denoting the same as y without affecting the denotation of j. Proposition 1. Let M be an SCI-model, let v be a valuation in M, let j be an SCI-formula containing a subformula y, and let j be the result of replacing some occurrences of y in j by a formula J. Then, M, v j= y J implies M, v j= j j . Axioms 2019, 8, 115 5 of 19 The proof of Proposition 1 is presented in [16]. It should be emphasized that two-valuedness and extensionality concern different levels. Two-valuedness is a property of truth values, while extensionality holds for denotations. As shown in [3], the logic SCI has the ﬁnite model property and is decidable: Theorem 1 (Finite model property and decidability of SCI). The logic SCI has the ﬁnite model property, i.e., every satisﬁable SCI-formula is satisﬁable in a ﬁnite SCI-model. Furthermore, the logic SCI is decidable. Corollary 1. Let T be a set of SCI-formulas such that T is true in all ﬁnite SCI-models. Then, T is true in all inﬁnite SCI-models as well. The proof of the above corollary can be found in [8]. A Hilbert-style axiomatization of SCI consists of axiom schemas of classical propositional logic PC, which characterize the operations :,_,^,!,$, and the following axiom schemas for the identity operation : ( ) j j; ( ) (j y) ! (:j :y); ( ) (j y) ! (j ! y); ( ) [(j y)^ (J x)] ! [(j#J) (y#x)], for # 2 f^,_,!,$,g. The only rule of inference is modus ponens. The notion of provability of a formula is deﬁned as usual. Thus, an SCI-formula j is said to be SCI-provable whenever there exists a ﬁnite sequence j , . . . , j of SCI-formulas, n 1, such that j = j and each j , i 2 f1, . . . , ng, is an SCI-axiom or 1 n n i follows from earlier formulas in the sequence by the modus ponens rule. It is easy to see that all theorems of classical propositional logic are SCI-provable formulas. Fact 2. For every PC-formula j, the following conditions are equivalent: 1. j is provable in the classical propositional logic. 2. j is SCI-provable. Soundness and completeness of SCI with respect to the class of SCI-models was proved in [3]. Theorem 2 (Soundness and Completeness of SCI). For every SCI-formula j, the following conditions are equivalent: 1. j is SCI-provable. 2. j is SCI-valid. The logic SCI is very weak as it does not impose any speciﬁc assumptions on the cardinality of the universe of situations (except that it has at least two elements). Furthermore, it does not assume any speciﬁc assumptions on the identities of equivalent formulas—for instance, the formula (j^ y) (y^ j) is not SCI-valid. Indeed, the reduct (U,,t,u) of an SCI-model is not necessarily a Boolean algebra, since, for example, au b = bu a is not true in all SCI-models. Consider an SCI-model M = (U,,t,u,),,,, D), where U = f0, 1, 2g, D = f1, 2g, and the operations ,t,u,),,, are deﬁned by: ( ( 0, if a 6= 0, 0, if a = 0 and b = 0, df df a = at b = 1, otherwise, 1, otherwise, 0, if a = 0, or b = 0, ( < df 0, if a 6= 0 and b = 0, df au b = 1, if b = 2 and a 6= 0, a ) b = 1, otherwise, 2, otherwise, Axioms 2019, 8, 115 6 of 19 0, if a 6= 0, b = 0 or a = 0, b 6= 0, df a , b = 1, otherwise, 0, if a 6= b, df a b = a, if a = b and a 6= 0, 1, otherwise. It is easy to verify that such a structure is an SCI-model. Then, the following hold in the model M: 2u 1 = 2 and 1u 2 = 1. Hence, au b = bu a is not true in this model. Therefore, if we remove from the SCI-language some of the classical propositional connectives and deﬁne them equationally as usual, then the logic obtained in this way would not be a notational variant of SCI. Indeed, suppose that we remove the connective _ from SCI-language, and we add the df deﬁnition j_ y = :j ! y. In such a logic, the formula (j_ y) (:j ! y) would be valid, while it is not an SCI-valid formula. However, in some applications, there may be a need to impose some speciﬁc properties of situations or interactions between them. If we add additional assumptions on the universe of situations, we will obtain an extension of SCI. For example, if we add to the set of SCI-axioms the so-called Fregean axiom (Fregean Axiom) (j $ y) ! (j y), which identiﬁes the denotations of sentences with their truth values, then we get classical propositional logic. It is easy to see that classical propositional logic is the strongest among all propositional extensions of SCI. As shown in [4], there are uncountably many different non-Fregean theories stronger than SCI and weaker than classical propositional logic. In the rest of the paper, we present and discuss two types of deduction systems for SCI: a sequent-style and a tableau-like systems. Although, as mentioned above, any restriction of the SCI-language leads to a different logic than the original SCI, to make the presentation more readable, we will assume that SCI-language consists of three connectives: :, !, and . In the context of deduction systems, this restriction is minor because each of the presented system can be easily extended to the full SCI-language without loss of soundness and completeness. 3. Sequent-Style Formalizations for SCI Sequent calculi constitute an important type of deduction systems. They were designed by Gerhard Gentzen for purely theoretical reasons, mainly as a theoretical framework for investigations properties of logical consequence. However, it turned out that Gentzen sequent calculus is not only another way of axiomatization of classical logic, but also a good alternative to Hilbert (axiomatic) systems: it is much easier and more convenient to use in practice. Anyone who has tried to construct an axiomatic proof of even a very simple formula knows that such a proof construction requires a lot of effort and creativity. The reason lies in the very nature of Hilbert systems: to prove a formula we must construct a sequence of formulas with this formula as the last element of the sequence. Thus, the main challenge in building axiomatic proofs is: How can we ﬁnd the way to the formula in question? The Hilbert system itself does not provide any strategy on how to ﬁnd proofs; it only says which sequences of formulas are proofs. In Gentzen systems, this weakness is mitigated by changing the notion of a proof: in order to build a proof of a formula, we start with that formula and decompose it according to the rules of the system; if the last formulas satisfy certain conditions, then we can conclude that a formula is a theorem. Thus, in each step of decomposition, a reasoner knows the given formulas and can analyze their possible derivations. This means that sequent calculus is a goal-oriented tool, and so it could be more easily implemented than Hilbert-style systems. In recent decades, systems that could be easily automated have become increasingly important, mainly due to growing interests in applications of logic and the rapid development of information technologies. Axioms 2019, 8, 115 7 of 19 Gentzen sequent calculus provides—among other systems like tableaux or resolution—a good tool for automated theorem proving. The ﬁrst sequent calculus for the logic SCI was built by Michaels (see [12]); then, it has been simpliﬁed by Wasilewska in [13]) and modiﬁed by Chlebowski in [14]. Below, we present the basics of a sequent calculus for SCI, which is a version of systems from [12] and [13] adjusted to the well known sequent axiomatization of classical propositional logic. By G, D, S, with indices if necessary, we will denote ﬁnite (possibly empty) sequences of SCI-formulas. If G and D are sequences j , . . . , j and y , . . . , y , respectively, then G,D denotes 1 n 1 m a sequence j , . . . , j , y , . . . , y . Similarly, if j is a formula and G = (j , . . . , j ) is a sequence of 1 n 1 m 1 n formulas, then j,G (resp. G, j) denotes the sequence j, j , . . . , j (resp. j , . . . , j , j). A sequence 1 n 1 n that contains only propositional variables (resp. identities of the form j y) will be referred to as an atomic sequence (resp. an identities sequence). If j, y, J are SCI-formulas, then, by j[y/J], we denote any sequence consisting of all formulas, including j, obtained from j by replacing at least one occurrence of y by J. Clearly, given formulas j, y, J, a sequence j[y/J] is ﬁnite. If G is a ﬁnite sequence of df SCI-formulas and y, J are SCI-formulas, then G[y/J] = fj[y/J] : j 2 Gg. A sequent is an expression of the form G ` D, where G (D) is referred to as antecedent (resp. succedent) of a sequent. Validity of a sequent G ` D, for G = (j , . . . , j ) and D = (y , . . . , y ) is equivalent with 1 n 1 m validity of a formula (j ^ . . .^ j ) ! (y _ . . ._ y ). Thus, if a sequence of formulas is on the left n m 1 1 of the `, then it is considered conjunctively, while, if it is on the right of the `, the sequence of formulas is considered disjunctively. Sequent rules can be divided on the left and right rules, which in general correspond to valid formulas of the form (j ^ . . .^ j ) ! (y _ . . ._ y ). Sequent rules have the 1 n 1 m following general forms: y , j , . . . , j ,G ` D j . . . j y , j , . . . , j ,G ` D 1 1 n m 1 n (left rule) , j , . . . , j ,G ` D 1 n G ` D, y , . . . , y , j j . . . j G ` D, y , . . . , y , j m m n 1 1 1 (right rule) . G ` D, y , . . . , y 1 m There are two major groups of sequent rules: logical and structural. A logical rule introduces a new formula either on the left or on the right of the `. A structural rule operates on the structure of the sequents, ignoring the exact shape of the formulas. Some sequents are distinguished as axioms. In order to prove a sequent G ` D, we write the sequent and then proceed to construct a tree in an upward direction. In each step, we follow the rules of a sequent calculus until we reach a closing sequent that is a sequent that is an axiom. If we apply a rule in which the symbol ‘j’ occurs, then the tree splits. Each split in a tree adds a new branch. If a given branch has at its top an axiom, then it is called closed; otherwise, it is open. If all branches are closed, then a derivation of a sequent is its proof. The sequent calculus for SCI, denoted by G , consists of logical rules for the classical connectives SCI from Table 1, the rule for the identity connective depicted in Table 2, and structural rules given in Table 3. G -axioms are sequents of either of the following forms, for any SCI-formula j and any ﬁnite SCI 0 0 0 0 0 sequences G, G , D, D of SCI-formulas: G, j,G ` D, j,D or G,` D, j j,D . Table 1. G -rules for classical connectives. SCI G ` j,D G, j ` D (: ) (: ) , L R G,:j ` D G ` :j,D 0 0 G ` j,D j G , y ` D G, j ` y,D (! ) (! ) , L R 0 0 G,G , j ! y ` D,D G ` j ! y,D where j, y are any SCI-formulas 0 0 G,G ,D,D are any ﬁnite (possibly empty) sequences of SCI-formulas Axioms 2019, 8, 115 8 of 19 Table 2. G -rule for the identity connective. SCI 0 0 0 0 G,S,G [j/y] ` D,D [j/y] j G,G [j/y] ` D,S,D [j/y] ( ) , SCI 0 0 G, j y, G ` D,D where j, y are any SCI-formulas and S is the sequence j, y, j y, y j 0 0 G,D are atomic sequences and G ,D are identities sequences Table 3. Structural rules of G -calculus. SCI G ` D G ` D (W ) (W ) L R G, j ` D G ` j,D G, j, j ` D G ` j, j,D (C ) (C ) L R G, j ` D G ` j,D 0 0 G, j, y,G ` D G ` D, j, y,D (P ) (P ) L R 0 0 G, y, j,G ` D G ` D, y, j,D 0 0 G ` j,D j j,G ` D (cut) 0 0 G,G ` D,D where j, y are any SCI-formulas 0 0 G,G ,D,D are any ﬁnite (possibly empty) sequences of SCI-formulas An SCI-formula j is said to be G -provable if and only if there is a G -proof for the sequent SCI SCI ` j. As proved in [12] (cf. [13]), the system G is sound and complete: SCI Theorem 3 (Soundness and Completeness of G ). Let j be an SCI-formula. Then, the following conditions SCI are equivalent: 1. j is SCI-valid; 2. j is G -provable. SCI Note that the rule ( ) for the identity connective is a branching rule, and it can be applied SCI only if no other logical rule can be applied that is all formulas in sequents are either propositional variables or identities. Furthermore, observe that the rule ( ) corresponds to the extensionality SCI property as stated in Proposition 1. This means that the rule ( ) reﬂects the following property of SCI 0 0 the logic SCI: if ((j y)^ J) ! c is SCI-valid, then ((j y)^ J ) ! c is SCI-valid, where j, y, J, c 0 0 are any SCI-formulas and J (resp. c ) is the result of replacing some occurrences of j in J (resp. c) by a formula y. Clearly, the rule ( ) uses substitution, thus it may produce many formulas which are not SCI necessary to close a tree. Chlebowski in 2018 proposed two sound and complete sequent calculi for SCI whose rules for identity do not make use of substitution. The idea of Chlebowski’s systems is to translate each of the SCI-axiom schemas ( )–( ) to sequent rules. For instance, a left rule 3 4 corresponding to the axiom schema ( ) for ! has the following form: (j ! J) (y ! c), j y, J c,G ` D j y, J c,G ` D For details of Chlebowski’s systems, we refer the reader to [14]. Figure 1 presents a closed G -derivation of the formula ( p p ) ! ( p ! p ), which is an SCI 1 2 1 2 instance of the axiom schema ( ), while, in Figure 2, we show how to prove in G the formula 3 SCI ( p p ) ! [( p p ) ! ( p p )], which expresses the fact that the identity connective represents 1 2 2 3 1 3 a transitive relation. Axioms 2019, 8, 115 9 of 19 closed closed p , p , p , p p , p p ` p j p ` p , p , p , p p , p p 1 1 2 1 2 2 1 2 1 2 1 2 1 2 2 1 ( ) SCI p , p p ` p 1 1 2 2 (P ) p p , p ` p 1 2 1 2 (! ) p p ` p ! p 1 2 1 2 (! ) ` ( p p ) ! ( p ! p ) 2 2 1 1 Figure 1. A G -proof of a formula ( p p ) ! ( p ! p ). SCI 1 2 1 2 closed closed p , p , p p , . . . ` p p j p p , . . . ` p , p , p p , . . . 2 3 1 3 1 3 1 3 2 3 1 3 ( ) SCI p p , p p ` p p 2 3 1 2 1 3 (P ) p p , p p ` p p 1 2 2 3 1 3 (! ) p p ` ( p p ) ! ( p p ) 1 2 2 3 1 3 (! ) ` ( p p ) ! [( p p ) ! ( p p )] 1 2 2 3 1 3 Figure 2. A G -proof of a formula ( p p ) ! [( p p ) ! ( p p )]. SCI 1 2 2 3 1 3 4. Dual Tableau System DT SCI Dual tableau systems are based on Rasiowa–Sikorski diagrams for classical predicate logic (see [17]). They are top–down systems determined by the rules of inferences and axioms. Rules have the following form (rule) , n 1, where F, F , . . . , F are ﬁnite sets of formulas. The set 1 n F j ...j F F is called the premise of the rule. Sets F , . . . , F are said to be conclusions. Some systems allow 1 n inﬁnitary rules with inﬁnitely countable many conclusions. The rules are supposed to preserve the validity of the sets of formulas to which they are applied, where the validity of a ﬁnite set of formulas is understood as the validity of the disjunction of its elements. Thus, a comma in the sets of a rule (rule) can be interpreted as the meta-disjunction, while branching ‘j’ as the meta-conjunction. The rules apply to ﬁnite sets of formulas. A rule (rule) is applicable to a ﬁnite set X, whenever X = F, and there is i 2 f1, . . . , ng such that X 6= F . Axioms are distinguished valid sets of formulas, also referred to as axiomatic sets. The key notion in the methodology of dual tableau systems is a proof tree. A proof tree for a formula j is a (ﬁnitely) branching tree whose root consists of the set fjg and each node of the tree, except the root, is obtained by an application of a rule to its predecessor node. A formula j is said to be provable, whenever there is a proof tree for j such that all of its branches ends with an axiom. Dual tableau systems are validity checkers that are in order to prove a formula j we build a proof tree directly for that formula. It distinguishes dual tableaux from tableau systems, which are unsatisﬁability checkers, as in tableau systems in order to prove a formula a proof tree for its negation is constructed. Over the years, dual tableaux have been constructed for a great variety of logics, in particular for modal, intuitionistic, relevant, many-valued, temporal, spatial, fuzzy, dynamic programming logics, among others. A very recent comprehensive survey on the foundations and applications of dual tableaux is the book [16]. The ﬁrst sound and complete dual tableau for the fragment of SCI-language was presented in [15]. A dual tableau for the full SCI-language is described in [16]. The system presented in [15] (resp. [16]) was deﬁned for SCI-language which among its classical connectives contains :, ^, and _ (resp. :, ^, _, !, $). In this section, we present the basics of a dual tableau from [16] adjusted to SCI-language that contains only three connectives :, !, and . For the simplicity of our presentation, we will write j 6 y instead of :(j y). The dual tableau system for SCI, denoted by DT , consists of DT -axiomatic sets, SCI SCI decomposition rules (:), (!), (:!) presented in Table 4, and the speciﬁc rule () depicted in Table 5. Axioms 2019, 8, 115 10 of 19 Decomposition rules enable us to decompose formulas built by means of the classical connectives : and !, while the speciﬁc rule reﬂects properties of the identity connective . DT -axiomatic sets SCI have either of the following forms, where j is an SCI-formula and X is a ﬁnite (possible empty) set of SCI-formulas: fj jg[ X or fj,:jg[ X. Table 4. DT -decomposition rules. SCI fj ! yg[ X f:(j ! y)g[ X (!) (:!) f:j, yg[ X fjg[ Xjf:yg[ X f::jg[ X (:) fjg[ X where j and y are any SCI-formulas, and X is a ﬁnite (possibly empty) set of SCI-formulas. Table 5. DT -speciﬁc rule for the identity connective . SCI fj(y)g[ X () fy J, j(y)g[ X j fj(y/J), j(y)g[ X where j and J are any SCI-formulas, y is any subformula of j, j(J) is obtained from j(y) by replacing some occurrences of y with J and X is a ﬁnite (possibly empty) set of SCI-formulas. A ﬁnite set of SCI-formulas fj , . . . , j g is said to be SCI-valid whenever the disjunction of its 1 n elements is SCI-valid that is for every SCI-model M and for every valuation v in M there exists i 2 f1, . . . , ng such that M, v j= j . A DT -proof tree for an SCI-formula j is a ﬁnitely branching tree i SCI whose nodes are sets of formulas satisfying the following conditions: the formula j is at the root of this tree, each node except the root is obtained by an application of a DT -rule to its predecessor node, SCI a node does not have successors whenever it is a DT -axiomatic set or none of the rules applies SCI to its set of formulas. A branch of a DT -proof tree is said to be closed whenever it contains a node with a SCI DT -axiomatic set of formulas. A DT -proof tree is closed whenever all of its branches are closed. SCI SCI A formula j is DT -provable whenever there is a closed DT -proof tree for j, which is then referred SCI SCI to as its DT -proof. SCI Figure 3 presents a DT -proof for the formula ( p p ) ! ( p ! p ), which is an instance SCI 1 2 1 2 of the axiom schema ( ). Figure 4 presents a closed DT -proof tree for the formula ( p p ) ! 3 1 2 SCI [( p p ) ! ( p p )]. In each node of the proof tree, we underline the formula to which a rule has 2 3 1 3 been applied during the construction of the proof tree, and we indicate only those formulas in a node which are essential for this construction. ( p p ) ! ( p ! p ) 1 2 1 2 (!) p 6 p , p ! p 1 2 1 2 (!) p 6 p ,: p , p 1 2 1 2 for y := p and J := p () 1 2 Hj p p , p 6 p , . . . : p , p , . . . 1 2 1 2 2 2 closed closed Figure 3. A DT -proof for the formula ( p p ) ! ( p ! p ). SCI 1 2 1 2 Axioms 2019, 8, 115 11 of 19 ( p p ) ! [( p p ) ! ( p p )] 1 2 2 3 1 3 (!) p 6 p , ( p p ) ! ( p p ) 1 2 2 3 1 3 (!) p 6 p , p 6 p , p p 1 2 2 3 1 3 () for y := p and J := p 1 2 Hj p p , p 6 p , . . . p 6 p , p p , . . . 2 2 2 3 2 3 1 1 closed closed Figure 4. A DT -proof for ( p p ) ! [( p p ) ! ( p p )]. SCI 1 2 2 3 1 3 The proof of soundness and completeness of DT -system is presented in [16] (cf. [15]): SCI Theorem 4 (Soundness and Completeness of DT ). Let j be an SCI-formula. Then, the following SCI conditions are equivalent: 1. j is SCI-valid; 2. j is DT -provable. SCI As in G -system, the rule for the identity connective of the system DT branches a tree and SCI SCI involves use of substitution. In the next section, we present a new dual tableau that has no such disadvantages. 5. A Substitution-Free Dual Tableau for SCI In this section, we present the system DT , which is a modiﬁcation of DT -system by replacing SCI SCI the rule () with several rules for the identity connective that do not involve substitutions. The system DT consists of DT -decomposition rules presented in Table 4 (see Section 4) and the speciﬁc rules SCI SCI presented in Table 6. The speciﬁc rule (ref) (resp. (sym), (tran)) expresses reﬂexivity (resp. symmetry, transitivity) of a relation which in SCI-models corresponds to the identity connective. Thus, speciﬁc rules (ref), (sym), and (tran) reﬂect the fact that the relation corresponding to the identity connective is an equivalence relation. The speciﬁc rule ( ) (resp. ( ), ( )) expresses the instance of SCI-axiom : ! ( ) (resp. ( ) for ! and ( ) for ) presented in Section 2. Therefore, speciﬁc rules ( ), ( ), 2 4 4 : ! and ( ) correspond to the extensionality property for connectives :, !, and (see Proposition 1). As the identity connective can be characterized as an operation that satisﬁes the extensionality property and represents an equivalence relation, we will show that speciﬁc rules (ref), (sym), (tran), ( ), ( ), and ( ) are sufﬁcient to prove completeness of the system DT . SCI The axiomatic sets of DT have either of the following forms, where j, y are any SCI-formulas SCI and X is a ﬁnite (possible empty) set of SCI-formulas: 1 2 (Ax ) fj jg[ X, (Ax ) fj,:jg[ X, DT DT SCI SCI 3 4 (Ax ) fj,:y, j 6 yg[ X, (Ax ) f:j, y, j 6 yg[ X. DT DT SCI SCI The notions of an SCI-valid set of formulas, a DT -proof tree, a closed branch of such a tree, SCI a closed DT -proof tree, and DT -provability are deﬁned in a similar way as for DT -system in SCI SCI SCI Section 4. Observe that none of the speciﬁc rules split a tree or use substitutions. Now, we will prove the soundness and completeness of DT -system. SCI Axioms 2019, 8, 115 12 of 19 Table 6. DT -speciﬁc rules for the identity connective. SCI X fj 6 yg[ X (ref ) (sym) fj 6 jg[ X fy 6 j, j 6 yg[ X fj 6 y, y 6 Jg[ X (tran) fj 6 J, j 6 y, y 6 Jg[ X fj 6 yg[ X ( ) f:j 6 :y, j 6 yg[ X fj 6 y, J 6 cg[ X ( ) f(j ! J) 6 (y ! c), j 6 y, J 6 cg[ X fj 6 y, J 6 cg[ X ( ) f(j J) 6 (y c), j 6 y, J 6 cg[ X where j, y, J, c are any SCI-formulas, and X is a ﬁnite (possibly empty) set of SCI-formulas. Proposition 3 (Correctness of DT -rules). For every DT -rule (rule), the premise of rule is SCI-valid if SCI SCI and only if all of its conclusions are SCI-valid. Proof. The proof for decomposition rules is straightforward, so we will prove the proposition for the speciﬁc rules of DT : (ref), (sym), (tran), ( ), ( ), ( ). Let j, y, J, c be any SCI-formulas : ! SCI and let X be a ﬁnite (possibly empty) set of SCI-formulas. Observe that, in each of the speciﬁc DT -rules, the premise of a rule is a subset of its conclusion. Thus, if the premise is SCI-valid, then so SCI is its conclusion. Therefore, it sufﬁces to show that SCI-validity of the conclusion of a rule implies SCI-validity of its premise. Correctness of the rule (ref) Assume fj 6 jg[ X is SCI-valid and suppose X is not SCI-valid. Then, there are an SCI-model M and a valuation v in M such that, for every x 2 X, M, v 6j= x. Thus, since fj 6 jg[ X is SCI-valid and M, v 6j= x for every x 2 X, we obtain M, v j= j 6 j, so M, v 6j= j j. However, all SCI-formulas, SCI-models M, and valuations satisfy M, v j= j j, a contradiction. Correctness of the rule (sym) Assume that fy 6 j, j 6 yg[ X is SCI-valid and suppose fj 6 yg[ X is not SCI-valid. Then, there exist an SCI-model M and a valuation v in M such that M, v 6j= j 6 y and, for every x 2 X, M, v 6j= x . Thus, M, v j= j y, which means that v(j) = v(y). Furthermore, by the assumption, the model M and the valuation v must satisfy the formula y 6 j, so v(y) 6= v(j), a contradiction. Correctness of the rule (tran) Assume fj 6 J, j 6 y, y 6 Jg [ X is SCI-valid and suppose fj 6 y, y 6 Jg [ X is not SCI-valid. Then, there exists an SCI-model M and a valuation v in M that do not satisfy any formula from the set fj 6 y, y 6 Jg [ X, so M, v j= j y and M, v j= y J. Hence, we obtain v(j) = v(y) = v(J). However, by the assumption, it must hold that M, v j= j 6 J, which imply v(j) 6= v(J), a contradiction. Correctness of the rule ( ) Assume f:j 6 :y, j 6 yg[ X is SCI-valid and suppose fj 6 yg[ X is not SCI-valid. Then, there exist an SCI-model M = (U,,),, D) and a valuation v such that M, v j= j y that is v(j) = v(y). On the other hand, by the assumption, M, v j= :j 6 :y, which imply v(:j) 6= v(:y). However, if v(j) = v(y), then clearly v(:j) = v(j) = v(y) = v(:y), which contradicts v(:j) 6= v(:y). Axioms 2019, 8, 115 13 of 19 Correctness of the rule ( ) Assume f(j ! J) 6 (y ! c), j 6 y, J 6 cg[ X is SCI-valid and suppose fj 6 y, J 6 cg[ X is not SCI-valid. Then, there exist an SCI-model M = (U,,),, D) and a valuation v such that M, v j= j y and M, v j= J c, that is, v(j) = v(y) and v(J) = v(c). Hence, due to the deﬁnition of an SCI-model, we obtain: v(j ! J) = v(j) ) v(J) = v(y) ) v(c) = v(y ! c). Therefore, M, v j= (j ! J) (y ! c). However, by the assumption, M, v j= (j ! J) 6 (y ! c), a contradiction. Correctness of the rule ( ) Assume f(j J) 6 (y c), j 6 y, J 6 cg[ X is SCI-valid and suppose fj 6 y, J 6 cg[ X is not SCI-valid. Then, there exist an SCI-model M = (U,,),, D) and a valuation v such that M, v j= j y and M, v j= J c that is v(j) = v(y) and v(J) = v(c). Thus, by the deﬁnition of an SCI-model, we obtain that v(j J) = v(j) v(J) = v(y) v(c) = v(y c), and so M, v j= (j J) (y c). By the assumption, M, v j= (j J) 6 (y c), a contradiction. Proposition 4 (Validity of DT -axiomatic sets). All the DT -axiomatic sets are SCI-valid. SCI SCI Proof. Let j, y be any SCI-formulas and let X be any ﬁnite (possibly empty) set of SCI-formulas. 1 2 The proof of validity of sets (Ax ) and (Ax ) is obvious. By way of example, we will prove DT DT SCI SCI 3 4 validity of sets (Ax ), since the proof for (Ax ) is similar. Suppose a set fj,:y, j 6 yg[ X is DT DT SCI SCI not SCI-valid. Then, there exist an SCI-modelM = (U,,),, D) and a valuation v such thatM, v 6j= j, M, v 6j= :y, and M, v 6j= j y. Thus, by the deﬁnition of an SCI-model, v(j) 62 D, v(y) 62 D, and (v(j) v(y)) 62 D. However, this means that v(j) 62 D, v(y) 2 D, and v(j) = v(y), which is not possible since the latter implies v(j) 2 D iff v(y) 2 D. Due to Propositions 3 and 4, the soundness of DT can be easily proved: SCI Theorem 5 (Soundness of DT ). If an SCI-formula is DT -provable, then it is SCI-valid. SCI SCI Proof. Let j be a DT -provable formula. Then, there exists a closed DT -proof tree for j that is SCI SCI all of its branches end with DT -axiomatic sets. By Proposition 4, all DT -axiomatic sets are SCI SCI SCI-valid, so the leaves in the closed DT -proof tree for j are SCI-valid sets of formulas. Moreover, SCI by Proposition 3, if conclusions of a rule are SCI-valid, then so is its premise. Therefore, going from the leaves to the root of the tree, in each step, we obtain nodes that are SCI-valid. Hence, the root fjg is SCI-valid, and so we conclude that the formula j is SCI-valid. In order to prove completeness of DT , we will construct an SCI-model and a valuation that SCI do not satisfy a formula, which is not DT -provable. We call a branch b of a DT -proof tree SCI SCI DT -complete whenever it satisﬁes the following completion conditions for all SCI-formulas j, y, J, c: SCI Cpl(:) If ::j 2 b, then j 2 b. Cpl(!) If j ! y 2 b, then both :j 2 b and y 2 b. Cpl(:!) If :(j ! y) 2 b, then either j 2 b or :y 2 b. Cpl(ref ) For every SCI-formula j, j 6 j 2 b. Cpl(sym) If j 6 y 2 b, then y 6 j 2 b. Cpl(tran) If j 6 y 2 b and y 6 J 2 b, then j 6 J 2 b. Cpl( ) If j 6 y 2 b, then :j 6 :y 2 b. Cpl( ) If j 6 y 2 b and J 6 c 2 b, then (j ! J) 6 (y ! c) 2 b. Cpl( ) If j 6 y 2 b and J 6 c 2 b, then (j J) 6 (y c) 2 b. Axioms 2019, 8, 115 14 of 19 A DT -proof tree is said to be DT -complete whenever each of its branches is either closed or SCI SCI DT -complete. The rules of DT -system guarantee that, for every SCI-formula, there is a complete SCI SCI DT -proof tree. A non-closed branch that is DT -complete will be referred to as open. The following SCI SCI property can be easily proved: Proposition 5 (Closed Branch Property). For every complete branch b of a DT -proof tree and for every SCI SCI-formula j, if both j 2 b and :j 2 b, then the branch b is closed. Proof. Let b be a complete branch of DT -proof tree and let j be an SCI-formula such that both j 2 b SCI and :j 2 b. Suppose b is not closed. We will prove the proposition by the induction on complexity of formulas. First, observe that all the DT -rules preserves propositional variables, negations of SCI propositional variables, identities and negations of identities, that is, if a node contains j or :j, for j 2 V[fy J; y, J 2 FORg, then all of its successors contain these formulas. Thus, if j 2 b and :j 2 b, then there exists a node t in branch b such that both j 2 t and :j 2 t, which means that a node t is DT -axiomatic, and branch b is closed. Hence, the proposition holds for formulas from the SCI set V[fy J; y, J 2 FORg. Assume the proposition holds for j and y. We will show that it holds for formulas:j and j ! y. Assume:j 2 b and::j 2 b. Then, as b is a non-closed complete branch and ::j 2 b, by the completion condition Cpl(:), j 2 b. Thus, we have :j 2 b and j 2 b, so by the inductive hypothesis, b is closed. Now, let j ! y 2 b and :(j ! y) 2 b. Since b is a non-closed complete branch and j ! y 2 b, by the completion condition Cpl(!) , we obtain that both :j 2 b and y 2 b. Similarly, by the completion condition Cpl(:!), we have that either j 2 b or :y 2 b. Therefore, either both j 2 b and:j 2 b or both y 2 b and:y 2 b. Hence, by the inductive hypothesis, the branch b must be closed, which ends the proof. Let b be an open branch of a DT -proof tree and let R be deﬁned on the set of all SCI-formulas SCI as follows: df (j, y) 2 R () (j 6 y) 2 b. Proposition 6. For every open branch b of a DT -proof tree, R is an equivalence relation on the set of all SCI SCI-formulas. Proof. Let b be an open branch of a DT -proof tree and let j be an SCI-formula. Then, by the SCI completion condition Cpl(ref ), j 6 j belongs to the branch b, and so (j, j) 2 R , that is, R is reﬂexive. Assume j and y are SCI-formulas such that (j, y) 2 R . Then, j 6 y 2 b, and by the completion condition Cpl(sym), y 6 j 2 b. Thus, (y, j) 2 R , which means that R is symmetric. Now, assume that (j, y) 2 R and (y, J) 2 R , that is, both formulas j 6 y and y 6 J are in b. Therefore, by the completion condition Cpl(tran), j 6 J 2 b, so (j, J) 2 R . Thus, the relation R is transitive. Hence, we have proved that R is an equivalence relation. Proposition 7. For every open branch b of a DT -proof tree, the relation R is compatible with all the SCI connectives of SCI. Proof. Let b be an open branch of a DT -proof tree and let j, y, J, c be SCI-formulas. Assume SCI (j, y) 2 R , that is, j 6 y 2 b. Then, due to the completion condition Cpl( ), :j 6 :y 2 b, so (:j,:y) 2 R . Thus, R is compatible with :. Now, let (j, y) 2 R and (J, c) 2 R , that is, j 6 y 2 b and J 6 c 2 b. Then, by the completion condition Cpl( ), we obtain (j ! J) 6 (y ! c) 2 b, that is, ((j ! J), (y ! c)) 2 R , so R is compatible with !. Finally, assume that (j, y) 2 R and (J, c) 2 R , that is, j 6 y 2 b and J 6 c 2 b. Then, by the completion condition Cpl( ), we have (j J) 6 (y c) 2 b, that is, ((j J), (y c)) 2 R , so R is compatible with , which ends the proof. Let p 2 V and let j, y be SCI-formulas. We deﬁne the depth of an SCI-formula as follows: Axioms 2019, 8, 115 15 of 19 d( p) = d(j y) = 0 d(:j) = d(j) + 1 d(j ! y) = max(d(j), d(y)) + 1. By FOR , we denote the set of all SCI-formulas of depth n. Given an SCI-formula j, by [j] we denote the equivalence class of R determined by j. Let b be an open branch of a DT -proof tree SCI b b b b b b and let M = (U , ,) , , D ) be the branch structure deﬁned as follows: U = f[j] : j 2 FORg, D = f[j] : j 2 D g, where R n2N D = fj 2 FOR : :j 2 bg, 1 2 D = D [ D , for n+1 n+1 n+1 n+1 D = f:j 2 FOR : j 62 D g n+1 S S 2 n+1 D = fj ! y 2 FOR : j 62 D or y 2 D )g, kn k kn k n+1 b b b operations , ) , are deﬁned as: df df df b b b [j] = [:j] [j] ) [y] = [j ! y] [j] [y] == [j y] . R R R R R R R R Proposition 8 (Branch Model Property). For every open branch b of a DT -proof tree, the branch structure SCI M is an SCI-model. Proof. Let b be an open branch of a DT -proof tree. Clearly, U is not empty. Observe also that, for SCI n n every formula j 2 FOR , it holds that j 2 D iff j 2 D . Hence, for every formula j 2 FOR , n n n2N [j] 2 D iff j 2 D . Moreover, by the completion condition Cpl(ref ), for every SCI-formula b b j, j 6 j 2 b, which means that j j 2 D , and so [j j] 2 D . Thus, D 6= Æ. Now, 0 R 1 b as j j 2 D and j 6 j 2 FOR , by the deﬁnition of D , j 6 j 62 D , and so [j 6 j] 62 D . 0 1 R b b Thus, U n D 6= Æ. b b b Due to Proposition 7, operations , ) , and are well deﬁned. Indeed, assume [j] = [y] , that is, (j, y) 2 R . Then, by Proposition 7, (:j,:y) 2 R , and so [:j] = [:y] . R R R b b b b Thus, since [j] = [:j] and [y] = [:y] , we get [j] = [y] . Therefore, R R R R R R b b b b b if [j] = [y] , then [j] = [y] . Now, let # 2 f!,g and let # be deﬁned as: # = ) , R R R R b b if # =!; and # = otherwise. Assume [j] = [y] and [J] = [c] , that is, (j, y) 2 R R R R R and (J, c) 2 R . By Proposition 7, we obtain that ((j#J), (y#c)) 2 R , and so [j#J] = [y#c] . R R Therefore, we have: b b [j] # [J] = [j#J] = [y#c] = [y] # [c] . R R R R R R b b b Hence, operations , ) , and are well deﬁned. Now, we will prove that they satisfy semantic b b conditions with respect to D . Note that D satisfy the following properties for every SCI-formula j and for all n, k 2 N: (*) If d(j) = n, then [j] 2 D iff j 2 D . R n (**) If j 2 D , then d(j) = n. (***) If d(j) = n and k 6= n, then j 62 D . b b b Let [j] 2 U be such that d(j) = n, for some n 2 N. Assume [j] 2 D , which by the R R b b deﬁnition of the operation means that [:j] 2 D . Thus, since d(:j) = n + 1, by (*), we have :j 2 D . Then, by the deﬁnition of D , it holds that j 62 D , and thus due to (*) we obtain that n+1 b b [j] 62 D . Now, assume that [j] 62 D , that is, by (*), we obtain j 62 D . Thus, by the deﬁnition R R n b b of D , we get :j 2 D , which due to (*) means that [:j] 2 D . Hence, by the deﬁnition of the n+1 R b b b b b b operation , we have [j] 2 D . Therefore, we have proved that [j] 2 D iff [j] 62 D . R R R b b b b Let [j] , [y] 2 U . Assume [j] ) [y] 2 D . Then, by the deﬁnition of ) , [j ! R R R R b b y] 2 D . By the deﬁnition of D , there exists n 2 N such that j ! y 2 D , which, by (**), implies R n d(j ! y) = n, and clearly n 1. Since j ! y 2 D , by the deﬁnition of D , we obtain that either S S S j 62 D or y 2 D . Clearly, d(j) < n, so, if j 62 D , then, due to (*), we get [j] 62 D . k k k R k<n k<n k<n Axioms 2019, 8, 115 16 of 19 Moreover, d(y) < n, so, if y 2 D , then, by (*), it holds that [y] 2 D . Hence, we have proved k<n k b b b b that, if [j] ) [y] 2 D , then either [j] 62 D or [y] 2 D . Now, let us assume that d(j) = i, R R R R b b d(y) = j, for some i, j 2 N, and either [j] 62 D or [y] 2 D . Thus, by (**), j 62 D or y 2 D . R R i j Let n = max(i, j) + 1. If j 62 D , then, by (***), it can be easily proved that j 62 D . If y 2 D , i k<n k j S S S then, by (*), y 2 D . Therefore, either j 62 D or y 2 D . Then, by the deﬁnition of k<n k k<n k k<n k b b D , it follows that j ! y 2 D , and, by (*), we have [j ! y] 2 D . Thus, by the deﬁnition of the b b b b b operation ) , we obtain that [j] ) [y] 2 D . Hence, we have proved that [j] ) [y] 2 D R R R R b b iff either [j] 62 D or [y] 2 D . R R Now, let [j] , [y] 2 U . Clearly, d(j y) = 0. Then, the following can be easily shown: R R b b b [j] [y] 2 D iff [j y] 2 D iff j y 2 D iff j 6 y 2 b iff (j, y) 2 R iff R R R 0 [j] = [y] . R R b b Hence, we have shown that [j] [y] 2 D iff [j] = [y] . Therefore, we have proved that R R R R the branch structure M is an SCI-model. b b b b b b LetM = (U , ,) , , D ) be the branch structure for an open branch b of a DT -proof tree. SCI b b b Let v : FOR ! U be a function such that v (j) = [j] , for all j 2 FOR. Due to the deﬁnition of M , the following can be easily proved: b b b b b b Proposition 9. Let b be an open branch of a DT -proof tree and let M = (U , ,) , , D ) be the SCI b b b branch structure. Then, the function v : FOR ! U such that v (j) = [j] , for all j 2 FOR, is an SCI-valuation in M , that is, for all SCI-formulas j and y, the following hold: b b b b b b v (:j) = [j] v (j ! y) = [j] ) [y] v (j y) = [j] [y] . R R R R R The valuation v will be referred to as the branch valuation. Now, we will prove the property that will enable us to prove the completeness theorem. b b b b b b Proposition 10 (Satisfaction in Branch Model Property). Let M = (U , ,) , , D ) be the branch b b structure for an open branch b of a DT -proof tree and let v be the branch valuation in M . Then, for every SCI b b SCI-formula j, if M , v j= j, then j 62 b. b b b b b b Proof. Let M = (U , ,) , , D ) be the branch structure for an open branch b of a DT -proof SCI b b tree and v the branch valuation in M . We will prove the proposition by the induction on the depth of SCI-formulas. Let j be an SCI-formula such that d(j) = 0. b b b b b b Assume M , v j= j. Note that the following holds: M , v j= j iff v (j) = [j] 2 D iff j 2 D iff :j 2 b. Thus, by the assumption, we obtain :j 2 b, which, by Proposition 5, implies j 62 b. b b b b b b Assume M , v j= :j. Then, M , v j= :j iff v (:j) = [:j] 2 D iff :j 2 D . Suppose R 1 :j 2 b. Then, j 2 D , so, by the deﬁnition of D , we have :j 62 D , a contradiction. 0 1 1 Assume that the proposition holds for SCI-formulas j and y and their negations. We will show that it holds for formulas ::j, j ! y, and :(j ! y). b b b b b Let M , v j= ::j. Since M is an SCI-model, by the assumption M , v j= j. Thus, by the inductive hypothesis, j 62 b. Suppose ::j 2 b. Then, by the completion condition Cpl(:), j 2 b, a contradiction. b b b b b b Let M , v j= j ! y. Then, either M , v j= :j or M , v j= y. Then, by the inductive hypothesis, either :j 62 b or y 62 b. Suppose j ! y 2 b. Then, by the completion condition Cpl(!), both :j 2 b and y 2 b, a contradiction. b b b b b b Let M , v j= :(j ! y). Then, both M , v j= j and M , v j= :y. Then, by the inductive hypothesis, both j 62 b and :y 62 b. Suppose :(j ! y) 2 b. Then, by the completion condition Cpl(:!), either j 2 b or :y 2 b, a contradiction. Now, we will prove completeness of an DT -system: SCI Axioms 2019, 8, 115 17 of 19 Theorem 6 (Completeness of DT ). If an SCI-formula is SCI-valid, then it is DT -provable. SCI SCI Proof. Let j be SCI-valid and suppose that a closed DT -proof tree for j does not exist. Then, there SCI exists a complete DT -proof tree for j with an open branch, say b. Clearly, j 2 b, so by Proposition 10, SCI b b b the branch structureM and the branch valuation v do not satisfy j. However, by Proposition 8,M is an SCI-model. Thus, j is not true in some SCI-model, and hence j is not SCI-valid, a contradiction. Theorems 5 and 6 imply: Theorem 7 (Soundness and Completeness of DT ). Let j be an SCI-formula. Then, the following SCI conditions are equivalent: 1. j is SCI-valid; 2. j is DT -provable. SCI Below, we present examples of DT -proofs, namely DT -proofs of ( p p ) ! ( p ! p ) 1 2 1 2 SCI SCI and ( p p ) ! [( p p ) ! ( p p )] are presented in Figures 5 and 6, respectively. Note 1 2 2 3 1 3 that DT -proofs are much shorter than the corresponding proofs of these formulas in the systems SCI G and DT . Furthermore, contrary to the proofs in G and DT , DT -proofs of formulas in SCI SCI SCI SCI SCI question are one-branching proofs. ( p p ) ! ( p ! p ) 2 2 1 1 (!) p 6 p , p ! p 1 2 1 2 (!) p 6 p ,: p , p 1 2 1 2 closed Figure 5. A DT -proof for the formula ( p p ) ! ( p ! p ). 2 2 1 1 SCI ( p p ) ! [( p p ) ! ( p p )] 1 2 2 3 1 3 (!) p 6 p , ( p p ) ! ( p p ) 1 2 2 3 1 3 (!) p 6 p , p 6 p , p p 1 2 2 3 1 3 (tran) p 6 p , p 6 p , p 6 p , p p 1 3 1 2 2 3 1 3 closed Figure 6. A DT -proof for ( p p ) ! [( p p ) ! ( p p )]. 1 2 2 3 1 3 SCI 6. Discussion All the systems presented in the previous sections are sound and complete deduction systems for SCI. Comparing with systems G and DT , the system DT seems to be simpler, more intuitive, SCI SCI SCI and more effective. Its rules for the identity connective do not split a branch of a tree and do not make use of substitution. It should also be emphasized that the only rule of DT -system that may introduce SCI branching is the rule (:!). Furthermore, although DT contains nine rules, while G -system has SCI SCI 12 rules, DT -system generates proofs that are much simpler and shorter than corresponding proofs SCI in G . SCI However, all the systems presented in this paper have one important disadvantage. The logic SCI is decidable, while the systems in question are not decision procedures for SCI as, in particular, Axioms 2019, 8, 115 18 of 19 they may generate inﬁnite trees. Although there is a decision procedure for SCI based on G -system, SCI as shown in [13], but a procedure described in [13] contains external machinery that is not a part of the system itself, so it provides rather another proof for decidability of SCI than a decision procedure itself. Hence, further research on deduction systems for SCI should focus on seeking its decision procedure. The system DT seems to have a signiﬁcant advantage over other systems G and DT , as its SCI SCI SCI relatively simple modiﬁcation could provide a decision procedure for SCI. A possible modiﬁcation of DT should restrict applicability of the rules for the identity connective as follows: (1) the rule SCI (ref) can be applied only for j that are subformulas or negated subformulas of the initial formula; (2) given the formulas j, y, J, the rules (sym) and (tran) can be applied only once; (3) the rules ( ), ( ), and ( ) can be applied to a ﬁnite set of formulas provided that the length of new formulas introduced by rules is not greater than the length of the initial formula plus 1. Additionally, we should also impose a general restriction on closeness of a branch, namely that, if a node is a ‘copy’ of some earlier node, then the branch is closed. It seems that such a modiﬁcation could guarantee termination of proof trees, and thus it could provide a decision procedure for SCI. 7. Conclusions We have presented and discussed two types of systems for SCI known from the literature: sequent calculus G and a dual tableau-like system DT . Then, we presented the system DT , which is SCI SCI SCI a new dual tableau system for the logic SCI. We proved soundness and completeness of DT and SCI we showed that it is more efﬁcient than G and DT : it does not involve any substitution rule, SCI SCI its rules for the identity connective do not branch a proof tree, and it generates shorter and simpler proof trees. Further research on deduction systems for non-Fregean logics should concentrate on decision procedures for SCI and a methodology of designing deduction systems in tableuax style for non-Fregean logics which are extensions and modiﬁcations of SCI. Author Contributions: Deﬁning the general research problem and the scientiﬁc ideas for its solution: J.G.-P.; Elaboration of the results known from the literature included in the thematic scope of the research problem studied in the paper: J.G.-P. and M.W.; Construction of the new system DT : J.G.-P.; Proving soundness and SCI completeness of the system: J.G.-P. and M.W.; Checking correctness of proofs: J.G.-P.; Writing the manuscript: J.G.-P. and M.W.; Editing and proofreading: J.G.-P. and M.W.; Funding: J.G.-P.; Supervision: J.G.-P. Funding: The research presented in the paper was funded by the National Science Centre, Poland, research project No. 2017/25/B/HS1/00503. Conﬂicts of Interest: The authors declare no conﬂict of interest. References 1. Suszko, R. Non-Fregean logic and theories. Analele Univ. Bucur. Acta Log. 1968, 11, 105–125. 2. Suszko, R. Abolition of the Fregean axiom. In Logic Colloquium: Symposium on Logic Held at Boston, 1972–73; Parikh, R., Ed.; Lecture Notes in Mathematics; Springer: Heidelberg, Germany, 1975; Volume 453, pp. 169–239. 3. Bloom, S.; Suszko, R. Investigation into the sentential calculus with identity. Notre Dame J. Form. Log. 1972, 13, 289–308. [CrossRef] 4. Golinska-Pilar ´ ek, J.; Huuskonen, T. Number of extensions of non-Fregean logics. J. Philos. Log. 2005, 34, 193–206. [CrossRef] 5. Golinska-Pilar ´ ek, J.; Huuskonen, T. Logic of descriptions. A new approach to the foundations of mathematics and science. Stud. Log. Gramm. Rhetor. 2012, 40, 63–94. 6. Golinska-Pilar ´ ek, J.; Huuskonen, T. Grzegorczyk’s non-Fregean logics and their formal properties. In Applications of Formal Philosophy; Urbaniak, R., Payette, G., Eds.; Logic, Argumentation and Reasoning; Springer International Publishing: New York, NY, USA, 2017; Volume 14, pp. 243–263. 7. Golinska-Pilar ´ ek, J.; Huuskonen, T. A mystery of Grzegorczyk’s logic of descriptions. In The Lvov-Warsaw School. Past and Present; Garrido, A., Wybraniec-Skardowska, U., Eds.; Studies in Universal Logic; Springer Nature: Stuttgart, Germany, 2018; pp. 731–745. Axioms 2019, 8, 115 19 of 19 8. Golinska-Pilar ´ ek, J.; Huuskonen, T. Non-Fregean propositional logic with quantiﬁers. Notre Dame J. Form. Log. 2016, 57, 249–279. [CrossRef] 9. Suszko, R. Identity connective and modality. Stud. Log. 1971, 27, 7–39. [CrossRef] 10. Malinowski, G. Identity, many-valuedness and referentiality. Log. Log. Philos. 2013, 22, 375–387. [CrossRef] 11. Golinska-Pilar ´ ek, J. On the minimal non-Fregean Grzegorczyk’s logic. Stud. Log. 2016, 104, 209–234. [CrossRef] 12. Michaels, A. A uniform proof proceduree for SCI tautologies. Stud. Log. 1974, 33, 299–310. [CrossRef] 13. Wasilewska, A. A sequence formalization for SCI. Stud. Log. 1976, 35, 213–217. [CrossRef] 14. Chlebowski, S. Sequent calculi for SCI. Stud. Log. 2018, 106, 541–563. [CrossRef] 15. Golinska-Pilar ´ ek, J. Rasiowa-Sikorski proof system for the non-Fregean sentential logic SCI. J. Appl.-Non-Class. Log. 2007, 17, 511–519. [CrossRef] 16. Orłowska, E.; Golinska-Pilar ´ ek, J. Dual Tableaux: Foundations, Methodology, Case Studies; Trends in Logic; Springer: Dordrecht Heidelberg London New York, NY, USA, 2011; Volume 33. 17. Rasiowa, H.; Sikorski, R. On Gentzen theorem. Fundam. Math. 1960, 48, 57–69. [CrossRef] c 2019 by the authors. Licensee MDPI, Basel, Switzerland. This article is an open access article distributed under the terms and conditions of the Creative Commons Attribution (CC BY) license (http://creativecommons.org/licenses/by/4.0/).
Axioms – Multidisciplinary Digital Publishing Institute
Published: Oct 17, 2019
You can share this free article with as many people as you like with the url below! We hope you enjoy this feature!
Read and print from thousands of top scholarly journals.
Already have an account? Log in
Bookmark this article. You can see your Bookmarks on your DeepDyve Library.
To save an article, log in first, or sign up for a DeepDyve account if you don’t already have one.
Copy and paste the desired citation format or use the link below to download a file formatted for EndNote
Access the full text.
Sign up today, get DeepDyve free for 14 days.
All DeepDyve websites use cookies to improve your online experience. They were placed on your computer when you launched this website. You can change your cookie settings through your browser.