OBS! Denne artikel får stadig besøg ind i mellem. Den er ikke blevet opdateret siden jeg skrev den. Der er en masse tegn i artiklen der ikke er korrekt formateret. Indholdet her er i stedet på vej over på min engelsksprogede del af siden: https://brkmnd.com/pages/logic/Default.aspx?id=11.
Bevisteori for prædikatlogik givet ved naturlig deduktion og tilhørende slutningsregler.
Beviser kan laves på ProofWeb.
Lighed - introduktion =i
der gælder for en term, t. Reglen siger at en term er lig sig selv. Reglen gælder uden præmisser og er derfor et aksiom.
Lighed - elimination =e
Hvor t1 og t2 skal være fri for x i φ.
Eksempel(1)
Reglen =e siger at med en lighed som præmis kan vi substituere.
Vi kan nu vise de to sidste egenskaber ved en ækvivalensrelation, nemlig:
og = er en ækvivalensrelation.
Alkvantor - elimination
der siger, at hvis ∀x φ er sand, kan vi konludere at φ[t/x] er sand. Reglen giver intuitivt god mening: ved vi at noget gælder for alle x, gælder det selvfølgeligt også for et specifikt/konkret tilfælde, t. Her skal t igen være fri for x i φ.
Eksempel(2)
Som et eksempel på hvornår det giver kvaler at substituere når t ikke er fri for x i φ:
Lad %phi = \exist y(x .lt y), og lad os snakke om heltal.
Vi kan feks. skrive: \forall x %phi som siger at der for alle heltal, x, eksisterer et y der er større. Dette er sandt.
Men hvis vi skriver %phi[y/x], får vi \exist y(y .lt y), altså at der eksisterer et heltal, y, der er mindre end sig selv. Dette er løgn.
Alkvantor - introduktion
Der siger, at kan vi antage et arbitrært x0 og bevise φ med dette, kan vi slutte ∀x φ. Ideen er at dette x0 er arbitrært og ikke forekommer andre steder. Siden vi ikke har antaget andet om dette x0, kan vi generalisere med det. Denne regel er ikke så intuitiv som eliminationsreglen.
Eksempel(3)
Vi vil gerne vise \forall x(P(x) .drarrow Q(x)), \forall x P(x) .assert \forall x Q(x)
Ideen er at vi pakker præmisserne ud af kvantorerne ved at bruge specialtilældet x0. Da begge præmisser gælder for alle x, gælder de også for et arbitrært x0. Dette x0 kan så bruges i konklusionen.
Eksistenskvantor - introduktion
Reglen siger blot at med et konkret t kan vi slutte at der eksisterer et x for hvilket φ gælder.
Eksistenskvantor - elimination
Reglen siger: Vi ved at der eksisterer et x for hvilket φ er sand. Hvis φ[x0/x] tillader os at bevise et Χ, må Χ være sand i de tilfælde x0 gør φ[x0/x] sand.
Eksempel(4)
Vi vil vise \forall x(P(x) .drarrow Q(x)), \exist x P(x) .assert \exist x Q(x)
Præmis nummer 2 skal eliminires hvilket er skyld i antagelsen P(x0). Nederst i scopet under x0 bruges ∃ i. Dette gøres sådan da x0 ikke kan fanges uden for scopet.
Eksempel(4a)
Vi vil vise \forall x(Q(x) .drarrow R(x)), \exist x(P(x) .and Q(x)) .assert \exist x(P(x) .and R(x))
Eksempel(4b)
Vi vil vise \exist x P(x), \forall x\forall y(P(x) .drarrow Q(y)) .assert \forall y Q(y)
...