View source for Lindenbaum method

{{TEX|done}}




= 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 [[Algebraic logic#Abstract algebraic logic|''Abstract algebraic logic'']].



== Lindenbaum's theorem ==

A formal propositional language, say $\mathcal{L}$, is understood as a nonempty set ${\cal V}_\mathcal{L}$ 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{{\cal V}_\mathcal{L}}}$ we denote the cardinality of ${\cal V}_\mathcal{L}$. 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 {\cal V}_\mathcal{L}$ 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 ${\cal V}(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{{\cal V}_\mathcal{L}}}$ with free generators ${\cal V}_\mathcal{L}$ 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 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 \Subset X $

if $Y$ is a finite (maybe 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 \Subset 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'' or ''substitution invariance'')

|}

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.

<br />

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 '''(Lindenbaum). 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" [10]. However, matrices had been employed earlier, e.g., by P. Bernays [1] 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 [11] 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 [10] without proof. Its proof appeared later on in the two independent publications of [9] and [7].

== Wójcicki's theorems ==

We get more $\mathcal{S}$-matrices, noticing the following. Let $\Sigma_\mathcal{S}$ be an $\mathcal{S}$-theory. The pair  $\left<Fr_\mathcal{L},\Sigma_\mathcal{S} \right>$ is called a ''Lindenbaum matrix'' relative to $\mathcal{S}$. We observe that  for any substitution $\sigma$,

$\quad \quad \quad \quad $ if  $X \ \vdash_\mathcal{S} \ A$  and $\sigma[X] \subseteq \Sigma_\mathcal{S}$, then $\sigma(A) \in \Sigma_\mathcal{S}$}.

That is to say,  any Lindenbaum matrix relative to a system $\mathcal{S}$ is an $\mathcal{S}$-model.

<br>

A deductive system $\mathcal{S}$ is said to be ''uniform'' if, given a set $X \subseteq Fr_\mathcal{S}$ and a consistent set $ Y \subseteq Fr_\mathcal{S}$, $X \cup Y \ \vdash_\mathcal{S} \ A$ and $Vr(Y) \cap Vr(A) = \emptyset$ imply $X \ \vdash_\mathcal{S} \ A$. A system $\mathcal{S}$ is ''couniform'' if for any collection $\{X_{i}\}_{i\in I}$ of formulas with $Vr(X_i) \cap Vr(X_j) = \emptyset$, providing $i \neq j$, if the set $\cup\{X_{i}\}_{i\in I}$ is inconsistent, then at least one $X_{i}$ is inconsistent as well.


'''Theorem 3''' (Wójcicki).
''A structural deductive system $\mathcal{S}$ has a strongly adequate matrix if and only if $\mathcal{S}$ is both uniform and couniform.''


For the "if" implication of the statement, the matrix of Theorem 2 is not enough. However, it is possible to extend the original language $\mathcal{L}$ to $\mathcal{L}^{+}$ in such a way that the ''natural extension'' $Cn_{\mathcal{S}^{+}}$ of $Cn_{\mathcal{S}}$ onto $\mathcal{L}^{+}$ allows one to define a Lindenbaum matrix $\left<\mathfrak{F}_{\mathcal{L}^{+}},Cn_{\mathcal{S}^{+}}(X)\right>$, for some $X \subseteq Fr_{\mathcal{L}^{+}}$, which is  strongly adequate for $\mathcal{S}$. (Cf.[21] for detail.)

<br>

A pair $\left<\mathfrak{A},\ \{\mathcal{F}_{i}\}_{i\in I}\right>$,  where $\mathfrak{A}$ is an $\mathcal{L}$-algebra and each $\mathcal{F}_{i}\subseteq|\mathfrak{A}|$, is called a ''generalized matrix'' (or a $g$-''matrix'' for short). A $g$-matrix is a $g$-$\mathcal{S}$-''model'' (or a $g$-$\mathcal{S}$-''matrix'') if each $\left<\mathfrak{A},\mathcal{F}_{i}\right>$ is an $\mathcal{S}$-model. (In [4] a $g$-matrix is called an ''atlas''.)


'''Theorem 4''' (Wójcicki).
''For every structural deductive system $\mathcal{S}$, there is a $g$-$\mathcal{S}$-matrix $\mathcal{M}$ of cardinality $\overline{\overline{\mathcal{V}}}+\aleph_{0}$, which is strongly adequate for'' $\mathcal{S}$.


Indeed, let $\{\Sigma_\mathcal{S}\}$ be the collection of all $\mathcal{S}$-theories. Then the $g$-matrix $\left<Fr_\mathcal{L},\{\Sigma_\mathcal{S}\}\right>$ is strongly adequate for $\mathcal{S}$. (Cf.[21],[4] for detail.)

We note that, alternatively, one could use the notion of a ''bundle of matrices''; a bundle is a set $\{\left<\mathfrak{A},\mathcal{F}_{i}\right> | i\in I \}$, where $\mathfrak{A}$ is an $\mathcal{L}$-algebra and each $\mathcal{F}_{i}$ is a filter of $\mathfrak{A}$.



=== Historical remarks === 
Theorem 3 was the result of the correction by R. Wójcicki of an erroneous assertion in [8], where the important question on the strong adequacy of a system was raised.

T. Smiley [15] was perhaps the first to propose $g$-matrices (known as ''Smiley matrices'') defined as pairs $\left<\mathfrak{A},Cn \right>$, where $\mathfrak{A}$ is an $\mathcal{L}$-algebra and an operator $Cn: \mathcal{P}(|\mathfrak{A}|) \rightarrow \mathcal{P}(|\mathfrak{A}|)$ satisfies the conditions $(c_1)-(c_3)$ (with $Cn$ instead of $Cn_\mathcal{S}$). Then, Smiley defined $x_1,..., x_n \ \vdash \ y$ if and only of $y \in  Cn(\{x_1,...,x_n\})$, where it is assumed that $|\mathfrak{A}| \subseteq U$, where $U$ is a universal set of sentences.

== Lindenbaum-Tarski algebra ==


The question of the possibility to decide, whether $X \ \vdash_\mathcal{S} \ A$ is true or not is central in theory of deduction. Although the notion we are about to introduce is less general than that of $\mathcal{S}$-matrix, it points out at a way, following which this question can be often fruitfully discussed.

An $\mathcal{S}$-matrix $\left<\mathfrak{A},\mathcal{F}\right>$ is said to be ''univalent'' (or $\mathcal{S}_u$-''matrix'') if the $\mathcal{S}$-filter $\mathcal{F}$ consists of one value, say $\mathcal{F} = \{ \mathbf{1} \}$, where $\mathbf{1} \in |\mathfrak{A}|$. Let us restrict our original question to the following: How can the property $\emptyset \ \vdash_\mathcal{S} \ A$ be characterized in matrix terms?

Let $\left<\mathfrak{A},\{\mathbf{1}\}\right>$ be an $\mathcal{S}_u$-matrix and $A$ be an $\mathcal{S}$-theorem. Then, in view of (3), $v(A)=\mathbf{1}$ for every valuation $v$ in $\mathfrak{A}$. It would be interesting to know when the converse is true too. Thus the main problem is: How can one obtain an $\mathcal{S}_u$-matrix?


'''Definition 1''' (Lindenbaum-Tarski algebra).
''Let $\Sigma_\mathcal{S}$ be an $\mathcal{S}$-theory and let $\Theta(\Sigma_\mathcal{S})$ be the congruence on $\mathfrak{F}_{\mathcal{L}}$ generated by $\Sigma_\mathcal{S}$;'' (cf. [3]). ''The quotient algebra $\mathfrak{F}_\mathcal{L}/\Theta(\Sigma_\mathcal{S})$ is called a Lindenbaum-Tarski algebra of $\mathcal{S}$ relative to $\Sigma_\mathcal{S}$. If $\Sigma_\mathcal{S} = T_\mathcal{S}$, then we call this quotient simply a Lindenbaum-Tarski algebra.''


An important conclusion from this definition is the following.


'''Theorem 5. '''
''Let $\mathcal{S}$ be a structural deductive system and $\Sigma_\mathcal{S}$ be a nonempty $\mathcal{S}$-theory. Assume that $\Sigma_\mathcal{S}$ is a congruence class with respect to $\Theta(\Sigma_\mathcal{S})$. Then $\left<\mathfrak{F}_\mathcal{L}/\Theta(\Sigma_\mathcal{S}),\{\Sigma_\mathcal{S}\}\right>$ is an $\mathcal{S}_u$-matrix; that is to say, denoting $\mathbf{1}=\Sigma_\mathcal{S}$, if $X \ \vdash_\mathcal{S} \ A$ and $v$ is a valuation in $\mathfrak{F}_\mathcal{L}/\Theta(\Sigma_\mathcal{S})$, then''

$ \quad \quad \quad \quad v[X]=\{\mathbf{1}\} \Longrightarrow v(A)=\mathbf{1}. \quad \quad \quad \quad (5)$

''Moreover, if $\Sigma_\mathcal{S} = T_\mathcal{S}$, then''

$\quad \quad \quad \quad A \in T_\mathcal{S} \Longleftrightarrow v(A)=\mathbf{1}$ ''for any valuation'' $v$ in $\mathfrak{F}_\mathcal{L}/\Theta(T_\mathcal{S}) \quad \quad \quad \quad (6)$

''Let the valuation'' $v_{0}(p)=p/\Theta(T_\mathcal{S})$ ''for every'' $p \in Vr_\mathcal{L}$. ''Then''

$\quad \quad \quad \quad A\in T_\mathcal{S} \Longleftrightarrow v_{0}(A)=\mathbf{1}. \quad \quad \quad \quad (7)$


''' Definition 2.'''
''Let $\mathcal{S}$ be a structural deductive system. We say that $\mathcal{S}$ admits the Lindenbaum-Tarski algebra'' (''relative to'' $\Sigma_\mathcal{S}$) ''if'' $T_\mathcal{S}$ ( $\Sigma_\mathcal{S}$ ''respectively'') ''is a congruence class with respect to $\Theta(T_\mathcal{S})$ (with respect to $\Theta(\Sigma_\mathcal{S})$) on $\mathfrak{F}_{\mathcal{L}}$.''

Now let us convert the propositional language $\mathcal{L}$ into a first order language $\mathcal{L}'$ so that the propositional variables  and the logical connectives of $\mathcal{L}$ become the individual variables and functional constants of $\mathcal{L}'$, respectively. The set of individual variables is denoted now by $Vr_{\mathcal{L}'}$.  Also, $\mathcal{L}'$ has an individual constant $\mathbf{1}$,  the equality symbol '$=$' and universal and existential quantifiers. (Actually, we will need only the former.) We can assume that there is no logical connectives in $\mathcal{L}'$. Since the formulas of $\mathcal{L}$ now become terms of $\mathcal{L}'$, each ''atomic formula'' of $\mathcal{L}'$ is an expression of the form:

$ \quad \quad \quad \quad A(p,\mathbf{1},...)=B(q,\mathbf{1},...)$,

where variables $p$ and $q$ are not necessarily distinct and they, as well as the constant $\mathbf{1}$, may or may not occur in the equality.

A universal closure (in the sense of first order logic) of an atomic formula of $\mathcal{L}'$ is often referred to as an ''identity''. We will deal with interpretations of identities only. Therefore, we semantically treat atomic formulas and their universal closures equally. An unspecified identity will be denoted by $\varphi$.

$\quad$ The $\mathcal{L}'$-formulas are interpreted in algebras $\mathfrak{B}$ of the type $\mathcal{L}$ endowed with a 0-ary operation $\mathbf{1}$. Then, for instance, an identity

$ \quad \quad \quad \quad A(p,\mathbf{1},...)=\mathbf{1}$

is said to be ''valid'' (or to ''hold'') in $\mathfrak{B}$, in symbols $\mathfrak{B} \ \models \ A(p,\mathbf{1},...)=\mathbf{1}$, if for any assignment $v: \mathcal{L}' \rightarrow |\mathfrak{B}|$

$ \quad \quad \quad \quad A(v(p),\mathbf{1},...)=\mathbf{1}.$

Given a system $\mathcal{S}$, we denote

$\quad \quad \quad \quad \mathfrak{F}_\mathcal{S} = \left<\mathfrak{F}_\mathcal{L}/\Theta(T_\mathcal{S}), \mathbf{1}\right>,$

where $\mathbf{1}$ is the congruence class generated by $T_\mathcal{S}$. Thus $\mathfrak{F}_\mathcal{S}$ is the expansion of $\mathfrak{F}_\mathcal{L}/\Theta(T_\mathcal{S})$ obtained by adding the constant $\mathbf{1}$ to the signature of the latter.

Then, we define:

$\quad \quad \quad \quad \Phi_{\mathcal{S}}= \{ A = \mathbf{1} | A \in T_\mathcal{S}\}$

and

$ \quad \quad \quad \quad K_{\mathcal{S}} = \{\mathfrak{B}| \mathfrak{B} \ \models \ \varphi$ for all $\varphi \in \Phi_{\mathcal{S}}\}$.

It is obvious that the class $K_{\mathcal{S}}$ is a variety.

'''Theorem 6.'''
''Let a structural deductive system $\mathcal{S}$ admit the Lindenbaum-Tarski algebra. Then the algebra $\mathfrak{F}_\mathcal{S}$ belongs in the variety $K_\mathcal{S}$. More than that,''

$ \quad \quad \quad \quad \mathfrak{F}_\mathcal{S} \ \models \ A = \mathbf{1}\Longleftrightarrow A \in T_\mathcal{S}.$

''Moreover, $\mathfrak{F}_\mathcal{S} \ \models \ A(p,\mathbf{1},...)=\mathbf{1}$ if and only if $A(p/\Theta(T_\mathcal{S}),\mathbf{1},...)=\mathbf{1}$ in $\mathfrak{F}_\mathcal{S}$, that is''
$A(p/\Theta(T_\mathcal{S}),T_\mathcal{S},...) = T_\mathcal{S}$ in $\mathfrak{F}_\mathcal{L}/\Theta(T_\mathcal{S})$.

$\quad $ Theorem 6 gives rise to the following questions: When is $\mathfrak{F}_\mathcal{S}$ functionally free [19] in $K_{\mathcal{S}}$? When is $\mathfrak{F}_\mathcal{S}$ a free algebra in $K_{\mathcal{S}}$?

=== Historical remarks === 

In two  parts, [17] and [18], of one paper, the English translation of which constitutes one chapter, ''Foundations of the Calculus of Systems'', of [19], A. Tarski showed that the Lindenbaum-Taski algebra of the system based on classical propositional calculus is a Boolean algebra.

== Alternative approach ==

Let $\left<\mathfrak{A},\mathcal{F}\right>$ be a matrix. A congruence (or an equivalence) $\theta$ on $\mathfrak{A}$ is said to be ''compatible'' with $\mathcal{F}$ if $\cup\{ x /\theta ~|~x \in \mathcal{F}\} = \mathcal{F}$. Since the identity relation is compatible with any $\mathcal{F}$, the set of compatible congruences (or equivalences) is not empty for any matrix. Then, it can be proven [2] that for any matrix $\mathcal{M} = \left<\mathfrak{A},\mathcal{F}\right>$, there is a largest congruence of $\mathfrak{A}$ compatible with $\mathcal{F}$. This congruence is called the ''Leibniz congruence'' of $\mathcal{M}$; it is denoted by $\Omega_{\mathfrak{A}}\mathcal{F}$ and can be defined as follows:

$ \quad \quad \quad \quad \Omega_\mathfrak{A}\mathcal{F} = \{(a,b)|\forall
A(p,p_0,...,p_n) \forall c_0,..., c_n \in |\mathfrak{A}|.~A(a,c_{0},...,c_n) \in \mathcal{F} \Leftrightarrow A(b,c_0,...,c_n) \in \mathcal{F} \}.$

If the matrix in question is a Lindenbaum one, say $\left<\mathfrak{F}_\mathcal{L},\Sigma_\mathcal{S}\right>$, then an example of a compatible equivalence on this matrix is a ''Frege relation'' $\Lambda \Sigma_\mathcal{S}$ defined as follows:

$ \quad \quad \quad \quad (A,B)\in\Lambda\Sigma_\mathcal{S} \Longleftrightarrow \Sigma_\mathcal{S}, A \ \vdash_\mathcal{S} \ B$ and $\Sigma_\mathcal{S}, B \ \vdash_\mathcal{S} \ A $. (''Frege relation relative to'' $\Sigma_\mathcal{S}$})

A system $\mathcal{S}$ is called ''Fregean'' if each $\Lambda\Sigma_\mathcal{S}$ is a congruence on $\mathfrak{F}_{\mathcal{L}}$. Obviously, if $\mathcal{S}$ is Fregean, it admits the Lindenbaum-Tarski algebra relative to any $\Sigma_\mathcal{S}$.

Another example of a compatible relation on $\left<\mathfrak{F}_\mathcal{L},\Sigma_\mathcal{S}\right>$ is the largest congruence of $\mathfrak{F}_{\mathcal{L}}$ contained in $\Lambda\Sigma_\mathcal{S}$, which is referred to as a ''Suszko congruence'':

$ \quad \quad \quad \quad (A,B)\in \widetilde{\Omega}\Sigma_\mathcal{S}\Longleftrightarrow$ for every $C(p)$, $\Sigma_\mathcal{S}, C(A/p)\ \vdash_\mathcal{S} \ C(B/p)$ and $\Sigma_\mathcal{S},C(B/p)\ \vdash_\mathcal{S} \ C(A/p)$. (''Suszko congruence relative to'' $\Sigma_\mathcal{S}$)

Obviously, a system $\mathcal{S}$ is Fregean if and only if $\Lambda\Sigma_\mathcal{S}=\widetilde{\Omega}\Sigma_\mathcal{S}$ for all $\Sigma_\mathcal{S}$.

The Leibniz congruence of a matrix $\left<\mathfrak{F}_\mathcal{L},\Sigma_\mathcal{S}\right>$ is referred to as ''Leinbniz congruence relative to'' $\Sigma_\mathcal{S}$. It  turns out that

$\quad \quad \quad \quad \Omega\Sigma_\mathcal{S} = \cap\{\widetilde{\Omega}\Sigma^\prime_\mathcal{S} | \Sigma_\mathcal{S} \subseteq \Sigma^\prime_\mathcal{S}\}$

and, therefore, each Suszko congruence $\widetilde{\Omega}\Sigma_\mathcal{S}$ is compatible with $\Sigma_\mathcal{S}$.

Thus we have:

$\quad \quad \quad \quad \widetilde{\Omega}\Sigma_\mathcal{S}\subseteq\Lambda\Sigma_\mathcal{S}$ and  $\widetilde{\Omega}\Sigma_\mathcal{S}\subseteq\Omega\Sigma_\mathcal{S}.$

Suszko and Leibniz congruences give rise to the $\mathcal{S}$-matrices $\left<\mathfrak{F}_\mathcal{S}/\widetilde{\Omega}\Sigma_\mathcal{S},\Sigma_\mathcal{S}/\widetilde{\Omega}\Sigma_\mathcal{S}\right>$ and $\left<\mathfrak{F}_\mathcal{L}/\Omega\Sigma_\mathcal{S},\Sigma_\mathcal{S}/\Omega\Sigma_\mathcal{S}\right>$, whose first components,
$\mathfrak{F}_\mathfrak{L}/\widetilde{\Omega}\Sigma_\mathcal{S}$ and $\mathfrak{F}_\mathcal{L}/\Omega\Sigma_\mathcal{S} $, in [[Algebraic logic#Abstract algebraic logic|''Abstract algebraic logic'']] are also referred to as ''Lindenbaum-Tarski algebras''. (See [5] and [6] for comprehensive surveys.)

== Specifications and applications ==

A structural deductive system $\mathcal{S}$ is called ''implicative extensional'' if
its  language $\mathcal{L}$ contains a binary connective $\rightarrow $ (will be written in the infix notation), and for any $\mathcal{S}$-theory $\Sigma_\mathcal{S}$ and any $A, B, C \in Fr_\mathcal{L}$, the following conditions hold:

{|
|-
| $\quad \quad \quad \quad (i_1)$ || $A \rightarrow A \in \Sigma_\mathcal{S};$ 
|-
| $\quad \quad \quad \quad (i_2)$ || $B\in\Sigma_\mathcal{S}\Longrightarrow A\rightarrow B\in\Sigma_\mathcal{S};$
|-
| $\quad \quad \quad \quad (i_3)$ || $
A\rightarrow B, B\rightarrow C\in\Sigma_\mathcal{S} \Longrightarrow
A\rightarrow C\in\Sigma_\mathcal{S};$
|-
| $\quad \quad \quad \quad (i_4)$ || $
A, A\rightarrow B\in\Sigma_\mathcal{S} \Longrightarrow B\in\Sigma_\mathcal{S};$
|-
| $\quad \quad \quad \quad (i_5)$ || $
A_{i}\rightarrow B_{i}, B_{i}\rightarrow A_{i}\in\Sigma_\mathcal{S}, 1\leq i\leq n, \Longrightarrow \Pi A_{1}... A_{n}\rightarrow\Pi B_{1}... B_{n}$ 
for each $n$-ary connective $\Pi$.
|}

Now, given $\mathcal{S}$, we consider the following relation on $Fr_\mathcal{L}$:

$\quad \quad \quad \quad A \approx_{\mathcal{S}} B \Longleftrightarrow A\rightarrow B, B\rightarrow A \in T_\mathcal{S}.$ (''Tarski relation'')

'''Theorem 7''' (Rasiowa).
''If $\mathcal{S}$ is an implicative extensional system, then the relation $\approx_{\mathcal{S}}$ is a congruence on $\mathfrak{F}_{\mathcal{L}}$. Moreover, $T_\mathcal{S}$ is a congruence class with respect to $\approx_{\mathcal{S}}$.

Applying Theorem 7  to $IPC$, one can observe (actually, it was shown in [13]) that
$\mathfrak{F}_\mathcal{L}/\!\!\approx_{IPC}$ is the free algebra of rank $\overline{\overline{\mathcal{V}}}$ in the variety of Heyting algebras. Using the Tarski relation $\approx_{IPC}$, Nishimura [11] gave an elegant description of the Lindenbaum-Tarski algebra of $IPC$ in a language with a single propositional variable. This algebra is also the free algebra of rank $1$ in the variety of Heyting algebras. See [[Free algebra]]. 

Also, it is worth noticing that, using a Lindenbaum-Tarski algebra as defined above, one can prove that there is an algorithm which decides whether two finite $g$-matrices define the same deductive system; this result is due A. Citkin and J. Zygmunt. In this connection see [[Decision problem]].

=== Historical remarks ===

In [17],[18] (see [20], chapter XII), Tarski gave the first specification of a system which admits the Lindenbaum-Tarski algebra. Later on, Rasiowa [13] summarized the work that had been done by the time in the notion of "the class of standard systems of implicative extensional propositional calculi," which is a simplified version of that we use above.
 
Also, if $\mathcal{S}$ is an implicative extensional system, then $\mathfrak{F}_\mathcal{S}$ as defined above is Rasiowa's $\mathscr{S}$-algebra [13], or nowadays known [2] as ''Hilbert algebra'' with compatible operations.

== 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] Josep Maria Font and Ramon Jansana, ''A general algebraic semantics for sentential logics'', second ed., Association for Symbolic Logic, 2009, Lecture Notes in Logic, vol. 7.

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

[8] 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)

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

[10] 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.

[11] 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)

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

[13] 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)

[14] 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)

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

[16] 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)

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

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

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

[20] 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)

[21] 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)

[22] 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)