Førsteordens predikatlogikk er i logikk et språk, med tilhørende semantikker og kalkyler, som beskriver objekter og deres relasjon til hverandre.
Et førsteordens språk er et tripel
⟨
C
,
F
,
R
⟩
{\displaystyle \langle C,F,{\mathcal {R}}\rangle }
C
=
{
c
1
,
…
}
{\displaystyle C=\{c_{1},\ldots \}}
F
=
{
f
1
,
…
}
{\displaystyle F=\{f_{1},\ldots \}}
R
=
{
R
1
,
…
}
{\displaystyle {\mathcal {R}}=\{R_{1},\ldots \}}
Disse symbolene kalles de ikke-logiske symbolene.
Gitt et språk
L
=
⟨
C
,
F
,
R
⟩
{\displaystyle {\mathcal {L}}=\langle C,F,{\mathcal {R}}\rangle }
L
{\displaystyle {\mathcal {L}}}
Alle variabler
x
{\displaystyle x}
L
{\displaystyle {\mathcal {L}}}
Alle konstantsymboler
c
∈
C
{\displaystyle c\in C}
L
{\displaystyle {\mathcal {L}}}
Hvis
f
∈
F
{\displaystyle f\in F}
n
{\displaystyle n}
t
1
{\displaystyle t_{1}}
t
n
{\displaystyle t_{n}}
L
{\displaystyle {\mathcal {L}}}
f
(
t
1
,
…
,
f
n
)
{\displaystyle f(t_{1},\ldots ,f_{n})}
L
{\displaystyle {\mathcal {L}}}
Gitt et språk
L
{\displaystyle {\mathcal {L}}}
L
{\displaystyle {\mathcal {L}}}
⊤
{\displaystyle \top }
L
{\displaystyle {\mathcal {L}}}
topp eller sant (eng: top ).
⊥
{\displaystyle \bot }
L
{\displaystyle {\mathcal {L}}}
bunn eller usann (eng: bottom ).Hvis
R
∈
R
{\displaystyle R\in {\mathcal {R}}}
n
{\displaystyle n}
t
1
{\displaystyle t_{1}}
t
n
{\displaystyle t_{n}}
L
{\displaystyle {\mathcal {L}}}
R
(
t
1
,
…
,
t
n
)
{\displaystyle R(t_{1},\ldots ,t_{n})}
L
{\displaystyle {\mathcal {L}}}
Hvis
A
{\displaystyle A}
B
{\displaystyle B}
L
{\displaystyle {\mathcal {L}}}
x
{\displaystyle x}
L
{\displaystyle {\mathcal {L}}}
¬
A
{\displaystyle \neg A}
A
{\displaystyle A}
A
∧
B
{\displaystyle A\land B}
A og B .
A
∨
B
{\displaystyle A\lor B}
A eller B .
A
→
B
{\displaystyle A\to B}
hvis A, så B eller A impliserer B . (Notasjonen
A
⊃
B
{\displaystyle A\supset B}
∀
x
.
A
{\displaystyle \forall x.\,A}
. Legg merke til at x kan forekomme som en variabel i A.
∃
x
.
A
{\displaystyle \exists x.\,A}
rediger
En standard måte å beskrive modeller for førsteordens logikk på er som følger.
En modell
M
{\displaystyle {\mathcal {M}}}
L
=
⟨
C
,
F
,
R
⟩
{\displaystyle {\mathcal {L}}=\langle C,F,{\mathcal {R}}\rangle }
D
{\displaystyle D}
(
.
)
M
{\displaystyle (.)^{\mathcal {M}}}
M
{\displaystyle {\mathcal {M}}}
c
M
∈
D
{\displaystyle c^{\mathcal {M}}\in D}
c
∈
C
{\displaystyle c\in C}
f
M
:
D
n
→
D
{\displaystyle f^{\mathcal {M}}:D^{n}\to D}
f
∈
F
{\displaystyle f\in F}
n
{\displaystyle n}
R
M
⊂
D
n
{\displaystyle R^{\mathcal {M}}\subset D^{n}}
R
∈
R
{\displaystyle R\in {\mathcal {R}}}
n
{\displaystyle n}
Det er altså en tolkning av alle de ikke-logiske symbolene inni domenet
D
{\displaystyle D}
Variabeltilordning og tolkning av termer
rediger
Før denne tolkningen kan løftes opp til alle termer, må en tolkning av variabler gis. En funksjon
δ
:
B
→
D
{\displaystyle \delta :\mathbb {B} \to D}
[
x
]
δ
M
=
δ
(
x
)
{\displaystyle [x]_{\delta }^{\mathcal {M}}=\delta (x)}
[
c
]
δ
M
=
c
M
{\displaystyle [c]_{\delta }^{\mathcal {M}}=c^{\mathcal {M}}}
[
f
(
t
1
,
…
,
t
n
)
]
δ
M
=
f
M
(
[
t
1
]
δ
M
,
…
,
[
t
n
]
δ
M
)
{\displaystyle [f(t_{1},\ldots ,t_{n})]_{\delta }^{\mathcal {M}}=f^{\mathcal {M}}([t_{1}]_{\delta }^{\mathcal {M}},\ldots ,[t_{n}]_{\delta }^{\mathcal {M}})}
Det at en formel
A
{\displaystyle A}
M
{\displaystyle {\mathcal {M}}}
δ
{\displaystyle \delta }
M
,
δ
⊨
A
{\displaystyle {\mathcal {M}},\delta \models A}
og er definert som følger:
M
,
δ
⊨
⊤
{\displaystyle {\mathcal {M}},\delta \models \top }
M
,
δ
⊨
⊥
{\displaystyle {\mathcal {M}},\delta \models \bot }
M
,
δ
⊨
R
(
t
1
,
…
,
t
n
)
{\displaystyle {\mathcal {M}},\delta \models R(t_{1},\ldots ,t_{n})}
⟨
[
t
1
]
δ
M
,
…
,
[
t
n
]
δ
M
⟩
∈
R
M
{\displaystyle \langle [t_{1}]_{\delta }^{\mathcal {M}},\ldots ,[t_{n}]_{\delta }^{\mathcal {M}}\rangle \in R^{\mathcal {M}}}
M
,
δ
⊨
¬
A
{\displaystyle {\mathcal {M}},\delta \models \neg A}
M
,
δ
⊨
A
{\displaystyle {\mathcal {M}},\delta \models A}
M
,
δ
⊨
A
∧
B
{\displaystyle {\mathcal {M}},\delta \models A\land B}
M
,
δ
⊨
A
{\displaystyle {\mathcal {M}},\delta \models A}
M
,
δ
⊨
B
{\displaystyle {\mathcal {M}},\delta \models B}
M
,
δ
⊨
A
∨
B
{\displaystyle {\mathcal {M}},\delta \models A\lor B}
M
,
δ
⊨
A
{\displaystyle {\mathcal {M}},\delta \models A}
M
,
δ
⊨
B
{\displaystyle {\mathcal {M}},\delta \models B}
M
,
δ
⊨
A
→
B
{\displaystyle {\mathcal {M}},\delta \models A\to B}
M
,
δ
⊨
A
{\displaystyle {\mathcal {M}},\delta \models A}
M
,
δ
⊨
B
{\displaystyle {\mathcal {M}},\delta \models B}
M
,
δ
⊨
∀
x
.
A
{\displaystyle {\mathcal {M}},\delta \models \forall x.\,A}
M
,
δ
[
x
↦
d
]
⊨
A
{\displaystyle {\mathcal {M}},\delta [x\mapsto d]\models A}
d
∈
D
{\displaystyle d\in D}
M
,
δ
⊨
∃
x
.
A
{\displaystyle {\mathcal {M}},\delta \models \exists x.\,A}
d
∈
D
{\displaystyle d\in D}
M
,
δ
[
x
↦
d
]
⊨
A
{\displaystyle {\mathcal {M}},\delta [x\mapsto d]\models A}
Basert på dette sier vi at en modell
M
{\displaystyle {\mathcal {M}}}
A
{\displaystyle A}
M
⊨
A
{\displaystyle {\mathcal {M}}\models A}
M
,
δ
⊨
A
{\displaystyle {\mathcal {M}},\delta \models A}
δ
{\displaystyle \delta }
Hvis
Γ
{\displaystyle \Gamma }
M
,
δ
⊨
Γ
{\displaystyle {\mathcal {M}},\delta \models \Gamma }
M
,
δ
⊨
A
{\displaystyle {\mathcal {M}},\delta \models A}
A
∈
Γ
{\displaystyle A\in \Gamma }
B
{\displaystyle B}
B
{\displaystyle B}
logisk konsekvens av
Γ
{\displaystyle \Gamma }
Γ
⊨
A
{\displaystyle \Gamma \models A}
M
{\displaystyle {\mathcal {M}}}
δ
{\displaystyle \delta }
M
,
δ
⊨
Γ
{\displaystyle {\mathcal {M}},\delta \models \Gamma }
M
,
δ
⊨
B
{\displaystyle {\mathcal {M}},\delta \models B}
Γ
=
∅
{\displaystyle \Gamma =\emptyset }
⊨
B
{\displaystyle \models B}
∅
⊨
B
{\displaystyle \emptyset \models B}
![{\displaystyle [x]_{\delta }^{\mathcal {M}}=\delta (x)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/fb93761587a35c342a5922a08cb9ad9612925e65)
![{\displaystyle [c]_{\delta }^{\mathcal {M}}=c^{\mathcal {M}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0c001b2936c55b775ec973a4fefe405f685da907)
![{\displaystyle [f(t_{1},\ldots ,t_{n})]_{\delta }^{\mathcal {M}}=f^{\mathcal {M}}([t_{1}]_{\delta }^{\mathcal {M}},\ldots ,[t_{n}]_{\delta }^{\mathcal {M}})}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f7be5282c5969a9857b0125637f7c0996dab842e)
![{\displaystyle \langle [t_{1}]_{\delta }^{\mathcal {M}},\ldots ,[t_{n}]_{\delta }^{\mathcal {M}}\rangle \in R^{\mathcal {M}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/9db44d3c78647e90e1c599e76c46c72be2ad617a)
![{\displaystyle {\mathcal {M}},\delta [x\mapsto d]\models A}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7db266f1423cde1b366018d91b819440ba1bdeee)
