1a) A | -(A & -A) ------------- S | S F F F | S F S tautologi, satisfierbar 1b) A B | (A -> (B -> A)) -> B -------------------------- S S | S S S S F | S S F F S | S F S F F | S S F satisfierbar 1c) A B C | ((A | B) & (B -> C)) -> (-A <-> C) ------------------------------------------ S S S | S S S F F F S S F | S F F S F S S F S | S S S F F F S F F | S S S S F S F S S | S S S S S S F S F | S F F S S F F F S | F F S S S S F F F | F F S S S F satisfierbar 2a) 1 A -> B P 2 -A -> C P 3 -B P 4 o- A P 5 | B 1,4 (->E) 6 | false 3,5 (false I) 7 o--- 8 -A 4-7 (-I) 9 C 2,9 (->E) 10 -A & C 8,9 (&I) 2b) 1 A | (B | C) P 2 A -> B & C P 3 B -> C P 4 o- A P 5 | B & C 2,4 (->E) 6 | C 5 (&E) 7 o--- 8 A -> C 4-7 (->I) 9 o- B | C P 10 | o- B P 11 | | C 3,10 (->E) 12 | o--- 13 | B -> C 10-12 (->I) 14 | o- C P 15 | o--- 16 | C -> C 14-15 (->I) 17 | C 9,13,16 (|E) 18 o--- 19 (B | C) -> C 9-18 (->I) 20 C 1,8,19 (|E) 2c) 1 o -(A | -A) P 2 | o- A P 3 | | A | -A 2 (|I) 4 | | false 1,3 (false I) 5 | o--- 6 | -A 2-5 (-I) 7 | A | -A 6 (|I) 8 | false 1,7 (false I) 9 o--- 10 A | -A 1-9 (-E) 3a) Ax (Planet(x) -> Ey (KretsarKring(x,y) & Stjärna(y))) 3b) Ey Ax (Människa(x) -> BorPå(x,y) & Planet(y)) 3c) Planet(jorden) & Beboelig(jorden) & -Ex (Planet(x) & Beboelig(x) & x != jorden) 4a) 1 Stålman(clark) & Ax (Stålman(x) -> x = clark) P 2 -(jimmy = clark) P 3 o- Stålman(jimmy) P 4 | Stålman(clark) 1 (&E) 5 | Ax (Stålman(x) -> x = clark) 1 (&E) 6 | Stålman(jimmy) -> jimmy = clark 5 (AE) 7 | jimmy = clark 3,6 (->E) 8 | false 2,7 (false I) 9 o--- 10 -Stålman(jimmy) 3-9 (-I) 4b) ==> 1 -Ex P(x) P 2 o- P(x) P 3 | Ex P(x) 2 (EI) 4 | false 1,3 (false I) 5 o--- 6 -P(x) 2-5 (-I) 7 Ax -P(x) 6 (AI) <== 1 Ax -P(x) P 2 o- Ex P(x) P 3 | o- P(x) P 4 | | -P(x) 1 (AE) 5 | | false 3,4 (false I) 6 | o--- 7 | false 2,3-5 (EE) 8 o--- 9 -Ex P(x) 2-8 (-I) 5a) m = (M,V) M = {a,b} V(P) = {a} V(Q) = {b} 5b) m = (M,V) M = {a,b,c} V(a) = a V(b) = b V(c) = c V(P) = {,,} 5c) m = (M,V) M = {0,1,2,...} V(0) = 0 V(f) = addition 6a) Formalisering: -Ex (-Myndig(x) & FårKöraBil(x)), Myndig(john) |= FårKöraBil(john) Men följande modell motbevisar detta. m = (M,V) M = {john} V(john) = John V(Myndig) = {John} V(FårKöraBil) = {} 6b) Formalisering: Ax (Bil(x) & -Besiktigad(x) -> Körförbud(x)), Ey (Äger(john,y) & Bil(y) & -Körförbud(y)) |= Ez (Äger(john,z) & Bil(z) & Besiktigad(z)) Bevis: 1 Ax (Bil(x) & -Besiktigad(x) -> Körförbud(x)) P 2 Ey (Äger(john,y) & Bil(y) & -Körförbud(y)) P 3 o- Äger(john,y) & Bil(y) & -Körförbud(y) P 4 | Bil(y) & -Besiktigad(y) -> Körförbud(y) 1 (AE) 5 | Bil(y) 4 (&E) 6 | o- -Besiktigad(y) P 7 | | Bil(y) & -Besiktigad(y) 5,6 (&I) 8 | | Körförbud(y) 4,7 (->E) 9 | | -Körförbud(y) 3 (&E) 10 | | false 8,9 (false I) 11 | o--- 12 | Besiktigad(y) 6-11 (-E) 13 | Äger(john,y) 3 (&E) 14 | Äger(john,y) & Bil(y) & Besiktigad(y) 5,12,13 (&I) 15 | Ez (Äger(john,z) & Bil(z) & Besiktigad(z)) 14 (EI) 16 o--- 17 Ez (Äger(john,z) & Bil(z) & Besiktigad(z)) 2,3-16 (EE) 7) Om A |= B så satisfieras B av alla modeller som satisfierar A. Om A |- B så finns det ett bevis för B från A i naturlig deduktion. (Bonus: Eftersom naturlig deduktion är ett fullständigt bevissystem så gäller dessa två relationer mellan samma formler.)