Logika dla informatyków/Ćwiczenia 5

Ćwiczenie 1.

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

• (A3')  $(\mathrm{\neg }\phi \to \mathrm{\neg }\psi )\to ((\mathrm{\neg }\phi \to \psi )\to \phi ).$

Dowieść, że obydwa systemy są równoważne, tzn., że dla dowolnego sekwentu $\mathrm{\Delta }⊢\phi$, zachodzi $\mathrm{\Delta }{⊢}_H\phi$ , gdy $\mathrm{\Delta }{⊢}_{H_1}\phi$.

Ćwiczenie 2.

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

• (A3")  $(\mathrm{\neg }\phi \to \mathrm{\neg }\psi )\to (\psi \to \phi ).$

Dowieść, że obydwa systemy są równoważne, tzn., że dla dowolnego sekwentu $\mathrm{\Delta }⊢\phi$, zachodzi $\mathrm{\Delta }{⊢}_H\phi$ , gdy $\mathrm{\Delta }{⊢}_{H_2}\phi$.

Ćwiczenie 3.

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

Ćwiczenie 4.

Dowieść ${⊢}_H\mathrm{\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{\phi \to \psi \mathrm{\neg }\psi }{\mathrm{\neg }\phi }$

tzn. pokazać, że jeśli $\mathrm{\Delta }{⊢}_H\phi \to \psi$ oraz $\mathrm{\Delta }{⊢}_H\mathrm{\neg }\psi$, to również mamy $\mathrm{\Delta }{⊢}_H\mathrm{\neg }\phi$.

Ćwiczenie 6.

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

Ćwiczenie 7.

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

(a)\ $⊢\mathrm{\perp }\to p$;

(b)\ $p\to q,q\to r⊢p\to r$;

(c)\ $⊢(\mathrm{\neg }p\to p)\to p$;

(d)\ $p,\mathrm{\neg }p⊢q$;

(e)\ $p\to (q\to r)⊢q\to (p\to r)$;

(f)\ $⊢(\mathrm{\neg }p\to \mathrm{\neg }q)\to (q\to p)$;

(g)\ $⊢\mathrm{\neg }(p\wedge q)\to (\mathrm{\neg }p\vee \mathrm{\neg }q)$.

Ćwiczenie 8.

Dowieść, że jeśli $\mathrm{\Delta }{⊢}_N\phi$, to dla dowolnej formuły $\psi$ zachodzi $\mathrm{\Delta },\psi {⊢}_N\phi$.

Ćwiczenie 9.

Dowieść, że je¶li $\mathrm{\Delta }{⊢}_N\mathrm{\perp }$, to dla dowolnej formuły $\phi$ zachodzi $\mathrm{\Delta }{⊢}_N\phi$.

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

${⊢}_G$ dowie¶ć, że je¶li sekwent $\mathrm{\Delta }⊢\phi$ jest wyprowadzalny w tym systemie oraz $S$ jest podstawieniem formuł na zmienne zdaniowe, to sekwent $\overrightarrow{S}(\mathrm{\Delta })⊢S(\phi )$ powstaj±cy w wyniku podstawienia jest też wyprowadzalny w tym systemie.

Udowodnić, że w rachunku sekwentów zamiana reguły $(\vee$ -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}

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

Czy można to zrobić używaj±c tylko sekwentów postaci $\mathrm{\Delta }⊢\phi$ (z jedn± formuł± po prawej)?