Logika dla informatyków/Ćwiczenia 5

Ćwiczenie 1.

1. Niech ${⊢}_{H_1}$ oznacza system dowodzenia otrzymany

z systemu ${⊢}_H$ przez zamianę aksjomatu (A3) na następujący aksjomat:

1. # (A3')  Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle (\neg\varphi\arr\neg\psi)\arr((\neg\varphi\arr \psi)\arr\varphi).}

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.

1. Niech ${⊢}_{H_2}$ oznacza system dowodzenia otrzymany

z systemu ${⊢}_H$ przez zamianę aksjomatu (A3) na ${⊢}_H$, następuj±cy aksjomat:

(A3")  Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle (\neg\varphi\arr\neg\psi)\arr(\psi\arr\varphi).}

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

1. Dowie¶ć, że aksjomatu (A3) nie da się wyprowadzić z

aksjomatów (A0--2) przy pomocy reguły odrywania.

1. Dowie¶ć Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vdash_H\neg p \arr(p\arr q)} używaj±c twierdzenia o

dedukcji oraz bez użycia tego twierdzenia.

1. Pokazać, że w systemie ${⊢}_H$ dopuszczalna jest

następuj±ca reguła:

Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \frac{\varphi\arr\psi\odstep \neg\psi}{\neg\varphi}}

tzn. pokazać, że je¶li Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \Delta\vdash_H\varphi\arr\psi} oraz $\mathrm{\Delta }{⊢}_H\mathrm{\neg }\psi$, to również mamy $\mathrm{\Delta }{⊢}_H\mathrm{\neg }\phi$.

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

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