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

Поделись знанием:
(перенаправлено с «Логическое исчисление»)
Перейти к: навигация, поиск

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

Формальная система — это совокупность абстрактных объектов, не связанных с внешним миром, в которой представлены правила оперирования множеством символов в строго синтаксической трактовке без учёта смыслового содержания, то есть семантики. Строго описанные формальные системы появились после того, как была поставлена задача Гильберта. Первые ФС появились после выхода книг Рассела и Уайтхеда «Формальные системы». Этим ФС были предъявлены определенные требования.





Основные положения

Формальная теория считается определенной, если[2]:

  1. Задано конечное или счётное множество произвольных символов. Конечные последовательности символов называются выражениями теории.
  2. Имеется подмножество выражений, называемых формулами.
  3. Выделено подмножество формул, называемых аксиомами.
  4. Имеется конечное множество отношений между формулами, называемых правилами вывода.

Обычно имеется эффективная процедура, позволяющая по данному выражению определить, является ли оно формулой. Часто множество формул задаётся индуктивным определением. Как правило, это множество бесконечно. Множество символов и множество формул в совокупности определяют язык или сигнатуру формальной теории.

Чаще всего имеется возможность эффективно выяснять, является ли данная формула аксиомой; в таком случае теория называется эффективно аксиоматизированной или аксиоматической. Множество аксиом может быть конечным или бесконечным. Если число аксиом конечно, то теория называется конечно аксиоматизируемой. Если множество аксиом бесконечно, то, как правило, оно задаётся с помощью конечного числа схем аксиом и правил порождения конкретных аксиом из схемы аксиом. Обычно аксиомы делятся на два вида: логические аксиомы (общие для целого класса формальных теорий) и нелогические или собственные аксиомы (определяющие специфику и содержание конкретной теории).

Для каждого правила вывода R и для каждой формулы A эффективно решается вопрос о том, находится ли выбранный набор формул в отношении R с формулой A, и если да, то A называется непосредственным следствием данных формул по правилу R.

Выводом называется всякая последовательность формул такая, что всякая формула последовательности есть либо аксиома, либо непосредственное следствие каких-либо предыдущих формул по одному из правил вывода.

Формула называется теоремой, если существует вывод, в котором эта формула является последней.

Теория, для которой существует эффективный алгоритм, позволяющий узнавать по данной формуле, существует ли её вывод, называется разрешимой; в противном случае теория называется неразрешимой.

Теория, в которой не все формулы являются теоремами, называется абсолютно непротиворечивой.

Определение и разновидности

Дедуктивная теория считается заданной, если:

  1. Задан алфавит (множество) и правила образования выражений (слов) в этом алфавите.
  2. Заданы правила образования формул (правильно построенных, корректных выражений).
  3. Из множества формул некоторым способом выделено подмножество T теорем (доказуемых формул).

Разновидности дедуктивных теорий

В зависимости от способа построения множества теорем:

Задание аксиом и правил вывода

В множестве формул выделяется подмножество аксиом, и задается конечное число правил вывода — таких правил, с помощью которых (и только с помощью их) из аксиом и ранее выведенных теорем можно образовать новые теоремы. Все аксиомы также входят в число теорем. Иногда (например в аксиоматике Пеано) теория содержит бесконечное количество аксиом, задающихся при помощи одной или нескольких схем аксиом. Аксиомы иногда называют «скрытыми определениями». Таким способом задается формальная теория (формальная аксиоматическая теория, формальное (логическое) исчисление).

Задание только аксиом

Задаются только аксиомы, правила вывода считаются общеизвестными.

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

Примеры

Геометрия

Задание только правил вывода

Аксиом нет (множество аксиом пусто), задаются только правила вывода.

По сути, заданная таким образом теория — частный случай формальной, но имеет собственное название: теория естественного вывода.

Свойства дедуктивных теорий

Непротиворечивость

Теория, в которой множество теорем покрывает всё множество формул (все формулы являются теоремами, «истинными высказываниями»), называется противоречивой. В противном случае теория называется непротиворечивой. Выяснение противоречивости теории — одна из важнейших и иногда сложнейших задач формальной логики. После выяснения противоречивости теория, как правило, не имеет дальнейшего ни теоретического, ни практического применения.

Полнота

Теория называется полной, если в ней для любого предложения (замкнутой формулы) <math>F</math> выводимо либо само <math>F</math>, либо его отрицание <math>\neg F</math>. В противном случае, теория содержит недоказуемые утверждения (утверждения, которые нельзя ни доказать, ни опровергнуть средствами самой теории), и называется неполной.

Независимость аксиом

Отдельная аксиома теории считается независимой, если эту аксиому нельзя вывести из остальных аксиом. Зависимая аксиома по сути избыточна, и её удаление из системы аксиом никак не отразится на теории. Вся система аксиом теории называется независимой, если каждая аксиома в ней независима.

Разрешимость

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

Важнейшие выводы

  • В 30-е гг. XX века Курт Гёдель показал, что есть целый класс теорий первого порядка, являющихся неполными. Более того, формула, утверждающая непротиворечивость теории, также невыводима средствами самой теории (см. Теоремы Гёделя о неполноте). Этот вывод имел огромное значение для математики, так как формальная арифметика (а на ней базируется теория действительных чисел, без которой нельзя представить современную математику) является как раз такой теорией первого порядка, а следовательно, формальная арифметика и все теории, содержащие её, в том числе теория действительных чисел, являются неполными.
  • Проблема неразрешимости логики предикатов. Чёрчем доказано, что не существует алгоритма, который для любой формулы логики предикатов устанавливает, логически общезначима формула или нет.
  • Исчисление высказываний является непротиворечивой, полной, разрешимой теорией, причем все три утверждения доказуемы в рамках самой логики высказываний.

См. также

Напишите отзыв о статье "Формальная система"

Примечания

  1. Клини С. К. [eqworld.ipmnet.ru/ru/library/books/Klini1957ru.djvu Введение в метаматематику]. — М.: ИЛ, 1957. — С. 59-60.
  2. Мендельсон Э. [eqworld.ipmnet.ru/ru/library/books/Mendelson1971ru.djvu Введение в математическую логику]. — М.: «Наука», 1971. — С. 36.

Литература

  • Галиев Ш. И. Математическая логика и теория алгоритмов. — Казань: Издательство КГТУ им. А. Н. Туполева. 2002.
  • Клини С. К. [eqworld.ipmnet.ru/ru/library/books/Klini1957ru.djvu Введение в метаматематику]. — М.: ИЛ, 1957. — 526 с.
  • Клини С. К. [eqworld.ipmnet.ru/ru/library/books/Klini1973ru.djvu Математическая логика]. — М.: «Мир», 1973. — 480 с.
  • Мендельсон Э. [eqworld.ipmnet.ru/ru/library/books/Mendelson1971ru.djvu Введение в математическую логику]. — М.: «Наука», 1971. — 320 с.
  • Новиков Ф. А. Дискретная математика для программистов. — СПб.: Питер, 2000. — 304 с.: ил. ISBN 5-272-00183-4.
  • Яновская С. А. Из истории аксиоматики // Историко-математические исследования. — М.: ГИТТЛ, 1958. — № 11. — С. 63-96.

См. также

Примеры формальных теорий

Отрывок, характеризующий Формальная система

Она оглянулась и, увидав, что ее друга нет в комнате, побежала за ней.
Вбежав в Сонину комнату и не найдя там свою подругу, Наташа пробежала в детскую – и там не было Сони. Наташа поняла, что Соня была в коридоре на сундуке. Сундук в коридоре был место печалей женского молодого поколения дома Ростовых. Действительно, Соня в своем воздушном розовом платьице, приминая его, лежала ничком на грязной полосатой няниной перине, на сундуке и, закрыв лицо пальчиками, навзрыд плакала, подрагивая своими оголенными плечиками. Лицо Наташи, оживленное, целый день именинное, вдруг изменилось: глаза ее остановились, потом содрогнулась ее широкая шея, углы губ опустились.
– Соня! что ты?… Что, что с тобой? У у у!…
И Наташа, распустив свой большой рот и сделавшись совершенно дурною, заревела, как ребенок, не зная причины и только оттого, что Соня плакала. Соня хотела поднять голову, хотела отвечать, но не могла и еще больше спряталась. Наташа плакала, присев на синей перине и обнимая друга. Собравшись с силами, Соня приподнялась, начала утирать слезы и рассказывать.
– Николенька едет через неделю, его… бумага… вышла… он сам мне сказал… Да я бы всё не плакала… (она показала бумажку, которую держала в руке: то были стихи, написанные Николаем) я бы всё не плакала, но ты не можешь… никто не может понять… какая у него душа.
И она опять принялась плакать о том, что душа его была так хороша.
– Тебе хорошо… я не завидую… я тебя люблю, и Бориса тоже, – говорила она, собравшись немного с силами, – он милый… для вас нет препятствий. А Николай мне cousin… надобно… сам митрополит… и то нельзя. И потом, ежели маменьке… (Соня графиню и считала и называла матерью), она скажет, что я порчу карьеру Николая, у меня нет сердца, что я неблагодарная, а право… вот ей Богу… (она перекрестилась) я так люблю и ее, и всех вас, только Вера одна… За что? Что я ей сделала? Я так благодарна вам, что рада бы всем пожертвовать, да мне нечем…
Соня не могла больше говорить и опять спрятала голову в руках и перине. Наташа начинала успокоиваться, но по лицу ее видно было, что она понимала всю важность горя своего друга.
– Соня! – сказала она вдруг, как будто догадавшись о настоящей причине огорчения кузины. – Верно, Вера с тобой говорила после обеда? Да?
– Да, эти стихи сам Николай написал, а я списала еще другие; она и нашла их у меня на столе и сказала, что и покажет их маменьке, и еще говорила, что я неблагодарная, что маменька никогда не позволит ему жениться на мне, а он женится на Жюли. Ты видишь, как он с ней целый день… Наташа! За что?…
И опять она заплакала горьче прежнего. Наташа приподняла ее, обняла и, улыбаясь сквозь слезы, стала ее успокоивать.
– Соня, ты не верь ей, душенька, не верь. Помнишь, как мы все втроем говорили с Николенькой в диванной; помнишь, после ужина? Ведь мы всё решили, как будет. Я уже не помню как, но, помнишь, как было всё хорошо и всё можно. Вот дяденьки Шиншина брат женат же на двоюродной сестре, а мы ведь троюродные. И Борис говорил, что это очень можно. Ты знаешь, я ему всё сказала. А он такой умный и такой хороший, – говорила Наташа… – Ты, Соня, не плачь, голубчик милый, душенька, Соня. – И она целовала ее, смеясь. – Вера злая, Бог с ней! А всё будет хорошо, и маменьке она не скажет; Николенька сам скажет, и он и не думал об Жюли.
И она целовала ее в голову. Соня приподнялась, и котеночек оживился, глазки заблистали, и он готов был, казалось, вот вот взмахнуть хвостом, вспрыгнуть на мягкие лапки и опять заиграть с клубком, как ему и было прилично.
– Ты думаешь? Право? Ей Богу? – сказала она, быстро оправляя платье и прическу.
– Право, ей Богу! – отвечала Наташа, оправляя своему другу под косой выбившуюся прядь жестких волос.
И они обе засмеялись.
– Ну, пойдем петь «Ключ».
– Пойдем.
– А знаешь, этот толстый Пьер, что против меня сидел, такой смешной! – сказала вдруг Наташа, останавливаясь. – Мне очень весело!
И Наташа побежала по коридору.
Соня, отряхнув пух и спрятав стихи за пазуху, к шейке с выступавшими костями груди, легкими, веселыми шагами, с раскрасневшимся лицом, побежала вслед за Наташей по коридору в диванную. По просьбе гостей молодые люди спели квартет «Ключ», который всем очень понравился; потом Николай спел вновь выученную им песню.
В приятну ночь, при лунном свете,
Представить счастливо себе,
Что некто есть еще на свете,
Кто думает и о тебе!
Что и она, рукой прекрасной,
По арфе золотой бродя,
Своей гармониею страстной
Зовет к себе, зовет тебя!
Еще день, два, и рай настанет…
Но ах! твой друг не доживет!
И он не допел еще последних слов, когда в зале молодежь приготовилась к танцам и на хорах застучали ногами и закашляли музыканты.

Пьер сидел в гостиной, где Шиншин, как с приезжим из за границы, завел с ним скучный для Пьера политический разговор, к которому присоединились и другие. Когда заиграла музыка, Наташа вошла в гостиную и, подойдя прямо к Пьеру, смеясь и краснея, сказала:
– Мама велела вас просить танцовать.
– Я боюсь спутать фигуры, – сказал Пьер, – но ежели вы хотите быть моим учителем…
И он подал свою толстую руку, низко опуская ее, тоненькой девочке.
Пока расстанавливались пары и строили музыканты, Пьер сел с своей маленькой дамой. Наташа была совершенно счастлива; она танцовала с большим , с приехавшим из за границы . Она сидела на виду у всех и разговаривала с ним, как большая. У нее в руке был веер, который ей дала подержать одна барышня. И, приняв самую светскую позу (Бог знает, где и когда она этому научилась), она, обмахиваясь веером и улыбаясь через веер, говорила с своим кавалером.
– Какова, какова? Смотрите, смотрите, – сказала старая графиня, проходя через залу и указывая на Наташу.
Наташа покраснела и засмеялась.
– Ну, что вы, мама? Ну, что вам за охота? Что ж тут удивительного?

В середине третьего экосеза зашевелились стулья в гостиной, где играли граф и Марья Дмитриевна, и большая часть почетных гостей и старички, потягиваясь после долгого сиденья и укладывая в карманы бумажники и кошельки, выходили в двери залы. Впереди шла Марья Дмитриевна с графом – оба с веселыми лицами. Граф с шутливою вежливостью, как то по балетному, подал округленную руку Марье Дмитриевне. Он выпрямился, и лицо его озарилось особенною молодецки хитрою улыбкой, и как только дотанцовали последнюю фигуру экосеза, он ударил в ладоши музыкантам и закричал на хоры, обращаясь к первой скрипке:
– Семен! Данилу Купора знаешь?
Это был любимый танец графа, танцованный им еще в молодости. (Данило Купор была собственно одна фигура англеза .)
– Смотрите на папа, – закричала на всю залу Наташа (совершенно забыв, что она танцует с большим), пригибая к коленам свою кудрявую головку и заливаясь своим звонким смехом по всей зале.
Действительно, всё, что только было в зале, с улыбкою радости смотрело на веселого старичка, который рядом с своею сановитою дамой, Марьей Дмитриевной, бывшей выше его ростом, округлял руки, в такт потряхивая ими, расправлял плечи, вывертывал ноги, слегка притопывая, и всё более и более распускавшеюся улыбкой на своем круглом лице приготовлял зрителей к тому, что будет. Как только заслышались веселые, вызывающие звуки Данилы Купора, похожие на развеселого трепачка, все двери залы вдруг заставились с одной стороны мужскими, с другой – женскими улыбающимися лицами дворовых, вышедших посмотреть на веселящегося барина.
– Батюшка то наш! Орел! – проговорила громко няня из одной двери.
Граф танцовал хорошо и знал это, но его дама вовсе не умела и не хотела хорошо танцовать. Ее огромное тело стояло прямо с опущенными вниз мощными руками (она передала ридикюль графине); только одно строгое, но красивое лицо ее танцовало. Что выражалось во всей круглой фигуре графа, у Марьи Дмитриевны выражалось лишь в более и более улыбающемся лице и вздергивающемся носе. Но зато, ежели граф, всё более и более расходясь, пленял зрителей неожиданностью ловких выверток и легких прыжков своих мягких ног, Марья Дмитриевна малейшим усердием при движении плеч или округлении рук в поворотах и притопываньях, производила не меньшее впечатление по заслуге, которую ценил всякий при ее тучности и всегдашней суровости. Пляска оживлялась всё более и более. Визави не могли ни на минуту обратить на себя внимания и даже не старались о том. Всё было занято графом и Марьею Дмитриевной. Наташа дергала за рукава и платье всех присутствовавших, которые и без того не спускали глаз с танцующих, и требовала, чтоб смотрели на папеньку. Граф в промежутках танца тяжело переводил дух, махал и кричал музыкантам, чтоб они играли скорее. Скорее, скорее и скорее, лише, лише и лише развертывался граф, то на цыпочках, то на каблуках, носясь вокруг Марьи Дмитриевны и, наконец, повернув свою даму к ее месту, сделал последнее па, подняв сзади кверху свою мягкую ногу, склонив вспотевшую голову с улыбающимся лицом и округло размахнув правою рукой среди грохота рукоплесканий и хохота, особенно Наташи. Оба танцующие остановились, тяжело переводя дыхание и утираясь батистовыми платками.