Logika dla informatyków/Ćwiczenia 2

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania

Ćwiczenie 1

Niech , gdzie:

wtedy i tylko wtedy, gdy ;
wtedy i tylko wtedy, gdy
.

Zbadać, czy formuły

    1. ;
    2. ;
    3. ;

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

, dla , a jest

relacją ;
, dla , a jest relacją .

Zbadać, czy formuły

  1. ;
  2. ,

są spełnione przy wartościowaniu , w strukturach i .

Ćwiczenie 3

Czy formuła jest spełniona przy wartościowaniu , i

  1. w strukturze , gdzie jest relacją podzielności?
  2. 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:

  1. ;
  2. ;
  3. ;
  4. .

Ć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 <cemter>. 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 ?