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

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
następna edycja →
WizualnieWikikod
Aneczka (dyskusja | edycje)
700 edycji
Nie podano opisu zmian
 
Aneczka (dyskusja | edycje)
700 edycji
Nie podano opisu zmian
Linia 1: Linia 1:
{{cwieczenie|1||
Rozpatrzmy system <math>\vdash_h</math>, którego aksjomatami są formuły postaci (A1--A9), a nie dowolne generalizacje takich formuł. Regułami wnioskowania w <math>\vdash_h</math> niech będą (MP) oraz 
''reguła generalizacji:''


sbsection*{Ćwiczenia}\begin{small}
#Rozpatrzmy system <math>\vdash_h</math>, którego aksjomatami są formuły
postaci (A1--A9), a nie dowolne generalizacje takich formuł. Regułami
wnioskowania w <math>\vdash_h</math> niech będą (MP) oraz 
''reguła generalizacji:\/''
<!--% -->
<center><math>\prooftree \var\varphi\justifies \forall x\,\var\varphi\endprooftree</math></center>  
<center><math>\prooftree \var\varphi\justifies \forall x\,\var\varphi\endprooftree</math></center>  
<!--% -->
 
Udowodnić, że twierdzenia systemów <math>\vdash_h</math> i <math>\vdash_H</math> są takie
Udowodnić, że twierdzenia systemów <math>\vdash_h</math> i <math>\vdash_H</math> są takie same, ale z <math>\Gamma\vdash_h\var\varphi</math> nie wynika <math>\Gamma\models\var\varphi</math>. }}
same, ale z  
 
<math>\Gamma\vdash_h\var\varphi</math> nie wynika <math>\Gamma\models\var\varphi</math>.  
{{cwiczenie|2||
#Udowodnić twierdzenie o pełności dla nieprzeliczalnych sygnatur.   
Udowodnić twierdzenie o pełności dla nieprzeliczalnych sygnatur.  }}
#System naturalnej dedukcji dla logiki pierwszego rzędu można otrzymać   
 
przez dodanie do systemu <math>&nbsp;\vdash_N</math> nastepujących reguł:  
{{cwiczenie|3||
<!--%% -->  
System naturalnej dedukcji dla logiki pierwszego rzędu można otrzymać   
</math></center>\prooftree{\Gamma\vdash\var\varphi(y/x)}\justifies  
przez dodanie do systemu <math>\vdash_N</math> nastepujących reguł:  
 
<center><math>\prooftree{\Gamma\vdash\var\varphi(y/x)}\justifies  
{\Gamma\vdash\forall {x}\ciut \var\varphi}\using{(\forall\mbox{\rm-intro})}  
{\Gamma\vdash\forall {x}\ciut \var\varphi}\using{(\forall\mbox{\rm-intro})}  
\endprooftree  
\endprooftree \hspace{3cm}\prooftree{\Gamma\vdash\forall {x}\ciut \var\varphi}\justifies  
\hspace{3cm}  
\prooftree{\Gamma\vdash\forall {x}\ciut \var\varphi}\justifies  
{\Gamma\vdash\var\varphi(t/x)}\using{(\forall\mbox{\rm-elim})}\endprooftree</math></center>  
{\Gamma\vdash\var\varphi(t/x)}\using{(\forall\mbox{\rm-elim})}\endprooftree</math></center>  
<!--% -->
 
</math></center>\prooftree{\Gamma\vdash\var\varphi(t/x)}\justifies  
<math></center>\prooftree{\Gamma\vdash\var\varphi(t/x)}\justifies  
{\Gamma\vdash\exists {x}\ciut \var\varphi}\using{(\exists\mbox{\rm-intro})}  
{\Gamma\vdash\exists {x}\ciut \var\varphi}\using{(\exists\mbox{\rm-intro})}  
\endprooftree  
\endprooftree \hspace{2cm} \prooftree{\Gamma\vdash\exists {x}\ciut \var\varphi\quad  \Gamma,\var\varphi(y/x)\vdash\psi} \justifies  
\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></center>  
{\Gamma\vdash\psi}\using{(\exists\mbox{\rm-elim})}\endprooftree</math></center>  


przy czym regułę <math>(\forall\mbox{\rm-intro})</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.  }}
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&nbsp;<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.   
 
#Zaproponować reguły rachunku sekwentów dla logiki pierwszego rzędu.


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

Wersja z 14:28, 27 wrz 2006

Szablon:Cwieczenie

Ć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 „\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 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=57277”