Доказуемость и выводимость

С помощью формул можно записывать точные формулировки свойств и утверждений в различных областях деятельности. Для этого необходимо выделить некоторое семейство исходных или первичных предикатов, с помощью которых записываются правила и закономерности. В качестве примера рассмотрим полную формулировку известного физического закона: при нагревании давление газа в замкнутом сосуде возрастает.

Соответствующая этому закону формула имеет вид:

Находиться (газ, x) & увеличиваться (температура, газ) &

являться (x, замкнутый сосуд) ®

увеличиваться (давление, газ).

Здесь использованы три первичных предиката: находиться, являться и увеличиваться. Наименования выбранных предикатов синонимичны отдельным фрагментам приведенной формулировки физического закона на естественном языке. Они подбираются с учетом требований точности передачи смысла и возможности применения в разных случаях.

В конкретных областях деятельности обычно применяют частично формализованные представления закономерностей и конкретных данных.

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

Всякий вывод осуществляется по определенным правилам. Такие правила носят характер схем, содержащих условия на структуру формул или соотношений, к которым применяется правило. Описания правил вывода удобно представлять выражениями вида: . Здесь A ₁,..., A _n - шаблоны посылок правила вывода, а A _n+1 - шаблон заключения или следствия.

К наиболее часто используемым правилам вывода относятся:

1) правило modus ponens ;

2) правило modus tollens ;

3) правило обобщения .

Корректность приведенных правил может быть установлена на основе приведенных ранее определений кванторов и таблиц истинности для логических связок.

Например, правило modus ponens утверждает, что если имеют место или справедливы соотношения, представляемые формулами A и A ® B, то справедливо и соотношение, выраженное формулой B. По таблице истинности для импликации, если A и A ® B являются истинными, то B - также истинная формула.

Логический вывод представляет собой цепочку соотношений, каждое из которых является либо исходным соотношением, либо получается из предыдущих соотношений последовательности по одному из правил вывода. Вывод решает некоторую задачу, если он содержит соотношение, являющееся целью этой задачи.

Возможны несколько методов построения выводов, решающих конкретные задачи.

Метод следствий использует правило modus ponens и состоит в порождении всевозможных следствий из исходных соотношений до тех пор, пока не будет получено заключение, являющееся решением задачи.

Метод рассуждений от противного использует правило modus tollens и основан на получении противоречия. К совокупности начальных истинных соотношений, добавляется отрицание утверждения - цели задачи. Это соответствует предположению о справедливости свойства, противоположного доказываемому свойству. Такое действие называется предположением о противном. Вывод, получаемый с помощью правила modus tollens, представляет собой цепочку отрицаний. Если в такой цепочке появляется соотношение Ø A, являющееся отрицанием некоторого начального соотношения A, то такая ситуация квалифицируется как противоречие, а предположение о противном - как неверное.

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