Ćwiczenie 1
Rozpatrzmy system , którego aksjomatami są formuły postaci (A1--A9), a nie dowolne generalizacje takich formuł. Regułami wnioskowania w niech będą (MP) oraz
reguła generalizacji:
Udowodnić, że twierdzenia systemów
i
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}
.
Ćwiczenie 2
Udowodnić twierdzenie o pełności dla nieprzeliczalnych sygnatur.
Ćwiczenie 3
System naturalnej dedukcji dla logiki pierwszego rzędu można otrzymać
przez dodanie do systemu nastepujących reguł:
Parser nie mógł rozpoznać (nieznana funkcja „\prooftree”): {\displaystyle \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}
Parser nie mógł rozpoznać (nieznana funkcja „\prooftree”): {\displaystyle </center>\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}
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
nie jest wolne w żadnej z formuł ze zbioru
. 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.
Ćwiczenie 4
Zaproponować reguły rachunku sekwentów dla logiki pierwszego rzędu.
