Войти
A формальная система используется для вывода теорем из аксиом по набору правил. Эти правила, которые используются для вывода теорем из аксиом, являются логическим исчислением формальной системы. Формальная система - это, по сути, «аксиоматическая система ». Филологу IV века до н.э. Панини приписывают первое использование формальной системы в грамматике санскрита. В 1921 году Давид Гильберт предложил использовать такую систему в качестве основы для познания в математике. Формальная система может представлять четко определенную систему абстрактного мышления.
Термин формализм иногда является грубым синонимом формальной системы, но он также относится к заданному стилю нотации, например, бюстгальтерная нотация Поля Дирака .
Каждая формальная система использует примитивные символы (которые вместе образуют алфавит ), чтобы окончательно сконструировать формальный язык из набора аксиом с помощью выводимых правил формирования.
Таким образом, система состоит из действительные формулы, построенные с помощью конечных комбинаций примитивных символов - комбинаций, предназначенных для med из аксиом в соответствии с установленными правилами.
Более формально это можно выразить следующим образом:
Формальная система называется рекурсивной (т.е. эффективной) или рекурсивно перечислимым, если набор аксиом и набор правил вывода являются разрешимыми наборами или полуразрешимыми наборами соответственно.
следствие системы по ее логическому основанию - это то, что отличает формальную систему от других, которые могут иметь некоторую основу в абстрактной модели. Часто формальная система будет основой или даже отождествляться с более крупной теорией или областью (например, евклидовой геометрией ), совместимой с использованием в современной математике, такой как теория моделей.
A Формальный язык - это язык, который определяется формальной системой. Как и языки в лингвистике, формальные языки обычно имеют два аспекта:
В информатике и лингвистике обычно только синтаксис формального языка рассматривается через понятие формальной грамматики. Формальная грамматика - это точное описание синтаксиса формального языка: набор из строк. Две основные категории формальной грамматики - это порождающие грамматики, которые представляют собой наборы правил того, как могут быть созданы строки в языке, и категория аналитических грамматик (или редуктивная грамматика,), которые представляют собой наборы правил того, как строка может быть проанализирована, чтобы определить, является ли она членом языка. Короче говоря, аналитическая грамматика описывает, как распознать, когда строки являются членами набора, тогда как порождающая грамматика описывает, как записывать только эти строки в наборе.
В математике формальный язык обычно описывается не формальной грамматикой, а (а) естественным языком, таким как английский. Логические системы определяются как дедуктивной системой, так и естественным языком. Дедуктивные системы, в свою очередь, определяются только естественным языком (см. Ниже).
Дедуктивная система, также называемая дедуктивным аппаратом или логикой, состоит из аксиом (или схемы аксиом ) и правила вывода, которые могут использоваться для вывода теорем системы.
Такие дедуктивные системы сохраняют дедуктивные качества в формулы , которые выражаются в системе. Обычно нас интересует истина, а не ложь. Однако вместо этого могут быть сохранены другие модальности, такие как обоснование или убеждение.
Чтобы поддерживать свою дедуктивную целостность, дедуктивный аппарат должен быть определен без ссылки на любую предполагаемую интерпретацию языка. Цель состоит в том, чтобы гарантировать, что каждая строка производной является просто синтаксическим следствием строк, которые ей предшествуют. В какой-либо интерпретации языка не должно быть элементов, которые связаны с дедуктивной природой системы.
Примером дедуктивной системы является логика предикатов первого порядка.
логическая система или язык (не путать с рассмотренным выше видом "формального языка", который описывается формальной грамматикой), представляет собой дедуктивную систему (см. раздел выше; чаще всего логика предикатов первого порядка ) вместе с дополнительными (нелогическими) аксиомами и семантикой. Согласно теоретико-модельной интерпретации, семантика логической системы описывает, удовлетворяется ли правильно сформированная формула данной структурой. Структура, удовлетворяющая всем аксиомам формальной системы, известна как модель логической системы. Логическая система здорова, если каждая правильно построенная формула, которая может быть выведена из аксиом, удовлетворяется каждой моделью логической системы. И наоборот, логическая система является полной, если каждая правильно сформированная формула, которой удовлетворяет каждая модель логической системы, может быть выведена из аксиом.
Пример логической системы: арифметика Пеано.
Ранние логические системы включают индийскую логику Панини, силлогистическую логику Аристотеля, логику высказываний стоицизма и китайской логики Гунсунь Лун (ок. 325–250 до н. э.). В последнее время участниками стали Джордж Буль, Август Де Морган и Готтлоб Фреге. Математическая логика была разработана в XIX веке Европа.
Дэвид Гильберт спровоцировал движение формалистов, которое в конечном итоге было сдержано Теоремы о неполноте.
Манифест QED представляет собой последующую, пока безуспешную попытку формализации известной математики.
Примеры формальных систем:
следующие системы являются вариациями формальных систем.
Формальные доказательства - это последовательности правильно построенных формул (или сокращенно wff). Для того, чтобы wff квалифицировалось как часть доказательства, это может быть либо аксиома , либо результат применения правила вывода к предыдущим wff в последовательности доказательств. Последний wff в последовательности распознается как теорема.
Точка зрения, согласно которой создание формальных доказательств - это все, что нужно для математики, часто называется формализмом. Дэвид Гильберт основал метаматематику как дисциплину для обсуждения формальных систем. Любой язык, на котором говорят о формальной системе, называется метаязыком. Метаязык может быть естественным языком, или он может быть частично формализован сам по себе, но, как правило, он менее полно формализован, чем формальный языковой компонент рассматриваемой формальной системы, который затем называется объектным языком, который есть, предмет обсуждаемого обсуждения.
Как только формальная система задана, можно определить набор теорем, которые могут быть доказаны внутри формальной системы. Этот набор состоит из всех wffs, для которых есть доказательство. Таким образом, все аксиомы считаются теоремами. В отличие от грамматики для wffs, нет никакой гарантии, что будет процедура принятия решения для решения, является ли данный wff теоремой или нет. Понятие только что определенной теоремы не следует путать с теоремами о формальной системе, которые во избежание путаницы обычно называются метатеоремами.
|
 | Поищите формализация в Викисловаре, бесплатном словаре. |
СМИ, связанные с формальными системами на Wikimedia Commons
Системный научный портал 
Философский портал