Доказать что следующие формулы являются теоремами P.

[ExploiT243]

Доказать что следующие формулы являются теоремами P.
Задача:

a) $ ((x+z = y+z) \to (x = y))$

b) $ ((\neg z = 0) \to ((x \cdot z=y \cdot z) \to (x=y))) $

(задача из учебника Лавров И.А., Максимова Л.Л. Задачи по теории множеств, математической логике и теории алгоритмов часть II, параграф 7, Номер 29)

[Deggial]

Тема перемещена из форума «Помогите решить / разобраться (М)» в форум «Карантин»
Причина переноса: формулы не оформлены ТеХом

Запишите формулы ТеХом. Инструкции по оформлению формул здесь или здесь (или в этом видеоролике).
Уберите ссылки на рисунки, сами аксиомы тоже запишите ТеХом в теме.
После исправлений сообщите в теме Сообщение в карантине исправлено, и тогда тема будет возвращена.

[Deggial]

Тема перемещена из форума «Карантин» в форум «Помогите решить / разобраться (М)»
вернул

[Someone]

А что такое "$P$"?

[ExploiT243]

Аксиомы равенства:
$ \forall x (x = x)$
$\forall x \forall y \forall z( (x = y \& y = z) \to x = z)$
$\forall x \forall y (x = y \to y = x)$

s(x)=x+1

Аксиомы теории Q:
$Q_1: \forall x \forall y ((s(x)=s(y)) \to( x = y))$
$Q_2: \forall x \neg s(x) = 0$
$Q_3: \forall x(\neg x = 0 \to \exists y(x = s(y)))$
$Q_4: \forall x ((x+0)=x)$
$Q_5: \forall x \forall y (x + s(y) = s(x + y))$
$Q_6: \forall x(x \cdot 0 = 0)$
$Q_7: \forall x \forall y (x \cdot s(y) = x \cdot y + x)$

Аксиомы теории P:
Все аксиомы $Q_1 - Q_7 + бесконечное множество формул вида P_A$

$P_A: \forall y((A(0) \& \forall x (A(x) \to A(s(x)))) \to A(y) )$

где A(x) - любая формула со свободной переменной x.
Формула $P_A$ называется $ \textit{аксиомой индукции для A}$.

[Someone]

Арифметика Пеано?

А какие у Вас идеи насчёт доказательства этих формул? Ну, хотя бы первой.
Применить индукцию пробовали?

[ExploiT243]

Я решал под а) сначала индукция, потом введение $\&$ получалось две ветки. 1)(левая) Введение импликации, введение $\&$ дальше понятно. 2)(правая) Введение импликации, расширение, дальше не знаю что делать

[ExploiT243]

Тема не актуальна. Можно удалить.