Język zdaniowy – trójka
L
=
⟨
P
,
F
,
ς
⟩
,
{\displaystyle {\mathcal {L}}=\langle {\textbf {P}},{\mathfrak {F}},\varsigma \rangle ,}
P
{\displaystyle {\textbf {P}}}
F
{\displaystyle {\mathfrak {F}}}
P
{\displaystyle {\textbf {P}}}
ς
:
F
→
N
0
.
{\displaystyle \varsigma :{\mathfrak {F}}\to \mathbb {N} _{0}.}
Elementy zbioru
P
{\displaystyle {\textbf {P}}}
zmiennymi zdaniowymi , elementy zbioru
F
{\displaystyle {\mathfrak {F}}}
spójnikami języka
L
,
{\displaystyle {\mathcal {L}},}
ς
{\displaystyle \varsigma }
sygnaturą .
Skończone ciągi elementów zbioru
P
∪
F
{\displaystyle {\textbf {P}}\cup {\mathfrak {F}}}
napisami języka
L
.
{\displaystyle {\mathcal {L}}.}
Najmniejszy (w sensie inkluzji) spośród zbiorów napisów zbiór
Y
{\displaystyle Y}
P
⊆
Y
{\displaystyle {\textbf {P}}\subseteq Y}
Y
{\displaystyle Y}
(1)
f
α
1
…
α
ς
(
f
)
∈
Y
,
α
1
,
…
,
α
ς
(
f
)
∈
Y
,
f
∈
F
{\displaystyle {\mathfrak {f}}\alpha _{1}\ldots \alpha _{\varsigma ({\mathfrak {f}})}\in Y,\quad \alpha _{1},\dots ,\alpha _{\varsigma ({\mathfrak {f}})}\in Y,\quad {\mathfrak {f}}\in {\mathfrak {F}}}
(2)
nazywany jest zbiorem formuł języka
L
{\displaystyle {\mathcal {L}}}
F
r
m
(
L
)
.
{\displaystyle \mathbf {Frm} ({\mathcal {L}}).}
O zbiorach spełniających warunki (1) i (2) mówi się, że są domknięte na budowę formuł języka
L
{\displaystyle {\mathcal {L}}}
.
Innymi słowy zbiór
F
r
m
(
L
)
{\displaystyle \mathbf {Frm} ({\mathcal {L}})}
F
r
m
(
L
)
.
{\displaystyle \mathbf {Frm} ({\mathcal {L}}).}
Niech
L
C
I
M
V
=
⟨
P
,
F
,
ς
L
K
⟩
,
{\displaystyle {\mathcal {L}}_{\mathbf {CIMV} }=\langle {\textbf {P}},{\mathfrak {F}},\varsigma _{\mathbf {LK} }\rangle ,}
gdzie
P
=
{
p
,
q
,
r
,
s
,
…
}
,
{\displaystyle \mathbf {P} =\{\mathbf {p} ,\mathbf {q} ,\mathbf {r} ,\mathbf {s} ,\dots \},}
F
=
{
C
,
A
,
K
,
N
,
E
}
{\displaystyle {\mathfrak {F}}=\{\mathbf {C} ,\mathbf {A} ,\mathbf {K} ,\mathbf {N} ,\mathbf {E} \}}
i niech
ς
L
K
(
C
)
=
2
,
ς
L
K
(
A
)
=
2
,
ς
L
K
(
K
)
=
2
,
ς
L
K
(
E
)
=
2
,
ς
L
K
(
N
)
=
1.
{\displaystyle \varsigma _{\mathbf {LK} }(\mathbf {C} )=2,\;\varsigma _{\mathbf {LK} }(\mathbf {A} )=2,\;\varsigma _{\mathbf {LK} }(\mathbf {K} )=2,\;\varsigma _{\mathbf {LK} }(\mathbf {E} )=2,\;\varsigma _{\mathbf {LK} }(\mathbf {N} )=1.}
Wówczas
C
C
N
p
q
A
p
q
{\displaystyle \mathbf {CCNpqApq} }
L
C
I
M
V
,
{\displaystyle {\mathcal {L}}_{\mathbf {CIMV} },}
C
C
N
p
q
q
A
p
q
{\displaystyle \mathbf {CCNpqqApq} }
C
C
N
p
N
A
p
q
{\displaystyle \mathbf {CCNpNApq} }
Język termów arytmetyki Peana
edytuj
Niech
ς
P
A
=
⟨
A
M
O
I
2
2
0
0
⟩
i niech
V
=
{
v
0
,
v
1
,
v
2
,
…
}
.
{\displaystyle \varsigma _{\mathbf {PA} }=\left\langle {\begin{array}{c|c|c|c}\mathbf {A} &\mathbf {M} &\mathbf {O} &\mathbf {I} \\\hline 2&2&0&0\end{array}}\right\rangle \qquad {\mbox{i niech}}\qquad \mathbf {V} =\{\mathbf {v} _{0},\mathbf {v} _{1},\mathbf {v} _{2},\dots \}.}
Język
L
P
A
t
=
⟨
V
,
{
A
,
M
,
O
,
I
}
,
ς
P
A
⟩
{\displaystyle {\mathcal {L}}_{\mathbf {PA} }^{t}=\langle \mathbf {V} ,\{\mathbf {A} ,\mathbf {M} ,\mathbf {O} ,\mathbf {I} \},\varsigma _{\mathbf {PA} }\rangle }
nazywa się językiem termów arytmetyki Peana . Formuły tego języka nazywa się termami
T
r
m
P
A
.
{\displaystyle \mathbf {Trm} _{\mathbf {PA} }.}
Dla wygody czasem zamiast
v
0
{\displaystyle \mathbf {v} _{0}}
x
,
{\displaystyle \mathbf {x} ,}
v
1
{\displaystyle \mathbf {v} _{1}}
y
{\displaystyle \mathbf {y} }
v
2
{\displaystyle \mathbf {v} _{2}}
z
.
{\displaystyle \mathbf {z} .}
Definiujemy indukcyjnie ciąg numerałów
Δ
0
:=
O
,
Δ
1
:=
I
,
Δ
n
+
1
:=
A
I
Δ
n
,
n
=
0
,
1
,
2
,
…
{\displaystyle {\boldsymbol {\Delta }}_{0}:=\mathbf {O} ,\quad {\boldsymbol {\Delta }}_{1}:=\mathbf {I} ,\quad {\boldsymbol {\Delta }}_{n+1}:=\mathbf {AI} {\boldsymbol {\Delta }}_{n},\quad n=0,1,2,\dots }
Język formuł arytmetyki PA
edytuj
Formułami atomowymi
E
q
τ
1
τ
2
{\displaystyle \mathbf {Eq} \tau _{1}\tau _{2}}
L
e
τ
1
τ
2
,
{\displaystyle \mathbf {Le} \tau _{1}\tau _{2},}
τ
1
,
τ
2
∈
T
r
m
P
A
.
{\displaystyle \tau _{1},\tau _{2}\in \mathbf {Trm} _{PA}.}
Zwyczajowo zamiast
E
q
τ
1
τ
2
,
{\displaystyle \mathbf {Eq} \tau _{1}\tau _{2},}
(
τ
1
≡
τ
2
)
,
{\displaystyle (\tau _{1}\equiv \tau _{2}),}
L
e
τ
1
τ
2
,
{\displaystyle \mathbf {Le} \tau _{1}\tau _{2},}
(
τ
1
⩽
τ
2
)
.
{\displaystyle (\tau _{1}\leqslant \tau _{2}).}
Zbiór formuł atomowych języka PA, oznaczymy
F
r
m
P
A
(
0
)
.
{\displaystyle \mathbf {Frm} _{\mathbf {PA} }^{(0)}.}
Przykład:
formułami atomowymi języka PA są
(Zero jest najmniejsze)
O
⩽
x
{\displaystyle \mathbf {O} \leqslant \mathbf {x} }
(Aksjomaty dla dodawania)
A
x
O
≡
x
,
{\displaystyle \mathbf {AxO} \equiv \mathbf {x} ,}
A
x
A
y
I
≡
A
A
x
y
I
{\displaystyle \mathbf {AxAyI} \equiv \mathbf {AAxyI} }
(Aksjomaty dla mnożenia)
M
x
O
≡
O
,
{\displaystyle \mathbf {MxO} \equiv \mathbf {O} ,}
M
x
A
y
I
≡
A
M
x
y
x
{\displaystyle \mathbf {MxAyI} \equiv \mathbf {AMxyx} }
(Przemienność dodawania i mnożenia)
A
x
y
≡
A
y
x
,
{\displaystyle \mathbf {Axy} \equiv \mathbf {Ayx} ,}
M
x
y
≡
M
y
x
{\displaystyle \mathbf {Mxy} \equiv \mathbf {Myx} }
(Łączność dodawania i mnożenia)
A
x
A
y
z
≡
A
A
x
y
z
,
{\displaystyle \mathbf {AxAyz} \equiv \mathbf {AAxyz} ,}
M
x
A
y
z
≡
M
M
x
y
z
{\displaystyle \mathbf {MxAyz} \equiv \mathbf {MMxyz} }
(2+3=5)
A
Δ
2
Δ
3
≡
Δ
5
{\displaystyle \mathbf {A} {\boldsymbol {\Delta }}_{2}{\boldsymbol {\Delta }}_{3}\equiv {\boldsymbol {\Delta }}_{5}}
(2*3=6)
M
Δ
2
Δ
3
≡
Δ
6
{\displaystyle \mathbf {M} {\boldsymbol {\Delta }}_{2}{\boldsymbol {\Delta }}_{3}\equiv {\boldsymbol {\Delta }}_{6}}
Formułami
⟨
F
r
m
P
A
(
0
)
,
{
A
,
K
,
N
,
C
,
E
}
∪
Q
∀
∪
Q
∃
,
ς
K
R
K
⟩
,
{\displaystyle \langle \mathbf {Frm} _{\mathbf {PA} }^{(0)},\{\mathbf {A} ,\mathbf {K} ,\mathbf {N} ,\mathbf {C} ,\mathbf {E} \}\cup {\mathfrak {Q}}^{\forall }\cup {\mathfrak {Q}}^{\exists },\varsigma _{\mathbf {KRK} }\rangle ,}
gdzie
Q
∀
=
{
(
Q
n
∀
)
:
n
=
0
,
1
,
2
,
…
}
,
Q
∃
=
{
(
Q
n
∃
)
:
n
=
0
,
1
,
2
,
…
}
{\displaystyle {\mathfrak {Q}}^{\forall }=\{(\mathbf {Q} _{n}^{\forall }):n=0,1,2,\dots \},\;{\mathfrak {Q}}^{\exists }=\{(\mathbf {Q} _{n}^{\exists }):n=0,1,2,\dots \}}
oraz gdzie
ς
K
R
K
{\displaystyle \varsigma _{\mathbf {KRK} }}
ς
L
K
{\displaystyle \varsigma _{\mathbf {LK} }}
{
A
,
K
,
N
,
C
,
E
}
∪
Q
∀
∪
Q
∃
,
{\displaystyle \{\mathbf {A} ,\mathbf {K} ,\mathbf {N} ,\mathbf {C} ,\mathbf {E} \}\cup {\mathfrak {Q}}^{\forall }\cup {\mathfrak {Q}}^{\exists },}
ς
L
K
(
Q
n
∀
)
=
ς
L
K
(
Q
n
∃
)
=
1
,
n
=
0
,
1
,
2
,
…
{\displaystyle \varsigma _{\mathbf {LK} }(\mathbf {Q} _{n}^{\forall })=\varsigma _{\mathbf {LK} }(\mathbf {Q} _{n}^{\exists })=1,\;n=0,1,2,\dots }
Zamiast pisać
(
Q
n
∀
)
α
,
{\displaystyle (\mathbf {Q} _{n}^{\forall })\alpha ,}
(
∀
v
n
)
α
,
{\displaystyle (\forall \mathbf {v} _{n})\alpha ,}
(
Q
n
∃
)
α
,
{\displaystyle (\mathbf {Q} _{n}^{\exists })\alpha ,}
(
∃
v
n
)
α
.
{\displaystyle (\exists \mathbf {v} _{n})\alpha .}
Przykład:
formułami języka PA są
E
(
x
⩽
y
)
(
∃
z
)
(
A
x
z
≡
y
)
{\displaystyle \mathbf {E} (\mathbf {x\leqslant y} )(\exists \mathbf {z} )(\mathbf {Axz\equiv y} )}
C
(
A
x
z
⩽
A
y
z
)
(
x
⩽
y
)
{\displaystyle \mathbf {C} (\mathbf {Axz\leqslant Ayz} )(\mathbf {x\leqslant y} )}
C
N
(
z
≡
O
)
C
(
M
x
z
⩽
M
y
z
)
(
x
⩽
y
)
{\displaystyle \mathbf {CN} (\mathbf {z\equiv O} )\mathbf {C} (\mathbf {Mxz\leqslant Myz} )(\mathbf {x\leqslant y} )}
Lemat (o kształcie formuł)
edytuj
Niech
L
{\displaystyle {\mathcal {L}}}
Wówczas dla każdej formuły
δ
{\displaystyle \delta }
δ
∈
P
{\displaystyle \delta \in \mathbf {P} }
(3)
δ
=
f
α
1
…
α
n
{\displaystyle \delta ={\mathfrak {f}}\alpha _{1}\ldots \alpha _{n}}
f
∈
F
{\displaystyle {\mathfrak {f}}\in {\mathfrak {F}}}
α
1
,
…
,
α
n
∈
F
r
m
(
L
)
{\displaystyle \alpha _{1},\dots ,\alpha _{n}\in \mathbf {Frm} ({\mathcal {L}})}
(4)
Dla dowodu tego lematu należy rozważyć zbiór
Y
{\displaystyle Y}
δ
{\displaystyle \delta }
(3) i (4) powyżej, a następnie pokazać, że jest on domknięty na budowę formuł.
Lemat (o jednoznaczności budowy)
edytuj
Niech
L
{\displaystyle {\mathcal {L}}}
α
1
,
…
,
α
n
,
β
1
,
…
,
β
m
{\displaystyle \alpha _{1},\dots ,\alpha _{n},\beta _{1},\dots ,\beta _{m}}
f
1
,
f
2
∈
F
{\displaystyle {\mathfrak {f_{1}}},{\mathfrak {f_{2}}}\in {\mathfrak {F}}}
f
1
α
1
…
α
n
=
f
2
β
1
…
β
m
.
{\displaystyle {\mathfrak {f_{1}}}\alpha _{1}\ldots \alpha _{n}={\mathfrak {f_{2}}}\beta _{1}\ldots \beta _{m}.}
Wówczas
f
1
=
f
2
,
n
=
m
{\displaystyle {\mathfrak {f_{1}}}={\mathfrak {f_{2}}},\;n=m}
α
1
=
β
1
,
…
,
α
n
=
β
m
.
{\displaystyle \alpha _{1}=\beta _{1},\,\dots ,\,\alpha _{n}=\beta _{m}.}
Lematy o kształcie formuł i jednoznaczności budowy pozwalają na indukcyjne zdefiniowanie pojęcia podformuły danej formuły oraz podstawienia w formule innej formuły w miejsce zmiennej :
Zbiorem podformuł
δ
{\displaystyle \delta }
S
b
f
(
δ
)
=
{
δ
,
jeśli
δ
∈
P
S
b
f
(
α
1
)
∪
…
∪
S
b
f
(
α
n
)
∪
{
δ
}
jeśli
δ
=
f
α
1
…
α
n
,
f
∈
F
.
{\displaystyle \mathbf {Sbf} (\delta )={\begin{cases}\delta ,&{\mbox{jeśli }}\delta \in \mathbf {P} \\\mathbf {Sbf} (\alpha _{1})\cup \ldots \cup \mathbf {Sbf} (\alpha _{n})\cup \{\delta \}&{\mbox{jeśli }}\delta ={\mathfrak {f}}\alpha _{1}\ldots \alpha _{n},\;{\mathfrak {f}}\in {\mathfrak {F}}.\end{cases}}}
Zmiennymi formuły
δ
{\displaystyle \delta }
A
t
(
δ
)
=
S
b
f
(
δ
)
∩
P
.
{\displaystyle \mathbf {At} (\delta )=\mathbf {Sbf} (\delta )\cap \mathbf {P} .}
S
b
f
(
C
C
N
p
q
A
p
q
)
=
{
p
,
q
,
A
p
q
,
N
p
,
C
N
p
q
,
C
C
N
p
q
A
p
q
}
{\displaystyle \mathbf {Sbf} (\mathbf {CCNpqApq} )=\{\mathbf {p} ,\mathbf {q} ,\mathbf {Apq} ,\mathbf {Np} ,\mathbf {CNpq} ,\mathbf {CCNpqApq} \}}
Podstawienie w formule
edytuj
Jednoczesne podstawienie kilku formuł
edytuj
W wielu wypadkach przydaje się umiejętność jednoczesnego
Podstawieniem w formule
δ
{\displaystyle \delta }
φ
1
,
…
,
φ
m
{\displaystyle \varphi _{1},\dots ,\varphi _{m}}
s
1
,
…
,
s
m
{\displaystyle s_{1},\dots ,s_{m}}
nazywamy formułę:
(
δ
)
[
φ
1
/
s
1
,
…
,
φ
m
/
s
m
]
=
{
p
jeśli
p
∈
P
∖
{
s
1
,
…
,
s
m
}
,
φ
j
jeśli
p
=
s
j
,
j
=
1
,
…
,
m
,
f
(
α
1
[
φ
1
/
s
1
,
…
,
φ
m
/
s
m
]
)
…
(
α
n
[
φ
1
/
s
1
,
…
,
φ
m
/
s
m
]
)
jeśli
δ
=
f
α
1
…
α
n
,
f
∈
F
.
{\displaystyle (\delta )[\varphi _{1}/s_{1},\dots ,\varphi _{m}/s_{m}]={\begin{cases}{p}&{{\mbox{jeśli }}p\in \mathbf {P} \setminus \{s_{1},\dots ,s_{m}\},}\\{\varphi _{j}}&{{\mbox{jeśli }}p=s_{j},\,j=1,\dots ,m,}\\{{\mathfrak {f}}(\alpha _{1}[\varphi _{1}/s_{1},\dots ,\varphi _{m}/s_{m}])\ldots (\alpha _{n}[\varphi _{1}/s_{1},\dots ,\varphi _{m}/s_{m}])}&{{\mbox{jeśli }}\delta ={\mathfrak {f}}\alpha _{1}\ldots \alpha _{n},\;{\mathfrak {f}}\in {\mathfrak {F}}.}\end{cases}}}
Wynik podstawienia nie zależy od kolejności:
(
δ
)
[
φ
1
/
s
1
,
…
,
φ
m
/
s
m
]
=
(
δ
)
[
φ
π
(
1
)
/
s
π
(
1
)
,
…
,
φ
π
(
m
)
/
s
π
(
m
)
]
{\displaystyle (\delta )[\varphi _{1}/s_{1},\dots ,\varphi _{m}/s_{m}]=(\delta )[\varphi _{\pi (1)}/s_{\pi (1)},\dots ,\varphi _{\pi (m)}/s_{\pi (m)}]}
dla dowolnej permutacji
π
{\displaystyle \pi }
{
1
,
2
,
…
,
n
}
.
{\displaystyle \{1,2,\dots ,n\}.}
Jeśli
p
,
q
∈
A
t
(
δ
)
{\displaystyle p,q\in \mathbf {At} (\delta )}
q
∉
A
t
(
φ
)
,
{\displaystyle q\notin \mathbf {At} (\varphi ),}
(
δ
)
[
φ
/
p
,
ψ
/
q
]
=
(
(
δ
)
[
φ
/
p
]
)
[
ψ
/
q
]
.
{\displaystyle (\delta )[\varphi /p,\psi /q]={\big (}(\delta )[\varphi /p]{\big )}[\psi /q].}
(
C
C
N
p
q
A
p
q
)
[
K
E
p
q
N
p
/
p
,
C
N
p
p
/
q
]
{\displaystyle (\mathbf {CCNpqApq} )[\mathbf {KEpqNp} /\mathbf {p} ,\mathbf {CNpp} /\mathbf {q} ]}
=
C
C
N
K
E
p
q
N
p
C
N
p
p
A
K
E
p
q
N
p
C
N
p
p
{\displaystyle =\mathbf {CCNKEpqNpCNppAKEpqNpCNpp} }
(
C
C
N
p
q
A
p
q
)
[
K
E
p
q
N
p
/
p
]
[
C
N
p
p
/
q
]
{\displaystyle (\mathbf {CCNpqApq} )[\mathbf {KEpqNp} /\mathbf {p} ][\mathbf {CNpp} /\mathbf {q} ]}
=
(
C
C
N
K
E
p
q
N
p
q
A
K
E
p
q
N
p
q
)
[
C
N
p
p
/
q
]
=
{\displaystyle =(\mathbf {CCNKEpqNpqAKEpqNpq} )[\mathbf {CNpp} /\mathbf {q} ]=}
=
C
C
N
K
E
p
C
N
p
p
N
p
C
N
p
p
A
K
E
p
C
N
p
p
N
p
C
N
p
p
{\displaystyle =\mathbf {CCNKEpCNppNpCNppAKEpCNppNpCNpp} }
Algebra formuł
edytuj
Język zdaniowy wyznacza dość ważną algebrę sygnatury
ς
:
{\displaystyle \varsigma {:}}
Algebrą formuł języka
L
{\displaystyle {\mathcal {L}}}
A
L
,
{\displaystyle {\mathfrak {A}}_{\mathcal {L}},}
uniwersum jest
F
r
m
(
L
)
{\displaystyle \mathbf {Frm} ({\mathcal {L}})}
A
L
(
f
)
(
α
1
,
…
,
α
ς
(
f
)
)
=
f
α
1
…
α
ς
(
f
)
,
dla
f
∈
F
.
{\displaystyle {\mathfrak {A}}_{\mathcal {L}}({\mathfrak {f}})(\alpha _{1},\dots ,\alpha _{\varsigma ({\mathfrak {f}})})={\mathfrak {f}}\alpha _{1}\ldots \alpha _{\varsigma ({\mathfrak {f}})},\qquad {\hbox{dla}}\;\;{\mathfrak {f}}\in {\mathfrak {F}}.}
Algebra języka jest algebrą wolną z
P
{\displaystyle \mathbf {P} }
wolnych generatorów w klasie algebr jej sygnatury:
Dla dowolnej algebry
C
{\displaystyle {\mathfrak {C}}}
L
{\displaystyle {\mathcal {L}}}
v
:
P
→
|
C
|
{\displaystyle v\colon \mathbf {P} \to |{\mathfrak {C}}|}
homomorfizm
A
L
,
v
^
:
A
L
→
C
{\displaystyle {\widehat {{\mathfrak {A}}_{\mathcal {L}},v}}\colon {\mathfrak {A}}_{\mathcal {L}}\to {\mathfrak {C}}}
v
.
{\displaystyle v.}
W przypadku, gdy język jest ustalony w danym kontekście homomorfizm ten oznaczamy po prostu symbolem
v
^
.
{\displaystyle {\widehat {v}}.}
Zauważmy, że
(
δ
)
[
φ
/
s
]
=
v
^
(
δ
)
,
{\displaystyle (\delta )[\varphi /s]={\widehat {v}}(\delta ),}
v
:
P
→
F
r
m
(
L
)
{\displaystyle v\colon \mathbf {P} \to \mathbf {Frm} ({\mathcal {L}})}
v
(
p
)
=
{
φ
,
p
=
s
p
,
p
∈
P
∖
{
s
}
.
{\displaystyle v(p)={\begin{cases}\varphi ,&p=s\\p,&p\in \mathbf {P} \setminus \{s\}.\end{cases}}}
Co więcej, jeśli
A
t
(
δ
)
=
{
s
1
,
…
,
s
n
}
{\displaystyle \mathbf {At} (\delta )=\{s_{1},\dots ,s_{n}\}}
v
:
P
:
→
F
r
m
(
L
)
,
{\displaystyle v:\mathbf {P} \colon \to \mathbf {Frm} ({\mathcal {L}}),}
v
^
(
δ
)
=
(
δ
)
[
v
(
s
1
)
/
s
1
,
…
,
v
(
s
n
)
/
s
n
]
.
{\displaystyle {\widehat {v}}(\delta )=(\delta )[v(s_{1})/s_{1},\dots ,v(s_{n})/s_{n}].}
Niech
X
{\displaystyle X}
L
.
{\displaystyle {\mathcal {L}}.}
S
b
L
(
X
)
=
{
v
^
(
δ
)
:
δ
∈
X
,
v
:
P
→
F
r
m
(
L
)
}
{\displaystyle \mathbf {Sb} _{\mathcal {L}}(X)={\Big \{}{\widehat {v}}(\delta ):\delta \in X,\;v\colon \mathbf {P} \to \mathbf {Frm} ({\mathcal {L}}){\Big \}}}
Reguła podstawiania
edytuj
Regułą podstawiania w języku
L
{\displaystyle {\mathcal {L}}}
reguła :
r
⋆
L
=
{
⟨
{
δ
}
,
v
^
(
δ
)
⟩
:
δ
∈
X
,
v
:
P
→
F
r
m
(
L
)
}
{\displaystyle \mathbf {r} _{\star }^{\mathcal {L}}={\Big \{}{\big \langle }\{\delta \},{\widehat {v}}(\delta ){\big \rangle }:\delta \in X,\;v\colon \mathbf {P} \to \mathbf {Frm} ({\mathcal {L}}){\Big \}}}
W przypadku, gdy język jest ustalony, indeks górny jest pomijany.
Bibliografia
edytuj
Pogorzelski Witold, Elementarny słownik logiki formalnej , wyd. Filii UW, Białystok 1992.
Pogorzelski Witold, Klasyczny rachunek zdań , Warszawa 1975.
Hunter Geoffrey, Metalogika , Warszawa, PWN 1982.
Shoenfield Joseph R., Mathematical Logic , Addison-Wesley, 1967. 
![{\displaystyle (\delta )[\varphi /s]={\begin{cases}p,&{\mbox{jeśli }}p\in \mathbf {P} \setminus \{s\}\\\varphi &{\mbox{jeśli }}p=s\\{\mathfrak {f}}(\alpha _{1}[\varphi /s])\ldots (\alpha _{n}[\varphi /s])&{\mbox{jeśli }}\delta ={\mathfrak {f}}\alpha _{1}\ldots \alpha _{n},\;{\mathfrak {f}}\in {\mathfrak {F}}.\end{cases}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d62b3162c39965e4adb25a60eda987a80b9e182b)
![{\displaystyle \delta [p/p]=\delta .}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a4f408551f511c768ef6bc8cf7c3b5c622519613)
![{\displaystyle \delta [\varphi /p]=\delta .}](https://wikimedia.org/api/rest_v1/media/math/render/svg/fa7c8727fe263eec18829943f3827119f6aa348c)
![{\displaystyle (\mathbf {CCNpqApq} )[\mathbf {KEpqNp} /\mathbf {q} ]=\mathbf {CCNpKEpqNpApKEpqNp} }](https://wikimedia.org/api/rest_v1/media/math/render/svg/14d0b45ba8090f0da1d08b39e927256b2a1ff26d)
![{\displaystyle (\delta )[\varphi _{1}/s_{1},\dots ,\varphi _{m}/s_{m}]={\begin{cases}{p}&{{\mbox{jeśli }}p\in \mathbf {P} \setminus \{s_{1},\dots ,s_{m}\},}\\{\varphi _{j}}&{{\mbox{jeśli }}p=s_{j},\,j=1,\dots ,m,}\\{{\mathfrak {f}}(\alpha _{1}[\varphi _{1}/s_{1},\dots ,\varphi _{m}/s_{m}])\ldots (\alpha _{n}[\varphi _{1}/s_{1},\dots ,\varphi _{m}/s_{m}])}&{{\mbox{jeśli }}\delta ={\mathfrak {f}}\alpha _{1}\ldots \alpha _{n},\;{\mathfrak {f}}\in {\mathfrak {F}}.}\end{cases}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/5f3febf13e4c4c8a5d80f368b8b3a5f640d4f6d3)
![{\displaystyle (\delta )[\varphi _{1}/s_{1},\dots ,\varphi _{m}/s_{m}]=(\delta )[\varphi _{\pi (1)}/s_{\pi (1)},\dots ,\varphi _{\pi (m)}/s_{\pi (m)}]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/61970bea9b46838415d6ef3438a50617a8d31c33)
![{\displaystyle (\delta )[\varphi /p,\psi /q]={\big (}(\delta )[\varphi /p]{\big )}[\psi /q].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f94c69245b57949952ce8a30c95d9a8c61ff8d4b)
![{\displaystyle (\mathbf {CCNpqApq} )[\mathbf {KEpqNp} /\mathbf {p} ,\mathbf {CNpp} /\mathbf {q} ]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f788347de178d4e58764a3a6936f9083ca71364f)
![{\displaystyle (\mathbf {CCNpqApq} )[\mathbf {KEpqNp} /\mathbf {p} ][\mathbf {CNpp} /\mathbf {q} ]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7732ab786e99a74467e194afcb0849299e8fe1cd)
![{\displaystyle =(\mathbf {CCNKEpqNpqAKEpqNpq} )[\mathbf {CNpp} /\mathbf {q} ]=}](https://wikimedia.org/api/rest_v1/media/math/render/svg/64fd11f0589d17ca75fb71608970f529f13bd050)
![{\displaystyle (\delta )[\varphi /s]={\widehat {v}}(\delta ),}](https://wikimedia.org/api/rest_v1/media/math/render/svg/13a19e495856a83f83cde6714c5047a5a8233cc3)
![{\displaystyle {\widehat {v}}(\delta )=(\delta )[v(s_{1})/s_{1},\dots ,v(s_{n})/s_{n}].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/1eef610bd88aac3f09149e92949cbf8aa6410be1)
