| Текущая версия |
Ваш текст |
| Строка 16: |
Строка 16: |
| | ''Какова бы ни была последовательность действительных чисел и отрезок [a, b] действительных чисел, если бесконечно много элементов этой последовательности содержится в данном отрезке, то хотя бы одна предельная точка данной последовательности также сожержится в этом отрезке.'' | | ''Какова бы ни была последовательность действительных чисел и отрезок [a, b] действительных чисел, если бесконечно много элементов этой последовательности содержится в данном отрезке, то хотя бы одна предельная точка данной последовательности также сожержится в этом отрезке.'' |
| | | | |
| - | φ<sub>1</sub> = (R(a) & R(b) & (a ≤ b)) | + | φ<sub>1</sub> = ∀ n (S(y) & N(n) & (∀ x E(x, n, y) & R(x))) |
| - | φ<sub>2</sub> = ∀ n<sub>1</sub> (N(n<sub>1</sub>) & ∃ n<sub>2</sub> (N(n<sub>2</sub>) & (n<sub>2</sub> ≥ n<sub>1</sub>) & ∃ x<sub>1</sub> (E(x<sub>1</sub>, n<sub>2</sub>, y) & ((a ≤ x<sub>1</sub>) & (x<sub>1</sub> ≤ b)))) | + | φ<sub>2</sub> = (R(a) & R(b) & (a ≤ b)) |
| - | φ<sub>3</sub> = ∃ p (A(p, y) & ((a ≤ p) & (p ≤ b))) | + | φ<sub>3</sub> = ∀ n<sub>1</sub> (N(n<sub>1</sub>) & ∃ n<sub>2</sub> ((n<sub>2</sub> ≥ n<sub>1</sub>) & ∃ x<sub>1</sub> (E(x<sub>1</sub>, n<sub>2</sub>, y) & ((a ≤ x<sub>1</sub>) & (x<sub>1</sub> ≤ b)))) |
| | + | φ<sub>4</sub> = ∃ p (A(p, y) & ((a ≤ p) & (p ≤ b))) |
| | | | |
| - | ∀ a ∀ b ∀ y (S(y) & φ<sub>1</sub> & φ<sub>2</sub> & (S(y) & φ<sub>1</sub> & φ<sub>2</sub> → φ<sub>3</sub>)) | + | ∀ a ∀ b ∀ y (φ<sub>1</sub> & φ<sub>2</sub> & φ<sub>3</sub> & (φ<sub>1</sub> & φ<sub>2</sub> & φ<sub>3</sub> → φ<sub>4</sub>)) |
| | | | |
| | === Задача 2 === | | === Задача 2 === |
| | ''Какова бы ни была последовательность действительных чисел, найдется отрезок, содержащий все ее предельные точки.'' | | ''Какова бы ни была последовательность действительных чисел, найдется отрезок, содержащий все ее предельные точки.'' |
| | | | |
| - | ∀ y S(y) & ∃ a ∃ b (R(a) & R(b) & (a ≤ b) ∀ p (A(p, y) & (a ≤ p) & (p ≤ b)))) | + | ∀ y ∀ n (S(y) & N(n) & (∀ x E(x, n, y) & R(x)) & ∃ a ∃ b (∀ p (A(p, y) & (a ≤ p) & (p ≤ b)))) |
| - | | + | |
| - | === Задача 3 ===
| + | |
| - | ''Каков бы ни был отрезок [a,b] действительных чисел, если почти все элементы произвольной последовательности действительных чисел лежат вне этого отрезка, то и все предельные точки этой последовательности лежат вне этого отрезка.''
| + | |
| - | | + | |
| - | φ<sub>1</sub> = (R(a) & R(b) & (a ≤ b))
| + | |
| - | φ<sub>2</sub> = ∃ n<sub>1</sub> (N(n<sub>1</sub>) & ∀ n<sub>2</sub> (N(n<sub>2</sub>) & (n<sub>2</sub> ≥ n<sub>1</sub>) & ∀ x<sub>1</sub> (E(x<sub>1</sub>, n<sub>2</sub>, y) & ((a > x<sub>1</sub>) ∨ (x<sub>1</sub> > b))))
| + | |
| - | φ<sub>3</sub> = ∀ p (A(p, y) & ((a > p) & (p > b)))
| + | |
| - |
| + | |
| - | ∀ a ∀ b ∀ y (S(y) & φ<sub>1</sub> & φ<sub>2</sub> & (S(y) & φ<sub>1</sub> & φ<sub>2</sub> → φ<sub>3</sub>))
| + | |
| - | | + | |
| - | === Задача 4 ===
| + | |
| - | ''Какова бы ни была последовательность действительных чисел, если эта последовательность содержит отрицательный элемент, то найдется хотя бы одна неположительная предельная точка этой последовательности.''
| + | |
| - | | + | |
| - | φ<sub>1</sub> = ∃ x ∃ n (R(x) & N(n) & E(x, n, y) & (x < 0))
| + | |
| - | φ<sub>2</sub> = ∃ p (A(p, y) & (p ≤ 0))
| + | |
| - |
| + | |
| - | ∀ y (S(y) & φ<sub>1</sub> & (S(y) & φ<sub>1</sub> → φ<sub>2</sub>))
| + | |
| - | | + | |
| - | === Задача 5 ===
| + | |
| - | ''Каковы бы ни были две последовательности действительных чисел такие, что первая одна из них → 0, а другая ограничена, тогда из произведение тоже → 0.''
| + | |
| - | | + | |
| - | φ<sub>1</sub> = ∃ M (R(M) & ∀ n (N(n) & ∃ x (R(x) & E(x, n, y) & (|x| < M))))
| + | |
| - | φ<sub>2</sub> = ∃ y<sub>3</sub> (S(y<sub>3</sub>) & ∀ n (N(n) ∃ x<sub>1</sub> ∃ x<sub>2</sub> ∃ x<sub>3</sub> (E(x<sub>1</sub>, n, y<sub>1</sub>) & E(x<sub>2</sub>, n, y<sub>2</sub>) & E(x<sub>3</sub>, n, y<sub>3</sub>) & (x<sub>3</sub> = x<sub>1</sub> × x<sub>2</sub>))))
| + | |
| - |
| + | |
| - | ∀ y<sub>1</sub> ∀ y<sub>2</sub> (S(y<sub>1</sub>) & S(y<sub>2</sub>) & M(0, y<sub>1</sub>) & φ<sub>1</sub> & φ<sub>2</sub> & (S(y<sub>1</sub>) & S(y<sub>2</sub>) & M(0, y) & φ<sub>1</sub> & φ<sub>2</sub> → M(0, y<sub>3</sub>)))
| + | |
| - | | + | |
| - | === Задача 6 ===
| + | |
| - | ''Нет такой сходящейся последовательности, что ее нельзя было бы представить как сумму двух сходящихся последовательностей.''
| + | |
| - | | + | |
| - | φ<sub>1</sub>(y) = S(y) & ∃ m (R(m) & M(m, y))
| + | |
| - | φ<sub>2</sub>(y<sub>1</sub>, y<sub>2</sub>, y<sub>3</sub>) = (S(y<sub>3</sub>) & ∀ n (N(n) ∃ x<sub>1</sub> ∃ x<sub>2</sub> ∃ x<sub>3</sub> (E(x<sub>1</sub>, n, y<sub>1</sub>) & E(x<sub>2</sub>, n, y<sub>2</sub>) & E(x<sub>3</sub>, n, y<sub>3</sub>) & (x<sub>3</sub> = x<sub>1</sub> + x<sub>2</sub>))))
| + | |
| - |
| + | |
| - | ¬(∃ y<sub>3</sub> (φ<sub>1</sub>(y) & ∀ y<sub>1</sub> ∀ y<sub>2</sub> (φ<sub>1</sub>(y<sub>1</sub>) & φ<sub>1</sub>(y<sub>2</sub>) & ¬φ<sub>2</sub>(y<sub>1</sub>, y<sub>2</sub>, y<sub>3</sub>))))
| + | |
| - | | + | |
| - | == Табличный вывод ==
| + | |
| - | === Правила ===
| + | |
| - | # <math>L\neg:\frac{<\neg\phi,\Gamma|\Delta>}{<\Gamma|\phi,\Delta>}</math>
| + | |
| - | # <math>R\neg:\frac{<\Gamma|\neg\phi,\Delta>}{<\phi,\Gamma|\Delta>}</math>
| + | |
| - | # <math>L\and:\frac{<\phi_1\and\phi_2,\Gamma|\Delta>}{<\phi_1,\phi_2,\Gamma|\Delta>}</math>
| + | |
| - | # <math>R\and:\frac{<\Gamma|\phi_1\and\phi_2,\Delta>}{<\Gamma|\phi_1,\Delta><\Gamma|\phi_2,\Delta>}</math>
| + | |
| - | # <math>L\lor:\frac{<\phi_1\lor\phi_2,\Gamma|\Delta>}{<\phi_1,\Gamma|\Delta><\phi_2,\Gamma|\Delta>}</math>
| + | |
| - | # <math>R\lor:\frac{<\Gamma|\phi_1\lor\phi_2,\Delta>}{<\Gamma|\phi_1,\phi_2,\Delta>}</math>
| + | |
| - | # <math>L\to:\frac{<\phi_1\to\phi_2,\Gamma|\Delta>}{<\phi_2,\Gamma|\Delta><\Gamma|\phi_1,\Delta>}</math>
| + | |
| - | # <math>R\to:\frac{<\Gamma|\phi_1\to\phi_2,\Delta>}{<\phi_1,\Gamma|\phi_2,\Delta>}</math>
| + | |
| - | | + | |
| - | ==== Дополнительные правила ====
| + | |
| - | # <math>L\forall:\frac{<\forall x\phi(x),\Gamma|\Delta>}{<\forall x\phi(x),\phi(x)\{^x/_t\},\Gamma|\Delta>}</math>, при условии, что переменная ''x'' свободна в ''φ(x)'' для терма ''t''.
| + | |
| - | # <math>R\forall:\frac{<\Gamma|\forall x\phi(x),\Delta>}{<\Gamma|\phi(x)\{^x/_c\},\Delta>}</math>, где ''c'' — константа, которая не содержитсяв Γ, Δ или ''φ(x)''
| + | |
| - | # <math>L\exist:\frac{<\exist x\phi(x),\Gamma|\Delta>}{<\phi(x)\{^x/_c\},\Gamma|\Delta>}</math>, где ''c'' — константа, которая не содержитсяв Γ, Δ или ''φ(x)''
| + | |
| - | # <math>R\exist:\frac{<\Gamma|\exist x\phi(x),\Delta>}{<\Gamma|\exist x\phi(x),\phi(x)\{^x/_t\},\Delta>}</math>, при условии, что переменная ''x'' свободна в ''φ(x)'' для терма ''t''.
| + | |
| - | | + | |
| - | === Задача 1 ===
| + | |
| - | С помощью метода семантических таблиц установить, общезначима ли формула:
| + | |
| - | | + | |
| - | <math>\forall{x}\forall{y}(P(x)\to R(y))\to(\exist{y}P(y)\to\forall{x}R(x))</math>
| + | |
| - | | + | |
| - | '''Решение.'''
| + | |
| - | | + | |
| - | <math>\begin{array}{ccc}
| + | |
| - | <\empty|\forall{x}\forall{y}(P(x)\to R(y))\to(\exist{y}P(y)\to\forall{x}R(x))> \\
| + | |
| - | \darr R\to \\
| + | |
| - | <\forall{x}\forall{y}(P(x)\to R(y))|(\exist{y}P(y)\to\forall{x}R(x))> \\
| + | |
| - | \darr R\to \\
| + | |
| - | <\forall{x}\forall{y}(P(x)\to R(y)),\exist{y}P(y)|\forall{x}R(x)> \\
| + | |
| - | \darr R\forall \\
| + | |
| - | <\forall{x}\forall{y}(P(x)\to R(y)),\exist{y}P(y)|R(c_1)> \\
| + | |
| - | \darr L\exist \\
| + | |
| - | <\forall{x}\forall{y}(P(x)\to R(y)),P(c_2)|R(c_1)> \\
| + | |
| - | \darr L\forall \\
| + | |
| - | <\forall{x}\forall{y}(P(x)\to R(y)),\forall{y}(P(t_1)\to R(y)),P(c_2)|R(c_1)> \\
| + | |
| - | \darr L\forall \\
| + | |
| - | <\forall{x}\forall{y}(P(x)\to R(y)),\forall{y}(P(t_1)\to R(y)),(P(t_1)\to R(t_2)),P(c_2)|R(c_1)> \\
| + | |
| - | \darr L\to \\
| + | |
| - | <\forall{x}\forall{y}(P(x)\to R(y)),\forall{y}(P(t_1)\to R(y)),R(t_2),P(c_2)|R(c_1)>, <\forall{x}\forall{y}(P(x)\to R(y)),\forall{y}(P(t_1)\to R(y)),P(c_2)|P(t_1),R(c_1)> \\
| + | |
| - | \end{array}</math>
| + | |
| - | | + | |
| - | Вторая таблица открыта, следовательно, формула не общезначима. (А разве нельзя провести унификацию терма t_2 = c_1, а t_1 = c_2?)
| + | |
| - | | + | |
| - | === Задача 2 ===
| + | |
| - | С помощью метода семантических таблиц установить, общезначима ли формула:
| + | |
| - | | + | |
| - | <math>(\exist{y}P(y)\to\forall{x}R(x))\to\forall{x}\forall{y}(P(x)\to R(y))</math>
| + | |
| - | | + | |
| - | '''Решение.'''
| + | |
| - | | + | |
| - | <math>\begin{array}{c}\begin{array}{ccc}
| + | |
| - | & <\empty|(\exist{y}P(y)\to\forall{x}R(x))\to\forall{x}\forall{y}(P(x)\to R(y))> \\
| + | |
| - | & \darr R\to \\
| + | |
| - | & <(\exist{y}P(y)\to\forall{x}R(x))|\forall{x}\forall{y}(P(x)\to R(y))> \\
| + | |
| - | & \darr L\to \\
| + | |
| - | <\forall{x}R(x)|\exist{y}P(y),\forall{x}\forall{y}(P(x)\to R(y))> & & <\empty|\exist{y}P(y),\forall{x}\forall{y}(P(x)\to R(y))> \\
| + | |
| - | \darr L\forall & & \darr R\exist \\
| + | |
| - | <\forall{x}R(x),R(t_1)|\forall{x}\forall{y}(P(x)\to R(y))> & & <\empty|\exist{y}P(y),P(t_2),\forall{x}\forall{y}(P(x)\to R(y))> \\
| + | |
| - | \darr R\forall & & \darr R\forall \\
| + | |
| - | <\forall{x}R(x),R(t_1)|\forall{y}(P(c_1)\to R(y))> & & <\empty|\exist{y}P(y),P(t_2),\forall{y}(P(c_2)\to R(y))> \\
| + | |
| - | \darr R\forall & & \darr R\forall \\
| + | |
| - | <\forall{x}R(x),R(t_1)|(P(c_1)\to R(c_3))> & & <\empty|\exist{y}P(y),P(t_2),P(c_2)\to R(c_4)> \\
| + | |
| - | \darr R\to & & \darr R\to \\
| + | |
| - | <\forall{x}R(x),R(t_1),P(c_1)|R(c_3)> & & <P(c_2)|\exist{y}P(y),P(t_2),R(c_4)> \\
| + | |
| - | \end{array}\end{array}</math>
| + | |
| - | | + | |
| - | Вторая таблица открыта, следовательно, формула не общезначима. (Аналогично унифицировав t_1 = c_3 и t_2 = c_2 мы получим закрытую таблицу).
| + | |
| - | | + | |
| - | == Метод резолюций ==
| + | |
| - | | + | |
| - | === Задача 1 ===
| + | |
| - | С помощью метода резолюций исследовать на противоречивость систему дизъюнктов S.
| + | |
| - | | + | |
| - | <math>\begin{cases}
| + | |
| - | D_1 = P(y_1, z_1)\lor\neg R(x_1, b) \\
| + | |
| - | D_2 = \neg Q(b, x_2)\lor\neg P(z_2, y_2) \\
| + | |
| - | D_3 = R(c, x_3)\lor P(x_3, g(y_3)) \\
| + | |
| - | D_4 = Q(y_4, y_4)\lor\neg P(x_4, g(y_4)) \\
| + | |
| - | D_5 = \neg P(x_5, y_5)\lor Q(f(x_5), y_5)
| + | |
| - | \end{cases}</math>
| + | |
| - | | + | |
| - | '''Решение.'''
| + | |
| - | | + | |
| - | (2)и(((1)и(5))и(3)) склеить в !(z2, g(b)), (1)и(3) склеить в P(b, g(b)).
| + | |
| - | <math>\begin{array}{l}
| + | |
| - | D^'_1 - D_1, D_5: R(x_1, b)\lor Q(f(x_5), x_5) \\
| + | |
| - | D^'_2 - D^'_1, D_3: P(b, g(y_3))\lor Q(f(x_5), x_5) \\
| + | |
| - | D^'_3 - D_2, D_4: \neg P(z_2, y_2) \lor \neg P(x_4, g(y_4)) \\
| + | |
| - | D^'_4 - D^'_3: \neg P(z_2, y_2) \\
| + | |
| - | D^'_5 - D_1, D_3: P(b, y_3)\lor P(y_1, z_1) \\
| + | |
| - | D^'_6 - D_1, D_3: P(b, y_3) \\
| + | |
| - | D^'_7 - D^'_4, D^'_6: []
| + | |
| - | \end{array}</math>
| + | |
| | | | |
| | {{Курс Математическая Логика}} | | {{Курс Математическая Логика}} |
