Формальное доказательство
В логике и математике формальное доказательство или вывод конечную последовательность предложений представляет собой (известных как правильно построенные формулы применительно к формальному языку ), каждое из которых является аксиомой , предположением или следует из предыдущих предложений в последовательности. по правилу вывода . Он отличается от аргумента на естественном языке тем, что он строгий, однозначный и механически проверяемый. [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 истина ⊤ |
|---|
