Logika dla informatyków/Ćwiczenia 7: Różnice pomiędzy wersjami

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
← poprzednia edycjanastępna edycja →
WizualnieWikikod
Aneczka (dyskusja | edycje)
700 edycji
Nie podano opisu zmian
Dorota (dyskusja | edycje)
376 edycji
Nie podano opisu zmian
Linia 23: Linia 23:
{\Gamma\vdash\psi}\using{(\exists\mbox{\rm-elim})}</math>
{\Gamma\vdash\psi}\using{(\exists\mbox{\rm-elim})}</math>


przy czym regułę <math>(\forall\mbox{\rm-intro})</math> wolno stosować tylko wtedy gdy <math>{y}\not\in\fv{\forall {x}\ciut \var\varphi}</math> oraz <math>y</math> nie jest wolne w żadnej z formuł ze zbioru <math>\Gamma</math>. Natomiast reguła <math>(\exists\mbox{\rm-intro})</math>używana jest przy zastrzeżeniu <math>{y}\not\in\fv{\Gamma\cup\{\exists {x}\ciut \var\varphi\}\cup\{\psi\}}</math>. Udowodnić twierdzenie o pełności dla tego systemu.  }}
przy czym regułę <math>(\forall\mbox{\rm-intro})</math> wolno stosować tylko wtedy, gdy <math>{y}\not\in\fv{\forall {x}\ciut \var\varphi}</math> oraz <math>y</math> nie jest wolne w żadnej z formuł ze zbioru <math>\Gamma</math>. Natomiast reguła <math>(\exists\mbox{\rm-intro})</math>używana jest przy zastrzeżeniu <math>{y}\not\in\fv{\Gamma\cup\{\exists {x}\ciut \var\varphi\}\cup\{\psi\}}</math>. Udowodnić twierdzenie o pełności dla tego systemu.  }}


{{cwiczenie|4||
{{cwiczenie|4||
Zaproponować reguły rachunku sekwentów dla logiki pierwszego rzędu.  
Zaproponować reguły rachunku sekwentów dla logiki pierwszego rzędu.  
}}
}}

Wersja z 10:52, 1 paź 2006

Ćwiczenie 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:

φ∀xφ

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

Ć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 ⊢N nastepujących reguł:

Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \frac{\Gamma\vdash\var\varphi(y/x)} {\Gamma\vdash\forall {x}\ciut \var\varphi}(\forall\mbox{\rm-intro}) \hspace{3cm}\frac{\Gamma\vdash\forall {x}\ciut \var\varphi} {\Gamma\vdash\var\varphi(t/x)}\using{(\forall\mbox{\rm-elim})}}


Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \frac{\Gamma\vdash\var\varphi(t/x)}{\Gamma\vdash\exists {x}\ciut \var\varphi}(\exists\mbox{\rm-intro})\hspace{2cm} \frac{\Gamma\vdash\exists {x}\ciut \var\varphi\quad \Gamma,\var\varphi(y/x)\vdash\psi} {\Gamma\vdash\psi}\using{(\exists\mbox{\rm-elim})}}

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

Źródło: „https://wazniak.mimuw.edu.pl/index.php?title=Logika_dla_informatyków/Ćwiczenia_7&oldid=61108”