Førsteordens predikatlogikk er i logikk et språk, med tilhørende semantikker og kalkyler, som beskriver objekter og deres relasjon til hverandre.
Førsteordens språk, termer og formler
rediger
Førsteordens språk
rediger
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.
Førsteordens termer
rediger
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}}} Førsteordens formler
rediger
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} Modellteori for førsteordens logikk
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}})} Tolkning av formler
rediger
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)
