4.2. Принципы построения формальных теорий.

Всякая точная теория определяется, во-первых, языком, т.е. некоторым множеством высказываний, имеющих смысл с точки зрения готовой теории, и, во-вторых, сово­купностью теорем – множеством языка состоящим из высказываний, истинных в данной теории.

Каким образом теория получает свои теоремы?

В математике с античных времен существовал образец систематического построения теории - геометрия Евклида, в которой все исходные предпосылки сформулированы явно, в виде аксиом, а теоремы выводятся из этих аксиом с помощью цепочек логических рассуждений, называемых доказательствами. Однако до середины 19 века математические теории, как правило, не считали нужным явно выделять действительно все исходные принципы. Критерии же строго доказательства и очевидности утверждений в математике в разные времена были различны и также явно не формулировались. Время от времени это приводило к необходимости пересмотра основ той или иной теории. Известно, например, что основания дифференциального и интегрального исчислений, разработанных в 18 - м веке Ньютоном и Лейбницем, в 19 веке подверглись серьезному пересмотру; математический анализ в его современном виде опирается на работы Коши, Больцано, Вейерштрасса по теории пределов. В конце 19 века такой пересмотр затронул общие принципы организации математических теорий

Это привело к созданию новой отрасли математики – оснований математики, предметом которой стало как раз построение математических теорий и утвержде­ний и которая поставила своей целью ответить на вопросы типа: “как должна быть построена теорема, чтобы в ней не возникало противоречий?”, “какими свой­ствами должны обладать методы доказательств, чтобы считаться достаточно стро­гими?”.

Одной из фундаментальных идей, на которую опираются исследования по основаниям математики, является идея формализации теорий, т.е. последователь­ного проведения аксиоматического метода построения теорий. При этом не допус­кается пользоваться какими-либо предположениями об объектах теории кроме тех, которые выражены явно в виде аксиом; аксиомы рассматриваются в виде формальных последовательностей символов (выражений), а доказательства – как ме­тоды получения одних выражений из других с помощью операций над симво­лами. Такой подход гарантирует чёткость исходных утверждений и однозначность выводов, однако, может сложиться впечатление, что осмысленность и истинность и формализованной теории не играет никакой роли. В действительности и аксиомы и правила вывода стремятся выбрать таким образом, чтобы построенная с их по­мощью формальная теория имела содержательный смысл.

Более конкретно формальная теория (или исчисление) строится следующим обра­зом:

1. Определяется множество формул или правильно построенных выра­жений, которые образуют язык теории. Это множество задаётся конструк­тивными средствами (как правило, индуктивным определением). Данное множество перечислимо и часто разрешимо.

2. Выделяется подмножество формул, называемых аксиомами теории. Подмножество может быть и бесконечным; во всяком случае, оно должно быть разрешимо.

3. Задаются правила вывода теории. Правило вывода R(F₁, … ,F_n, σ) – это вычисляемое отношение на множестве формул. Если формулы F₁, … ,F_n, σ находятся в отношении R, то формула σ называется непосредственно выводимой из F₁, … ,F_n по правилу R.

Часто правило R(F₁, … ,F_n ,σ ) записывается в виде (F₁, … ,F_n)/σ. Формулы F₁, … , F_n называются посылками правила R, а σ – его следствием или заключением. Примеры аксиом и правил вывода будут приведены не­сколько позднее. Выводом формулы В из формул A₁, … ,A_n называется по­следовательность формул F₁, … , F_m, такая, что F_m=B, а любая F_ί (ί=1,2, … ,m) есть либо аксиома, либо одна из исходных формул А₁, … ,А_n, либо не­посредственно выводима из формул F₁, … ,F_ί-1 (или какого-нибудь из под­множеств) по одному из правил вывода. Если существует вывод В из А₁, …,А_n, то говорят, что В выводима из A₁, … ,A_n. Этот факт обозначается так: A₁, … ,A_n├ B. Формулы A₁, … ,A_n называются гипотезами или посыл­ками вывода. Переход в выводе от F_ί–1 к F_ί называется ί-м шагом вы­вода.

Доказательством формулы В в теории Т называется вывод В из пус­того множества формул, т.е. вывод, в котором в качестве исходных формул используются только аксиомы. Формула В, для которой существует доказа­тельство, называется формулой, доказуемой в теории Т, или теоремой тео­рии Т; факт доказуемости В обозначается ├ В.

Очевидно, что присоединение формул к гипотезам не нарушает выводи­мости. Поэтому если ├ В, то А ├ В, и если А₁, . . . ,А_n ├ В, то А₁, . . . , А_n, А_n+1├ В для любых А₁ и А_n+1. Порядок гипотез в списке несуще­ствен.

При изучении формальных теорий мы имеем дело с двумя типами вы­сказываний: во-первых, с высказываниями самой теории (теоремами), кото­рые рассматриваются как чисто формальные объекты, определенные ранее, а во-вторых, с высказываниями о теории (о свойствах ее теорем, доказа­тельств и т.д.), которые формулируются на языке, внешнем по отношению к теории, – метаязыке и называются метатеоремами. Различие между тео­ремами и метатеоремами не всегда будут проводиться явно, но его обяза­тельно надо иметь в виду.

Например, если удалось построить вывод В из А₁, . . . , А_n, то высказы­вание “А₁, . . . ,А_n ├ В ” является метатеоремой; ее можно рассматри­вать как дополнительное (“произвольное”) правило вывода, которое можно присоединить к исходным и использовать в дальнейшем.

Ясно, что общезначимые (тождественно-истинные) высказывания типа А  Ā или (x)  (Y), имеющие силу общих логических законов, должны содержаться в любой теории, претендующей на логический смысл. Поэтому изучение конкретных формальных теорий начнём с исчислений, порождаю­щих все общеизвестные формулы.