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}$,

$ A \in Cn_\mathcal{S} {X} \Longleftrightarrow X \ \vdash_\mathcal{S} \ A,$

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