Составляющие формальной системы. Язык формальной теории. Синтаксис формального языка, отношение между формулой и подформулой, сложные и атомарные формулы (стр. 5 )

Доказывается эта теорема очень просто. То, что все выводимые формулы -- это тавтологии, факт совершенно очевидный. Обратное нужно обосновать. То есть надо доказать, что любая тавтология Ф выводима (доказуема). Если это не так, то теория T, состоящая из одной аксиомы Ф, должна быть непротиворечивой. Потому что вывод противоречия тем самым доказывал бы "от противного" формулу Ф. А поскольку всякая непротиворечивая теория имеет модель, то мы получили бы такую модель, в которой формула Ф истинна. Это означало бы, что Ф ложна в данной модели (интерпретации). Но это противоречит тому, что Ф является тождественно истинной (тавтологией).Заметим, что теорема Гёделя о полноте исчисления предикатов формально не является усилением теоремы о полноте исчисления высказываний -- это разные теоремы.

Первая теорема Гёделя о неполноте.

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

Иначе говоря, в любой достаточно сложной непротиворечивой теории существует утверждение, которое средствами самой теории невозможно ни доказать, ни опровергнуть. Например, такое утверждение можно добавить к системе аксиом, оставив её непротиворечивой. При этом для новой теории (с увеличенным количеством аксиом) также будет существовать недоказуемое и неопровержимое утверждение.

21.  Двойственность кванторов общности и существования, доказательство.

Квантор — общее название для логических операций, ограничивающих область истинности какого-либо предиката. Чаще всего упоминают квантор всеобщности (обозначение: , читается: «для всех…», «для любого…» или «любой…») и квантор существования (обозначение: , читается: «существует…» или «найдется…»). Кванторы являются способом сокращенной записи конъюнктивных и дизъюнктивных формул. Так как область определения предикатов может быть бесконечной.

Квантор существования - специальный указатель на то, что некоторое P имеет место (или истинно) при некоторых переменных, перечисленных в этом указателе, причем конкретные значения, обеспечивающие это, не указываются, а фиксируется лишь то, что они существуют. Переменные, перечисленные в указателе, называются связанными. обозначается как где xi - имена переменных, которые являются связанными. Квантор общности - Специальный указатель на то, что некоторое содержащее переменные, распространяется на все формулы, получаемые при подстановке вместо переменных, перечисленных в этом указателе, любых значений из областей определения этих переменных. К. О. обозначает как где xi имена тех переменных, на которые распространяется его действие.

Двойственность кванторов.

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

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

Если предварённая нормальная форма является кванторной формулой существования, то каждая во всех вхождениях переменная, связанная квантором заменяется, константой, которая отсутствует в формуле, и процесс повторяется для оставшейся подформулы выглядит следующим образом. .

22.  Формальное доказательство переименования связанных переменных.

Переменные в логике играют роль, аналогичную их роли в алгебре или анализе. Прежде всего они позволяют указать в структуре математического объек­та те места, которые при использовании этого объекта будут заняты другими объектами. Например, линей­ная функция f может быть записана классической формулой f(x)=x + 6 или еще с помощью обозначения, подчеркивающего статус объекта f, формулой типа f = lx. x + 6.

В этом контексте х означает не объект, а место для объекта. Можно без хлопот переобозначить х, т. е. за­менить два вхождения х, например, на у. Очевидно, что нельзя заменить только одно вхождение, а дру­гое оставить без изменения. Такой тип замены назы­вается одновременной подстановкой. Говорят, что х — связанная переменная, желая тем самым отра­зить то обстоятельство, что первое вхождение х описывает связь, которой подчинено второе вхождение х. Переименование связанной переменной допустимо, так как сколько было различных вхожде­ний переменных до одновременной подстановки, столько же останется и после. Например, выражение lху. х * у равняется luy. u * y, но не lии. и * и. Теперь рассмотрим такой контекст, где х тем или иным образом представляет число 3, a sq — квадра­тичная функция. Можно написать sq (х) = х + 6, но, очевидно, уже нельзя заменять х на у, так как на этот раз через х обозначен вполне определенный объект. Переменная х называется свободной, точнее, два вхождения х называются свободными.

Рассмотрим следующий пример:

Единственной связанной переменной здесь является i. Связь вводится первым вхождением i. Остальные символы представляют свободные переменные или функциональные константы. Можно переименовать i в j или l, но не в k или п. Наконец, в выражении

связанные переменные — х и t. Связи вводятся соот­ветственно первым вхождением х и последним вхож­дением t.

Теперь вернемся к логике. Из интуитивного пони­мания квантификации вытекает, что имеется связь между вхождениями переменной, содержащейся в квантификации. В формуле "x [Н (х) É М (х)] переменная х «связана». Связь вводится первым вхождением, которое следует непосредственно после квантора общности. Область действия некоторой квантификации есть формула, к которой применяется эта квантификация. Вхождение переменной х, появляющейся в кванти-фикациях "x или $x, называется квантифицированным. Каждое вхождение переменной х в область дей­ствия этой квантификации является связанным. Вхождение переменной х свободное, если оно не яв­ляется ни квантифицированным, ни связанным.

23.  Правило резолюций. Хорновские дизъюнкты. Минимальная модель.

Метод резолюций. Главная идея метода резолюций состоит в том, что, если одна и та же атомарная формула (или сопоставимые формулы) появляется (-ются) в одном дизъюнкте без отрицания, а в другом - с отрицанием, то дизъюнкт, называемый резольвентой и получаемый в результате соединения этих двух дизъюнктов, из которых вычеркнута упоминавшаяся повторяющаяся формула (или сопоставимые формулы), является следствием указанных дизъюнктов. Пусть C1 и C2 - два предложения в исчислении высказываний, и пусть , а , где P - пропозициональная переменная, а C'1 и C'2 - любые предложения (в частности, может быть, пустые или состоящие только из одного литерала). Правило вывода: называется правилом резолюции. Предложения C1 и C2 называются резольвируемыми (или родительскими), предложение - резольвентой, а формулы P и - контрарными литералами. Метод резолюций является обобщением метода "доказательства от противного". Вместо того чтобы пытаться вывести некоторую формулу-гипотезу из имеющегося непротиворечивого множества аксиом, мы добавляем отрицание нашей формулы к множеству аксиом и пытаемся вывести из него противоречие. Пользуясь законом исключенного третьего мы приходим к выводу, что исходная формула была выводима из множества аксиом.

Дизъюнкт - это совокупность литер, одни из которых не содержат, а другие содержат знак отрицания. Если первые записывать через точку с запятой слева от знака ":-", а вторые - без знака отрицания через запятую справа от знака ":-" и в конце каждого дизъюнкта ставить точку, то получим выражение вида: A1;A2;…;An: - B1,B2,…,Bm. Хорновский дизъюнкт - это дизъюнкт, содержащий не более одной литеры без отрицания. Например:

A:-B, C,D; A:-B1,B2,Bn. Существует два вида хорновских дизъюнктов.

Хорновский дизъюнкт с заголовком - это дизъюнкт, содержащий одну литеру без отрицания. Он может содержать одну или несколько литер с отрицанием или не содержать их вообще, например: A:-B, C, ...,D; A:-B; A:-. Последний из приведенных дизъюнктов можно записывать без знака ":-", то есть в виде А. Хорновский дизъюнкт без заголовка - это дизъюнкт, не содержащий литер без отрицания, например: :-B, C, ...,D; : - A.