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.~\cite{sur82}.) 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~\ref{P:absolutely-free} 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)