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]
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.
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.
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.
En standard måte å beskrive modeller for førsteordens logikk på er som følger.
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:
.
.
.
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
.
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å
.
Dirk Van Dalen. Logic and Structure, Universitext. ISBN 978-3-540-20879-2.