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_i$ 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$.