х
у
7) ¬ (0''' = 0') ⇒ ¬ (0'''' = 0'') [6; ⇒ ¬];
8) ¬ (0''' = 0') [5, 2; MP];
9) ¬ (0'''' = 0'') [7, 8; MP].
Остаётся заметить, что последним в списке стоит интересующее нас предложение ¬ (0′′′′ = 0′′).
Если мы теперь запишем все эти 9 предложений друг за другом, разделив их каким-нибудь знаком (для определённости – решёткой #), получим то, что называется формальным доказательством предложения ¬ (0'''' = 0''):
#
формальным доказательством
¬ ∃ x (x' = 0) # ¬ (0'' = 0) # (x' = у') ⇒ (х = у) # (0''' = 0') ⇒ (0'' = 0) # ¬ (0'' = 0) ⇒ ¬ (0''' = 0') # (0'''' = 0'') ⇒ (0''' = 0') # ¬ (0''' = 0') ⇒ ¬ (0'''' = 0'') # ¬ (0''' = 0') # ¬ (0'''' = 0'').
x
x
x
у
х
у
На этом примере состоялось знакомство с важнейшим понятием формального доказательства. Неформальные доказательства (которые называют ещё содержательными или психологическими) представляют собою убедительные рассуждения, т. е. прежде всего тексты, состоящие из утверждений (не любые такие тексты, разумеется). Формальное же доказательство есть цепочка предложений, особым образом организованная. Читатель может возразить, что в начальном разделе статьи сообщалось, что формальное доказательство есть цепочка символов. Тут нет противоречия: ведь каждое предложение есть цепочка символов, и если составить их вместе, разделив каким-либо разделительным знаком, то снова возникнет не что иное, как цепочка символов, как это и видно из нашего примера. Таким образом, формальное доказательство есть слово, которое составлено из букв дополненного разделительным знаком алфавита.