В дедуктивных системах имеется операция, обозначаемая "" или "".
Она связывает какие-нибудь формулы, например:
A B (1)
Такая запись означает, что формула B может быть доказана в данной дедуктивной системе на основе формулы A.
Это можно сформулировать и в виде условного высказывания:
"Если формула A доказана в данной дедуктивной системе, то в этой же системе можно построить доказательство и для формулы B. (2)
Часто понятия "доказано" и "истинно" смешивают, хотя между ними существуют определенные различия. Но допустим, что истинной
называется всякая формула, которую можно доказать в данной дедуктивной системе. Тогда высказывание (1) можно переформулировать так:
"Если A, то B". (3)
Очень похоже на то, что нужно. Осталось лишь найти ту самую дедуктивную систему. Какой она должна быть? Формулами в ней должны
быть высказывания. Правила доказательства (их называют "правилами вывода") должны быть такими, чтобы всякому доказательству (1)
соответствовало истинное условное высказывание в форме (3). И наоборот: надо, чтобы для всякого истинного условного высказывания
(3) можно было бы найти доказательство вида (1).
Где взять такую дедуктивную систему? Таких систем много. Например, классическое исчисление высказываний и классическое исчисление
предикатов позволяют доказывать условные высказывания, в которых A и B - формулы с логическими
связками "и", "или", "не", материальной импликацией, кванторами и др. Это довольно обширный круг формул, позволяющий математически
выражать истинность разнообразных высказываний, сформулированных на обычном языке примерно по такой схеме:
X & Y - "X и Y"
X Y - "X или Y, или и то, и другое вместе."
X Y - "Либо X, либо Y, но не то, и другое вместе."
~X - "неправда, что X"
X Y - "Неправда, что X или Y, или и то, и другое вместе."
(обратите внимание, что материальная импликация не переводится по схеме "если... то...").
X Y - "X и Y имеют одинаковую истинность."
(обратите внимание, что этот перевод не делается по схеме "...необходимо и достаточно...").
P(x) - некоторое высказывание, истинность которого зависит от выбора x.
P(x, y) - некоторое высказывание, истинность которого зависит от выбора x и y.
x P(x) - "Для любого x истинно высказывание P(x)"
x P(x) - "Существует x, для которого истинно высказывание P(x)"
Таким образом, во многих случаях условное высказывание вида (3) в самом деле может быть выражено через формулу вида (1). Однако
проблема состоит в том, что зачастую на "выражении через" все и заканчивается. Допустим, у нас есть некоторое высказывание вида (3).
Мы пишем формулу вида (1). Возникает вопрос: ну и чему равна истинность формулы (1)? Нужно как-то ее определить. Ответ, исходя из принятого
соглашения: она истинна, если можно построить цепочку доказательств от A до B. Следующий вопрос: а
как определить, можно или нельзя? Этот вопрос очень сложен, и зачастую нерешаем даже путем полного перебора (из-за того, что
количество вариантов может быть бесконечным). На этот вопрос часто ссылаются как на вопрос о "выводимости" или "доказуемости".
Ответ на него дается обычно только для ограниченного круга формул вида A, которые называются аксиомами.
В общем случае для произвольных A и B определенного ответа нет. В ряде дедуктивных систем есть точный
ответ для произвольной аксиомы A и произвольной формулы B, и наличие таких ответов называется "полнотой",
а отсутствие некоторых ответов - "неполнотой".
Однако обычно нет ответа для произвольной формулы (а не только аксиомы)
A и произвольной формулы B. Можно попытаться
перечислить некоторые случаи, или даже некоторые множества случаев, но
для всех возможных случаев ответа нет.
Еще одна неясность состоит в том, что в принципе мы можем сотворить любую дедуктивную систему, очень далекую от классической, и
непонятно, что тогда получится. Будет ли операция "" в формуле (1) для этой дедуктивной системы
соответствовать условному высказыванию (3)? В общем случае не будет, поскольку ничто не мешает нам написать намеренно бредовые правила
вывода и аксиомы, не имеющие даже отдаленного отношения к тому, что мы называем "истиной". Но как в общем случае узнать, какие
дедуктивные системы подходят, а какие нет?