Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску

Формальная система используется для выведения из аксиом теоремы в соответствии с набором правил. Эти правила, которые используются для вывода теорем из аксиом, являются логическим исчислением формальной системы. Формальная система - это, по сути, « аксиоматическая система ». [1]

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

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

Фон [ править ]

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

Таким образом, система состоит из действительных формул, построенных с помощью конечных комбинаций примитивных символов - комбинаций, образованных из аксиом в соответствии с установленными правилами. [3]

Более формально это можно выразить так:

  1. Конечный набор символов, известный как алфавит, который объединяет формулы, так что формула представляет собой всего лишь конечную строку символов, взятых из алфавита.
  2. Грамматика , состоящая из правил , чтобы сформировать формулы из простых формул. Формула считается правильно построенной, если она может быть сформирована с использованием правил формальной грамматики. Часто требуется, чтобы существовала процедура принятия решения о том, правильно ли составлена ​​формула.
  3. Набор аксиом или схем аксиом , состоящий из правильно составленных формул.
  4. Набор правил вывода . Правильно построенная формула, которая может быть выведена из аксиом, известна как теорема формальной системы.

Рекурсивный [ править ]

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

Вывод и следствие [ править ]

Воплощение системы ее логическим фундаментом является то , что отличает официальную систему от других , которые могут иметь некоторую основу в абстрактной модели. Часто формальная система является основой или даже отождествляется с более крупной теорией или областью (например, евклидовой геометрией ), совместимой с использованием в современной математике, такой как теория моделей . [ требуется разъяснение ]

Официальный язык [ править ]

Основные статьи: формальный язык и формальная грамматика

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

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

В информатике и лингвистике обычно рассматривается только синтаксис формального языка через понятие формальной грамматики . Формальная грамматика является точным описанием синтаксиса формального языка: с набором из строк . Две основные категории формальной грамматики - это порождающие грамматики , которые представляют собой наборы правил того, как могут быть созданы строки в языке, и категория аналитических грамматик (или редуктивных грамматик, [4] [5] ), которые представляют собой наборы правил. о том, как можно проанализировать строку, чтобы определить, является ли она членом языка. Короче говоря, аналитическая грамматика описывает, как распознаватькогда строки являются членами набора, тогда как порождающая грамматика описывает, как записывать только эти строки в наборе.

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

Дедуктивная система [ править ]

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

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

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

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

Логическая система [ править ]

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

Пример логической системы - арифметика Пеано .

История [ править ]

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

Формализм [ править ]

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

Программа Гильберта [ править ]

Основная статья: программа Гильберта

Давид Гильберт спровоцировал формалистическое движение, которое в конечном итоге было сдержано теоремами Гёделя о неполноте .

Манифест QED [ править ]

Основная статья: Манифест QED

Манифест QED представляет собой последующую, пока безуспешную попытку формализации известной математики.

Примеры [ править ]

Основная статья: Список формальных систем

Примеры формальных систем включают:

  • Лямбда-исчисление
  • Исчисление предикатов
  • Исчисление высказываний

Варианты [ править ]

Следующие системы являются вариациями формальных систем [ требуется пояснение ] .

Система доказательств [ править ]

Основные статьи: Система доказательств и формальное доказательство

Формальные доказательства - это последовательности хорошо составленных формул (или сокращенно wff). Чтобы wff квалифицировалось как часть доказательства, это может быть либо аксиома, либо продукт применения правила вывода к предыдущим wff в последовательности доказательств. Последний wff в последовательности признается теоремой .

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

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

См. Также [ править ]

Ссылки [ править ]

  1. ^ "Формальная система, ENCYCLOPDIA BRITANNICA" .
  2. ^ "Программа Гильберта, Стэнфордская энциклопедия философии" .
  3. ↑ Encyclopdia Britannica,Определение формальной системы , 2007.
  4. ^ Редуктивная грамматика: ( информатика ) Набор синтаксических правил для анализа строк, чтобы определить, существуют ли строки в языке. «Научно-технический словарь МакГроу-Хилл, Словарь научных и технических терминов» (6-е изд.). Макгроу-Хилл.[ ненадежный источник? ] Об авторе Составлено редакторами Энциклопедии науки и технологий McGraw-Hill (Нью-Йорк, штат Нью-Йорк), штатным сотрудником, который представляет передовые навыки, знания и инновации в научных публикациях. [1]
  5. ^ "Существует два класса схем написания компилятором определений формального языка.Подходпродуктивной грамматики является наиболее распространенным. Продуктивная грамматика состоит в основном из набора правил, которые описывают метод генерации всех возможных строк языка. Редуктивная илиметод аналитической грамматики устанавливает набор правил, которые описывают метод анализа любой строки символов и принятия решения о том, находится ли эта строка на языке ".« Система компилятора-компилятора TREE-META: система мета-компилятора для Univac 1108 и General Electric 645 , Технический отчет Университета Юты RADC-TR-69-83. С. Стивен Карр, Дэвид А. Лютер, Шериан Эрдманн» ( PDF) . Дата обращения 5 января 2015. .
  6. ^ Хантер, Джеффри, Metalogic: Введение в метатеорию стандартной логики первого порядка, Калифорнийский университет Pres, 1971

Дальнейшее чтение [ править ]

  • Раймонд М. Смуллян , 1961. Теория формальных систем: Анналы математических исследований , Princeton University Press (1 апреля 1961 г.) 156 страниц ISBN 0-691-08047-X 
  • Стивен Коул Клини , 1967. Математическая логика, перепечатанная Дувром, 2002. ISBN 0-486-42533-9 
  • Дуглас Хофштадтер , 1979. Гедель, Эшер, Бах: вечная золотая коса ISBN 978-0-465-02656-2 . 777 страниц. 

Внешние ссылки [ править ]

  • СМИ, связанные с формальными системами на Викискладе?
  • Британская энциклопедия, Определение формальной системы , 2007.
  • Что такое формальная система? : Некоторые цитаты из книги Джона Хогеланда «Искусственный интеллект: сама идея» (1985), стр. 48–64.
  • Питер Субер, Формальные системы и машины: изоморфизм , 1997.