Напишите, пожалуйста, кто-нибудь два исходных высказывания этой теоремы.
Я не знаю, что Вы называете "исходными высказываниями теоремы". Для меня исходными высказываниями теоремы являются аксиомы математической логики, аксиомы той теории, к которой относится теорема (возможно, не все, что указывается в формулировке теоремы), а также дополнительные утверждения, которые автор добавляет к аксиомам. Также подразумеваются соответствующие правила вывода.
С точки зрения синтаксиса в формуле

здесь есть три терма

,

и

(термы — имена "вещей"; при этом "

" является переменной, а "

и "

" — константы), из которых с помощью символа бинарного отношения "

" построены две элементарные формулы

и

(эти формулы называются элементарными, потому что внутри них нельзя выделить частей, которые можно было бы рассматривать как высказывания; в исчислении высказываний такие формулы называются атомарными). Из них с помощью пропозициональной связки "

" строится формула

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

. Мы предполагаем, что эта формула взята из теории поля действительных чисел

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

. Поскольку тщательное следование формально определённому синтаксису с множеством скобок может оказаться муторным, обычно договариваются о сокращениях, позволяющих сделать запись формулы более короткой и понятной человеку, следя за тем, чтобы структура формулы распознавалась однозначно. То, что написал
arseniiv, как раз и есть такое сокращение того, что написал я.
Так доказательство противоречия в исчислении высказываний будет?
Вообще-то импликацию надо обозначать

В разной литературе используются разные обозначения: "

", "

", "

". Может быть, и ещё какие-нибудь есть. Давайте не будем обсуждать обозначения. Они достаточно разнообразны, и мы это побороть не сможем.