Logika dla informatyków/Ćwiczenia 5: Różnice pomiędzy wersjami

Wersja z 21:32, 21 wrz 2006

Ćwiczenie 1.

Niech $⊢_{H_{1}}$ oznacza system dowodzenia otrzymany z systemu $⊢_{H}$ przez zamianę aksjomatu (A3) na następujący aksjomat:

(A3') $(\neg φ \to \neg ψ) \to ((\neg φ \to ψ) \to φ) .$

Dowieść, że obydwa systemy są równoważne, tzn., że dla dowolnego sekwentu $Δ ⊢ φ$ , zachodzi $Δ ⊢_{H} φ$ , gdy $Δ ⊢_{H_{1}} φ$ .

Ćwiczenie 2.

Niech $⊢_{H_{2}}$ oznacza system dowodzenia otrzymany z systemu $⊢_{H}$ przez zamianę aksjomatu (A3) na $⊢_{H}$ , następujący aksjomat:

(A3") $(\neg φ \to \neg ψ) \to (ψ \to φ) .$

Dowieść, że obydwa systemy są równoważne, tzn., że dla dowolnego sekwentu $Δ ⊢ φ$ , zachodzi $Δ ⊢_{H} φ$ , gdy $Δ ⊢_{H_{2}} φ$ .

Ćwiczenie 3.

Dowieść, że aksjomatu (A3) nie da się wyprowadzić z aksjomatów (A0-2) przy pomocy reguły odrywania.

Ćwiczenie 4.

Dowieść $⊢_{H} \neg p \to (p \to q)$ używając twierdzenia o dedukcji oraz bez użycia tego twierdzenia.

Ćwiczenie 5.

Pokazać, że w systemie $⊢_{H}$ dopuszczalna jest następująca reguła:

\frac{φ \to ψ \neg ψ}{\neg φ}

tzn. pokazać, że jeśli $Δ ⊢_{H} φ \to ψ$ oraz $Δ ⊢_{H} \neg ψ$ , to również mamy $Δ ⊢_{H} \neg φ$ .

Ćwiczenie 6.

Dowieść, że dla każdej formuły $φ$ , nie będącej tautologią, istnieje maksymalny zbiór formuł $Δ$ (nad daną sygnaturą) o tej własności, że $Δ ⊢_{H} φ$ .

Ćwiczenie 7.

Każdy z poniższych sekwentów wyprowadzić w systemie $⊢_{H^{+}}$ , $⊢_{N}$ , $⊢_{G}$ .

(a)\

⊢ ⊥ \to p

;

(b)\

p \to q, q \to r ⊢ p \to r

;

(c)\

⊢ (\neg p \to p) \to p

;

(d)\

p, \neg p ⊢ q

;

(e)\

p \to (q \to r) ⊢ q \to (p \to r)

;

(f)\

⊢ (\neg p \to \neg q) \to (q \to p)

;

(g)\

⊢ \neg (p \land q) \to (\neg p \lor \neg q)

.

Ćwiczenie 8.

Dowieść, że jeśli $Δ ⊢_{N} φ$ , to dla dowolnej formuły $ψ$ zachodzi $Δ, ψ ⊢_{N} φ$ .

Ćwiczenie 9.

Dowieść, że je¶li $Δ ⊢_{N} ⊥$ , to dla dowolnej formuły $φ$ zachodzi $Δ ⊢_{N} φ$ .

Dla każdego z sytemów $⊢_{H^{+}}$ , $⊢_{N}$ ,

$⊢_{G}$ dowie¶ć, że je¶li sekwent $Δ ⊢ φ$ jest wyprowadzalny w tym systemie oraz $S$ jest podstawieniem formuł na zmienne zdaniowe, to sekwent $\vec{S} (Δ) ⊢ S (φ)$ powstaj±cy w wyniku podstawienia jest też wyprowadzalny w tym systemie.

Udowodnić, że w rachunku sekwentów zamiana reguły  $(\lor$  -prawa  $)$

na dwie reguły:

Parser nie mógł rozpoznać (nieznana funkcja „\prooftree”): {\displaystyle \displaystyle \prooftree{\Delta\vdash\Gamma,\varphi} \justifies{\Delta\vdash\Gamma,\varphi\vee\psi} \endprooftree \hspace{3cm} \prooftree{\Delta\vdash\Gamma,\psi} \justifies{\Delta\vdash\Gamma,\varphi\vee\psi} \endprooftree}

daje w wyniku równoważny system dowodzenia (wyprowadzalne s± te same sekwenty).

Udowodnić, że następuj±ce reguły osłabiania s± dopuszczalne w rachunku sekwentów:

Parser nie mógł rozpoznać (nieznana funkcja „\prooftree”): {\displaystyle \displaystyle \prooftree{\Delta\vdash\Gamma}\justifies{\Delta,\varphi\vdash\Gamma} \endprooftree \hspace{3cm} \prooftree{\Delta\vdash\Gamma}\justifies{\Delta\vdash\Gamma,\varphi} \endprooftree}

Wyprowadzić w rachunku sekwentów:
1. $⊢ p \lor \neg p$ ;
2. $⊢ ((p \to q) \to p) \to p$ .

Czy można to zrobić używaj±c tylko sekwentów postaci $Δ ⊢ φ$ (z jedn± formuł± po prawej)?

@@ Linia 61: / Linia 61: @@
 Każdy z poniższych sekwentów wyprowadzić w  systemie
 <math>\displaystyle \vdash_{H^+}</math>, <math>\displaystyle \vdash_{N}</math>, <math>\displaystyle \vdash_G</math>.
- <nowiki> =</nowiki>   2pt
-:(a)<math>\displaystyle \vdash \bot\to p</math>;
+:(a)\ <math>\displaystyle \vdash \bot\to p</math>;
-## <math>\displaystyle p\arr q,q\arr r\vdash p\arr r</math>;
+:(b)\ <math>\displaystyle p\to q,q\to r\vdash p\to r</math>;
-## <math>\displaystyle \vdash(\neg p\arr p)\arr p</math>;
+:(c)\ <math>\displaystyle \vdash(\neg p\to p)\to p</math>;
-## <math>\displaystyle p,\neg p\vdash q</math>;
+:(d)\ <math>\displaystyle p,\neg p\vdash q</math>;
-## <math>\displaystyle p\arr(q\arr r)\vdash q\arr(p\arr r)</math>;
+:(e)\ <math>\displaystyle p\to(q\to r)\vdash q\to(p\to r)</math>;
-## <math>\displaystyle \vdash (\neg p\arr \neg q)\arr (q\arr p)</math>;
+:(f)\ <math>\displaystyle \vdash (\neg p\to \neg q)\to (q\to p)</math>;
-## <math>\displaystyle \vdash \neg(p\wedge q)\arr(\neg p\vee\neg q)</math>.
+:(g)\ <math>\displaystyle \vdash \neg(p\wedge q)\to(\neg p\vee\neg q)</math>.
-# Dowie¶ć, że je¶li <math>\displaystyle \Delta\vdash_{N}\varphi</math>, to dla dowolnej
+Ćwiczenie 8.
+Dowieść, że jeśli <math>\displaystyle \Delta\vdash_{N}\varphi</math>, to dla dowolnej
 formuły <math>\displaystyle \psi</math> zachodzi <math>\displaystyle \Delta,\psi\vdash_{N}\varphi</math>.
-# Dowie¶ć, że je¶li <math>\displaystyle \Delta\vdash_{N}\bot</math>, to dla dowolnej
+Ćwiczenie 9.
+Dowieść, że je¶li <math>\displaystyle \Delta\vdash_{N}\bot</math>, to dla dowolnej
 formuły <math>\displaystyle \varphi</math> zachodzi <math>\displaystyle \Delta\vdash_{N}\varphi</math>.
 # Dla każdego z sytemów <math>\displaystyle \vdash_{H^+}</math>, <math>\displaystyle \vdash_{N}</math>,

Logika dla informatyków/Ćwiczenia 5: Różnice pomiędzy wersjami

Wersja z 21:32, 21 wrz 2006

Menu nawigacyjne

Działania na stronie

Opcje strony

Narzędzia osobiste

Nawigacja

Szukaj

Narzędzia