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$.

 =   2pt

1. 1. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vdash \bot\arr p} ;
   2. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle p\arr q,q\arr r\vdash p\arr r} ;
   3. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vdash(\neg p\arr p)\arr p} ;
   4. $p,\mathrm{\neg }p⊢q$;
   5. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle p\arr(q\arr r)\vdash q\arr(p\arr r)} ;
   6. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vdash (\neg p\arr \neg q)\arr (q\arr p)} ;
   7. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vdash \neg(p\wedge q)\arr(\neg p\vee\neg q)} .
2. Dowie¶ć, że je¶li $\mathrm{\Delta }{⊢}_N\phi$, to dla dowolnej

formuły $\psi$ zachodzi $\mathrm{\Delta },\psi {⊢}_N\phi$.

1. 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)?