=Paper=
{{Paper
|id=Vol-2509/paper3
|storemode=property
|title=Tableau-based Decision Procedure for the Logic SCI
|pdfUrl=https://ceur-ws.org/Vol-2509/paper3.pdf
|volume=Vol-2509
|authors=Joanna Golińska-Pilarek,Michał Zawidzki
|dblpUrl=https://dblp.org/rec/conf/aiia/Golinska-Pilarek19
}}
==Tableau-based Decision Procedure for the Logic SCI==
https://ceur-ws.org/Vol-2509/paper3.pdf
Proceedings of the
1st Workshop on Artificial Intelligence and Formal Verification, Logics, Automata and Synthesis (OVERLAY),
Rende, Italy, November 19–20, 2019
Tableau-based Decision Procedure for the Logic SCI∗
Joanna Golińska-Pilarek1 and Michał Zawidzki2
1
Institute of Philosophy, University of Warsaw, Poland
2
Department of Logic and Methodology of Science, University of Łódź, Poland
1
j.golinska@uw.edu.pl
2
michal.zawidzki@filozof.uni.lodz.pl
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.
1 Introduction1
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.
∗ Research reported in this paper is supported by the National Science Centre, Poland (grant number: UMO-
2017/25/B/HS1/00503).
1 A thorough exposition of non-Fregean logics can be found in [8].
Copyright c 2020 for this paper by its authors.
Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
24 J. Golińska-Pilarek and M. Zawidzki
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 iff V (ϕ) ∈
/D
V (ϕ → ψ) ∈ D iff V (ϕ) ∈
/ D or V (ψ) ∈ D
V (ϕ ≡ ψ) ∈ D iff 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).
Tableau-based Decision Procedure for the Logic SCI 25
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) ϕ≡ϕ (I3) ϕ ≡ ψ → (χ ≡ θ → (ϕ#χ) ≡ (ψ#θ)), where # ∈ {→, ≡}
(I2) ϕ ≡ ψ → ¬ϕ ≡ ¬ψ (I4) ϕ ≡ ψ → (ϕ → ψ).
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 Tableaux
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.
Tableau calculus for SCI
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
26 J. Golińska-Pilarek and M. Zawidzki
(¬ϕ, w+ , A) (¬ϕ, w− , A) (ϕ → ψ, w+ , A) −
− (ϕ → ψ, w , A)
(¬+ ) (¬− ) (→ +
) (→ ) +
(ϕ, v − , ∅) (ϕ, v + , ∅) (ϕ, v − , ∅) | (ψ, u+ , ∅) (ϕ, v , ∅)
(ψ, u− , ∅)
(ϕ ≡ ψ, w+ , A) (ϕ ≡ ψ, w− , A)
(≡+ ) −
(≡− )
+
(ϕ, v , ∅) (ϕ, v , ∅) (ϕ, v , {u }) (ϕ, v + , ∅) (ϕ, v − , ∅) (ϕ, v − , {u− })
+ +
−
+
(ψ, v , ∅) (ψ, v , ∅) (ψ, u+ , {v + }) (ψ, u− , ∅) (ψ, u+ , ∅) (ψ, u− , {v − })
(ϕ, w∗ , A), (ψ, w∗ , B), (¬ϕ, v ∗ , C), (¬ψ, u∗ , E)
(≡¬ )
(¬ψ, v ∗ , C ∪ E)
(ϕ, w∗ , A), (ψ, w∗ , B), (χ, v ∗ , C), (θ, v ∗ , E), (ϕ → χ, u∗ , F ), (ψ → θ, y ∗ , G)
(≡→ )
(ψ → θ, u∗ , F ∪ G)
(ϕ, w∗ , A), (ψ, w∗ , B), (χ, v ∗ , C), (θ, v ∗ , E), (ϕ ≡ χ, u∗ , F ), (ψ ≡ θ, y ∗ , G)
(≡≡ )
(ψ ≡ θ, u∗ , F ∪ G)
(ϕ, w∗ , A), (ϕ, v ∗ , B), (ψ, v ∗ , C) (ϕ, w∗ , A ∪ {w∗ }) (ϕ, w+ , A), (ϕ, v − , B)
(F) (⊥1 ) (⊥2 )
(ψ, w∗ , A ∪ B ∪ C) ⊥ ⊥
Figure 1: Tableau calculus TCSCI .
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)
Tableau-based Decision Procedure for the Logic SCI 27
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
the rules (R) ∈ {(¬+ ), (¬− ), (→+ ), (→− ), (≡+ ), (≡− )} were not applied to those formulas which were
proto-reduced for these rules.
The termination of TCSCI + PE can be proved combinatorially by showing that there are at most |ϕ| ·
6
2|ϕ|·22|ϕ| distinct labelled formulas on B and, thus, a branch can contain at most 10· |ϕ| · 2|ϕ| · 22|ϕ| +1
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
28 J. Golińska-Pilarek and M. Zawidzki
tableau-based dedcision procedure for SCI naturally complements the logic itself, for it not only enables to
verify formulas’ validity, but also straightforwardly generates simple models of satisfiable formulas given
as an input.
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.