Напишите, пожалуйста, кто-нибудь два исходных высказывания этой теоремы.
Я не знаю, что Вы называете "исходными высказываниями теоремы". Для меня исходными высказываниями теоремы являются аксиомы математической логики, аксиомы той теории, к которой относится теорема (возможно, не все, что указывается в формулировке теоремы), а также дополнительные утверждения, которые автор добавляет к аксиомам. Также подразумеваются соответствующие правила вывода.
С точки зрения синтаксиса в формуле
![$\forall x\in\mathbb R.\;x>4\Rightarrow x>2$ $\forall x\in\mathbb R.\;x>4\Rightarrow x>2$](https://dxdy-03.korotkov.co.uk/f/2/7/3/2730829666d26f9e58831aa6e85a851682.png)
здесь есть три терма
![$x$ $x$](https://dxdy-04.korotkov.co.uk/f/3/3/2/332cc365a4987aacce0ead01b8bdcc0b82.png)
,
![$4$ $4$](https://dxdy-03.korotkov.co.uk/f/e/c/f/ecf4fe2774fd9244b4fd56f7e76dc88282.png)
и
![$2$ $2$](https://dxdy-04.korotkov.co.uk/f/7/6/c/76c5792347bb90ef71cfbace628572cf82.png)
(термы — имена "вещей"; при этом "
![$x$ $x$](https://dxdy-04.korotkov.co.uk/f/3/3/2/332cc365a4987aacce0ead01b8bdcc0b82.png)
" является переменной, а "
![$4$ $4$](https://dxdy-03.korotkov.co.uk/f/e/c/f/ecf4fe2774fd9244b4fd56f7e76dc88282.png)
и "
![$2$ $2$](https://dxdy-04.korotkov.co.uk/f/7/6/c/76c5792347bb90ef71cfbace628572cf82.png)
" — константы), из которых с помощью символа бинарного отношения "
![$>$ $>$](https://dxdy-03.korotkov.co.uk/f/6/d/e/6de15a59c5cd495a7f9f6484e738623b82.png)
" построены две элементарные формулы
![$x>4$ $x>4$](https://dxdy-02.korotkov.co.uk/f/d/6/9/d6927ba13192d08d76925a34320b0b7e82.png)
и
![$x>2$ $x>2$](https://dxdy-03.korotkov.co.uk/f/e/6/d/e6d0e5ad5e4108d0601ee2738ecefee282.png)
(эти формулы называются элементарными, потому что внутри них нельзя выделить частей, которые можно было бы рассматривать как высказывания; в исчислении высказываний такие формулы называются атомарными). Из них с помощью пропозициональной связки "
![$\Rightarrow$ $\Rightarrow$](https://dxdy-04.korotkov.co.uk/f/7/7/7/777d001ea1ec5971b67bb546ed760f9782.png)
" строится формула
![$(x>4)\Rightarrow(x>2)$ $(x>4)\Rightarrow(x>2)$](https://dxdy-01.korotkov.co.uk/f/4/d/d/4ddec4ff90775d0fc0cc5e3d415fc4e982.png)
. Как я уже говорил, обычно формула со свободной переменной интерпретируется так, будто по этой переменной есть квантор всеобщности, то есть, как
![$\forall x((x>4)\Rightarrow(x>2))$ $\forall x((x>4)\Rightarrow(x>2))$](https://dxdy-04.korotkov.co.uk/f/b/c/2/bc21adacbcc7c9031fbf3e469aed7a3982.png)
. Мы предполагаем, что эта формула взята из теории поля действительных чисел
![$\mathbb R$ $\mathbb R$](https://dxdy-04.korotkov.co.uk/f/b/c/0/bc0baa1bd1772406881ea71a3524054d82.png)
, поэтому область действия квантора можно не указывать. Если же имеется в виду более широкая теория, то ограничение области действия квантора делается так:
![$\forall x((x\in\mathbb R)\Raightarrow((x>4)\Rightarrow(x>2)))$ $\forall x((x\in\mathbb R)\Raightarrow((x>4)\Rightarrow(x>2)))$](https://dxdy-04.korotkov.co.uk/f/7/2/b/72bad9a397fdffaf9eb32c34be63ea0582.png)
. Поскольку тщательное следование формально определённому синтаксису с множеством скобок может оказаться муторным, обычно договариваются о сокращениях, позволяющих сделать запись формулы более короткой и понятной человеку, следя за тем, чтобы структура формулы распознавалась однозначно. То, что написал
arseniiv, как раз и есть такое сокращение того, что написал я.
Так доказательство противоречия в исчислении высказываний будет?
Вообще-то импликацию надо обозначать
![$\rightarrow$ $\rightarrow$](https://dxdy-03.korotkov.co.uk/f/e/5/d/e5d134f35dc4949fab12ec64d186248a82.png)
В разной литературе используются разные обозначения: "
![$\to$ $\to$](https://dxdy-03.korotkov.co.uk/f/e/4/9/e49c6dac8af82421dba6bed976a80bd982.png)
", "
![$\Rightarrow$ $\Rightarrow$](https://dxdy-04.korotkov.co.uk/f/7/7/7/777d001ea1ec5971b67bb546ed760f9782.png)
", "
![$\supset$ $\supset$](https://dxdy-03.korotkov.co.uk/f/2/5/7/257dca152ad46effcbe4eff50b39c8f782.png)
". Может быть, и ещё какие-нибудь есть. Давайте не будем обсуждать обозначения. Они достаточно разнообразны, и мы это побороть не сможем.