Формальная система — это абстрактная структура или формализация аксиоматической системы , используемая для вывода теорем из аксиом с помощью набора правил вывода . [1]
В 1921 году Дэвид Гильберт предложил использовать формальную систему в качестве основы математических знаний . [2]
Термин « формализм» иногда является грубым синонимом формальной системы , но он также относится к определенному стилю обозначений , например, к нотации Бракета Поля Дирака .
Формальная система имеет следующее: [3] [4] [5]
Формальная система называется рекурсивной (т.е. эффективной) или рекурсивно перечислимой, если набор аксиом и набор правил вывода являются разрешимыми множествами или полуразрешимыми множествами соответственно.
Формальный язык — это язык, который определяется формальной системой. Как и языки в лингвистике , формальные языки обычно имеют два аспекта:
Обычно через понятие формальной грамматики рассматривается только синтаксис формального языка . Двумя основными категориями формальных грамматик являются порождающие грамматики , которые представляют собой наборы правил записи строк на языке, и аналитические грамматики ( или редуктивные грамматики [6] [7] ), которые представляют собой наборы правил. о том, как можно проанализировать строку, чтобы определить, является ли она членом языка.
Дедуктивная система , также называемая дедуктивным аппаратом , [8] состоит из аксиом (или схем аксиом ) и правил вывода , которые можно использовать для вывода теорем системы. [9]
Такие дедуктивные системы сохраняют дедуктивные качества формул , выраженных в системе. Обычно нас интересует истина , а не ложь. Однако вместо этого могут быть сохранены другие модальности , такие как оправдание или убеждение .
Чтобы сохранить свою дедуктивную целостность, дедуктивный аппарат должен быть определяемым без ссылки на какую-либо предполагаемую интерпретацию языка. Цель состоит в том, чтобы гарантировать, что каждая строка вывода является просто логическим следствием строк, которые ей предшествуют. Не должно быть никакого элемента какой-либо интерпретации языка, связанного с дедуктивной природой системы.
Логическое следствие (или следствие) системы из ее логического основания — это то, что отличает формальную систему от других, которые могут иметь некоторую основу в абстрактной модели. Часто формальная система будет основой или даже отождествлена с более широкой теорией или областью (например, евклидовой геометрией ), совместимой с использованием в современной математике, такой как теория моделей . [ нужны разъяснения ]
Примером дедуктивной системы является логика первого порядка .
Двумя основными типами дедуктивных систем являются системы доказательств и формальная семантика. [8]
Формальные доказательства — это последовательности правильно сформированных формул (или для краткости WFF), которые могут быть либо аксиомой , либо результатом применения правила вывода к предыдущим WFF в последовательности доказательства. Последний WFF в последовательности признается теоремой .
Как только формальная система задана, можно определить набор теорем, которые можно доказать внутри формальной системы. Этот набор состоит из всех WFF, для которых существует доказательство. Таким образом, все аксиомы считаются теоремами. В отличие от грамматики WFF, нет никакой гарантии, что будет существовать процедура принятия решения, является ли данная WFF теоремой или нет.
Точку зрения, согласно которой создание формальных доказательств — это все, что есть в математике, часто называют формализмом . Дэвид Гильберт основал метаматематику как дисциплину для обсуждения формальных систем. Любой язык, на котором говорят о формальной системе, называется метаязыком . Метаязык может быть естественным языком или сам частично формализован, но он, как правило, менее полностью формализован, чем формальный языковой компонент рассматриваемой формальной системы, который тогда называется объектным языком , то есть объектом языка. обсуждение под вопросом. Понятие только что определенной теоремы не следует путать с теоремами о формальной системе , которые во избежание путаницы обычно называют метатеоремами .
Логическая система — это дедуктивная система (чаще всего логика первого порядка ) вместе с дополнительными нелогическими аксиомами . Согласно теории моделей , логической системе могут быть даны интерпретации , которые описывают, удовлетворяет ли данная структура (отображение формул определенному значению) правильно сформированной формуле. Структура, удовлетворяющая всем аксиомам формальной системы, называется моделью логической системы.
Логическая система – это:
Примером логической системы является арифметика Пеано . Стандартная модель арифметики определяет областью обсуждения неотрицательные целые числа и придает символам их обычное значение. [10] Существуют также нестандартные модели арифметики .
Ранние логические системы включают индийскую логику Панини , силлогистическую логику Аристотеля, пропозициональную логику стоицизма и китайскую логику Гунсунь Луна (ок. 325–250 до н. э.). В более поздние времена среди авторов были Джордж Буль , Огастес Де Морган и Готтлоб Фреге . Математическая логика была разработана в Европе 19 века .
Давид Гильберт спровоцировал формалистическое движение под названием «Программа Гильберта» как предложенное решение фундаментального кризиса математики , который в конечном итоге был смягчен теоремами Гёделя о неполноте . [2] Манифест КЭД представлял собой последующую, пока еще безуспешную попытку формализации известной математики.
СМИ, связанные с формальными системами, на Викискладе?
