Формальная система

Формальная система — это абстрактная структура и формализация используемая аксиоматической системы, для вывода теорем из аксиом с помощью набора правил вывода . ^[1]

В 1921 году Дэвид Гильберт предложил использовать формальные системы в качестве основы знаний в математике . ^[2]

Термин «формализм» иногда является грубым синонимом формальной системы , но он также относится к определенному стилю обозначений , например, Поля Дирака к нотации Бракета .

Концепции

Формальная система имеет следующее: ^[3]^[4]^[5]

Формальный язык , представляющий собой набор правильно построенных формул , представляющих собой строки символов из алфавита , образованных формальной грамматикой (состоящей из правил производства или правил формирования ).
Дедуктивная система, дедуктивный аппарат или система доказательств , которая имеет правила вывода , использующие аксиомы и выводящие теоремы , которые являются частью формального языка.

Формальная система называется рекурсивной (т.е. эффективной) или рекурсивно перечислимой, если набор аксиом и набор правил вывода являются разрешимыми множествами или полуразрешимыми множествами соответственно.

Официальный язык

Формальный язык — это язык, который определяется формальной системой. Как и языки в лингвистике , формальные языки обычно имеют два аспекта:

синтаксис — это то, как выглядит язык (более формально: набор возможных выражений, которые являются допустимыми высказываниями на языке)
семантика - это то, что означают высказывания языка (что формализуется различными способами, в зависимости от типа рассматриваемого языка)

Обычно только синтаксис формального языка рассматривается через понятие формальной грамматики . Двумя основными категориями формальных грамматик являются порождающие грамматики , которые представляют собой наборы правил записи строк на языке, и аналитические грамматики (или редуктивные грамматики). ^[6]^[7]), которые представляют собой наборы правил того, как можно проанализировать строку, чтобы определить, является ли она членом языка.

Дедуктивная система

, Дедуктивная система также называемая дедуктивным аппаратом , ^[8] состоит из аксиом (или схем аксиом ) и правил вывода , которые можно использовать для вывода теорем системы. ^[9]

Такие дедуктивные системы сохраняют дедуктивные качества формул , выраженных в системе. Обычно нас интересует истина, а не ложь. Однако другие модальности , такие как оправдание или убеждение вместо этого могут быть сохранены .

Чтобы сохранить свою дедуктивную целостность, дедуктивный аппарат должен быть определяемым без ссылки на какую-либо предполагаемую интерпретацию языка. Цель состоит в том, чтобы гарантировать, что каждая строка вывода является просто логическим следствием строк, которые ей предшествуют. Не должно быть никакого элемента какой-либо интерпретации языка, связанного с дедуктивной природой системы.

Логическое следствие (или следствие) системы из ее логического основания — это то, что отличает формальную систему от других, которые могут иметь некоторую основу в абстрактной модели. Часто формальная система будет основой или даже отождествлена с более широкой теорией или областью (например, евклидовой геометрией ), совместимой с использованием в современной математике, такой как теория моделей . ^{[ нужны разъяснения ]}

Примером дедуктивной системы могут служить правила вывода и аксиомы равенства, используемые в логике первого порядка .

Двумя основными типами дедуктивных систем являются системы доказательств и формальная семантика. ^[8]

Система доказательств

Формальные доказательства — это последовательности правильно сформированных формул (или для краткости WFF), которые могут быть либо аксиомой , либо результатом применения правила вывода к предыдущим WFF в последовательности доказательства. Последний WFF в последовательности признается теоремой .

Как только формальная система задана, можно определить набор теорем, которые можно доказать внутри формальной системы. Этот набор состоит из всех WFF, для которых существует доказательство. Таким образом, все аксиомы считаются теоремами. В отличие от грамматики WFF, нет никакой гарантии, что будет существовать процедура принятия решения , является ли данная WFF теоремой или нет.

Точку зрения, согласно которой создание формальных доказательств — это все, что есть в математике, часто называют формализмом . Дэвид Гильберт основал метаматематику как дисциплину для обсуждения формальных систем. Любой язык, на котором говорят о формальной системе, называется метаязыком . Метаязык может быть естественным языком или сам частично формализован, но он, как правило, менее полностью формализован, чем формальный языковой компонент рассматриваемой формальной системы, который тогда называется объектным языком , то есть объектом языка. обсуждение под вопросом. Понятие только что определенной теоремы не следует путать с теоремами о формальной системе , которые во избежание путаницы обычно называют метатеоремами .

Формальная семантика логической системы

Логическая система — это дедуктивная система (чаще всего логика первого порядка ) вместе с дополнительными нелогическими аксиомами . Согласно теории моделей , логической системе могут быть даны интерпретации , которые описывают, удовлетворяет ли данная структура (отображение формул определенному значению) правильно сформированной формуле. Структура, удовлетворяющая всем аксиомам формальной системы, называется моделью логической системы.

Логическая система – это:

Здорово , если каждая правильно составленная формула, которую можно вывести из аксиом, удовлетворяет каждой модели логической системы.
Семантически полная , если каждая правильно составленная формула, которой удовлетворяет каждая модель логической системы, может быть выведена из аксиом.

Примером логической системы является арифметика Пеано . Стандартная модель арифметики определяет областью обсуждения неотрицательные целые числа и придает символам их обычное значение. ^[10] Существуют и нестандартные модели арифметики .

История

Ранние логические системы включают индийскую логику Панини , силлогистическую логику Аристотеля, пропозициональную логику стоицизма и китайскую логику Гунсунь Луна (ок. 325–250 до н.э.). В более поздние времена среди авторов были Джордж Буль , Огастес Де Морган и Готтлоб Фреге . Математическая логика была разработана в Европе 19 века .

Давид Гильберт спровоцировал формалистическое движение под названием «Программа Гильберта» как предложенное решение фундаментального кризиса математики , который в конечном итоге был смягчен теоремами Гёделя о неполноте . ^[2] Манифест КЭД представлял собой последующую, пока еще безуспешную попытку формализации известной математики.

См. также

Список формальных систем
Формальный метод – математические спецификации программы.
Формальная наука - Отрасль науки
Логический перевод - перевод текста в логическую систему.
Система переписывания — замена подтермина в формуле другим термином.
Экземпляр замены — концепция в логике.
Теория (математическая логика) – Набор предложений формального языка.

Ссылки

^ «Формальная система | Логика, символы и аксиомы | Британника» . www.britanica.com . Проверено 10 октября 2023 г.
^ Jump up to: ^а ^б Зак, Ричард (31 июля 2003 г.). «Программа Гильберта» . Программа Гильберта, Стэнфордская энциклопедия философии . Лаборатория метафизических исследований Стэнфордского университета.
^ «формальная система» . Planetmath.org . Проверено 10 октября 2023 г.
^ Рапапорт, Уильям Дж. (25 марта 2010 г.). «Синтаксис и семантика формальных систем» . Университет Буффало .
^ «Определение: Формальная система — ProofWiki» . prowiki.org . Проверено 16 октября 2023 г.
^ Редуктивная грамматика: ( информатика ) Набор синтаксических правил для анализа строк, чтобы определить, существуют ли строки в языке. «Научно-технический словарь Научно-технических терминов МакГроу-Хилла» (6-е изд.). МакГроу-Хилл. ^{[ ненадежный источник? ]} Об автореСоставлено редакторами Энциклопедии науки и технологий McGraw-Hill (Нью-Йорк, штат Нью-Йорк), штатными сотрудниками, которые представляют собой передовые навыки, знания и инновации в области научных публикаций. [1]
^ «Существует два класса схем написания компиляторов определений формального языка. Продуктивный грамматический подход является наиболее распространенным. Продуктивная грамматика состоит в первую очередь из набора правил, которые описывают метод генерации всех возможных строк языка. Редуктивный или Техника аналитической грамматики устанавливает набор правил, которые описывают метод анализа любой строки символов и принятия решения о том, присутствует ли эта строка в языке». « Система компилятора-компилятора TREE-META: система метакомпилятора для Univac 1108 и General Electric 645 , Технический отчет Университета Юты RADC-TR-69-83. К. Стивен Карр, Дэвид А. Лютер, Шериан Эрдманн» ( PDF) . Проверено 5 января 2015 г.
^ Jump up to: ^а ^б «Определение: Дедуктивный аппарат — ProofWiki» . prowiki.org . Проверено 10 октября 2023 г.
^ Хантер, Джеффри, Металогика: Введение в метатеорию стандартной логики первого порядка, University of California Press, 1971
^ Кэй, Ричард (1991). «1. Стандартная модель». Модели арифметики Пеано . Оксфорд: Кларендон Пресс. п. 10. ISBN 9780198532132 .

Дальнейшее чтение

Раймонд М. Смаллян , 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.
Дэниел Ричардсон, Формальные системы, логика и семантика
Уильям Дж. Рапапорт, Синтаксис и семантика формальных систем
PlanetMath, формальная система
Pr∞fWiki, Определение: Формальная система
Pr∞fWiki, Определение: Дедуктивный аппарат
Энциклопедия математики, Формальная система
Питер Субер, Формальные системы и машины: изоморфизм. Архивировано 24 мая 2011 г. в Wayback Machine , 1997.
Рэй Таол, Формальные системы
Что такое формальная система? : Некоторые цитаты из книги Джона Хаугленда «Искусственный интеллект: сама идея» (1985), стр. 48–64.

[1] «Формальная система | Логика, символы и аксиомы | Британника» . www.britanica.com . Проверено 10 октября 2023 г.

[:0-2] Jump up to: ^а ^б Зак, Ричард (31 июля 2003 г.). «Программа Гильберта» . Программа Гильберта, Стэнфордская энциклопедия философии . Лаборатория метафизических исследований Стэнфордского университета.

[3] «формальная система» . Planetmath.org . Проверено 10 октября 2023 г.

[4] Рапапорт, Уильям Дж. (25 марта 2010 г.). «Синтаксис и семантика формальных систем» . Университет Буффало .

[5] «Определение: Формальная система — ProofWiki» . prowiki.org . Проверено 16 октября 2023 г.

[6] Редуктивная грамматика: ( информатика ) Набор синтаксических правил для анализа строк, чтобы определить, существуют ли строки в языке. «Научно-технический словарь Научно-технических терминов МакГроу-Хилла» (6-е изд.). МакГроу-Хилл. ^{[ ненадежный источник? ]} Об автореСоставлено редакторами Энциклопедии науки и технологий McGraw-Hill (Нью-Йорк, штат Нью-Йорк), штатными сотрудниками, которые представляют собой передовые навыки, знания и инновации в области научных публикаций. [1]

[7] «Существует два класса схем написания компиляторов определений формального языка. Продуктивный грамматический подход является наиболее распространенным. Продуктивная грамматика состоит в первую очередь из набора правил, которые описывают метод генерации всех возможных строк языка. Редуктивный или Техника аналитической грамматики устанавливает набор правил, которые описывают метод анализа любой строки символов и принятия решения о том, присутствует ли эта строка в языке». « Система компилятора-компилятора TREE-META: система метакомпилятора для Univac 1108 и General Electric 645 , Технический отчет Университета Юты RADC-TR-69-83. К. Стивен Карр, Дэвид А. Лютер, Шериан Эрдманн» ( PDF) . Проверено 5 января 2015 г.

[:1-8] Jump up to: ^а ^б «Определение: Дедуктивный аппарат — ProofWiki» . prowiki.org . Проверено 10 октября 2023 г.

[9] Хантер, Джеффри, Металогика: Введение в метатеорию стандартной логики первого порядка, University of California Press, 1971

[10] Кэй, Ричард (1991). «1. Стандартная модель». Модели арифметики Пеано . Оксфорд: Кларендон Пресс. п. 10. ISBN 9780198532132 .

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

v т и Основные темы Основ математики
Mathematical logic	Peano axioms Mathematical induction Formal system Axiomatic system Hilbert system Natural deduction Mathematical proof Model theory Mathematical constructivism Modal logic List of mathematical logic topics
Set theory	Set Naive set theory Axiomatic set theory Zermelo set theory Zermelo–Fraenkel set theory Constructive set theory Descriptive set theory Determinacy Russell's paradox List of set theory topics
Type theory	Axiom of reducibility Simple type theory Dependent type theory Intuitionistic type theory Homotopy type theory Univalent foundations Girard's paradox
Category theory	Category Topos theory Category of sets Higher category theory ∞-groupoid ∞-topos theory Mathematical structuralism Glossary of category theory List of category theory topics