Докажите, что ¬∃x ∀y (E(x, y) ↔ ¬E(y, y)) без предпосылок

введите описание изображения здесь

Единственный способ, который я мог придумать для решения этой проблемы, - это reductio, но, поскольку два биусловных термина не противоречат друг другу, я сильно застрял.

Можно ли использовать закон исключенного третьего?
Я думаю, что вы выполняете экзистенциальную и универсальную элиминацию в своей предпосылке reductio и приходите к противоречию.

Ответы (3)

Пахнет Парадоксом Рассела...

В любом случае, да, у вас была совершенно правильная идея: доказательство от противного! И два условных оператора будут противоречить до тех пор, пока вы создаете их с одной и той же константой a:

введите описание изображения здесь

E(x,y) <-> ¬ E(y,y) явно ложно, если x и y совпадают, потому что тогда утверждение становится E(x,x) <-> ¬ E(x,x).

Что бы мы ни выбрали для x, E(x,y) <-> ¬E(y,y) не верно для всех y, потому что это неверно для y = x.

Это правильно только в классической логике; см. обсуждение под моим ответом.

Вот доказательство с использованием закона исключенного третьего. После устранения квантора существования, чтобы получить x , примените универсальную количественную оценку к самому x , чтобы получить E(x,x) ↔ ¬E(x,x). Это неверно, если E(x,x) истинно или ложно.

введите описание изображения здесь

В Коке:

Variable P : Prop -> Prop -> Prop.
Axiom LEM : forall p, p \/ ~p.

Goal ~exists x, forall y, (P x y -> ~P y y) /\ (~P y y -> P x y).
intro.
elim H.
intros.
assert (P x x \/ ~P x x) by apply LEM.
elim H1; intro.
apply H0 with x; assumption.
apply H0 with x; apply H0; assumption.
Qed.
Неясно, означает ли «отсутствие предпосылок» отсутствие закона исключенного третьего. Если да, я удалю это.
Поскольку вы можете доказать ЛЭМ без каких-либо предпосылок, вы всегда можете начать с этого доказательства и удовлетворить условия вопроса.
@Dennis LEM не соответствует интуиционистской логике.
Я предполагал, что ОП работает в классической системе. Поскольку большинство вводных книг по логике предполагают такую ​​систему, это кажется вероятным, но вы правы в том, что это не будет интуиционистски достоверным доказательством.