Prædikatlogik : Bevisteori - Nørderier/Teori

Bevisteori for prædikatlogik givet ved naturlig deduktion og tilhørende slutningsregler.

Beviser kan laves på ProofWeb.

Lighed

Lighed - introduktion =i

{ }over{t = t}

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

{t_1=t_2 %phi[t_1/x]}over{%phi[t_2/x]}

Hvor t1 og t2 skal være fri for x i φ.

Eksempel(1)

(x + 1) = (1 + x) CN_(premis) (x + 1 .gt 1) .drarrow (x + 1 .gt 0) CN_(premis) (1 + x .gt 1) .drarrow (1 + x .gt 0) CN_(= e)

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:

t_1 = t_2 .drarrow t_2 = t_1 CN_(Symmetri) t_1 = t_2 .and t_2 = t_3 .drarrow t_1 = t_3 CN_(Transitivitet) (Symmetri) t_1 = t_2 CN_(præmis) t_1 = t_1 CN_(=i) t_2 = t_1 CN_(=e) (Transitivitet) t_1 = t_2 CN_(præmis) t_2 = t_3 CN_(præmis) t_1 = t_3 CN_(=e)

og = er en ækvivalensrelation.

Alkvantor

Alkvantor - elimination

{\forall x %phi}over{%phi[t/x]}

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

{x_0 ... %phi[x_0/x]}over{\forall x %phi}

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)

\forall x(P(x) .imp Q(x)) __(præmis) \forall x P(x) __(præmis) .scopeStart x_0 __(scope) P(x_0) .imp Q(x_0) __(.forall e) P(x_0) __(.forall e) Q(x_0) __(.imp e) .scopeSlut \forall x Q(x) __(.forall i)

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.

Eskistenskvantor

Eksistenskvantor - introduktion

{%phi[t/x]}over{\exist x %phi}

Reglen siger blot at med et konkret t kan vi slutte at der eksisterer et x for hvilket φ gælder.

Eksistenskvantor - elimination

{\exist x %phi, %phi[x_0/x] ... %Chi}over{%Chi}

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)

\forall x(P(x) .imp Q(x)) __(præmis) \exist x P(x) __(præmis) .scopeStart x_0 __(scope) P(x_0) __(antagelse) P(x_0) .imp Q(x_0) __(.forall e) Q(x_0) __(.imp e) \exist x Q(x) __(.exist i) .scopeSlut \exist x Q(x) __(.exist e)

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

\forall x(Q(x) .imp R(x)) __(præmis) \exist x(P(x) .and Q(x)) __(præmis) .scopeStart x_0 __(scope) P(x_0) .and Q(x_0) __(antagelse) P(x_0) __(.and e) Q(x_0) __(.and e) Q(x_0) .imp R(x_0) __(.forall e) R(x_0) __(.imp e) P(x_0) .and R(x_0) __(.and i) \exist x (P(x) .and R(x)) __(.exist i) .scopeSlut \exist x (P(x) .and R(x)) __(.exist e)

Eksempel(4b)

Vi vil vise \exist x P(x), \forall x\forall y(P(x) .drarrow Q(y)) .assert \forall y Q(y)

\exist x P(x) __(præmis) \forall x\forall y(P(x) .imp Q(y)) __(præmis) .scopeStart y_0 __(scope) .scopeStart x_0 __(scope) P(x_0) __(antagelse) \forall y (P(x_0) .imp Q(y)) __(\forall x e) P(x_0) .imp Q(y_0) __(\forall y e) Q(y_0) __(.imp e) .scopeSlut Q(y_0) __(\exist x e) .scopeSlut \forall y Q(y) __(\forall y i)

...