Lindenbaum method

Lindenbaum method (propositional language)

Lindenbaum method is named after the Polish logician Adolf Lindenbaum who prematurely and without a clear trace disappeared in the turmoil of the Second World War at the age of about 37. (Cf.[15].) The method is based on the symbolic nature of formalized languages of deductive systems and opens a gate for applications of algebra to logic and, thereby, to Abstract algebraic logic.

Lindenbaum's theorem

A formal propositional language, say $\mathcal{L}$, is understood as a nonempty set $\mathcal{V}$ of symbols $p_0, p_1,... p_{\gamma}...$ called propositional variables and a finite set $\Pi$ of symbols $F_0, F_1,..., F_n$ called logical connectives. By $\overline{\overline{Vr_\mathcal{V}}}$ we denote the cardinality of $Vr_\mathcal{V}$. For each connective $F_i$, there is a natural number $\#(F_i)$ called the arity of the connective $F_i$. The notion of a statement (or a formula) is defined as follows:

$(f_1)$	Each variable $p\in\mathcal{V}$ is a formula;
$(f_2)$	If $F_i$ is a connective of the arity 0, then $F_i$ is a formula;
$(f_3)$	If $A_1, A_2,..., A_n$, $n\geq 1$, are formulas, and $F_n$ is a connective of arity $n$, then the symbolic expression $F_{n}A_{1}A_{2}... A_n$ is a formula;
$(f_4)$	A formula can be constructed only according to the rules $(f_1)-(f_3)$.

The set of formulas will be denoted by $Fr_\mathcal{L}$ and $P(Fr_\mathcal{L})$ denotes the power set of $Fr_\mathcal{L}$. Given a set $X \subseteq Fr_\mathcal{L}$, we denote by $Vr(X)$ the set of propositional variables that occur in the formulas of $X$. Two formulas are counted equal if they are represented by two copies of the same string of symbols. (This is the key observation on which Theorem 1 is grounded.) Another key observation (due to Lindenbaum) is that $Fr_\mathcal{L}$ along with the connectives $\Pi$ can be regarded as an algebra of the similarity type associated with $\mathcal{L}$, which exemplifies an $\mathcal{L}$-algebra. We denote this algebra by $\mathfrak{F}_\mathcal{L}$. The importance of $\mathfrak{F}_\mathcal{L}$ can already be seen from the following observation.

Theorem 1. Algebra $\mathfrak{F}_\mathcal{L}$ is a free algebra of rank $\overline{\overline{\mathcal{V}}}$ with free generators $\mathcal{V}$ in the class $($variety$)$ of all $\mathcal{L}$-algebras. In other words, $\mathfrak{F}_\mathcal{L}$ is an absolutely free algebra of this class.

A useful feature of the set $Fr_\mathcal{L}$ is that it is closed under (simultaneous) substitution. More than that, any substitution $\sigma$ is an endomorphism

$\sigma: \mathfrak{F}_\mathcal{L}\longrightarrow \mathfrak{F}_\mathcal{L}$.

A monotone deductive system (or a deductive system or simply a system) is a relation between subsets and elements of $Fr_\mathcal{L}$. Each such system $\vdash_S$ is subject to the following conditions: For all $X,Y \subseteq \mathfrak{Fr}_\mathcal{L}$,

$(s_1)$	if $A \in X$, then $X \ \vdash_\mathcal{S} \ A$;
$(s_2)$	if $X \ \vdash_\mathcal{S} \ B$ for all $B \in Y$, and $Y \ \vdash_\mathcal{S} \ A$, then $X \ \vdash_\mathcal{S} \ A$;
$(s_3)$	if $X \ \vdash_\mathcal{S} \ A$, then for every substitution $\sigma$, $\sigma[X] \ \vdash_\mathcal{S} \ \sigma(A)$.

If $A$ is a formula and $\sigma$ is a substitution, $\sigma(A)$ is called a substitution instance of $A$. Thus, by $\sigma[X]$ above, one means the instances of the formulas of $X$ with respect to $\sigma$.

Given two sets $Y$ and $X$, we write

$\quad \quad \quad Y \sqsubseteq X $

if $Y$ is a finite (may be empty) subset of $X$.

A deductive system is said to be finitary if, in addition, it satisfies the following:

$(s_4)$

if $X \ \vdash_\mathcal{S} \ A$, then there is $Y \sqsubseteq X$ such that $Y \ \vdash_\mathcal{S} \ A$.

We note that the monotonicity property

$\quad \quad \quad \quad$ if $X \subseteq Y$ and $X \ \vdash_\mathcal{S} \ A$, then $Y \ \vdash_\mathcal{S} \ A$

is not postulated, because it follows from $(s_1)$ and $(s_2)$.

Each deductive system $\vdash_\mathcal{S}$ induces the (monotone structural) consequence operator $Cn_{\mathcal{S}}$ defined on the power set of $Fr_\mathcal{L}$ as follows: For every $X \subseteq Fr_\mathcal{L}$,

$\quad \quad \quad \quad A \in Cn_\mathcal{S}(X) \Longleftrightarrow X \ \vdash_\mathcal{S} \ A, \quad \quad \quad \quad \quad \quad \quad \quad (1)$

so that the following conditions are fulfilled: For all $X,Y \subseteq Fr_\mathcal{L}$ and any substitution $\sigma$,

$(c_1)$	$X \subseteq Cn_\mathcal{S}(X);$	(Reflexivity)
$(c_2)$	$Cn_\mathcal{S}(Cn_\mathcal{S}(X)) = Cn_\mathcal{S}(X);$	(Idenpotency)
$(c_3)$	if $X \subseteq Y$, then $Cn_\mathcal{S}(X) \subseteq Cn_\mathcal{S}(Y);$	(Monotonicity)
$(c_4)$	$\sigma[Cn_\mathcal{S}(X)] \subseteq Cn_\mathcal{S}(\sigma[X]).$	(Structurality)

If $\vdash_\mathcal{S}$ is finitary, then

$(c_5)$

$Cn_\mathcal{S}(X) = \bigcup\lbrace Cn_\mathcal{S}(Y) \ | \ Y \Subset X \rbrace$

in which case $Cn_{\mathcal{S}}$ is called finitary.

Conversely, if an operator $Cn:\cal{P}(Fr_\mathcal{L})\rightarrow \cal{P}(Fr_\mathcal{L})$ satisfies the conditions $(c_1)-(c_4)$ (with $Cn$ instead of $Cn_\mathcal{S}$), then the equivalence

$\quad \quad \quad \quad X \ \vdash_\mathcal{S} \ A \Longleftrightarrow A \in {Cn}(X)$

defines a deductive system, $\mathcal{S}$. Thus (1) allows one to use the deductive system and consequence operator (in a fixed formal language) interchangeably or even in one and the same context. For instance, we call $T_\mathcal{S} = Cn_\mathcal{L}(\emptyset)$ the set of theorems of the system $\vdash_\mathcal{S}$ (i.e. $\mathcal{S}$-theorems), and given a subset $X \subseteq Fr_\mathcal{S}$, $Cn-|mathcal{S}{X}$ is called the $\mathcal{S}$-theory generated by $X$. A subset $X \subseteq Fr_\mathcal{S}$, as well as the theory $Cn_\mathcal{S}(X)$, is called inconsistent if $Cn_\mathcal{S}(X) = Fr_\mathcal{S}$; otherwise both are consistent. Thus, given a system $\vdash_\mathcal{S}$, $T_\mathcal{S}$ is one of the system's theories; that is to say, if $X \subseteq T_\mathcal{S}$ and $X \vdash_\mathcal{S} A$, then $A \in T_\mathcal{S}$. This simple observation sheds light on the central idea of Lindenbaum method, which will be explained soon. For now, let us fix the ordered pair $\left<\mathcal{F}_\mathcal{L},T\mathcal{L}\right>$ and call it a Lindenbaum matrix. (The full definition will be given later.) We note that an operator $Cn$ satisfying $(c_1)-(c_3)$ can be obtained from a "closure system" over $Fr_\mathcal{L}$; that is for any subset $\cal{A}\subseteq P(Fr_\mathcal{L})$, which is closed under arbitrary intersection, we define:

$\quad \quad \quad \quad Cn_\mathcal{A}(X)=\cap \lbrace Y \ | \ X \subseteq Y \mbox{ and } Y \in \cal{A} \rbrace.$

Another way of defining deductive systems is through the use of logical matrices. Given a language $\mathcal{L}$, a logical $\mathcal{L}$-matrix (or simply a matrix) is a pair $\mathcal{M} = \left<\mathfrak{A},\mathcal{F}\right>$, where $\mathfrak{A}$ is an $\mathcal{L}$-algebra and $\mathcal{F}\subseteq|\mathfrak{A}|$, where the latter is the universe of $\mathfrak{A}$. The set $\mathcal{F}$ is called the filter of the matrix and its elements are called designated. Given a matrix $\mathcal{M} = \left<\mathfrak{A},\mathcal{F}\right>$, the cardinality of $|\mathfrak{A}|$ is also the cardinality of $\mathcal{M}$.

Given a matrix $\mathcal{M}=\left<\mathfrak{A},\mathcal{F}\right>$, any homomorphism of $\mathfrak{A}$ into $\mathfrak{A}$ is called a valuation (or an assignment). Each such homomorphism can be obtained simply by assigning elements of $|\mathfrak{A}|$ to the variables of $Vr_\mathcal{L}$, since, by virtue of Theorem 1, any $v: Vr_\mathcal{L} \longrightarrow |\mathfrak{A}|$ can be extended uniquely to a homomorphism $\hat{v}: \mathfrak{A} \longrightarrow \mathfrak{A}$. Usually, $v$ is meant under a valuation (or an assignment) of variables in a matrix.

Now let $\sigma$ be a substitution and $v$ be any assignment in an algebra {\mathfrak{A}}. Then, defining

$\quad \quad \quad \quad v_{\sigma}=v\circ\sigma, \quad \quad \quad \quad \quad \quad \quad \quad (2)$

we observe that $v_{\sigma}$ is also an assignment in $\mathfrak{A}$.

With each matrix $\mathcal{M}=\left<\mathfrak{A},\mathcal{F}\right>$, we associate a relation $\models_\mathcal{M}$ between subsets of $Fr_\mathcal{L}$ and formulas of $Fr_\mathcal{L}$. Namely we define

$ \quad \quad \quad \quad X \ \models_\mathcal{M} \ A \Longleftrightarrow \text{ for every assignment } v, \text{ if } v[X]\subseteq \mathcal{F}, \text{ then } v(A)\in \mathcal{F}$.

Then, we observe that the following properties hold:

$(m_1)$	if $A \in X$, then $X \ \models_\mathcal{M} \ A$
$(m_2)$	if $X\models_\mathcal{M} B$ for all $B\in Y$, and $Y \ \models_\mathcal{M} \ A$, then $X \ \models_\mathcal{M} \ A.$

Also, with help of the definition (2), we derive the following:

$(m_3)$

if $X \ \models_\mathcal{M} \ A$, then for every substitution $\sigma$, $\sigma[X] \ \models_\mathcal{M} \ \sigma(A)$.

Comparing the condition $(m_1)-(m_3)$ with $(s_1)-(s_3)$, we conclude that every matrix defines a structural deductive system and hence, in view of (1), a structural consequence operator.

Given a system $\mathcal{S}$, suppose a matrix $\mathcal{M}=\left<\mathfrak{A},\mathcal{F}\right>$ satisfies the condition

$\quad \quad \quad \quad $ if $X \ \vdash_\mathcal{S} A$ and $v[X] \subseteq \mathcal{F}$, then $v(A) \in \mathcal{F} \quad \quad \quad \quad (3)$

Then the filter $\mathcal{F}$ is called an $\mathcal{S}$-filter and the matrix $\mathcal{M}$ is called an $\mathcal{S}$-matrix (or an $\mathcal{S}$-model). In view of (3), $\mathcal{S}$-matrices are an important tool in showing that $X \ \vdash_\mathcal{S} \ A$ does not hold. This idea has been employed in proving that one axiom is independent from a group of others in the search for an independent axiomatic system, as well as for semantic completeness results.

As Lindenbaum's famous theorem below explains, every structural system $\mathcal{S}$ has an $\mathcal{S}$-model.

Theorem 2. For any structural deductive system $\mathcal{S}$, the matrix $\left<Fr_\mathcal{L},Cn_\mathcal{S}(\emptyset)\right>$ is an $\mathcal{S}$-model. Moreover, for any formula $A$,

$\quad \quad \quad \quad A \in T_\mathcal{S} \Longleftrightarrow v(A)\in Cn_\mathcal{S}(\emptyset)$ for any valuation $v$.

A matrix $\left<\mathfrak{A},\mathcal{F}\right>$ is said to be weakly adequate for a deductive system $\mathcal{S}$ if for any formula $A$,

$\quad \quad \quad \quad A \in T_\mathcal{S} \Longleftrightarrow v(A)\in \mathcal{F}$ for any valuation $v$.

Thus, according to Theorem 2, every structural system $\mathcal{S}$ has a weakly adequate $\mathcal{S}$-matrix of cardinality less than or equal to $\overline{\overline{\mathcal{V}}}+\aleph_0$.

An $\mathcal{S}$-matrix is called strongly adequate for $\mathcal{S}$ if for any set $X \subseteq Fr_\mathcal{L}$ and any formula $A$,

$ \quad \quad \quad \quad X \ \vdash_\mathcal{S} \ A \Longleftrightarrow X \ \models_\mathcal{M} \ A. \quad \quad \quad \quad (4)$

We note that, if $\overline{\overline{\mathcal{V}}} \leq \aleph_{0}$, Theorem 2 cannot be improved to include strong adequacy of an denumerable matrix, for if $\mathcal{S} = IPC$ (intuitionistic propositional calculus), there is no denumerable matrix $\mathcal{M}$ with (4). (Cf.[21].)

Historical remarks

A. Tarski seems to be the first who promoted "the view of matrix formation as a general method of constructing systems" [9]. However, matrices had been employed earlier, e.g., by P. Bernays [q] and others either in the search for an independent axiomatic system or for defining a system different from classical logic. Also, later on J.C.C. McKinsey [10] used matrices to prove independence of logical connectives in intuitionistic propositional logic.

Theorem 2 was discovered by A. Lindenbaum. Although this theorem was not published by the author, it had been known in Warsaw-Lvov logic circles at the time. In a published form it appeared for the first time in [9] without proof. Its proof appeared later on in the two independent publications of [8] and [6].

References

[1] Paul Bernays, Untersuchung des Aussagenkalküls der “Principia Mathematica”, Math. Z. 25 (1926), 305–320.

[2] W. J. Blok and Don Pigozzi, Algebraizable logics, Mem. Amer. Math. Soc. 77 (1989), no. 396, vi+78. MR 973361 (90d:03140)

[3] Stanley Burris and H. P. Sankappanavar, A course in universal algebra, Graduate Texts in Mathematics, vol. 78, Springer-Verlag, New York, 1981. MR 648287 (83k:08001)

[4] J. Michael Dunn and Gary M. Hardegree, Algebraic methods in philosophical logic, Oxford Logic Guides, vol. 41, The Clarendon Press Oxford University

Press, New York, 2001, Oxford Science Publications. MR 1858927 (2002j:03001)

[5] J. M. Font, R. Jansana, and D. Pigozzi, A survey of abstract algebraic logic, Studia Logica 74 (2003), no. 1-2, 13–97, Abstract algebraic logic, Part II (Barcelona, 1997). MR 1996593 (2004m:03241)

[6] Hans Hermes, Zur Theorie der aussagenlogischen Matrizen, Math. Z. 53 (1951), 414–418. MR 0040241 (12,663c)

[7] J. Łós and R. Suszko, Remarks on sentential logics, Nederl. Akad.Wetensch. Proc. Ser. A 61 = Indag. Math. 20 (1958), 177–183. MR 0098670 (20 #5125)

[8] Jerzy Łós, On logical matrices, Trav. Soc. Sci. Lett. Wrocław. Ser. B. (1949), no. 19, 42. MR 0089812 (19,724b)

[9] Jan Łukasiewicz and Alfred Tarski, Untersuchungen über den Aussagenkalkül, Comptes rendus des séances de la Société des Sciences et des Lettres de Varsovie, CI III 23 (1930), 30–50.

[10] J. C. C. McKinsey, Proof of the independence of the primitive symbols of Heyting’s calculus of propositions, J. Symbolic Logic 4 (1939), 155–158. MR 0000805 (1,131f)

[11] Iwao Nishimura, On formulas of one variable in intuitionistic propositional calculus., J. Symbolic Logic 25 (1960), 327–331 (1962). MR 0142456 (26 #25)

[12] Helena Rasiowa, An algebraic approach to non-classical logics, North-Holland Publishing Co., Amsterdam, 1974, Studies in Logic and the Foundations of Mathematics, Vol. 78. MR 0446968 (56 #5285)

[13] Helena Rasiowa and Roman Sikorski, The mathematics of metamathematics, third ed., PWN—Polish Scientific Publishers, Warsaw, 1970, Monografie Matematyczne, Tom 41. MR 0344067 (49 #8807)

[14] Timothy Smiley, The independence of connectives, J. Symbolic Logic 27 (1962), 426–436. MR 0172784 (30 #3003)

[15] Stanisław J. Surma, On the origin and subsequent applications of the concept of the Lindenbaum algebra, Logic, methodology and philosophy of science, VI (Hannover, 1979), Stud. Logic Foundations Math., vol. 104, North-Holland, Amsterdam, 1982, pp. 719–734. MR 682440 (84g:01045)

[16] Alfred Tarski, Grundzüge der systemenkalkül. Erter teil, Fundamenta Mathematica 25 (1935), 503–526.

[17] Alfred Tarski, Grundzüge der systemenkalkül. Zweiter teil, Fundamenta Mathematica 26 (1936), 283–301.

[18] Alfred Tarski, A remark on functionally free algebras, Ann. of Math. (2) 47 (1946), 163–165. MR 0015038 (7,360a)

[19] Alfred Tarski, Logic, Semantics, Metamathematics. Papers from 1923 to 1938, Oxford at the Clarendon Press, 1956, Translated by J. H. Woodger. MR 007829 (17,1171a)

[20] Ryszard Wójcicki, Theory of logical calculi, Synthese Library, vol. 199, Kluwer Academic Publishers Group, Dordrecht, 1988, Basic theory of consequence operations. MR 1009788 (90j:03001)

[21] Andrzej Wrónski, On cardinalities of matrices strongly adequate for the intuitionistic propositional logic, Rep. Math. Logic (1974), no. 3, 67–72. MR 0387011 (52 #7858)