Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла

Размещено на http://www.allbest.ru/

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

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

Введение

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1. Противоречивость. Теория, в которой множество теорем покрывает всё множество формул (все формулы являются теоремами, «истинными высказываниями»), называется противоречивой. В противном случае теория называется непротиворечивой. Выяснение противоречивости теории – одна из важнейших и иногда сложнейших задач формальной логики. После выяснения противоречивости теория, как правило, не имеет дальнейшего ни теоретического, ни практического применения.

2. Полнота. Теория называется полной, если в ней для любой формулы F выводима либо сама F, либо ее отрицание. В противном случае, теория содержит недоказуемые утверждения (утверждения, которые нельзя ни доказать, ни опровергнуть средствами самой теории), и называется неполной.

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

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

2. Основные понятия логики первого порядка

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

Язык логики первого порядка строится на основе сигнатуры, состоящей из следующих символов:

1) логические

– символы логических операций ¬, , , ↔, →;

– символы кванторных операций , ;

– служебные символы: скобки и запятая.

2) нелогические

– множество предикатных символов, с которым связана арность, то есть число возможных аргументов P⁽ⁿ⁾, Q^(m), …, P₁⁽ⁿ⁾, P₂⁽ⁿ⁾;

– символы пропозициональных переменных X, Y, Z, …, X₁, X₂, … (можно считать, что символы пропозициональных переменных – это нульместные предикатные символы);

– символы предметных переменных x, y, z, …, x₁, x₂,…;

– символы предметных констант a, b, c, …, a₁, a₂, …

n-местным предикатом P (x1, x2,…, xn) называется функция P: M₁ЧM₂Ч…ЧM_n → {1,0}, определенная на наборах длины n элементов некоторого множества M= M₁ЧM₂Ч…ЧM_n и принимающая значения в области {1,0}. Множество М называется предметной областью предиката, его элементы – предметными константами.

Отрицанием предиката P(x₁, x₂,…, x_n), определенного на множестве M₁ЧM₂Ч…ЧM_n называется предикат ¬P(x₁, x₂,…, x_n), определенный на том же множестве, который на наборе (a₁, a₂,…, a_n) M₁ЧM₂Ч…ЧM_n

Конъюнкцией предикатов P(x₁, x₂,…, x_n), определенного на множестве M₁ЧM₂Ч…ЧM_n, и Q(y₁, y₂,…, y_m), определенного на множестве N₁ЧN₂Ч…ЧN_m, называется предикат P Q(x₁, x₂,…, x_n, y1, y2,…, ym) c пердметной областью M₁ЧM₂Ч…ЧM_nЧN₁ЧN₂Ч…ЧN_n, который на наборе (a₁, a₂,…, a_n, b₁, b₂,…, b_m) M₁ЧM₂Ч…ЧM_nЧN₁ЧN₂Ч…ЧN_n

Дизъюнкцией предикатов P(x₁, x₂,…, x_n), определенного на множестве M₁ЧM₂Ч…ЧM_n, и Q(y₁, y₂,…, y_m), определенного на множестве N₁ЧN₂Ч…ЧN_m, называется предикат P Q(x₁, x₂,…, x_n, y1, y2,…, yn) c пердметной областью M₁ЧM₂Ч…ЧM_nЧN₁ЧN₂Ч…ЧN_n, который на наборе (a₁, a₂,…, a_n, b₁, b₂,…, b_m) M₁ЧM₂Ч…ЧM_nЧN₁ЧN₂Ч…ЧN_n

Импликацией предикатов P(x₁, x₂,…, x_n), определенного на множестве M₁ЧM₂Ч…ЧM_n, и Q(y₁, y₂,…, y_m), определенного на множестве N₁ЧN₂Ч…ЧN_m, называется предикат P → Q(x₁, x₂,…, x_n, y1, y2,…, yn) c пердметной областью M₁ЧM₂Ч…ЧM_nЧN₁ЧN₂Ч…ЧN_n, который на наборе (a₁, a₂,…, a_n, b₁, b₂,…, b_m) M₁ЧM₂Ч…ЧM_nЧN₁ЧN₂Ч…ЧN_n

Эквивалентностью предикатов P(x₁, x₂,…, x_n), определенного на множестве M₁ЧM₂Ч…ЧM_n, и Q(y₁, y₂,…, y_m), определенного на множестве N₁ЧN₂Ч…ЧN_m, называется предикат P(x₁, x₂,…, x_n) ↔ Q (y1, y2,…, yn) c пердметной областью M₁ЧM₂Ч…ЧM_nЧN₁ЧN₂Ч…ЧN_n, который на наборе (a₁, a₂,…, a_n, b₁, b₂,…, b_m) M₁ЧM₂Ч…ЧM_nЧN₁ЧN₂Ч…ЧN_n

Операцией связывания квантором общности переменной xi в n-местном предикате P(x₁, x₂,…, x_n)), определенном на множестве M₁ЧM₂Ч…ЧM_n, называется операция, в результате которой получается n-1-местный предикат x_i P(x₁, x₂,…, x_i-1, x_i+1,…, x_n), который при значениях x₁ = a₁, …, x_i-1 = a_i-1, x_i-1 = a_i-1, …, x_n = a_n истинен, если при любых значениях x_i = a_i высказывание P(a₁, a₂,…, a_n) истинно.

Операцией связывания квантором существования переменной xi в n-местном предикате P(x₁, x₂,…, x_n) называется операция, в результате которой получается n-1-местный предикат x_i P(x₁, x₂,…, x_i-1, x_i+1,…, x_n), который при значениях x₁ = a₁, …, x_i-1 = a_i-1, x_i-1 = a_i-1, …, x_n = a_n истинен, если при некотором значении x_i = a_i высказывание P(a₁, a₂,…, a_n) истинно.

Характеристики

Тип файла документ

Документы такого типа открываются такими программами, как Microsoft Office Word на компьютерах Windows, Apple Pages на компьютерах Mac, Open Office - бесплатная альтернатива на различных платформах, в том числе Linux. Наиболее простым и современным решением будут Google документы, так как открываются онлайн без скачивания прямо в браузере на любой платформе. Существуют российские качественные аналоги, например от Яндекса.

Будьте внимательны на мобильных устройствах, так как там используются упрощённый функционал даже в официальном приложении от Microsoft, поэтому для просмотра скачивайте PDF-версию. А если нужно редактировать файл, то используйте оригинальный файл.

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

Список файлов курсовой работы