Førsteordens logikk

Fra Wikipedia, den frie encyklopedi
Hopp til navigering Hopp til søk

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 | rediger kilde]

Førsteordens språk[rediger | rediger kilde]

Et førsteordens språk er et tripel , hvor er en mengde konstantsymboler, er en mengde funksjonssymboler, og 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[rediger | rediger kilde]

Gitt et språk så er -termer definert induktivt som:

  • Alle variabler er -termer.
  • Alle konstantsymboler er -termer.
  • Hvis er et funksjonssymbol med aritet , og til er -termer, så er er -term.

Førsteordens formler[rediger | rediger kilde]

Gitt et språk , så er mengden med -formler definert induktivt som:

  • er en -formel. Les topp eller sant (eng: top).
  • er en -formel. Les bunn eller usann (eng: bottom).
  • Hvis er et relasjonssymbol med aritet , og til er -termer, så er en -formel.
  • Hvis og er -formeler og er en variabel, så er følgende -formler:
    • : negasjonen av .
    • : konjunksjon. Les A og B.
    • : disjunksjon. Les A eller B.
    • : implikasjon. Les "hvis A, så B eller A impliserer B. (Notasjonen brukes også.)
    • : all-kvantor. Les "for alle x, så holder A. Legg merke til at x kan forekomme som en variabel i 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[rediger | rediger kilde]

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

Modell[rediger | rediger kilde]

En modell for et språk er en ikke-tom mengde , kalt domenet, sammen med en tolkning av alle symbolene i slik at:

  • for alle konstansymboler .
  • for alle funksjonssymboler med aritet .
  • for alle relasjonssymboler med aritet .

Det er altså en tolkning av alle de ikke-logiske symbolene inni domenet .

Variabeltilordning og tolkning av termer[rediger | rediger kilde]

Før denne tolkningen kan løftes opp til alle termer, må en tolkning av variabler gis. En funksjon kalles en variabeltilordning. Gitt en variabeltilordning, så er det en unik funksjon som løfter tolkningen til alle termer:

  • .
  • .
  • .

Tolkning av formler[rediger | rediger kilde]

Det at en formel er sann i en modell med en variabeltilordning skrives som

.

og er definert som følger:

  • holder alltid.
  • holder aldri.
  • holder hvis og bare hvis .
  • holder hvis og bare hvis ikke holder.
  • holder hvis og bare hvis holder og holder.
  • holder hvis og bare hvis holder eller holder.
  • holder hvis og bare hvis: hvis holder, så holder .
  • holder hvis og bare hvis holder for alle .
  • holder hvis og bare hvis: det eksisterer en slik at holder.

Basert på dette sier vi at en modell oppfyller en formel , notasjon , hvis for alle variabel-tilordninger .

Hvis er en mengde formler, så skriver vi hvis for alle . Videre, hvis er en formel, så er en logisk konsekvens av , notasjon , hvis for alle modeller og tilordninger , så impliserer at holder. Et særtilfelle er når , hvor man kun skriver i stede for .

Kalkyler[rediger | rediger kilde]

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 hvis det finnes en utledig i en gitt kalkyle for fra antagelsene .

Det er tre viktige egenskaper en kalkyle kan besitte:

  • Konsistent: Det er umulig å gi en utledning for .
  • Sunn: Hvis , så .
  • Komplett: Hvis , så .

Litteratur[rediger | rediger kilde]

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