Redigerer Førsteordens logikk (avsnitt)

== Modellteori for førsteordens logikk ==
En standard måte å beskrive modeller for førsteordens logikk på er som følger. 

=== Modell ===
En modell <math>\mathcal{M}</math> for et språk <math>\mathcal{L} = \langle C, F, \mathcal{R}\rangle </math> er en
ikke-tom mengde <math>D</math>, kalt domenet, sammen med en tolkning <math>(.)^\mathcal{M}</math> av alle symbolene i <math>\mathcal{M}</math> slik at:
* <math>c^\mathcal{M} \in D</math> for alle konstansymboler <math>c \in C</math>.
* <math>f^\mathcal{M} : D^n \to D</math> for alle funksjonssymboler <math>f \in F</math> med aritet <math>n</math>.
* <math>R^\mathcal{M} \subset D^n</math> for alle relasjonssymboler <math>R \in \mathcal{R}</math> med aritet <math>n</math>.
Det er altså en tolkning av alle de ikke-logiske symbolene inni domenet <math>D</math>.

=== Variabeltilordning og tolkning av termer ===
Før denne tolkningen kan ''løftes'' opp til alle termer, må en tolkning av variabler gis. En funksjon <math>\delta : \mathbb{B} \to D</math>
kalles en variabeltilordning. Gitt en variabeltilordning, så er det en unik funksjon som løfter tolkningen til alle termer:
* <math>[x]^\mathcal{M}_\delta = \delta(x)</math>.
* <math>[c]^\mathcal{M}_\delta = c^\mathcal{M}</math>.
* <math> [f(t_1, \ldots, t_n)]^\mathcal{M}_\delta = f^\mathcal{M}([t_1]^\mathcal{M}_\delta, \ldots, [t_n]^\mathcal{M}_\delta)</math>.

=== Tolkning av formler ===
Det at en formel <math>A</math> er sann i en modell <math>\mathcal{M}</math> med en variabeltilordning <math>\delta</math> skrives som
:<math> \mathcal{M}, \delta \models A</math>.
og er definert som følger:
* <math> \mathcal{M}, \delta \models \top</math> holder alltid.
* <math> \mathcal{M}, \delta \models \bot</math> holder aldri.
* <math> \mathcal{M}, \delta \models R(t_1, \ldots, t_n)</math> holder hvis og bare hvis <math>\langle [t_1]^\mathcal{M}_\delta, \ldots, [t_n]^\mathcal{M}_\delta\rangle \in R^\mathcal{M}</math>.
* <math> \mathcal{M}, \delta \models \neg A</math> holder hvis og bare hvis <math> \mathcal{M}, \delta \models A</math> ikke holder.
* <math> \mathcal{M}, \delta \models A \land B</math> holder hvis og bare hvis <math> \mathcal{M}, \delta \models A</math> holder og <math> \mathcal{M}, \delta \models B</math> holder.
* <math> \mathcal{M}, \delta \models A \lor B</math> holder hvis og bare hvis <math> \mathcal{M}, \delta \models A</math> holder eller <math> \mathcal{M}, \delta \models B</math> holder.
* <math> \mathcal{M}, \delta \models A \to B</math> holder hvis og bare hvis: hvis <math> \mathcal{M}, \delta \models A</math> holder, så holder <math> \mathcal{M}, \delta \models B</math>.
* <math> \mathcal{M}, \delta \models \forall x. \, A</math> holder hvis og bare hvis <math> \mathcal{M}, \delta[x \mapsto d] \models A</math> holder for alle <math> d \in D</math>.
* <math> \mathcal{M}, \delta \models \exists x.\, A</math> holder hvis og bare hvis: det eksisterer en <math> d \in D</math> slik at <math> \mathcal{M}, \delta[x \mapsto d] \models A</math> holder.

Basert på dette sier vi at en modell <math>\mathcal{M}</math> oppfyller en formel <math>A</math>, notasjon <math> \mathcal{M} \models A</math>,
hvis <math>\mathcal{M}, \delta \models A</math> for alle variabel-tilordninger <math>\delta</math>.

Hvis <math>\Gamma</math> er en mengde formler, så skriver vi <math>\mathcal{M}, \delta \models \Gamma</math> hvis <math>\mathcal{M}, \delta \models A</math> for alle <math>A \in \Gamma</math>.
Videre, hvis <math>B</math> er en formel, så er <math>B</math> en ''logisk konsekvens'' av <math>\Gamma</math>, notasjon <math>\Gamma \models A</math>,
hvis for alle modeller <math>\mathcal{M}</math> og tilordninger <math>\delta</math>, så impliserer <math>\mathcal{M}, \delta \models \Gamma</math> at <math>\mathcal{M}, \delta \models B</math> holder.
Et særtilfelle er når <math>\Gamma = \emptyset</math>, hvor man kun skriver <math> \models B</math> i stede for <math>\emptyset \models B</math>.