Namespaces
Variants
Actions

Difference between revisions of "Lindenbaum method"

From Encyclopedia of Mathematics
Jump to: navigation, search
Line 6: Line 6:
 
== Lindenbaum's theorem ==
 
== 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:
+
A formal propositional language, say $\mathcal{L}$, is understood as a nonempty set $\mathcal{V}$ of symbols $p_0, p_1,... p_{\gamma}...$ called propo
 +
sitional 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:
  
 
{|
 
{|
Line 65: Line 66:
  
 
{|
 
{|
 
 
|-
 
|-
 
 
| $(s_4)$ || if $X \ \vdash_\mathcal{S} \ A$, then there is $Y \sqsubseteq X$ such that $Y \ \vdash_\mathcal{S} \ A$.
 
| $(s_4)$ || if $X \ \vdash_\mathcal{S} \ A$, then there is $Y \sqsubseteq X$ such that $Y \ \vdash_\mathcal{S} \ A$.
 
 
|}
 
|}
  
Line 80: Line 78:
 
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}$,
 
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,$
+
$\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$,
 
so that the following conditions are fulfilled: For all $X,Y \subseteq Fr_\mathcal{L}$ and any substitution $\sigma$,
Line 88: Line 86:
 
|-
 
|-
  
| $(c_1)$ || $X \subseteq Cn_\mathcal{S}{X};$ || (''Reflexivity'')
+
| $(c_1)$ || $X \subseteq Cn_\mathcal{S}(X);$ || (''Reflexivity'')
  
 
|-
 
|-
  
| $(c_2)$ || $Cn_\mathcal{S}{Cn_\mathcal{S}{X}} = Cn_\mathcal{S}{X};$ || (''Idenpotency'')
+
| $(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_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'')
+
| $(c_4)$ || $\sigma[Cn_\mathcal{S}(X)] \subseteq Cn_\mathcal{S}(\sigma[X]).$ ||(''Structurality'')
  
 
|}
 
|}
Line 110: Line 108:
 
|-
 
|-
  
| $(c_5)$ || $Cn_\mathcal{S}{X} = \bigcup\lbrace Cn_\mathcal{S}{Y} \ | \ Y \Subset X \rbrace$
+
| $(c_5)$ || $Cn_\mathcal{S}(X) = \bigcup\lbrace Cn_\mathcal{S}(Y) \ | \ Y \Subset X \rbrace$
  
 
|}
 
|}
Line 124: Line 122:
 
|}
 
|}
  
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:
+
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:
  
 
{|
 
{|
Line 135: Line 133:
  
 
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}$.
 
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.''' 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$.''

Revision as of 12:56, 14 April 2013

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 propo sitional 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$.

How to Cite This Entry:
Lindenbaum method. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Lindenbaum_method&oldid=29614