Lemat Lindenbauma – twierdzenie metamatematyczne, zwane tradycyjnie lematem . Sformułowane przez polskiego logika ze szkoły lwowsko-warszawskiej , Adolfa Lindenbauma . Ma ono szerokie zastosowanie w teorii modeli , m.in. w dowodach twierdzenia o pełności tzw. metodą henkinowską .
Lemat Lindenbauma głosi, że dowolny niesprzeczny zbiór formuł można rozszerzyć do niesprzecznego i zupełnego zbioru formuł.
Zapis formalny jest następujący (przez X oznaczamy zbiór formuł, a przez Fm zbiór wszystkich formuł nad danym przeliczalnym alfabetem):
∀
X
(
¬
∀
φ
∈
F
m
[
X
⊢
φ
]
⇒
∃
Y
[
{
X
⊆
Y
}
∧
¬
∀
φ
∈
F
m
{
Y
⊢
φ
}
∧
∀
φ
∈
F
m
{
Y
⊢
φ
∨
Y
⊢
¬
φ
}
]
)
.
{\displaystyle \forall _{X}(\neg \forall _{\varphi \in Fm}[X\vdash \varphi ]\Rightarrow \exists _{Y}[\{X\subseteq Y\}\wedge \neg \forall _{\varphi \in Fm}\{Y\vdash \varphi \}\wedge \forall _{\varphi \in Fm}\{Y\vdash \varphi \vee Y\vdash \neg \varphi \}]).}
edytuj
Tw.
∀
X
(
¬
∀
φ
∈
F
m
[
X
⊢
φ
]
⇒
∃
Y
[
{
X
⊆
Y
}
∧
¬
∀
φ
∈
F
m
{
Y
⊢
φ
}
∧
∀
φ
∈
F
m
{
Y
⊢
φ
∨
Y
⊢
¬
φ
}
]
)
.
{\displaystyle \forall _{X}(\neg \forall _{\varphi \in Fm}[X\vdash \varphi ]\Rightarrow \exists _{Y}[\{X\subseteq Y\}\wedge \neg \forall _{\varphi \in Fm}\{Y\vdash \varphi \}\wedge \forall _{\varphi \in Fm}\{Y\vdash \varphi \vee Y\vdash \neg \varphi \}]).}
Dowód:
Niech X będzie zbiorem niesprzecznym. Niech ciąg formul
α
0
,
α
1
,
…
{\displaystyle \alpha _{0},\alpha _{1},\dots }
Y
0
=
X
,
{\displaystyle Y_{0}=X,}
Y
n
+
1
=
{
Y
n
∪
{
α
n
}
,
gdy
⌜
¬
α
n
⌝
∉
C
n
(
Y
n
)
Y
n
∪
{
¬
α
n
}
,
gdy
⌜
¬
α
n
⌝
∈
C
n
(
Y
n
)
,
{\displaystyle Y_{n+1}={\begin{cases}Y_{n}\cup \{\alpha _{n}\},&{\text{gdy }}\ \ulcorner \neg \alpha _{n}\urcorner \notin Cn(Y_{n})\\[2pt]Y_{n}\cup \{\neg \alpha _{n}\},&{\text{gdy }}\ \ulcorner \neg \alpha _{n}\urcorner \in Cn(Y_{n})\end{cases}},}
Y
=
⋃
n
∈
N
Y
n
.
{\displaystyle Y=\bigcup _{n\in \mathbb {N} }Y_{n}.}
(Oznaczenia
⌜
α
⌝
{\displaystyle \ulcorner \alpha \urcorner }
Aby udowodnić lemat Lindenbauma, musimy pokazać trzy rzeczy: (a) zawieranie się X w Y (b) zupełność Y i (c) niesprzeczność Y.
X
⊆
Y
.
{\displaystyle X\subseteq Y.}
Y
=
⋃
n
∈
N
Y
n
{\displaystyle Y=\bigcup _{n\in \mathbb {N} }Y_{n}}
Y
0
=
X
.
{\displaystyle Y_{0}=X.}
Twierdzimy, że
Y
{\displaystyle Y}
∀
φ
∈
F
m
(
Y
⊢
φ
∨
Y
⊢
¬
φ
)
.
{\displaystyle \forall _{\varphi \in Fm}(Y\vdash \varphi \vee Y\vdash \neg \varphi ).}
φ
.
{\displaystyle \varphi .}
φ
=
α
n
.
{\displaystyle \varphi =\alpha _{n}.}
Przypadek 1.
⌜
¬
α
n
⌝
∉
C
n
(
Y
n
)
;
{\displaystyle \ulcorner \neg \alpha _{n}\urcorner \notin Cn(Y_{n});}
Przypadek 2.
⌜
¬
α
n
⌝
∈
C
n
(
Y
n
)
.
{\displaystyle \ulcorner \neg \alpha _{n}\urcorner \in Cn(Y_{n}).}
Ad 1:
α
n
∈
Y
n
+
1
,
{\displaystyle \alpha _{n}\in Y_{n+1},}
α
n
∈
Y
.
{\displaystyle \alpha _{n}\in Y.}
Ad 2:
⌜
¬
α
n
⌝
∈
Y
n
+
1
,
{\displaystyle \ulcorner \neg \alpha _{n}\urcorner \in Y_{n+1},}
¬
α
n
∈
Y
.
{\displaystyle \neg \alpha _{n}\in Y.}
Twierdzimy, że Y jest niesprzeczny. Dowodzimy przez indukcję po n, że dla każdego n
Y
n
{\displaystyle Y_{n}}
(0)
Y
0
{\displaystyle Y_{0}}
(i) załóżmy, że
Y
n
{\displaystyle Y_{n}}
(T)
Y
n
+
1
{\displaystyle Y_{n+1}}
Fakt:
∀
X
∀
φ
[
X
⊬
¬
φ
⇒
X
∪
{
φ
}
j
e
s
t
n
i
e
s
p
r
z
e
c
z
n
e
]
{\displaystyle \forall _{X}\forall _{\varphi }[X\not \vdash \neg \varphi \Rightarrow X\cup \{\varphi \}\ jest\ niesprzeczne]}
Przypadek 1.
Y
n
+
1
=
Y
n
∪
{
α
n
}
.
{\displaystyle Y_{n+1}=Y_{n}\cup \{\alpha _{n}\}.}
Y
n
:
{\displaystyle Y_{n}{:}}
⌜
¬
α
⌝
∉
C
n
(
Y
n
)
.
{\displaystyle \ulcorner \neg \alpha \urcorner \notin Cn(Y_{n}).}
Y
n
∪
{
α
n
}
{\displaystyle Y_{n}\cup \{\alpha _{n}\}}
Przypadek 2.
Y
n
+
1
=
Y
n
∪
{
¬
α
n
}
.
{\displaystyle Y_{n+1}=Y_{n}\cup \{\neg \alpha _{n}\}.}
⌜
¬
α
n
⌝
∈
C
n
(
Y
n
)
.
{\displaystyle \ulcorner \neg \alpha _{n}\urcorner \in Cn(Y_{n}).}
C
n
(
Y
n
)
=
C
n
(
Y
n
+
1
)
.
{\displaystyle Cn(Y_{n})=Cn(Y_{n+1}).}
Y
n
+
1
{\displaystyle Y_{n+1}}
![{\displaystyle \forall _{X}(\neg \forall _{\varphi \in Fm}[X\vdash \varphi ]\Rightarrow \exists _{Y}[\{X\subseteq Y\}\wedge \neg \forall _{\varphi \in Fm}\{Y\vdash \varphi \}\wedge \forall _{\varphi \in Fm}\{Y\vdash \varphi \vee Y\vdash \neg \varphi \}]).}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e0107efe63578e68210d7031403388e6132e2f79)
![{\displaystyle Y_{n+1}={\begin{cases}Y_{n}\cup \{\alpha _{n}\},&{\text{gdy }}\ \ulcorner \neg \alpha _{n}\urcorner \notin Cn(Y_{n})\\[2pt]Y_{n}\cup \{\neg \alpha _{n}\},&{\text{gdy }}\ \ulcorner \neg \alpha _{n}\urcorner \in Cn(Y_{n})\end{cases}},}](https://wikimedia.org/api/rest_v1/media/math/render/svg/39d28aab429e84c77d97e301b88bf71a902ec5ac)
![{\displaystyle \forall _{X}\forall _{\varphi }[X\not \vdash \neg \varphi \Rightarrow X\cup \{\varphi \}\ jest\ niesprzeczne]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/84ae21c43d5bdbde5f919776c50839d115d40a16)
