КУРСОВАЯ РАБОТА

"Неразрешимость логики первого порядка"

Введение

формальный неразрешимость логика остановка

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

Истоки идей формальной логики можно найти в работах философов древней Греции, но ее становление как математической дисциплины фактически началась с трудов Джорджа Буля (1815–1864), который детально разработал логику высказываний, или булеву логику. В 1879 году Готтлоб Фреге (1848–1925) расширил булеву логику для включения в нее объектов и отношений, создав логику первого порядка, которая в настоящее время используется как наиболее фундаментальная система представления знаний.

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

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

1.  Изучить основные понятия логики первого порядка.

2.  Рассмотреть понятие машины Тьюринга и доказать неразрешимость проблемы остановки.

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

4.  Разобрать доказательство неразрешимости логики первого порядка методом Геделя.

1. Понятие формальной системы

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

Формальная теория считается определенной, если:

-  задано конечное или счётное множество произвольных символов (конечные последовательности символов называются выражениями теории);

-  имеется подмножество выражений, называемых формулами;

-  выделено подмножество формул, называемых аксиомами;

-  имеется конечное множество отношений между формулами, называемых правилами вывода.

Обычно имеется эффективная процедура, позволяющая по данному выражению определить, является ли оно формулой. Часто множество формул задаётся индуктивным определением. Как правило, это множество бесконечно. Множество символов и множество формул в совокупности определяют язык или сигнатуру формальной теории.

Чаще всего имеется возможность эффективно выяснять, является ли данная формула аксиомой; в таком случае теория называется эффективно аксиоматизированной или аксиоматической. Множество аксиом может быть конечным или бесконечным. Если множество аксиом бесконечно, то, как правило, оно задаётся с помощью конечного числа схем аксиом и правил порождения конкретных аксиом из схемы аксиом. Обычно аксиомы делятся на два вида: логические аксиомы (общие для целого класса формальных теорий) и нелогические или собственные аксиомы (определяющие специфику и содержание конкретной теории).

Для каждого правила вывода R и для каждой формулы A эффективно решается вопрос о том, находится ли выбранный набор формул в отношенни R с формулой A, и если да, то A называется непосредственным следствием данных формул по правилу R.

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

Формула называется теоремой, если существует вывод, в котором эта формула является последней.

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

Теория, в которой не все формулы являются теоремами, называется абсолютно непротиворечивой.

Дедуктивная теория считается заданной, если:

– задан алфавит (множество) и правила образования выражений (слов) в этом алфавите;

– заданы правила образования формул (правильно построенных, корректных выражений);

– из множества формул некоторым способом выделено подмножество T теорем (доказуемых формул).

Свойства дедуктивных теорий:

1.  Противоречивость. ............