Игошин Математическая логика и теория алгоритмов (1019110), страница 62
Текст из файла (страница 62)
Алфавит состоит из символов: Х„Хп ..., Х„, ..., —, -ь, (,). Определено понятие формулы (см. определение 2.1). Из множества всех формул вьщелено множество всех аксиом (они определяются схемами аксиом (А1) — (АЗ)). Наконец, единственным отношением А, называемым правилом вывода, является тернарное 251 отношение, в которое входят такие тройки формул Г, 6, Н, что средняя формула 6 имеет вид Г-ь Н.
Таким образом, формула Н называется непосрелственным следствием формул Г и à — ь Н. Это правило вывода было названо правилом заключения, или модус поненс (МР). Определение 28.2. Выводом в формальной аксиоматической теории Т называется всякая последовательность В„..., В„формул этой теории, такая, что для любого 1 (1 < 1 < и) формула В; есть либо аксиома теории Т, либо непосредственное следствие каких- либо предьщущих формул по одному из правил вывода.
Формула Г теории Т называется теоремой этой теории, если существует вывод в Т, последней формулой которого является Г; такой вывод называется выводом (или доказательством) формулы Г. В примере 15.2 был приведен вывод формулы à — ь Гв формализованном исчислении высказываний, т.е. доказательство того, что эта формула есть теорема данной формальной теории. Далее, аналогично соответствующему понятию в формализованном исчислении высказываний (см. определение! 5.1) определяется понятие вывода формулы Гиз множества формул Г в формальной аксиоматической теории Т и устанавливаются простейшие свойства этого понятия (см.
теорему 15.3). Вторым примером формальной аксиоматической теории может служить формализованное исчисление предикатов, рассмотренное в э 25. Итак, формальная аксиоматическая теория отличается от неформальной (содержательной), во-первых, тем, что она имеет дело с выражениями, составленными из символов некоторого алфавита, лишенных какого бы то ни было содержательного смысла, а во-вторых, расплывчатое понятие логического умозаключения, на основании которого мы выводили из одних содержательных утверждений другие, теперь заменено четким понятием отношения между выражениями из символов.
Таким образом, развитие формальной аксиоматической теории есть процесс оперирования с формальными символами на основе четких формальных правил. Раз так, то такой процесс может быть поручен электронно-вычислительной машине, что сделано в отношении, например, формализованного исчисления высказываний и некоторых других формальных аксиоматических теорий. Язык и метаязык, теоремы и метатеоремы формальной теории. Описание формальных аксиоматических теорий ведется на некотором общепонятном языке, например на русском.
Такой язык по отношению к языку формальной теории называется метаязыком. Он используется для формулировок утверждений о формальной теории. Язык же формальной теории (символы алфавита, слова) используется для формулировок высказываний внутри самой формальной теории и называется предметным языком (или язы- 252 «ом-объектом). Используя метаязык, можем изучать формальную аксиоматическую теорию как бы извне, можем формулировать и доказывать те или иные свойства формальной теории — свойства ее теорем, доказательств, ее самой. Причем при доказательстве этих свойств должны использоваться общепонятные и бесспорные средства обычной логики. В результате получаем набор теорем о формальной теории, устанавливающих те или иные ее свойства.
Такие теоремы называются метатеоремами. Различие между теоремами и метатеоремами в рассмотренных формальных теориях не всегда проводилось явно, но его непременно нужно иметь в виду. Например, если удалось построить вывод формулы 6 из формул Гь ..., Г, то высказывание «Гь ...„Г»- 6» является метатеоремой. В частности, теорема о дедукции, производные правила вывода в ФИВ и ФИП, а также теоремы о непротиворечивости, полноте (или неполноте), разрешимости тех или иных формальных теорий являются метатеоремами по отношению к этим теориям. В частности, утверждение «Теория групп непротиворечива» есть утверждение на метаязыке о формальной теории групп, т.е. является мета- теоремой.
Напротив, утверждение «(Ъх)(чу)(чг)(х* у= х «г -» у= з)» есть высказывание самой теории групп, записанное на предметном языке, т.е. теорема. Интерпретации и модели формальной теории. Обычно теории (и не только формальные) создаются для того, чтобы описать те или иные явления окружающего мира. Поэтому ценность всякой теории в конечном счете определяется тем, насколько хорошо справляется теория с этой задачей, т. е. насколько предоставляемое ею описание адекватно описываемому явлению, участвующим в нем объектам и связям между ними. Теория (и в особенности математическая теория), созданная для описания одних объектов, нередко оказывается применимой и для описания других.
Поэтому один из первых для любой теории вопросов — это вопрос о том, для описания каких объектов пригодна данная теория. Применительно к формальным аксиоматическим теориям проблема адекватности такой формальной аксиоматической теории первого порядка сигнатуры о и описываемых ею объектов представляет собой чисто математическую задачу о соответствии межлу множеством теорем этой теории, построенном как формальное исчисление, и содержательно построенной теорией, рассматРиваемой как множество объектов с операциями и отношениями на нем (т.е.
как алгебраическая система), или моделью формальной аксиоматической теории. Приладим точный математический смысл интуитивно осознаваемым понятиям интерпретации и модели формальной теории. Пусть задана сигнатура о = (с, с„, ~'"', у;"', ..., Рд'"', Р1'«,. ), т.е.
сг» сь .. — символы предметных или индивидных констант (симво- 253 лы выделенных элементов), Д',~"', ... — функциональные буквы, Рп» Р, ... — предикатные буквы. При этом верхние индеко * сы предикатных и функциональных букв указывают число аргументов предиката или функции соответственно, которые могут быть подставлены вместо этих букв. Дадим интерпретацию каждому символу этой сигнатуры.
Для этого выберем некоторое множество Ми однозначно сопоставим каждой т-местной предикатной букве Р; т-арное отношение Рм на М (т.е. интерпретируем букву Р; как конкретное отношение Ри на конкретном множестве), каждой и-местной функциональной букве б сопоставим и-арную операцию (и-местную функцию) Тм на М, каждой предметной кони станте с, — элемент с„из М. Постоянные термы (не содержащие предметных переменных) при таком определении также отобразятся на элементы из М.
Таким образом, мы приходим к алгебраической системе М = <М; сьи, с»', ...; ~,"', Я", ...; Ром, Р|н, ... >, которая и представляет собой интерпретацию формальной теории данной сигнатуры о.. Всякая замкнутая (т.е. не содержащая свободных предметных переменных) формула формальной теории (узкого исчисления предикатов) сигнатуры о при этой интерпретации превращается в высказывание об элементах из М, отношениях и функциях на М, которое может быть истинным или ложным. Открытая формула превращается в некоторое отношение (предикат) на М.
Открытая формула Гназывается выполнимой в данной интерпретации М, если существует такая подстановка с» предметных констант, при которой она превращается в истинное высказывание. Запись: М м „Е Открытая формула Гназывается истинной в данной интерпретации М; или говорят, что Р выполняется в М, если она превращается в истинное высказывание при любой подстановке констант.
Этот факт записывают так: М и Г и говорят, что интерпретация (алгебраическая система) М является моделью формулы Е Формула, истинная во всех интерпретациях, называется об»цезначимой, или тавтологией. Запись: ~ Е Интерпретация (алгебраическая система) М называется моделью (для) множества формул Ф, если любая формула из Ф истинна в данной интерпретации. Запись: М и Ф. Интерпретация М называется моделью теории Т, если она является моделью множества всех теорем теории Т, т.е. если всякая формула, доказуемая (выводимая) в Т, истинна в данной интерпретации. Для множества Ф формул обозначим через М(Ф) совокупность (класс) всех моделей этого множества формул.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
