какие функциональные символы содержит сигнатура теории элементарной арифметики ea

Зюзьков В.М.Лекции по теории алгоритмов

Чтобы разобраться, как можно преодолеть эту трудность, рассмотрим следующие операторы из F в F :

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

Пусть p k ( k = 0, 1, 2,…) обозначает последовательность простых чисел 2, 3, 5, 7, 11, … Для данного θ F положим

Сформулируем теперь наше определение.

Пример. Оператор Φ ( f ) = 2 f является рекурсивным оператором. Чтобы убедиться в этом, положим

не определена в остальных случаях.

Отсюда Φ – рекурсивный оператор.

Важное свойство рекурсивных операторов состоит в том, что они непрерывны и монотонны в следующем смысле.

Теорема 2. Любой рекурсивный оператор является непрерывным и монотонным. Доказательство см., например, [7, с. 194–195].

Первая теорема о рекурсии Клини представляет собой теорему о неподвижной точке для рекурсивных операторов, и ее зачастую называют также теоремой о неподвижной точке (из теории рекурсии).

Доказательство см., например, [7, с. 203–204].

Теорема вызывает недоумение: пусть оператор Φ задан так: функция f ( x ) отображается в функцию f ( x )+1. Это отображение конечно можно задать с помощью алгоритма (т.е. оператор рекурсивный), но разве у этого оператора есть неподвижная точка? Да, это функция, которая нигде не определена.

Наш программисткий опыт говорит о том, что определения, даваемые в терминах примитивной рекурсии, имеют смысл. В случае более сложных рекурсивных определений (см., например, функцию Аккермана) это не так очевидно – вполне можно представить себе, что функций, удовлетворяющих тому или иному определению, вообще не существует. Именно здесь оказывается полезной теорема 3. Рекурсивные определения весьма общего типа могут быть представлены уравнением вида

«Куином» называется программа, которая на своем выходе генерирует собственный исходный текст. Этот термин предложил Д. Хофштадтер в честь американского фи-

лософа и математика Willard van Orman Quine (1908 – 2000).

Докажем, что куины существуют для любого универсального языка программирования. Действительно, теорему Клини о рекурсии (или о неподвижной точке) можно сформулировать в следующем виде: «Нельзя найти алгоритма, преобразующего программы, который бы по каждой программе давал бы другую (не эквивалентную ей)».

Пусть теперь дано преобразование программ:

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

напечатать два раза, второй раз в кавычках, такой текст: «напечатать два раза, второй раз в кавычках, такой текст:»

Сравнительно легко можно написать куин на функциональном языке, таком как лисп. Написание куинов на процедурных языках требует некоторых хитростей. Вот пример на Паскале:

var a:array[1..7] of string; i:integer;

a[1]:=’var a:array[1..7] of string;’; a[2]:=’ i:integer;’; a[3]:=’begin’;

a[4]:=’for i:=1 to 3 do writeln(a[i]);’;

a[5]:=’for i:=1 to 7 do writeln(#97#91,i,#93#58#61#39,a[i],#39#59);’; a[6]:=’for i:=4 to 7 do writeln(a[i]);’;

Чтобы понять эту программу полезно иметь в виду соответствие между символами

Предложенный текст куина на Паскале имеет существенный недостаток: он использует значения кодов ASCII – но коды не являются частью самого языка Паскаль. Следующий куин исправляет этот недостаток (автор Dan Hoey: hoey@aic.nrl.navy.mil):

program s;const bbb=’program s;const bbb’;a=’a’;b=’b’;bb=’);writeln(‘; aa=»»;ab=’=»’;ba=»’;’;

aaa=’begin writeln(bbb,ab,bbb,ba,a,ab,a,ba,b,ab,b,ba,b,b,ab,bb,ba’; aba=’a,a,ab,aa,aa,ba,a,b,ab,ab,aa,ba,b,a,ab,aa,ba,ba’; abb=’a,a,a,ab,aaa,ba);writeln(a,b,a,ab,aba,ba);writeln(a,b,b,ab,abb,ba’; baa=’b,a,a,ab,baa,ba);writeln(b,a,b,ab,bab,ba);writeln(aaa,bb’; bab=’aba,bb);writeln(abb);writeln(bb,baa);writeln(bb,bab)end.’;

begin writeln(bbb,ab,bbb,ba,a,ab,a,ba,b,ab,b,ba,b,b,ab,bb,ba);writeln( a,a,ab,aa,aa,ba,a,b,ab,ab,aa,ba,b,a,ab,aa,ba,ba);writeln( a,a,a,ab,aaa,ba);writeln(a,b,a,ab,aba,ba);writeln(a,b,b,ab,abb,ba );writeln(b,a,a,ab,baa,ba);writeln(b,a,b,ab,bab,ba);writeln(aaa,bb );writeln(aba,bb);writeln(abb);writeln(bb,baa);writeln(bb,bab)end.

Как видим, вопреки общепринятому мнению, куин на процедурном языке не обязан содержать итерацию или рекурсию.

1.7. Некоторые алгоритмически неразрешимые проблемы

. Найти задачу – не меньшая радость, чем отыскать решение.

– Это же проблема Бен Бецалеля. Калиостро же доказал, что она не имеет решения. Как же искать решения, когда его нет? Бессмыслица какая-то.

– Бессмыслица – искать решение, если оно и так есть. Речь идет о том, как поступать с задачей, которая решения не имеет.

А. и Б. Стругацкие. Понедельник начинается в субботу

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

В контексте разрешимости предикаты часто называются проблемами.

Имея точное определение вычислимости, удалось доказать, что некоторые проблемы неразрешимы.

• Теорема Черча о неразрешимости логики предикатов. Не существует алгоритма, который для любой формулы логики предикатов устанавливает, общезначима она или нет.

• Проблема остановки неразрешима [7, с. 108]. Не существует никакого общего алгоритма, позволяющего установить, остановится ли некоторая конкретная программа (на любом языке программирования), запущенная после введения в неё некоторого конкретного набора данных. Смысл этого утверждения для теоретического программиро-

вания очевиден: не существует совершенно общего метода проверки программ на наличие в них бесконечных циклов.

• Не существует никакого общего алгоритма, позволяющего установить, вычисляет ли некоторая конкретная программа (на любом языке программирования) постоянную нулевую функцию [7, с. 110]. То же самое справедливо и для любой другой конкретной вычислимой функции. И как следствие, можно утверждать, что вопрос о том, вычисляют ли две данные программы одну и ту же одноместную функцию, также неразрешим. Тем самым, мы получаем, что в области тестирования компьютерных программ, мы имеем принципиальные ограничения.

Диофантовы уравнения [7, с. 114]. Современная математика вообще изобилует

разрешимыми и неразрешимыми проблемами. Одна из проблем связана с диофантовыми уравнениями.

для которого мы ищем только целые решения, называется диофантовым уравнением. Диофантовы уравнения не обязательно имеют решения. Например, не имеет решения уравнение x 2 –2 = 0.

Десятая проблема Гильберта, сформулированная в 1900 году, состоит в том, чтобы установить, существует ли алгоритм, с помощью которого можно было бы проверить, имеет ли данное диофантово уравнение решение. В 1970 году советский математик Ю. Матиясевич доказал, что такого алгоритма не существует. Доступное доказательство этого можно найти в [14].

Отметим также, что доказательство теоремы Гёделя о неполноте использует теорию алгоритмов. Элементарное доказательство приведено в [23]. Занимательному изложению вопросов вычислимости, вплоть до получения доказательства теоремы Гёделя, посвящена книга Р. Смаллиана [20].

2. Элементарная арифметика и неполнота

2.1. Элементарная арифметика

3. Двухместный предикат =.

интерпретируются как натуральные числа 1, 2, 3 и т.д. Знаки + и × интерпретируются как обозначения операций сложения и умножения.

– как «для всех натуральных чисел».

Средствами языка EA легко записываются простейшие утверждения о свойствах натуральных чисел, например:

« x – четное число» y ( x = y + y );

«существует бесконечно много простых чисел» x y (« x y » & « y – простое число»). Все, что мы до сих пор говорили о нашем «понимании» языка элементарной ариф-

Собственные аксиомы (схемы аксиом) элементарной арифметики :

P 1 : ( P ( 0 ) & x ( P ( x ) P ( S ( x ))) zP ( z ) (принцип математической индукции, P – произвольная формула),

P 4 : t 1 = t 2 ( t 1 = t 3 t 2 = t 3 ),

Аксиомы P 4 и P 5 обеспечивают некоторые необходимые свойства равенства. Аксиомы P 3 и P 2 обеспечивают существование нуля и операции «непосредственно следующий». Аксиомы P 6 – P 9 представляют собой рекурсивные равенства, служащие определениями операций сложения и умножения.

С помощью MP из схемы аксиом P 1 мы можем получить следующее правило индукции: из P ( 0 ) и x ( P ( x ) P (S( x ))) выводится xP ( x ).

Сейчас удобно на примере системы EA пояснить, почему необходима аксиома A 4 для определения теории первого порядка – она предотвращает коллизию переменных.

Для теории первого порядка должна выполняться аксиома

Вывод в теории EA организован таким образом, что все теоремы элементарной арифметики являются истинными утверждениями математики[16].

A ( x ) или 0 + x = x (гипотеза), 0 + S ( x )= S ( 0 + x ) (частный случай аксиомы), 0 + x = x S ( 0 + x )= S ( x ) (свойство равенства),

S ( 0 + x )= S ( x ) (modus ponens),

0 + S ( x )= S ( x ) или A ( S ( x )) (транзитивность равенства).

2.2. Арифметические функции и отношения

Как можно трактовать в теории EA операцию возведения в степень, если соответствующего символа в языке теории нет? Другой вопрос: мы пишем формулы, заменяющие в EA интуитивно понимаемые предикаты вроде « x – простое число»:

Какие требования мы должны предъявлять к такого рода формулам? Если кто-то предлагает формулу и утверждает, что она «выражает» то-то и то-то, как это проверить? Для таких ситуаций вводятся понятия выразимости предикатов и представимости функций.

Арифметическими функциями называются функции, у которых область определения и множество значений состоят из натуральных чисел, а арифметическим отношением является всякое отношение, заданное на множестве натуральных чисел. Так, например, умножение есть арифметическая функция с двумя аргументами, а выражение x + y z определяет некоторое арифметическое отношение с тремя аргументами. Арифметические функции и отношения являются понятиями интуитивными и не связанными ни с какой формальной системой.

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

1, если R ( x ) истинно,

0, если R ( x ) ложно.

Оказывается, что класс выразимых отношений в EA также оказывается очень широк. Но сначала нам потребуется определение.

2.3. Гёделева нумерация

тельно различать математические и метаматематические рассуждения. Нарушение этого условия приводит к парадоксам. Пример см. в разделе 1.4.

Таким образом, основной символ алфавита получает в качестве гёделева номера число, не превосходящее 10. Например, соответствие может быть задано таблицей:

Источник

Сигнатура и интерпретация

Сигнатура

При построении формальной теории сначала фиксируется её сигнатура. Для этого необходимо задать:

Если \(t_i\) — термы, а \(P(x_1,x_2. )\) — предикат сигнатуры, то \(P(t_1,t_2. )\) называется атомарной формулой. Из атомарных формул при помощи логических связок и кванторов строиться любая формула.

Одну и ту же теорию можно формулировать в различных сигнатурах. Так, вместо функций можно использовать предикаты (скажем, в арифметике считать истинным \(A(x,y,z)\), если \(x+y=z\)). Предметная область (множество всех сущностей) на этом этапе не фиксируется. Сигнатура только вводит обозначения с которыми оперирует теория.

Интерпретация

Интерпретация теории — это придание всем символам сигнатуры содержательного (конструктивного) смысла. Для этого необходимо задать не пустое множество \(\mathbb X = \\) (конечное или бесконечное, одно или несколько), называемое носителем интерпретации. На нём определяется действие функций (например, \(f(a_1)=a_2\), \(f(a_2)=a_8\), и т.д.). Затем предикатам приписываются истинностные значения (для \(E(x,y)\) определить, что \(E(a_1, a_1)=\T\), а \(E(a_1, a_2)=\F\), и т.д.).

Формула называется общезначимой или тавтологией, если она истинна на любой интерпретации при любой оценке свободных переменных (придании им конкретных значений). Например \(\neg A(x)\vee A(x)\) — тавтология. Отметим, что если формула истинна на всех конечных интерпретациях (конечных множествах), она может оказаться ложной для бесконечных множеств (пример: существование максимального элемента в упорядоченных множествах.

Формула называется невыполнимой (= противоречивой), если она ложна в любой интерпретации. Пример: \(\neg A(x)\,\&\, A(x)\).

Формула называется выполнимой (= непротиворечивой), если существует (хотя бы одна) интерпретация, где она истинна. Пример: \(A\vee B\).

Аксиомы

Система аксиом любой формальной теории разбивается на две группы — общелогические и предметные аксиомы. Общелогические аксиомы — это тавтологии. Например \(P\,\&\,Q\equiv Q\,\&\, P\) или \(P \to ( P \vee Q )\) справедливы в любой теории. В этих аксиомах символы \(P,Q\) обозначают любые формулы. Получаемые из общелогических аксиом теоремы, справедливы во всех теориях.

Общелогические аксиомы дополняются правилами получения новых формул. К ним относятся правила с кванторами (\(\forall_x P_x

\Rightarrow \exists_x P_x\)) или без них (\(\neg P\vee Q,

Q\vee S\)). Понятие истинности при этом отходит на второй план и выведенные формулы считаются верными, даже если их истинность невозможно проверить при помощи таблиц.

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

Источник

Языки реляционных баз данных

7.3 Исчисление высказываний

Определение. Высказывание — это утверждение, которое имеет однозначно определенное значение истинности. Высказывание в логике предикатов — это формула, все переменные которой связаны кванторами.

Заметьте, что нас по-прежнему не волнует смысл. Иначе говоря, исчисление дает форму, в которой могут быть сделаны правильные выводы, то есть утверждает, что из набора ППФ можно (или нельзя) построить заданную ППФ. И ничего более.

Определение. Правильно построенные формулы (ППФ):

Системы аксиом исчисления высказываний (например, аксиоматика Кли-ни) хорошо исследованы, но мы их не рассматриваем, так как не будем строить доказательства, исходя из выбранной системы аксиом.

7.4 Исчисление предикатов

7.4.1 ППФ в исчислении предикатов

Логика высказываний расширяется до логики предикатов путем включения в формулы утверждений, являющихся предикатами. Естественно, появляются и предикатные переменные. Поэтому определение ППФ усложняется.

7.4.2 Замечание о функциональных символах

При внимательном прочтении приведенного выше определения терма должны возникнуть вопросы:

Ответ на первый вопрос: -местный предикат на множестве задает отображение, а -местная функция определяет отображение.

Ответ на второй вопрос: 0-местная функция отождествляется с элементом множества . Не всегда удобно иметь отдельный символ для каждого элемента множества . Функциональные символы позволяют дать более сжатое представление. Например, фраза естественного языка «моя левая нога» может пониматься как существование левой ноги у субъекта «Я» и записываться как функция «ЛеваяНога(Я)», что позволяет не именовать по отдельности левые ноги всех людей.

Учтите, что за определенной таким образом функцией не предполагается никакой процедуры ее вычисления.

7.4.3 Определение узкого исчисления предикатов

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

Определение. Символы исчисления предикатов — это символы переменных, констант, функций и предикатов, символы значений истинности , символы логических связок и кванторы общности и существования .

Правильно построенные формулы и входящие в них термы определены выше. Набор аксиом включает аксиомы исчисления высказываний и следующие дополнительные аксиомы:

Дополнительные правила вывода:

К дополнительным правилам вывода относят еще «исключение &», «введение &» и «универсальное инстанцирование».

Определение. «Исключение &» —это вывод истинности обоих конъюнктов и из истинности .

Определение. «Введение &» — это вывод истинности из истинности обоих конъюнктов А и В.

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

7.4.4 Порядок исчисления предикатов

Исчисление первого порядка: В исчислении первого порядка можно связывать знаком квантора только переменные, но не функции или предикаты.

Исчисление высших порядков: В исчислении предикатов высших порядков можно связывать знаком квантора не только переменные, но и функции и предикаты.

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

в которой квантор навешен на имя предиката Р.

В рамках реляционной теории можно работать только с кортежами, но не с отношениями. В реализациях баз данных существует словарь. Это база метаданных, обычно реляционного типа. Словарь содержит сведения о созданных таблицах, их столбцах, ограничениях целостности и т.д. В реляционной модели данных словарь не предполагается. В этом одно из существенных различий между реляционной моделью и моделями данных реальных СУБД. Именно наличие словаря позволяет писать запросы в логике второго порядка.

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

Пример: Исчисление предикатов с равенством.

Источник

Теории и модели

Полные теории

В этом разделе мы попытаемся систематизировать уже известные нам понятия и факты.

Говорят, что замкнутая формула выводима в теории (является теоремой теории ), если формула получается из аксиом исчисления предикатов и формул теории по правилам вывода. (Обозначение: .)

Формула выводима в теории тогда и только тогда, когда в исчислении предикатов выводится некоторая формула вида , где — конъюнкция конечного числа формул из .

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

117. Покажите, что добавление к теории любой ее теоремы не меняет множества теорем.

Прежде чем переходить к примерам, сделаем два простых наблюдения.

Теорема 65 (критерий Лося-Воота). Непротиворечивая теория с равенством в конечной или счетной сигнатуре, не имеющая конечных моделей и категоричная в счетной мощности, полна.

Предположим, что ни одна из формул и не выводима в теории . Тогда обе теории и непротиворечивы. По теореме 47) они имеют счетные модели, которые остаются счетными после факторизации (перехода к нормальным моделям), поскольку теория не имеет конечных моделей. Эти счетные модели должны быть изоморфными (в силу категоричности). С другой стороны, в одной из них истинна формула , а в другой — формула , так что они даже не элементарно эквивалентны (мы знаем из раздела «Элементарная эквивалентность «, что такого быть не может).

Аналогично доказывается и общая форма критерия Лося-Воота:

Теорема 66. Непротиворечивая теория с равенством в конечной или счетной сигнатуре, не имеющая конечных моделей и категоричная в данной несчетной мощности , полна.

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

118. Условие конечности или счетности сигнатуры в этой теореме можно ослабить. Как это сделать?

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

Заметим, что это наблюдение согласовано со знаменитой (и трудной!) теоремой Морли; эта теорема утверждает, что теория с равенством, категоричная в одной несчетной мощности, категорична и во всех несчетных мощностях. (Подробно о теореме Морли можно прочесть, например, в учебнике Кейслера и Чэна [13])

Теорема 67. Конечно аксиоматизируемая полная теория в конечной сигнатуре разрешима.

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

Это доказательство неконструктивно в том смысле, что не дает никакой оценки на время работы алгоритма. Отметим также, что не обязательно требовать конечной аксиоматизируемости теории; достаточно, чтобы она имела разрешимое или перечислимое множество аксиом (см. [5]).

Проиллюстрируем все эти понятия на нескольких (в основном уже обсуждавшихся нами) примерах.

Источник