Формальная система используется для выведения из аксиом теоремы в соответствии с набором правил. Эти правила, которые используются для вывода теорем из аксиом, являются логическим исчислением формальной системы. Формальная система - это, по сути, « аксиоматическая система ». [1]
В 1921 году Дэвид Гильберт предложил использовать такую систему в качестве основы для математических знаний . [2] Формальная система может представлять собой четко определенную систему абстрактного мышления .
Термин формализм иногда грубый синоним формальной системы , но она также относится к данному стилю обозначений , например, Поль Дирак «s Бра и кет .
Задний план
Каждая формальная система использует примитивные символы (которые вместе образуют алфавит ) для конечного построения формального языка из набора аксиом с помощью логических правил формирования .
Таким образом, система состоит из действительных формул, построенных с помощью конечных комбинаций примитивных символов - комбинаций, образованных из аксиом в соответствии с установленными правилами. [3]
Более формально это можно выразить так:
- Конечный набор символов, известный как алфавит, который объединяет формулы, так что формула представляет собой всего лишь конечную строку символов, взятых из алфавита.
- Грамматика , состоящая из правил , чтобы сформировать формулы из простых формул. Формула считается правильно построенной, если она может быть сформирована с использованием правил формальной грамматики. Часто требуется, чтобы существовала процедура принятия решения о том, правильно ли составлена формула.
- Набор аксиом или схем аксиом , состоящий из правильно составленных формул.
- Набор правил вывода . Правильно построенная формула, которую можно вывести из аксиом, известна как теорема формальной системы.
Рекурсивный
Формальная система называется рекурсивной (т. Е. Эффективной) или рекурсивно перечислимой, если набор аксиом и набор правил вывода являются разрешимыми множествами или полуразрешимыми множествами , соответственно.
Вывод и следствие
Воплощение системы ее логическим фундаментом является то , что отличает официальную систему от других , которые могут иметь некоторую основу в абстрактной модели. Часто формальная система является основой или даже отождествляется с более крупной теорией или областью (например, евклидовой геометрией ), совместимой с использованием в современной математике, такой как теория моделей . [ требуется разъяснение ]
Формальный язык
Формальный язык является языком , который определяется формальной системой. Как и языки в лингвистике , формальные языки обычно имеют два аспекта:
- синтаксис языка является то , что язык выглядит (более формально: множество возможных выражений , которые являются допустимым высказыванием в языке) , изучаемые в теории формальных языков
- что семантика зыка то , что высказывания языка среднего (который формализованные различными способами, в зависимости от типа языка в вопросе)
В информатике и лингвистике обычно рассматривается только синтаксис формального языка через понятие формальной грамматики . Формальная грамматика является точным описанием синтаксиса формального языка: с набором из строк . Две основные категории формальной грамматики - это порождающие грамматики , которые представляют собой наборы правил того, как могут быть созданы строки в языке, и категория аналитических грамматик (или редуктивных грамматик, [4] [5] ), которые представляют собой наборы правил. о том, как можно проанализировать строку, чтобы определить, является ли она членом языка. Короче говоря, аналитическая грамматика описывает, как распознать, когда строки являются членами в наборе, тогда как генеративная грамматика описывает, как записывать только эти строки в наборе.
В математике формальный язык обычно описывается не формальной грамматикой, а (а) естественным языком, например английским. Логические системы определяются как дедуктивной системой, так и естественным языком. Дедуктивные системы, в свою очередь, определяются только естественным языком (см. Ниже).
Дедуктивная система
Дедуктивная система , которая также называется дедуктивной аппаратом или логика , состоит из аксиом (или аксиомы схем ) и правил вывода , которые могут быть использованы для вывести теоремы системы. [6]
Такие дедуктивные системы сохраняют дедуктивные качества в формулах , которые выражаются в системе. Обычно нас интересует правда, а не ложь. Однако вместо этого могут быть сохранены другие условия , такие как оправдание или убеждение .
Чтобы поддерживать свою дедуктивную целостность, дедуктивный аппарат должен быть определен без ссылки на любую предполагаемую интерпретацию языка. Цель состоит в том, чтобы гарантировать, что каждая строка производной является просто синтаксическим следствием строк, которые ей предшествуют. В какой-либо интерпретации языка не должно быть элемента , связанного с дедуктивной природой системы.
Примером дедуктивной системы является логика предикатов первого порядка .
Логическая система
Логическая система или язык (не следует путать с рода «формальный язык» обсуждалось выше , которая описывается формальной грамматики), является дедуктивной системой (см раздел выше, наиболее часто логики предикатов первого порядка ) вместе с дополнительным (не логические) аксиомы и семантика [ оспариваются ] . Согласно теоретико-модельной интерпретации , семантика логической системы описывает, удовлетворяется ли правильно сформированная формула данной структурой. Структура, удовлетворяющая всем аксиомам формальной системы, известна как модель логической системы. Логическая система является здоровой, если каждая правильно построенная формула, которая может быть выведена из аксиом, удовлетворяется каждой моделью логической системы. И наоборот, логическая система является полной, если каждая правильно сформированная формула, которой удовлетворяет каждая модель логической системы, может быть выведена из аксиом.
Пример логической системы - арифметика Пеано .
История
Ранние логические системы включают индийскую логику Панини , силлогистическую логику Аристотеля, логику высказываний стоицизма и китайскую логику Гунсун Лун (ок. 325–250 до н. Э.). В последнее время участниками стали Джордж Буль , Август Де Морган и Готлоб Фреге . Математическая логика была разработана в Европе 19 века .
Формализм
Программа Гильберта
Давид Гильберт спровоцировал формалистическое движение, которое в конечном итоге было сдержано теоремами Гёделя о неполноте .
Манифест QED
Манифест QED представляет собой последующую, пока безуспешную попытку формализации известной математики.
Примеры
Примеры формальных систем включают:
- Лямбда-исчисление
- Исчисление предикатов
- Исчисление высказываний
Варианты
Следующие системы являются вариациями формальных систем [ требуется пояснение ] .
Система доказательств
Формальные доказательства - это последовательности хорошо составленных формул (или сокращенно wff). Чтобы wff квалифицировалось как часть доказательства, это может быть либо аксиома, либо продукт применения правила вывода к предыдущим wff в последовательности доказательств. Последний wff в последовательности признается теоремой .
Точку зрения, что создание формальных доказательств - это все, что нужно для математики, часто называют формализмом . Дэвид Гильберт основал метаматематику как дисциплину для обсуждения формальных систем. Любой язык, на котором говорят о формальной системе, называется метаязыком . Метаязык может быть естественным языком или может быть частично формализован сам по себе, но, как правило, он менее полно формализован, чем формальный языковой компонент рассматриваемой формальной системы, который затем называется объектным языком , то есть объектом обсуждаемое обсуждение.
Как только формальная система задана, можно определить набор теорем, которые могут быть доказаны внутри формальной системы. Этот набор состоит из всех wffs, для которых есть доказательство. Таким образом, все аксиомы считаются теоремами. В отличие от грамматики для wffs, нет никакой гарантии, что будет процедура принятия решения для определения того, является ли данный wff теоремой или нет. Понятие только что определенной теоремы не следует путать с теоремами о формальной системе , которые во избежание путаницы обычно называют метатеоремами .
Смотрите также
|
|
Рекомендации
- ^ "Формальная система, ENCYCLOPDIA BRITANNICA" .
- ^ "Программа Гильберта, Стэнфордская энциклопедия философии" .
- ↑ Encyclopdia Britannica,Определение формальной системы , 2007.
- ^ Редуктивная грамматика: ( информатика ) Набор синтаксических правил для анализа строк, чтобы определить, существуют ли строки в языке. "Научно-технический словарь Макгроу-Хилл Словарь научных и технических терминов" (6-е изд.). Макгроу-Хилл.[ ненадежный источник? ] Об авторе Составлено редакторами Энциклопедии науки и технологий McGraw-Hill (Нью-Йорк, штат Нью-Йорк), штатным сотрудником, который представляет передовые навыки, знания и инновации в научных публикациях. [1]
- ^ "Существует два класса схем написания компилятором определений формального языка.Подходпродуктивной грамматики является наиболее распространенным. Продуктивная грамматика состоит в основном из набора правил, которые описывают метод генерации всех возможных строк языка. Редуктивная илиметод аналитической грамматики устанавливает набор правил, которые описывают метод анализа любой строки символов и принятия решения о том, находится ли эта строка на языке ". « Система компилятора-компилятора TREE-META: система мета-компилятора для Univac 1108 и General Electric 645 , Технический отчет Университета Юты RADC-TR-69-83. С. Стивен Карр, Дэвид А. Лютер, Шериан Эрдманн» ( PDF) . Проверено 5 января 2015 года .
- ^ Хантер, Джеффри, Metalogic: Введение в метатеорию стандартной логики первого порядка, Калифорнийский университет Pres, 1971
дальнейшее чтение
- Раймонд М. Смуллян , 1961. Теория формальных систем: Анналы математических исследований , Princeton University Press (1 апреля 1961 г.) 156 страниц ISBN 0-691-08047-X
- Стивен Коул Клини , 1967. « Математическая логика», перепечатанная Dover, 2002. ISBN 0-486-42533-9
- Дуглас Хофштадтер , 1979. Гедель, Эшер, Бах: вечная золотая косаISBN 978-0-465-02656-2 . 777 страниц.
Внешние ссылки
- СМИ, связанные с формальными системами на Викискладе?
- Британская энциклопедия, Определение формальной системы , 2007.
- Что такое формальная система? : Некоторые цитаты из книги Джона Хогеланда «Искусственный интеллект: сама идея» (1985), стр. 48–64.
- Питер Субер, Формальные системы и машины: изоморфизм , 1997.