Førsteordens logikk

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 ==


=== Førsteordens språk ===
Et førsteordens språk er et tripel 
  
    
      
        ⟨
        C
        ,
        F
        ,
        
          
            R
          
        
        ⟩
      
    
    {\displaystyle \langle C,F,{\mathcal {R}}\rangle }
  , hvor 
  
    
      
        C
        =
        {
        
          c
          
            1
          
        
        ,
        …
        }
      
    
    {\displaystyle C=\{c_{1},\ldots \}}
  
er en mengde konstantsymboler, 
  
    
      
        F
        =
        {
        
          f
          
            1
          
        
        ,
        …
        }
      
    
    {\displaystyle F=\{f_{1},\ldots \}}
   er en mengde funksjonssymboler,
og 
  
    
      
        
          
            R
          
        
        =
        {
        
          R
          
            1
          
        
        ,
        …
        }
      
    
    {\displaystyle {\mathcal {R}}=\{R_{1},\ldots \}}
   er en mengde relasjonssymboler.
Assosiert med hvert funksjon- og relasjonssymbol er ariteten, som er et naturlig tall som forteller hvor mange argumenter 
symbolet forventer. 
Disse symbolene kalles de ikke-logiske symbolene.


=== Førsteordens termer ===
Gitt et språk 
  
    
      
        
          
            L
          
        
        =
        ⟨
        C
        ,
        F
        ,
        
          
            R
          
        
        ⟩
      
    
    {\displaystyle {\mathcal {L}}=\langle C,F,{\mathcal {R}}\rangle }
   så er 
  
    
      
        
          
            L
          
        
      
    
    {\displaystyle {\mathcal {L}}}
  -termer definert induktivt
som:

Alle variabler 
  
    
      
        x
      
    
    {\displaystyle x}
   er 
  
    
      
        
          
            L
          
        
      
    
    {\displaystyle {\mathcal {L}}}
  -termer.
Alle konstantsymboler 
  
    
      
        c
        ∈
        C
      
    
    {\displaystyle c\in C}
   er 
  
    
      
        
          
            L
          
        
      
    
    {\displaystyle {\mathcal {L}}}
  -termer.
Hvis 
  
    
      
        f
        ∈
        F
      
    
    {\displaystyle f\in F}
   er et funksjonssymbol med aritet 
  
    
      
        n
      
    
    {\displaystyle n}
  , og 
  
    
      
        
          t
          
            1
          
        
      
    
    {\displaystyle t_{1}}
   til 
  
    
      
        
          t
          
            n
          
        
      
    
    {\displaystyle t_{n}}
   er 
  
    
      
        
          
            L
          
        
      
    
    {\displaystyle {\mathcal {L}}}
  -termer, så er 
  
    
      
        f
        (
        
          t
          
            1
          
        
        ,
        …
        ,
        
          f
          
            n
          
        
        )
      
    
    {\displaystyle f(t_{1},\ldots ,f_{n})}
   er 
  
    
      
        
          
            L
          
        
      
    
    {\displaystyle {\mathcal {L}}}
  -term.


=== Førsteordens formler ===
Gitt et språk 
  
    
      
        
          
            L
          
        
      
    
    {\displaystyle {\mathcal {L}}}
  , så er mengden med 
  
    
      
        
          
            L
          
        
      
    
    {\displaystyle {\mathcal {L}}}
  -formler definert induktivt som:

  
    
      
        ⊤
      
    
    {\displaystyle \top }
   er en 
  
    
      
        
          
            L
          
        
      
    
    {\displaystyle {\mathcal {L}}}
  -formel. Les topp eller sant (eng: top).

  
    
      
        ⊥
      
    
    {\displaystyle \bot }
   er en 
  
    
      
        
          
            L
          
        
      
    
    {\displaystyle {\mathcal {L}}}
  -formel. Les bunn eller usann (eng: bottom).
Hvis 
  
    
      
        R
        ∈
        
          
            R
          
        
      
    
    {\displaystyle R\in {\mathcal {R}}}
   er et relasjonssymbol med aritet 
  
    
      
        n
      
    
    {\displaystyle n}
  , og 
  
    
      
        
          t
          
            1
          
        
      
    
    {\displaystyle t_{1}}
   til 
  
    
      
        
          t
          
            n
          
        
      
    
    {\displaystyle t_{n}}
   er 
  
    
      
        
          
            L
          
        
      
    
    {\displaystyle {\mathcal {L}}}
  -termer, så er 
  
    
      
        R
        (
        
          t
          
            1
          
        
        ,
        …
        ,
        
          t
          
            n
          
        
        )
      
    
    {\displaystyle R(t_{1},\ldots ,t_{n})}
   en 
  
    
      
        
          
            L
          
        
      
    
    {\displaystyle {\mathcal {L}}}
  -formel.
Hvis 
  
    
      
        A
      
    
    {\displaystyle A}
   og 
  
    
      
        B
      
    
    {\displaystyle B}
   er 
  
    
      
        
          
            L
          
        
      
    
    {\displaystyle {\mathcal {L}}}
  -formeler og 
  
    
      
        x
      
    
    {\displaystyle x}
   er en variabel, så er følgende 
  
    
      
        
          
            L
          
        
      
    
    {\displaystyle {\mathcal {L}}}
  -formler:

  
    
      
        ¬
        A
      
    
    {\displaystyle \neg A}
  : negasjonen av 
  
    
      
        A
      
    
    {\displaystyle A}
  .

  
    
      
        A
        ∧
        B
      
    
    {\displaystyle A\land B}
  : konjunksjon. Les A og B.

  
    
      
        A
        ∨
        B
      
    
    {\displaystyle A\lor B}
  : disjunksjon. Les A eller B.

  
    
      
        A
        →
        B
      
    
    {\displaystyle A\to B}
  : implikasjon. Les hvis A, så B eller A impliserer B. (Notasjonen 
  
    
      
        A
        ⊃
        B
      
    
    {\displaystyle A\supset B}
   brukes også.)

  
    
      
        ∀
        x
        .
        
        A
      
    
    {\displaystyle \forall x.\,A}
  : all-kvantor. Les "for alle x, så holder A. Legg merke til at x kan forekomme som en variabel i A.

  
    
      
        ∃
        x
        .
        
        A
      
    
    {\displaystyle \exists x.\,A}
  : eksistens-kvantor. Les "det eksisterer en x, sånn at A holder". Igjen så kan x forekomme som en variabel i A.


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


=== Modell ===
En modell 
  
    
      
        
          
            M
          
        
      
    
    {\displaystyle {\mathcal {M}}}
   for et språk 
  
    
      
        
          
            L
          
        
        =
        ⟨
        C
        ,
        F
        ,
        
          
            R
          
        
        ⟩
      
    
    {\displaystyle {\mathcal {L}}=\langle C,F,{\mathcal {R}}\rangle }
   er en
ikke-tom mengde 
  
    
      
        D
      
    
    {\displaystyle D}
  , kalt domenet, sammen med en tolkning 
  
    
      
        (
        .
        
          )
          
            
              M
            
          
        
      
    
    {\displaystyle (.)^{\mathcal {M}}}
   av alle symbolene i 
  
    
      
        
          
            M
          
        
      
    
    {\displaystyle {\mathcal {M}}}
   slik at:

  
    
      
        
          c
          
            
              M
            
          
        
        ∈
        D
      
    
    {\displaystyle c^{\mathcal {M}}\in D}
   for alle konstansymboler 
  
    
      
        c
        ∈
        C
      
    
    {\displaystyle c\in C}
  .

  
    
      
        
          f
          
            
              M
            
          
        
        :
        
          D
          
            n
          
        
        →
        D
      
    
    {\displaystyle f^{\mathcal {M}}:D^{n}\to D}
   for alle funksjonssymboler 
  
    
      
        f
        ∈
        F
      
    
    {\displaystyle f\in F}
   med aritet 
  
    
      
        n
      
    
    {\displaystyle n}
  .

  
    
      
        
          R
          
            
              M
            
          
        
        ⊂
        
          D
          
            n
          
        
      
    
    {\displaystyle R^{\mathcal {M}}\subset D^{n}}
   for alle relasjonssymboler 
  
    
      
        R
        ∈
        
          
            R
          
        
      
    
    {\displaystyle R\in {\mathcal {R}}}
   med aritet 
  
    
      
        n
      
    
    {\displaystyle n}
  .Det er altså en tolkning av alle de ikke-logiske symbolene inni domenet 
  
    
      
        D
      
    
    {\displaystyle D}
  .


=== Variabeltilordning og tolkning av termer ===
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}
  
kalles en variabeltilordning. Gitt en variabeltilordning, så er det en unik funksjon som løfter tolkningen til alle termer:

  
    
      
        [
        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 ===
Det at en formel 
  
    
      
        A
      
    
    {\displaystyle A}
   er sann i en modell 
  
    
      
        
          
            M
          
        
      
    
    {\displaystyle {\mathcal {M}}}
   med en variabeltilordning 
  
    
      
        δ
      
    
    {\displaystyle \delta }
   skrives som

  
    
      
        
          
            M
          
        
        ,
        δ
        ⊨
        A
      
    
    {\displaystyle {\mathcal {M}},\delta \models A}
  .og er definert som følger:

  
    
      
        
          
            M
          
        
        ,
        δ
        ⊨
        ⊤
      
    
    {\displaystyle {\mathcal {M}},\delta \models \top }
   holder alltid.

  
    
      
        
          
            M
          
        
        ,
        δ
        ⊨
        ⊥
      
    
    {\displaystyle {\mathcal {M}},\delta \models \bot }
   holder aldri.

  
    
      
        
          
            M
          
        
        ,
        δ
        ⊨
        R
        (
        
          t
          
            1
          
        
        ,
        …
        ,
        
          t
          
            n
          
        
        )
      
    
    {\displaystyle {\mathcal {M}},\delta \models R(t_{1},\ldots ,t_{n})}
   holder hvis og bare hvis 
  
    
      
        ⟨
        [
        
          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}
   holder hvis og bare hvis 
  
    
      
        
          
            M
          
        
        ,
        δ
        ⊨
        A
      
    
    {\displaystyle {\mathcal {M}},\delta \models A}
   ikke holder.

  
    
      
        
          
            M
          
        
        ,
        δ
        ⊨
        A
        ∧
        B
      
    
    {\displaystyle {\mathcal {M}},\delta \models A\land B}
   holder hvis og bare hvis 
  
    
      
        
          
            M
          
        
        ,
        δ
        ⊨
        A
      
    
    {\displaystyle {\mathcal {M}},\delta \models A}
   holder og 
  
    
      
        
          
            M
          
        
        ,
        δ
        ⊨
        B
      
    
    {\displaystyle {\mathcal {M}},\delta \models B}
   holder.

  
    
      
        
          
            M
          
        
        ,
        δ
        ⊨
        A
        ∨
        B
      
    
    {\displaystyle {\mathcal {M}},\delta \models A\lor B}
   holder hvis og bare hvis 
  
    
      
        
          
            M
          
        
        ,
        δ
        ⊨
        A
      
    
    {\displaystyle {\mathcal {M}},\delta \models A}
   holder eller 
  
    
      
        
          
            M
          
        
        ,
        δ
        ⊨
        B
      
    
    {\displaystyle {\mathcal {M}},\delta \models B}
   holder.

  
    
      
        
          
            M
          
        
        ,
        δ
        ⊨
        A
        →
        B
      
    
    {\displaystyle {\mathcal {M}},\delta \models A\to B}
   holder hvis og bare hvis: hvis 
  
    
      
        
          
            M
          
        
        ,
        δ
        ⊨
        A
      
    
    {\displaystyle {\mathcal {M}},\delta \models A}
   holder, så holder 
  
    
      
        
          
            M
          
        
        ,
        δ
        ⊨
        B
      
    
    {\displaystyle {\mathcal {M}},\delta \models B}
  .

  
    
      
        
          
            M
          
        
        ,
        δ
        ⊨
        ∀
        x
        .
        
        A
      
    
    {\displaystyle {\mathcal {M}},\delta \models \forall x.\,A}
   holder hvis og bare hvis 
  
    
      
        
          
            M
          
        
        ,
        δ
        [
        x
        ↦
        d
        ]
        ⊨
        A
      
    
    {\displaystyle {\mathcal {M}},\delta [x\mapsto d]\models A}
   holder for alle 
  
    
      
        d
        ∈
        D
      
    
    {\displaystyle d\in D}
  .

  
    
      
        
          
            M
          
        
        ,
        δ
        ⊨
        ∃
        x
        .
        
        A
      
    
    {\displaystyle {\mathcal {M}},\delta \models \exists x.\,A}
   holder hvis og bare hvis: det eksisterer en 
  
    
      
        d
        ∈
        D
      
    
    {\displaystyle d\in D}
   slik at 
  
    
      
        
          
            M
          
        
        ,
        δ
        [
        x
        ↦
        d
        ]
        ⊨
        A
      
    
    {\displaystyle {\mathcal {M}},\delta [x\mapsto d]\models A}
   holder.Basert på dette sier vi at en modell 
  
    
      
        
          
            M
          
        
      
    
    {\displaystyle {\mathcal {M}}}
   oppfyller en formel 
  
    
      
        A
      
    
    {\displaystyle A}
  , notasjon 
  
    
      
        
          
            M
          
        
        ⊨
        A
      
    
    {\displaystyle {\mathcal {M}}\models A}
  ,
hvis 
  
    
      
        
          
            M
          
        
        ,
        δ
        ⊨
        A
      
    
    {\displaystyle {\mathcal {M}},\delta \models A}
   for alle variabel-tilordninger 
  
    
      
        δ
      
    
    {\displaystyle \delta }
  .
Hvis 
  
    
      
        Γ
      
    
    {\displaystyle \Gamma }
   er en mengde formler, så skriver vi 
  
    
      
        
          
            M
          
        
        ,
        δ
        ⊨
        Γ
      
    
    {\displaystyle {\mathcal {M}},\delta \models \Gamma }
   hvis 
  
    
      
        
          
            M
          
        
        ,
        δ
        ⊨
        A
      
    
    {\displaystyle {\mathcal {M}},\delta \models A}
   for alle 
  
    
      
        A
        ∈
        Γ
      
    
    {\displaystyle A\in \Gamma }
  .
Videre, hvis 
  
    
      
        B
      
    
    {\displaystyle B}
   er en formel, så er 
  
    
      
        B
      
    
    {\displaystyle B}
   en logisk konsekvens av 
  
    
      
        Γ
      
    
    {\displaystyle \Gamma }
  , notasjon 
  
    
      
        Γ
        ⊨
        A
      
    
    {\displaystyle \Gamma \models A}
  ,
hvis for alle modeller 
  
    
      
        
          
            M
          
        
      
    
    {\displaystyle {\mathcal {M}}}
   og tilordninger 
  
    
      
        δ
      
    
    {\displaystyle \delta }
  , så impliserer 
  
    
      
        
          
            M
          
        
        ,
        δ
        ⊨
        Γ
      
    
    {\displaystyle {\mathcal {M}},\delta \models \Gamma }
   at 
  
    
      
        
          
            M
          
        
        ,
        δ
        ⊨
        B
      
    
    {\displaystyle {\mathcal {M}},\delta \models B}
   holder.
Et særtilfelle er når 
  
    
      
        Γ
        =
        ∅
      
    
    {\displaystyle \Gamma =\emptyset }
  , hvor man kun skriver 
  
    
      
        ⊨
        B
      
    
    {\displaystyle \models B}
   i stede for 
  
    
      
        ∅
        ⊨
        B
      
    
    {\displaystyle \emptyset \models B}
  .


== Kalkyler ==
Det finnes flere forskjellige kalkyler. I motsetning til semantiske modeller, så fanger kalkyler inn meningen til formelen ved syntaktiske ressonement.
Mest kjent er naturlig deduksjon, sekventkalkyle og Hilbert system.
Man skriver gjerne 
  
    
      
        Γ
        ⊢
        A
      
    
    {\displaystyle \Gamma \vdash A}
   hvis
det finnes en utledig i en gitt kalkyle for 
  
    
      
        A
      
    
    {\displaystyle A}
   fra antagelsene 
  
    
      
        Γ
      
    
    {\displaystyle \Gamma }
  .
Det er tre viktige egenskaper en kalkyle kan besitte:

Konsistent: Det er umulig å gi en utledning for 
  
    
      
        ⊢
        ⊥
      
    
    {\displaystyle \vdash \bot }
  .
Sunn: Hvis 
  
    
      
        Γ
        ⊢
        A
      
    
    {\displaystyle \Gamma \vdash A}
  , så 
  
    
      
        Γ
        ⊨
        A
      
    
    {\displaystyle \Gamma \models A}
  .
Komplett: Hvis 
  
    
      
        Γ
        ⊨
        A
      
    
    {\displaystyle \Gamma \models A}
  , så 
  
    
      
        Γ
        ⊢
        A
      
    
    {\displaystyle \Gamma \vdash A}
  .


== Litteratur ==
Dirk Van Dalen. Logic and Structure, Universitext. ISBN 978-3-540-20879-2.