Формальное доказательство
В логике и математике формальное доказательство или вывод представляет собой конечную последовательность предложений . (называемых корректными формулами в случае формального языка ), каждое из которых является аксиомой , предположением или следует из предыдущих предложений в последовательности по правилу вывода . Он отличается от аргумента на естественном языке тем, что он строгий, однозначный и механически проверяемый. [1] Если множество предположений пусто, то последнее предложение формального доказательства называется теоремой формальной системы . Понятие теоремы в целом неэффективно , поэтому не может быть метода, с помощью которого мы всегда могли бы найти доказательство данного предложения или определить, что его не существует. Концепции доказательства в стиле Фитча , секвенциального исчисления и естественной дедузии являются обобщениями концепции доказательства. [2] [3]
Теорема является синтаксическим следствием всех предшествующих ей в доказательстве корректных формул. Чтобы правильно построенная формула могла считаться частью доказательства, она должна быть результатом применения правила дедуктивного аппарата (некоторой формальной системы) к предыдущим правильно построенным формулам в последовательности доказательства.
Формальные доказательства часто строятся с помощью компьютеров при интерактивном доказательстве теорем (например, с помощью средства проверки доказательств и автоматического доказательства теорем ). [4] Примечательно, что эти доказательства могут быть проверены автоматически, в том числе с помощью компьютера. Проверка формальных доказательств обычно проста, в то время как проблема поиска доказательств (автоматическое доказательство теорем) обычно неразрешима с вычислительной точки зрения и/или разрешима лишь наполовину , в зависимости от используемой формальной системы.
Предыстория [ править ]
Формальный язык [ править ]
Формальный язык это набор конечных последовательностей символов . — Такой язык можно определить без ссылки на какие-либо значения любого из его выражений; оно может существовать до того, как ему будет присвоена какая-либо интерпретация , то есть до того, как оно обретет какое-либо значение. Формальные доказательства выражаются на некоторых формальных языках.
Формальная грамматика [ править ]
Формальная грамматика (также называемая правилами формирования ) — это точное описание правильно построенных формул формального языка. Это синоним набора строк в алфавите формального языка, которые составляют правильно составленные формулы. Однако он не описывает их семантику (то есть, что они означают).
Формальные системы [ править ]
Формальная система (также называемая логическим исчислением или логической системой ) состоит из формального языка вместе с дедуктивным аппаратом (также называемым дедуктивной системой ). Дедуктивный аппарат может состоять из набора правил преобразования (также называемых правилами вывода ) или набора аксиом , либо иметь и то, и другое. Формальная система используется для получения одного выражения из одного или нескольких других выражений.
Интерпретации [ править ]
Интерпретация формальной системы — это присвоение значений символам и значений истинности предложениям формальной системы. Изучение интерпретаций называется формальной семантикой . Предоставление интерпретации является синонимом построения модели .
См. также [ править ]
- Аксиоматическая система
- Формальная проверка
- Математическое доказательство
- Помощник по доказательствам
- Исчисление доказательств
- Теория доказательств
- Доказательство (истина)
- Фактор Брюйна
Ссылки [ править ]
- ^ Кассиос, Яннис (20 февраля 2009 г.). «Формальное доказательство» (PDF) . cs.utoronto.ca . Проверено 12 декабря 2019 г.
- ^ Кембриджский философский словарь, дедукция
- ^ Барвайз, Джон; Этчеменди, Джон Этчеменди (1999). Язык, доказательства и логика (1-е изд.). Seven Bridges Press и CSLI.
- ^ Харрисон, Джон (декабрь 2008 г.). «Формальное доказательство — теория и практика» (PDF) . ams.org . Проверено 12 декабря 2019 г.
Внешние ссылки [ править ]
- «Специальный выпуск о формальных доказательствах» . Уведомления Американского математического общества . Декабрь 2008 года.
- 2πix.com: Логика Часть серии статей, посвященных математике и логике.
- Архив формальных доказательств
- Домашняя страница плотника
- Pr∞fWiki, Определение: Система доказательств/Формальное доказательство
Логическая Logical truth истина ⊤ |
|---|
