Редактирование: Математическая Логика, решение задач/variant 2004

Материал из eSyr's wiki.

Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.

Правка не может быть отменена из-за несовместимости промежуточных изменений.

== Построение предиката по утверждению ==

=== Условные обозначения ===
* почти все = все, кроме конечного числа;

==== Доступные предикаты ====
* R(x) — вещественное число;
* N(x) — натуральное число;
* S(y) — y — последовательность действительных чисел;
* E(x, n, y) — x — элемент y с номером n;
* A(p, y) — p — предельная точка последовательности y;
* M(x, y) — x — предел последовательности y;
* x &lt; y, x = y — сравнение и равенство.

=== Задача 1 ===
''Какова бы ни была последовательность действительных чисел и отрезок [a, b] действительных чисел, если бесконечно много элементов этой последовательности содержится в данном отрезке, то хотя бы одна предельная точка данной последовательности также сожержится в этом отрезке.''

&phi;1 = (R(a) &amp; R(b) &amp; (a &le; b))
 &phi;2 = &forall; n1 (N(n1) &amp; &exist; n2 (N(n2) &amp; (n2 &ge; n1) &amp; &exist; x1 (E(x1, n2, y) &amp; ((a &le; x1) &amp; (x1 &le; b))))
 &phi;3 = &exist; p (A(p, y) &amp; ((a &le; p) &amp; (p &le; b)))
 
 &forall; a &forall; b &forall; y (S(y) &amp; &phi;1 &amp; &phi;2 &amp; (S(y) &amp; &phi;1 &amp; &phi;2 &rarr; &phi;3))

=== Задача 2 ===
''Какова бы ни была последовательность действительных чисел, найдется отрезок, содержащий все ее предельные точки.''

&forall; y  S(y) &amp; &exist; a &exist; b (R(a) &amp; R(b) &amp; (a &le; b) &forall; p (A(p, y) &amp; (a &le; p) &amp; (p &le; b))))

=== Задача 3 ===
''Каков бы ни был отрезок [a,b] действительных чисел, если почти все элементы произвольной последовательности действительных чисел лежат вне этого отрезка, то и все предельные точки этой последовательности лежат вне этого отрезка.''

&phi;1 = (R(a) &amp; R(b) &amp; (a &le; b))
 &phi;2 = &exist; n1 (N(n1) &amp; &forall; n2 (N(n2) &amp; (n2 &ge; n1) &amp; &forall; x1 (E(x1, n2, y) &amp; ((a &gt; x1) &or; (x1 &gt; b))))
 &phi;3 = &forall; p (A(p, y) &amp; ((a &gt; p) &amp; (p &gt; b)))
 
 &forall; a &forall; b &forall; y (S(y) &amp; &phi;1 &amp; &phi;2 &amp; (S(y) &amp; &phi;1 &amp; &phi;2 &rarr; &phi;3))

=== Задача 4 ===
''Какова бы ни была последовательность действительных чисел, если эта последовательность содержит отрицательный элемент, то найдется хотя бы одна неположительная предельная точка этой последовательности.''

&phi;1 = &exist; x &exist; n (R(x) &amp; N(n) &amp; E(x, n, y) &amp; (x &lt; 0))
 &phi;2 = &exist; p (A(p, y) &amp; (p &le; 0))
 
 &forall; y (S(y) &amp; &phi;1 &amp; (S(y) &amp; &phi;1 &rarr; &phi;2))

=== Задача 5 ===
''Каковы бы ни были две последовательности действительных чисел такие, что первая одна из них &rarr; 0, а другая ограничена, тогда из произведение тоже &rarr; 0.''

&phi;1 = &exist; M (R(M) &amp; &forall; n (N(n) &amp; &exist; x (R(x) &amp; E(x, n, y) &amp; (|x| &lt; M))))
 &phi;2 = &exist; y3 (S(y3) &amp; &forall; n (N(n) &exist; x1 &exist; x2 &exist; x3 (E(x1, n, y1) &amp; E(x2, n, y2) &amp; E(x3, n, y3) &amp; (x3 = x1 &times; x2))))
 
 &forall; y1 &forall; y2 (S(y1) &amp; S(y2) &amp; M(0, y1) &amp; &phi;1 &amp; &phi;2 &amp; (S(y1) &amp; S(y2) &amp; M(0, y) &amp; &phi;1 &amp; &phi;2 &rarr; M(0, y3)))

=== Задача 6 ===
''Нет такой сходящейся последовательности, что ее нельзя было бы представить как сумму двух сходящихся последовательностей.''

&phi;1(y) = S(y) &amp; &exist; m (R(m) &amp; M(m, y))
 &phi;2(y1, y2, y3) = (S(y3) &amp; &forall; n (N(n) &exist; x1 &exist; x2 &exist; x3 (E(x1, n, y1) &amp; E(x2, n, y2) &amp; E(x3, n, y3) &amp; (x3 = x1 + x2))))
 
 &not;(&exist; y3 (&phi;1(y) &amp; &forall; y1 &forall; y2 (&phi;1(y1) &amp; &phi;1(y2) &amp; &not;&phi;2(y1, y2, y3))))

== Табличный вывод ==
=== Правила ===
# <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'' свободна в ''&phi;(x)'' для терма ''t''.
# <math>R\forall:\frac{<\Gamma|\forall x\phi(x),\Delta>}{<\Gamma|\phi(x)\{^x/_c\},\Delta>}</math>, где ''c'' — константа, которая не содержитсяв &Gamma;, &Delta; или ''&phi;(x)''
# <math>L\exist:\frac{<\exist x\phi(x),\Gamma|\Delta>}{<\phi(x)\{^x/_c\},\Gamma|\Delta>}</math>, где ''c'' — константа, которая не содержитсяв &Gamma;, &Delta; или ''&phi;(x)''
# <math>R\exist:\frac{<\Gamma|\exist x\phi(x),\Delta>}{<\Gamma|\exist x\phi(x),\phi(x)\{^x/_t\},\Delta>}</math>, при условии, что переменная ''x'' свободна в ''&phi;(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>

Пожалуйста, обратите внимание, что все ваши добавления могут быть отредактированы или удалены другими участниками. Если вы не хотите, чтобы кто-либо изменял ваши тексты, не помещайте их сюда.
Вы также подтверждаете, что являетесь автором вносимых дополнений, или скопировали их из источника, допускающего свободное распространение и изменение своего содержимого (см. eSyr's_wiki:Авторское право).
НЕ РАЗМЕЩАЙТЕ БЕЗ РАЗРЕШЕНИЯ ОХРАНЯЕМЫЕ АВТОРСКИМ ПРАВОМ МАТЕРИАЛЫ!

Описание изменений:

Отменить | Справка по редактированию (в новом окне)

Шаблоны, использованные на этой странице: