Logika dla informatyków/Ćwiczenia 2: Różnice pomiędzy wersjami
m |
|||
(Nie pokazano 1 wersji utworzonej przez jednego użytkownika) | |||
Linia 7: | Linia 7: | ||
<center><math> <a,b>\in q^\mathfrak A</math> wtedy i tylko wtedy, gdy <math>b=a+2</math></center>. | <center><math> <a,b>\in q^\mathfrak A</math> wtedy i tylko wtedy, gdy <math>b=a+2</math></center>. | ||
− | Zbadać czy formuły | + | Zbadać, czy formuły |
##<math>\forall x p(x,y) \to \exists x q(x,y)</math>; | ##<math>\forall x p(x,y) \to \exists x q(x,y)</math>; | ||
##<math>\forall x p(x,y) \to \forall x q(x,y)</math>; | ##<math>\forall x p(x,y) \to \forall x q(x,y)</math>; | ||
Linia 21: | Linia 21: | ||
<math>f^\mathfrak B(m,n) = m^2+n^2</math>, dla <math>m,n\in\mathbb Z</math>, a <math>r^\mathfrak B</math> jest relacją <math>\leq</math>. | <math>f^\mathfrak B(m,n) = m^2+n^2</math>, dla <math>m,n\in\mathbb Z</math>, a <math>r^\mathfrak B</math> jest relacją <math>\leq</math>. | ||
</center> | </center> | ||
− | Zbadać czy formuły | + | Zbadać, czy formuły |
#<math>\forall y(\forall x(r(z,f(x,y))\to r(z,y)))</math>; | #<math>\forall y(\forall x(r(z,f(x,y))\to r(z,y)))</math>; | ||
#<math>\forall y(\forall x(r(z,f(x,y)))\to r(z,y))</math>, | #<math>\forall y(\forall x(r(z,f(x,y)))\to r(z,y))</math>, | ||
Linia 58: | Linia 58: | ||
Niech <math>f</math> będzie jednoargumentowym symbolem funkcyjnym, który nie występuje w formule <math>\var\varphi</math>. | Niech <math>f</math> będzie jednoargumentowym symbolem funkcyjnym, który nie występuje w formule <math>\var\varphi</math>. | ||
Pokazać, że formuła <math>\forall x\exists y \var\varphi</math> jest spełnialna | Pokazać, że formuła <math>\forall x\exists y \var\varphi</math> jest spełnialna | ||
− | wtedy i tylko wtedy gdy formuła <math>\forall x \var\varphi | + | wtedy i tylko wtedy gdy formuła <math>\forall x \var\varphi(f(x)/y)</math> jest |
spełnialna. | spełnialna. | ||
}} | }} | ||
Linia 64: | Linia 64: | ||
{{Cwiczenie|8|| | {{Cwiczenie|8|| | ||
Udowodnić, że zdanie | Udowodnić, że zdanie | ||
− | < | + | <center><math>\forall x\exists y p(x,y)\wedge \forall x\neg p(x,x) \wedge \forall x\forall y\forall z(p(x,y)\wedge p(y,z)\to p(x,z))</math></center> |
ma tylko modele nieskończone. | ma tylko modele nieskończone. | ||
}} | }} |
Aktualna wersja na dzień 19:57, 22 paź 2006
Ćwiczenie 1
Niech
, gdzie:Zbadać, czy formuły
- ;
- ;
- ;
są spełnione przy wartościowaniu
, w strukturze .Ćwiczenie 2
Niech Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathfrak A = \<\mathbb Z, f^\mathfrak A, r^\mathfrak A >} i Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathfrak B = \< \mathbb Z, f^\mathfrak b, r^\mathfrak b >} , gdzie
relacją
, dla , a jest relacją .
Zbadać, czy formuły
- ;
- ,
są spełnione przy wartościowaniu
, w strukturach i .Ćwiczenie 3
Czy formuła
jest spełniona przy wartościowaniu , i- w strukturze , gdzie jest relacją podzielności?
- w strukturze , gdzie jest relacją przystawania modulo 7?
Ćwiczenie 4
W jakich strukturach prawdziwa jest formuła
? A formuła otrzymana przez "naiwne" podstawienie na ?Ćwiczenie 5
Podaj przykład modelu i wartościowania, przy którym formuła
jest: a) spełniona b) nie spełniona.
Ćwiczenie 6
Zbadać, czy następujące formuły są tautologiami i czy są spełnialne:
- ;
- ;
- ;
- .
Ćwiczenie 7
Niech
będzie jednoargumentowym symbolem funkcyjnym, który nie występuje w formule Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} . Pokazać, że formuła Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \forall x\exists y \var\varphi} jest spełnialna wtedy i tylko wtedy gdy formuła Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \forall x \var\varphi(f(x)/y)} jest spełnialna.Ćwiczenie 8
Udowodnić, że zdanie
ma tylko modele nieskończone.
Ćwiczenie 9
Dla każdego
napisać takie zdanie Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi_n} , że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \mathfrak A\models\var\varphi_n} zachodzi \wtw, gdy ma dokładnie elementów.Ćwiczenie 10
Czy jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \mathfrak A \models \exists x \var\varphi} , to także Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \mathfrak A \models \var\varphi[t/x]} , dla pewnego termu
?