Напишите, пожалуйста, кто-нибудь два исходных высказывания этой теоремы.
Я не знаю, что Вы называете "исходными высказываниями теоремы". Для меня исходными высказываниями теоремы являются аксиомы математической логики, аксиомы той теории, к которой относится теорема (возможно, не все, что указывается в формулировке теоремы), а также дополнительные утверждения, которые автор добавляет к аксиомам. Также подразумеваются соответствующие правила вывода.
С точки зрения синтаксиса в формуле
здесь есть три терма
,
и
(термы — имена "вещей"; при этом "
" является переменной, а "
и "
" — константы), из которых с помощью символа бинарного отношения "
" построены две элементарные формулы
и
(эти формулы называются элементарными, потому что внутри них нельзя выделить частей, которые можно было бы рассматривать как высказывания; в исчислении высказываний такие формулы называются атомарными). Из них с помощью пропозициональной связки "
" строится формула
. Как я уже говорил, обычно формула со свободной переменной интерпретируется так, будто по этой переменной есть квантор всеобщности, то есть, как
. Мы предполагаем, что эта формула взята из теории поля действительных чисел
, поэтому область действия квантора можно не указывать. Если же имеется в виду более широкая теория, то ограничение области действия квантора делается так:
. Поскольку тщательное следование формально определённому синтаксису с множеством скобок может оказаться муторным, обычно договариваются о сокращениях, позволяющих сделать запись формулы более короткой и понятной человеку, следя за тем, чтобы структура формулы распознавалась однозначно. То, что написал
arseniiv, как раз и есть такое сокращение того, что написал я.
Так доказательство противоречия в исчислении высказываний будет?
Вообще-то импликацию надо обозначать
В разной литературе используются разные обозначения: "
", "
", "
". Может быть, и ещё какие-нибудь есть. Давайте не будем обсуждать обозначения. Они достаточно разнообразны, и мы это побороть не сможем.