Tableau-based Decision Procedure for the Logic SCI∗

Abstract

In this note, we present a sound, complete, and terminating labelled tableau calculus for the logic SCI (Sentential Calculus with Identity). To the best of our knowledge, it is the first tableau-based decision procedure for this logic. The logic SCI (Sentential Calculus with Identity) belongs to the wide class of non-Fregean logics that reject the so-called Fregean axiom which identifies denotations of sentences with their truth values. 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 sentences; that is, it connects two sentences and forms a new one which is true whenever both of its arguments refer to the same semantic correlate (they describe the same situation). On the formal side, SCI extends classical propositional logic with the axioms characterizing the identity connective as equivalence which obeys the extensionality principle. Models of SCI are based on structures built of the universe of situations, operations interpreting the logical connectives and a distinguished subset of the universe, called the set of facts which are semantical correlates of true sentences. For details see Section 2. A sound and complete semantics for SCI was designed by Suszko and Bloom in [2]. The logic SCI is the weakest non-Fregean propositional logic which is extensional and two-valued. A detailed description of the philosophical assumptions of SCI can be found in [17]. The non-Fregean approach can be seen as a powerful logical alternative to the classical one. It comprises logical systems which are relatively simple and intuitive and at the same time very expressive. Indeed, it is known that classical propositional logic as well as many non-classical propositional logics, for instance some modal logics and many-valued logics of Łukasiewicz, can be formulated within a general framework of SCI as subcalculi of the latter. The high expresiveness of the logic SCI is demonstrated, among others, by the fact that the class of all of its non-equivalent elementary extensions is uncountable (see [7]). Moreover, it is also known that a seemingly minor extension of SCI with quantifiers binding propositional variables, and some fairly natural axioms involving these quantifiers, is able to express many interesting first-order theories, such as the theories of groups, rings, and fields, as well as a weak fragment of Peano arithmetic. For this reason, research on non-Fregean logics can lead to a better understanding of the interrelations between logics with mutually incompatible languages and semantics.

-

Originally, the non-Fregean logic has been constructed to formalize an ontology of situations, in particular to provide definitions of notions such as fact or possible and neccessary situations. Thus, according to the standard interpretation, propositional variables of SCI represent situations in an ontology and the connective ≡ represents the identity of situations. However, there are several other interpretations of what propositional variables and the connective ≡ represent. For instance, in [ 6 ], the very weak non-Fregean logic MGL has been proposed to formalize the equivalence of meaning or synonimity. In MGL the formula ϕ ≡ ψ is interpreted as ‘ϕ and ψ have the same meaning’. The logic MGL is very weak, for instance involution of the negation and commutativity of the conjunction are not its preconditions. Thus, it could be a good tool to represent natural language constructors, in particular temporal conjunction. Furthermore, it is also claimed that the non-Fregean logics can be used to represent dynamic systems, in particular program verification.

In such an approach situations represent states of machines, while formulas describe both programs and the conditions to be verified. In this framework, the expression (ϕ ∧ ψ) ≡ (ψ ∧ ϕ) can be read as ’an execution of the programs ϕ and then ψ terminates with the same upshot as an execution of the programs ψ and then ϕ’, or, to put it more concisely, ‘Regardless of the ordering, a consecutive execution of the programs ϕ and ψ always leads to the same result’. Consequently, by means of non-Fregean logic we are able to check whether syntactically different programs yield the same outputs. Furthermore, if we add temporal and other dynamic operators to non-Fregean logic we obtain a very attractive tool for verification of program correctness.

In this note, we present a tablau-based decision procedure for the logic SCI the rules of which straightforwardly reflect the semantics and axiomatization of a logic. Although several sequent calculi have been devised for SCI thus far, to the best of our knowledge no tableau calculus has been proposed for this logic as of yet.

In Sect. 2 we provide the syntax, semantics and axiomatization of SCI. Sect. 3 exhibits the tableau calculus TCSCI and contains proof sketches of its soundness, completeness, and termination. In Sect. 4 we briefly discuss alternative deductive systems for SCI. Sect. 5 summarizes the content of the paper. 2

The logic SCI

Syntax Let LSCI be a language of the logic SCI with the alphabet hAF, ¬, →, ≡i, where AF = {p, q, r, . . .} is a denumerable set of atomic formulas. The set WFFSCI of SCI-well-formed formulas is defined by the following abstract grammar:

' ::= p | ¬' | ' → ' | ' ≡ ', where p ∈ AF. We define the connectives ∨, →, ↔ as standard abbreviations, i.e, for any ', ∈ WFFSCI: ' ∨ := ¬' → , ' ∧ := ¬(' → ¬ ), ' ↔ := (' → ) ∧ ( → ').

As we can see, the language of SCI is a standard propositional language augmented with a binary identity connective ≡.

Semantics Let U 6= ∅, D ⊆ U , and let V : WFFSCI −→ U . An SCI-model is a triple M = hU, D, |=i, where U , D, |= are called, respectively, universe of situations, set of facts (situations that actually hold) and valuation, and the following conditions are satisfied for all ', ∈ form and being substitutions of the SCI-axioms schemes:

V ( ) ∈ D

V (¬') ∈ D V (' → ) ∈ D V (' ≡ ) ∈ D iff iff iff

V (') ∈/ D V (') ∈/ D or V ( ) ∈ D V (') = V ( ).

The identity connective standing between two formulas is then interpreted as an identity of the situations represented by these formulas. The semantics of SCI does not impose any specific restrictions on the number of situations except that there must exist at least two situations (among which at least one is a fact and at least one is not a fact). Axiomatization The logic SCI is axiomatized by modus ponens and the rule of substitution as the only derivation rules, the set of axiom schemes for classical propositional logic and the following set of identity axiom schemes: (I1) (I2) ' ≡ ' ' ≡ → ¬' ≡ ¬ (I3) (I4) ' ≡ ' ≡ → ( ≡ → (' → → ('# ) ≡ ( # )), where # ∈ {→, ≡} ).

Their intuitive interpretation is as follows. (I1) states that the situation represented by a formula is always identical to itself. (I2) and (I3) allow to replace a subformula of a formula with any formula representing the same situation without changin the denotation of the initial formula. (I4) says that two formulas representing the same situation must have the same truth value.

The logic SCI is two-valued in the sense that given a model and an interpretation, a formula is satisfied if and only if its negation is not satisfied. Furthermore, SCI has the finite model property and is decidable.

The ontology of situations underlying SCI is extremely weak, as it only assumes the existence of at least two situations. Note that if we add to SCI-axiom schemes the so-called Fregean axiom saying that there are at most two situations, we get classical propositional logic. Indeed, since SCI-models of such an extension are just structures with two situations (truth values), in classical propositional logic the identity connective is indistinguishable from the equivalence connective.

Note also that SCI does not impose any particular restrictions on the identities of equivalent formulas – for instance, the formula ϕ ∧ ψ ≡ ψ ∧ ϕ is not SCI-valid as the algebra underlying SCI-models is not Boolean. For instance, the formula ϕ ∧ ψ ≡ ψ ∧ ϕ is not satisfied in an SCI-model with the universe {0, 1, 2}, the distinguished set of facts {1, 2}, and V satisfying: V (' ∧ ψ) = 1 and V (ψ ∧ ϕ) = 2. 3 In this section we provide a characterization of sound, complete and terminating labelled tableau calculus for the logic SCI. The main advantage of the calculus presented below lies in the fact that it straightforwardly generates simple models of (satisfiable) formulas. In AI, broadly conceived, model generation itself is widely used in, i.a., fault analysis, system verification [ 14, 1 ] or ontology debugging [ 13 ]. A particular focus are minimal models or models with a restricted cardinality of the universe [ 12 ]. Thus, regardless of the concrete domain we want to formalize by means of SCI, a tableau algorithm yielding a simple model for each satisfiable formula given as its imput is a natural complementation of the formalization itself.

We will now describe the structure of a tableau generated by our calculus. Let L+, L− be countably infinite sets and let L = L+ ∪ L−. We will call an expression of the form (', w∗, A), where ' ∈ WFFSCI, w∗ ∈ L, ∗ ∈ {+, −}, and A ⊆ L, labelled formula and w∗ will be called label. We assume that labels superscribed with ‘+’ belong to L+ and the ones superscribed with ‘ ’ belong to L−. Intuitively, w∗ − stands for the denotation of ' in an intended model and A contains those elements of the universe which are known not to be the denotations of '. Labels with ‘+’ in the superscript denote elements of D (facts), whereas labels with superscribed ‘ ’ represent elements of U \ D (non-facts).

−

The notions of tableau, branch, node, formula reduction for a rule, branch (tableau)-openness, branch (tableau)-closeness, and branch (tableau)-expandedness, used in the remainder of the paper, are standard and we refer the reader to [ 4, 9, 16 ] for further details.

Analytic tableaux are satisfiability checkers, so a tableau proof of a formula ' is a closed tableau with a labelled formula (', w−, ∅) at its root. On the other hand, a formula ϕ is tableau-satisfiable if there exists an open and fully expanded tableau with a labelled formula (', w+, ∅) at its root.

A tableau calculus is called sound iff each satisfiable input formula ' is tableau-satisfiable; complete iff for each valid input formula ' there exists a tableau proof of '; terminating if all tableaus generated by the set of rules of this calculus are finite. Finally a tableau calculus is a decision procedure if it is sound, complete and terminating. The rules presented in Fig. 1 constitute a sound and complete tableau system TCSCI for the logic SCI. We assume that in the rules (¬+), (¬−), (→+), (→−), (≡+), (≡−) all labels occurring in the denominators

→ , u∗, F ∪ G) are fresh. If in a rule a label is superscribed with ‘∗’ rather than ‘+’ or ‘−’, it means that the rule applies to both types of labels.

The rules (¬+), (¬−), (→+), (→−), (≡+), (≡−) reflect the semantics of ¬, → and ≡ defined in the conditions for the valuation function V presented in Sect. 2. A few words of extra commentary on the rule (≡−) are in place. It decomposes a formula involving the ≡ connective, which is assumed to be false. By the semantics of ≡ we know that the constituents of the initial ≡-formula have distinct denotations. If these denotations have different polarities, representing different truth values (disjuncts 2 and 3 in the denominator of the rule), then no additional information has to be stored about the distinctness of these denotations. If, on the other hand, the denotations have the same polarity, representing the same truth value (disjuncts 1 and 4 in the denominator of the rule), then extra information is added to the resulting labelled formulas about the labels that are not the denotations of respective SCI-formulas. The rules (≡¬), (≡→) and (≡≡) are tableau-counterparts of the axiom schemes (I2) and (I3). The rule (F) ensures that a valuation which can be read off from an open branch is a function, i.e., that it does not assign two denotations which are necessarily distinct, to the same formula.

Soundness, completeness and termination In order to prove soundness and completeness of the tableau calculus TCSCI we take the appropriate conditions in the contrapositive form.

Theorem 1 (Soundness). The tableau calculus TCSCI is sound.

Proof idea. Standard verification of the calculus’ rules.

Theorem 2 (Completeness). The tableau calculus TCSCI is complete.

Proof idea. Standard construction of a (counter)model out of an open and fully-expanded branch of a tableau.

It turns out that if we slightly modify the notion of labelled formula reduction for a rule (see [9, Def. 4.3]), we retain the completeness and termination of the tableau calculus and, on the other hand, avoid many superfluous steps in tableau derivations. Let (', w∗, A) be a labelled formula occurring on a branch B. If there exists a labelled formula (', v∗, B) on B such that w∗ and v∗ have the same polarity and a rule (R) ∈ {(¬+), (¬−), (→+), (→−), (≡+), (≡−)} was applied to (', v∗, B), then we call (', w∗, A) proto-reduced for (R). In the case of other rules the notion of proto-reduction a formula coincides with the notion of reduction of a formula. The calculus TCSCI in which no rule (R) can be applied to a labelled formula that is proto-reduced for (R) (rather than reduced for (R)), will be denoted by TCSCI + PE. Theorem 3. The tableau calculus TCSCI + PE is sound, complete and terminating.

Proof idea. The soundness of TCSCI straightforwardly follows from the soundness of TCSCI and the fact that both calculi share all the rules.

Proving that TCSCI + PE retains the completeness of TCSCI amounts to showing that for the same input formula (', w−, ∅) whenever a closure rule (⊥1) or (⊥2) is applied on a branch B of a TCSCI-derivation, then the same closure rule can be applied on a branch B0 ⊆ B, with (', w−, ∅) at the root of B0, where ( +), (¬−), (→+), (→−), (≡+), (≡−)} were not applied to those formulas which were the rules (R) ∈ { ¬ proto-reduced for these rules. 2|'|·22|'| distinct labelled formulas on B and, thus, a branch can contain at most 10· |'| · 2|'| · 22|'| nodes (the last component of the above-mentioned formula represents an application of a closure rule).

The upper bound constraining the number of nodes in a tableau branch is exponential in the size of an input formula. We believe, however, that it is possible to establish an upper bound which is polynomial in the size of an input formula, hence we formulate the following: Conjecture 1. The maximal number of nodes of a branch B of a tableau T yielded by the calculus TCSCI + PE is polynomial in the size of the input formula, thus TCSCI + PE runs in NP.

Moreover, we believe that even the original calculus TCSCI can be shown to be terminating, so we formulate the following: Conjecture 2. The tableau calculus TCSCI is terminating. 4

Discussion

So far, several alternative deductive systems for the logic SCI have been devised. The first sequent calculus for the logic SCI was built by Michaels (see [ 10 ]), then it was simplified by Wasilewska in [ 18 ], and modified by Chlebowski in [ 3 ]. The first two systems enjoy the termination property and as such constitute decision procedures for SCI, however they employ substantial external techniques to ensure that all sequent derivations always terminate. The last mentioned sequent calculus is not a decision procedure. Wasilewska also proposed a system of the so-called DFC-algorithms in [ 19 ]. In [ 15 ] Rogava proved that the cut-elimination theorem holds for a sequent calculus for SCI.

The first sound and complete dual tableau for the fragment of SCI-language was presented in [ 5 ]. A dual tableau for the full SCI-language is described in [ 11 ]. The system presented in [ 5 ] (resp. [ 11 ]) was defined for the SCI-language which contains ¬, ∧, and ∨ (resp., ¬, ∧, ∨, →, ↔) among its classical connectives. These dual tableau calculi are not labelled in the sense of TCSCI, i.e., no direct reference to the denotations of formulas is made during the derivation. Also, termination has not been proven for these systems.

What distinguishes our calculus from the ones recalled above is the use of labels in the calculus’ rules thanks to which all of them enjoy the subformula property. Consequently, the termination of the calculus is relatively easy to establish. Another result of involving labels in the calculus is that we do not need to add extra rules which guarantee that ≡ is an equivalence relation, as it is implicitly ensured by the existing rules. 5

Summary

In this note, we presented SCI – a propositional logic that allows to formalize a simple ontology of situations and thanks to its non-standard identity connective ≡ shows a potential of representing other fields of knowledge, such as program behaviour or temporal dimension of different logical connectives. The

References

[1] P. Baumgartner , P. Fröhlich , U. Furbach , and W. Nejdl . Tableaux for diagnosis applications . In D. Galmiche, editor, Automated Reasoning with Analytic Tableaux and Related Methods , pages 76 - 90 , Berlin, Heidelberg, 1997 . Springer Berlin Heidelberg.

[2] S. L. Bloom and R. Suszko . Investigations into the sentential calculus with identity . Notre Dame J. Formal Logic , 13 ( 3 ): 289 - 308 , 07 1972 .

[3] S. Chlebowski . Sequent calculi for SCI. Studia Logica , 106 ( 3 ): 541 - 563 , 2018 .

[4] M. D'Agostino , D. M. Gabbay , R. Hähnle , and J. Posegga, editors. Handbook of Tableau Methods . Springer, Dordrecht, 1999 .

[5] J. Golińska-Pilarek . Rasiowa-Sikorski proof system for the non-Fregean sentential logic SCI . Journal of Applied Non-Classical Logics , 17 ( 4 ): 511 - 519 , 2007 .

[6] J. Golińska-Pilarek . On the minimal non-fregean grzegorczyk logic . Studia Logica , 104 ( 2 ): 209 - 234 , 2016 .

[7] J. Golińska-Pilarek and T. Huuskonen . Number of extensions of non-fregean logics . Journal of Philosophical Logic , 34 ( 2 ): 193 - 206 , 2005 .

[8] J. Golińska-Pilarek and M. Welle . Deduction in non-fregean propositional logic sci . Axioms , 8 ( 4 ): 115 , 2019 .

[9] F. Massacci . Single step tableaux for modal logics . Journal of Automated Reasoning , 24 ( 3 ): 319 - 364 , 2000 .

[10] A. Michaels . A uniform proof procedure for SCI tautologies . Studia Logica , 33 ( 3 ): 299 - 310 , 1974 .

[11] E. Orłowska and J. Golińska-Pilarek . Dual Tableaux: Foundations, Methodology, Case Studies, , volume 33 of Trends in Logic. Springer Netherlands, 2011 .

[12] F. Papacchini . Minimal Model Reasoning for Modal Logic . PhD thesis , University of Manchester, 2015 .

[13] B. Parsia , E. Sirin, and A. Kalyanpur . Debugging OWL ontologies . In Proceedings of the 14th International Conference on World Wide Web, WWW '05 , pages 633 - 640 , New York, NY, USA, 2005 . ACM.

[14] R. Reiter . A theory of diagnosis from first principles . Artificial Intelligence , 32 ( 1 ): 57 - 95 , 1987 .

[15] M. Rogava . Cut elimination in SCI. Bulletin of the Section of Logic , 4 ( 3 ): 119 - 122 , 1975 .

[16] R. A. Schmidt and D. Tishkovsky . Automated synthesis of tableau calculi. Logical Methods in Computer Science , 7 ( 2 :6): 1 - 32 , 2011 .

[17] R. Suszko . Abolition of the Fregean axiom . In R. Parikh, editor, Logic Colloquium , pages 169 - 239 , Berlin, Heidelberg, 1975 . Springer Berlin Heidelberg.

[18] A. Wasilewska . A sequence formalization for SCI . Studia Logica , 35 ( 3 ): 213 - 217 , 1976 .

[19] A. Wasilewska . DFC-algorithms for Suszko logic and one-to-one Gentzen type formalizations . Studia Logica , 43 ( 4 ): 395 - 404 , 1984 .