Формальные системы – это системы операций над объектами, пони-маемыми как последовательность символов. Предполагается, что между символами не существует никаких связей и отношений кроме тех, которые явно описаны средствами самой формальной системы.
Задача. Упорядочить объекты 53, 109, 3?
Скорее всего их расположат в порядке 3,53,109, т.е. этой задаче будет дана обычная арифметическая интерпретация: последовательность цифр рассматривается как изображение чисел в десятичной системе; упорядочение этих последовательностей есть расположение изображаемых ими чисел по возрастанию, а правила сравнения таких изображений чисел известны настолько хорошо, что о них никто и не задумывается.
В действительности, такое толкование задачи не вытекает из ее текста. Его можно понимать как задачу лексикографического упорядочения (и тогда результат будет 109,3,53), как задачу распределения бегунов с указанными номерами по дорожкам (решение которой связано с процедурой распределения и заведомо не связано с числовой интерпретацией объектов) и т.д.
Возможность неоднозначного извлечения задач из указанного текста означает, что этот текст не содержит формального определения задачи. Для такого определения необходимо четко описать класс объектов, для которых задача решается и явно ввести для них понятие упорядочения, описав его как систему локальных операций над символами, из которых эти объекты состоят.
Исторически понятие формальной системы возникло в рамках оснований математики при исследовании строения аксиоматических теорий и методов доказательства в таких теориях.
Всякая точная теория определяется, во-первых, языком, т.е некоторым множеством высказываний, имеющих смысл с точки зрения этой теории, и, во-вторых, совокупностью теорем – подмножеством языка, состоящим из высказываний, истинных в данной теории.
|
|
Одной из фундаментальных идей по основаниям математики является идея формализации теорий, т.е. последовательного проведения аксиоматического метода построения теорий. При этом не допускается пользоваться какими-либо предположениями об объектах теории, кроме тех, которые явно выражены в виде аксиом; аксиомы рассматриваются как формальные последовательности символов, а методы доказательств – как методы получения одних выражений из других с помощью операций над символами.
Такой подход гарантирует четкость исходных утверждений и однозначность выводов, однако создается впечатление, что осмысленность и истинность в формализованной теории не играют роли. Однако, в действительности, и аксиомы и правила вывода стремятся выбирать так, чтобы построенной с их помощью формальной теории можно было придать содержательный смысл.
Более конкретно, формальная теория строится следующим образом:
1. Определяется множество формул, или правильно построенных выражений, образующих язык теории. Это множество задается конструктивными средствами (как правило, индуктивным определением) и, следовательно, оно перечислимо, обычно оно и разрешимо.
2. Выделяется подмножество формул, называемых аксиомами теории. Это подмножество может быть и бесконечным, но во всяком случае оно должно быть разрешимо.
3. Задаются правила вывода теории. Правило вывода – это вычислимое отношение на множестве формул. Формулы называются посылками правила, а его следствием или заключением.
|
|
Выводом формулы В из формул А1,А2,...Аn называется последовательность формул F1,F2,...Fm такая, что Fm=B, а любая Fi есть либо аксиома, либо одна из исходных формул А1,А2,...Аn, либо непосредственно выводима из F1,...Fi-1 по одному из правил вывода.
В выводима из А1,А2,...Аn, если существует вывод В из А1,А2,...Аn. Этот факт обозначается А1,А2,...Аn В. А1,А2,...Аn называются гипотезами или посылками вывода.
Доказательством формулы В в теории Т называется вывод В из пустого множества формул, т.е. вывод, в котором в качестве исходных формул используются только аксиомы. Формула В, для которой существует доказательство, называется формулой, доказуемой в теории Т или теоремой теории Т.
Факт доказуемости формулы В обозначается 
В. Очевидно, что присоединение формул к гипотезам не нарушает выводимости. Поэтому, если В (В – доказуема), то А В (то есть В доказуема и с некоторой формулой А.
При изучении формальных теорий имеют дело с двумя типами высказываний:
1. с высказываниями самой теории, т.е. теоремами, которые рассматриваются как чисто формальные объекты, определенные ранее;
2. с высказываниями о теории (о свойствах теорем, доказательств, и т.д.), которые формулируются на языке, внешнем по отношению к теории, и называются метатеоремами.