Сделать вывод

[knizhnik]

Нужно доказать утверждение $\forall x \ A(x,x) \supset \forall x \exists y \ A(x,y)$. Детали вывода я себе не представляю. С чего начать?

[anr13r]

А а это что, если не секрет?

[knizhnik]

anr13r в сообщении #1166098 писал(а):

А а это что, если не секрет?

Утверждение в логике. Вы знаете, как это доказывать?

Karan в сообщении #1166103 писал(а):

доказать это утверждение неформально

Скорее всего идея в том, что в правой части $x$ берется за $y$, и тем самым объясняется $\exists y$. Но мне нужна не идейная, а формальная сторона задачи.

Karan в сообщении #1166103 писал(а):

список аксиом

$\forall x \ A(x) \supset A[t/x]$
$A[t/x] \supset \exists x \ A(x)$

Karan в сообщении #1166123 писал(а):

Приведите еще правила вывода в том виде, как они у Вас приводились.

${\tfrac {A\;\;(A\to B)}{B}}}$
${\tfrac {A(x)\to B}{\exists x \ A(x)\to B}}}$, $ B \neq B(x)$
${\tfrac {B\to A(x)}{B \to \forall x \ A(x)}}}$, $B \neq B(x)$

[anr13r]

Извините с логикой у меня проблемы, если додумаюсь напишу(((

[Karan]

knizhnik в сообщении #1166097 писал(а):

С чего начать?

Начните с того, что объясните, что Вы уже пытались сделать, например, можете ли Вы доказать это утверждение неформально. И приведите список аксиом, которым Вы пользуетесь, они от книги к книге немного отличаются.

[Karan]

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

- отсутствуют собственные содержательные попытки решения задач(и).

Исправьте все Ваши ошибки и сообщите об этом в теме Сообщение в карантине исправлено.
Настоятельно рекомендуется ознакомиться с темами Что такое карантин и что нужно делать, чтобы там оказаться и Правила научного форума.

[Karan]

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

[arseniiv]

Насколько помню (поправьте меня, если в вашем источнике не так), в схемах аксиом (назовём их $\forall^-$ и $\exists^+$) допускается заменять не все, а лишь некоторые свободные вхождения $x$ в $A$ на $t$. В таком случае, например, $A(x,x)\supset \exists y\,A(x,y)$ будет экземпляром схемы $\exists^+$ (проследите, что здесь $A,t,x$ из схемы). Осталось разобраться, как навесить $\forall x$ в обоих частях импликации. Попробуйте идти в обратную сторону, смотря на то, какими правилами вывода, применёнными к чему, можно получить искомое.

Вообще, конечно, вы ещё не привели аксиомы, доставшиеся в наследство от исчисления высказываний. Оно аксиоматизируется не единственным способом. Так что с точностью до аксиом из этой части пока ничем помочь будет нельзя.

(О записи)

knizhnik в сообщении #1166100 писал(а):

$ B \neq B(x)$

Не, я знаю, конечно, что это значит «$B$ не содержит свободных вхождений $x$», но кто не знает, вряд ли догадается.

knizhnik в сообщении #1166100 писал(а):

$\forall x \ A(x) \supset A[t/x]$

Тут тоже вообще классная смесь. Или уж $A\supset A[t/x]$, или $A(x)\supset A(t)$.

[knizhnik]

arseniiv в сообщении #1166149 писал(а):

не привели аксиомы, доставшиеся в наследство от исчисления высказываний. Оно аксиоматизируется не единственным способом.

Думаю, неважно какие аксиомы. Лучше сразу пользоваться всеми готовыми логическими законами для высказываний и не тратить времени на их доказательство.

arseniiv в сообщении #1166149 писал(а):

в схемах аксиом (назовём их $\forall^-$ и $\exists^+$) допускается заменять не все, а лишь некоторые свободные вхождения $x$ в $A$ на $t$.

Вообще, надо расписывать это правило, когда можно, но я не стал.

arseniiv в сообщении #1166149 писал(а):

В таком случае, например, $A(x,x)\supset \exists y\,A(x,y)$ будет экземпляром схемы $\exists^+$ (проследите, что здесь $A,t,x$ из схемы).

Вот это очень странно. Первое, что сбивает с толку: аксиомы касаются только одноместных предикатов, а не двухместных, как в задаче. Затем, почему мы меняем лишь второй икс, но не оба сразу? Разве не должно быть $A(x,x)\supset \exists y\,A(y,y)$? Или может, я плохо понял, как выполняется подстановка...

arseniiv в сообщении #1166149 писал(а):

Осталось разобраться, как навесить $\forall x$ в обоих частях импликации.

Здесь нужна какая-то лемма вида: $(A(x) \supset B(x)) \supset (\forall x \ A(x) \supset \forall x \ B(x))$. Нужно ее доказать.

(о записи)

(Оффтоп)

А еще стрелочки разные. Потому что правила вывода стянул из инета (с небольшими правками). Набирать поленился.

[Xaositect]

knizhnik в сообщении #1166173 писал(а):

аксиомы касаются только одноместных предикатов, а не двухместных, как в задаче.

Ни в коем случае, иначе с двуместными предикатами вообще ничего нельзя было бы сделать. Читайте учебник, там должно быть написано подробно, в каких условиях применимы аксиомы и почему $A(x,x) = A(x,y)[x/y]$.

-- Сб ноя 05, 2016 08:33:08 --

knizhnik в сообщении #1166173 писал(а):

Здесь нужна какая-то лемма вида: $(A(x) \supset B(x)) \supset (\forall x \ A(x) \supset \forall x \ B(x))$. Нужно ее доказать.

Ее нельзя доказать, потому что она не общезначима. А вот вывод $\dfrac{A \to B}{\forall x A \to \forall x B}$ всегда существует.

[knizhnik]

Xaositect в сообщении #1166184 писал(а):

вывод $\dfrac{A \to B}{\forall x A \to \forall x B}$ всегда существует.

Нужно доказать эту формулу. Как доказать? У меня нет идей, поскольку в правилах Бернайса обязательно есть независимый от $x$ предикат. В этой формуле все зависимые.

-- 05.11.2016, 03:06 --

knizhnik в сообщении #1166260 писал(а):

В этой формуле все зависимые.

То есть должны быть зависимые для доказательства основного утверждения.

[Xaositect]

knizhnik в сообщении #1166260 писал(а):

Нужно доказать эту формулу. Как доказать? У меня нет идей, поскольку в правилах Бернайса обязательно есть независимый от $x$ предикат. В этой формуле все зависимые.

Не предикат, а формула.

Сначала докажите, что из $A \to B$ выводится $\forall x A \to B$. Теперь слева стоит формула $\forall x A$, в которой все вхождения $x$ связаны, и можно применить правило Бернайса.

[knizhnik]

Пусть дано $A \to B$. Нужно взять общезначимую формулу высказываний, пусть это будет закон исключенного третьего, обозначим его как $1$. Тогда справедливо $1 \to (A \to B)$. Тогда $\dfrac{1 \to A \to B}{1 \to \forall x (A \to B)}$, затем $1 \to \forall x (A \to B)$ и по modus ponens $\forall x (A \to B)$. Формула $\forall x (A \to B) \to (\forall x A \to \forall x B) $ общезначима, но доказать это сложно. Может быть сложнее, чем исходное утверждение. Есть другие варианты?

Xaositect в сообщении #1166267 писал(а):

докажите, что из $A \to B$ выводится $\forall x A \to B$

Без подсказки я не разберусь, что делать.

[knizhnik]

Если бы я мог своими силами решить эту задачу, то я бы сюда не обратился. Что делать? Искать другой форум?