Logika dla informatyków/Ćwiczenia 7

sbsection*{Ćwiczenia}\begin{small}

1. Rozpatrzmy system ${⊢}_h$, którego aksjomatami są formuły

postaci (A1--A9), a nie dowolne generalizacje takich formuł. Regułami wnioskowania w ${⊢}_h$ niech będą (MP) oraz reguła generalizacji:\/

Parser nie mógł rozpoznać (nieznana funkcja „\prooftree”): {\displaystyle \prooftree \var\varphi\justifies \forall x\,\var\varphi\endprooftree}

Udowodnić, że twierdzenia systemów ${⊢}_h$ i ${⊢}_H$ są takie same, ale z Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma\vdash_h\var\varphi} nie wynika Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma\models\var\varphi} .

1. Udowodnić twierdzenie o pełności dla nieprzeliczalnych sygnatur.
2. System naturalnej dedukcji dla logiki pierwszego rzędu można otrzymać

przez dodanie do systemu Parser nie mógł rozpoznać (błąd składni): {\displaystyle  \vdash_N} nastepujących reguł:

</math>\prooftree{\Gamma\vdash\var\varphi(y/x)}\justifies

{\Gamma\vdash\forall {x}\ciut \var\varphi}\using{(\forall\mbox{\rm-intro})} \endprooftree \hspace{3cm} \prooftree{\Gamma\vdash\forall {x}\ciut \var\varphi}\justifies

{\Gamma\vdash\var\varphi(t/x)}\using{(\forall\mbox{\rm-elim})}\endprooftree</math> </math>\prooftree{\Gamma\vdash\var\varphi(t/x)}\justifies

{\Gamma\vdash\exists {x}\ciut \var\varphi}\using{(\exists\mbox{\rm-intro})} \endprooftree \hspace{2cm} \prooftree{\Gamma\vdash\exists {x}\ciut \var\varphi\quad \Gamma,\var\varphi(y/x)\vdash\psi} \justifies

{\Gamma\vdash\psi}\using{(\exists\mbox{\rm-elim})}\endprooftree</math>

przy czym regułę Parser nie mógł rozpoznać (błąd składni): {\displaystyle (\forall\mbox{\rm-intro})} wolno stosować tylko wtedy gdy Parser nie mógł rozpoznać (nieznana funkcja „\fv”): {\displaystyle {y}\not\in\fv{\forall {x}\ciut \var\varphi}} oraz $y$ nie jest wolne w żadnej z formuł ze zbioru $\mathrm{\Gamma }$. Natomiast reguła Parser nie mógł rozpoznać (błąd składni): {\displaystyle (\exists\mbox{\rm-intro})} używana jest przy zastrzeżeniu Parser nie mógł rozpoznać (nieznana funkcja „\fv”): {\displaystyle {y}\not\in\fv{\Gamma\cup\{\exists {x}\ciut \var\varphi\}\cup\{\psi\}}} . Udowodnić twierdzenie o pełności dla tego systemu.

1. Zaproponować reguły rachunku sekwentów dla logiki pierwszego rzędu.

\end{small}