Формальное доказательство - Formal proof

В логика и математика, а формальное доказательство или же происхождение конечный последовательность из фразы (называется правильные формулы в случае формальный язык ), каждый из которых является аксиома, предположение, или следует из предыдущие предложения в последовательности на правило вывода.[1] Он отличается от аргументации на естественном языке тем, что является строгим, недвусмысленным и механически проверяемым.[2] Если набор предположений пуст, то последнее предложение в формальном доказательстве называется теорема из формальная система. Понятие теоремы не является общим эффективный, следовательно, может не быть метода, с помощью которого мы всегда можем найти доказательство данного предложения или определить, что его не существует. Концепции Доказательства в стиле Fitch, последовательное исчисление и естественный вычет находятся обобщения концепции доказательства.[3][4]

Теорема является синтаксическое следствие всех корректных формул, предшествующих ему в доказательстве. Чтобы правильно сформированная формула могла считаться частью доказательства, она должна быть результатом применения правила дедуктивный аппарат (некоторой формальной системы) к предыдущим правильно построенным формулам в последовательности доказательств.

Формальные доказательства часто строятся с помощью компьютеров в интерактивное доказательство теорем (например, с использованием корректор и автоматическое доказательство теорем ).[5] Примечательно, что эти доказательства могут быть проверяется автоматически, также с помощью компьютера. Проверка формальных доказательств обычно проста, в то время как проблема находка доказательства (автоматическое доказательство теорем ) обычно вычислительно трудноразрешимый и / или только полуразрешимый в зависимости от используемой формальной системы.

Фон

Формальный язык

Основная статья: Формальный язык

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

Формальная грамматика

Основные статьи: Формальная грамматика и Правило формирования

А формальная грамматика (также называемый правила формирования) - точное описание правильные формулы формального языка. Это синоним набора струны над алфавит формального языка, которые составляют хорошо составленные формулы. Однако он не описывает их семантика (т.е. что они означают).

Формальные системы

Основная статья: Формальная система

А формальная система (также называемый логическое исчисление, или логическая система) состоит из формального языка вместе с дедуктивный аппарат (также называемый дедуктивная система). Дедуктивный аппарат может состоять из набора правила трансформации (также называемый правила вывода) или набор аксиомы или и то, и другое. Формальная система используется для выводить одно выражение из одного или нескольких других выражений.

Интерпретации

Основные статьи: Формальная семантика (логика) и Интерпретация (логика)

An интерпретация формальной системы - это присвоение значений символам и значений истинности предложениям формальной системы. Изучение интерпретаций называется формальная семантика. Давать интерпретацию является синонимом строительство модель.

Смотрите также

Рекомендации

  1. ^ "Окончательный глоссарий высшего математического жаргона - строгость". Математическое хранилище. 2019-08-01. Получено 2019-12-12.
  2. ^ Кассиос, Яннис (20 февраля 2009 г.). «Формальное доказательство» (PDF). cs.utoronto.ca. Получено 2019-12-12.
  3. ^ Кембриджский философский словарь, вычет
  4. ^ Барвайз, Джон; Этчменди, Джон Этчменди (1999). Язык, доказательства и логика (1-е изд.). Seven Bridges Press и CSLI.
  5. ^ Харрисон, Джон (декабрь 2008 г.). «Формальное доказательство - теория и практика» (PDF). ams.org. Получено 2019-12-12.

внешняя ссылка