54. Основные свойства формальных систем: непротиворечивость, полнота, разрешимость. Полнота и непротиворечивость исчисления высказываний. Полнота и непротиворечивость исчисления предикатов.

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

Теория, в которой множество теорем покрывает всё множество формул (все формулы являются теоремами, «истинными высказываниями»), называется противоречивой. В противном случае теория называется непротиворечивой. 

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

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

Исчисление высказываний(ИВ) – формальная теория.

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

Множество формул Ф называется полным, если можно доказать либо Ф├ В, либо Ф├ ¬В.

А что такое полнота исчисления предикатов? Это утверждение о том, что любая общезначимая формула выводима в исчислении предикатов, то есть То есть вывести мы можем всё, что истинно всегда и везде.

Или сильная форма утверждения о полноте исчисления предикатов (когда добавляются аксиомы теории)

Непротиворечивость - ни одна формула не может быть выведена одновременно со своим отрицанием

55. Прикладные исчисления предикатов. Формальная арифметика. Теорема Генцена о непротиворечивости формальной арифметики.

Формальная арифметика – эгалитарное прикладное исчисление, в котором дополнительно имеются:

1. предметная константа 0

2. двуместные операции + и * и одноместная операция ‘.

3. знак равенства =

4. нелогические аксиомы равенства и следующие нелогические аксиомы арифметики:

где А – любая формула, а t, t1, t2 – любые термы (переменные для объектов).

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

55. Теоремы о неполноте формальных систем, смысл и значение теорем Геделя для практической информатики.

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

2. Для любой формально рекурсивно перечислимой (то есть эффективно генерируемой) теории <math>T</math>, включая базовые арифметические истинностные высказывания и определённые высказывания о формальной доказуемости, данная теория <math>T</math> включает в себя утверждение о своей непротиворечивости тогда и только тогда, когда теория <math>T</math> противоречива.

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

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

55. Неклассические логики.

НЕКЛАССИЧЕСКИЕ ЛОГИКИ — широкая область логических исследований, выходящая за пределы или, наоборот, сужающая область исследований классической логики высказываний и логики предикатов.

1. Интуиционистская логика (это логика, для которой не выполняется один из основных законов классической логики, - закон исключенного третьего, т.е. ╞А v ¬А)

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

3. модальные логики (логика, в которой кроме стандартных логических связок, переменных и/или предикатов есть модальности (модальные операторы))

4. временные логики (это модальные логики. Они строятся добавлением к логике высказываний новых законов, отражающих свойства времени)

5. алгоритмические логики (создавались с целью описания семантики языков программирования)

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

55. Интуиционистская логика.

Интуиционистская логика - это логика, для которой не выполняется один из основных законов классической логики, - закон исключенного третьего, т.е. ╞ А v ¬А.

Отказ от этого закона приводит к признанию существования «третьей возможности». Но в таком случае, естественно, приходим к запрету доказывать теоремы методом от противного. Последнее приводит к отказу от аксиомы ╞ (¬¬А А).

При доказательстве от противного предполагают, что верно на самом деле ¬А, и затем приходят к некоторому противоречию. Это показывает, что «не верно» ¬А, т.е. «верно» ¬¬А. последнее позволяет утверждать, что «верно» А. иначе говоря, имеем утверждение ╞ (¬¬А А).

59. Нечеткая логика.

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

Нечеткая логика отличается от двузначной классической логики тем, что допускает континуальное число истинностных значений для высказываний. В простейшем случае эти значения принадлежат отрезку [0,1] действительных чисел. Иначе говоря, между значение 0, соответствующим классическому ┴(ложь) и 1, или ┬(истина), имеется нечетное число промежуточных истинностных значений а (0,1).

60. Модальные логики. Типы модальностей.

Логика, в которой кроме стандартных логических связок, переменных и/или предикатов есть модальности (модальные операторы).

Типы модальностей:

1. алетические модальности – это высказывания, содержащие такие виды модальности, как «необходимо», «возможно», «невозможно», «случайно».

2. деонтические модальности – это модальности, связанные с характеристиками действий и поступками людей в обществе. Например, «обязательно», «разрешено», «запрещено», «безразлично».

3. эпистемические модальности – характеристики наших знаний. Можно назвать такие виды модальности этого типа, как «доказано», «опровергнуто», «не доказано», «не опровергнуто», «знает», «верит», «убежден», «сомневается».

61. Временные логики. Приложение временных логик к программированию.

Это модальные логики. Они строятся добавлением к логике высказываний новых законов, отражающих свойства времени.

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

Программа называется частично правильной по отношению к и , если всякий раз, когда предусловие истинно перед выполнением и заканчивает работу, постусловие будет также истинно. В этом случае используется запись { } { }.

Программа называется тотально правильной по отношению к и , если она частично правильна по отношению к и , и обязательно завершает работу, если истинно. В этом случае используется запись { } { }.

Предусловие и постусловие связаны с конкретной задачей, которую требуется решить и для решения которой и написана программа . Нам нужно доказать, что она правильна!

Проверка того, что программа действительно выполняет задачи, для решения которых она создавалась, - это задачи тестирования и верификации программы.

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

Основные идеи приложения временных логик к программированию сводятся к следующим двум положениям:

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

2. верификация программ. Использовать аппарат формальной теории временной логики для доказательства того, что данная программа обладает интересующим нас свойством.

62. Алгоритмические логики. Принципы построения алгоритмической логики. Алгоритмическая логика Хоара.

Алгоритмические логики создавались с целью описания семантики языков программирования. Алгоритмические логики включают высказывания вида { }S{ }, читающиеся как «если до выполнения оператора S было выполнено , то после него будет ».

Опишем принципы построения алгоритмической логики .

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

Программа в состоит из операторов. Исходный оператор – присваивание х := е, где х – идентификатор, а е – выражение, составленное из идентификаторов и натуральных чисел.

Пусть состояние памяти после присваивания удовлетворяет условию А(х), где А – формула формальной арифметики. Тогда состояние, которое было до присвоения, опишем формулой А(х|е). иначе говоря, имеем высказывание {А(х|е)}х := е{А(х)}.

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

.

Условный оператор – это конструкция

IF FI,

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

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

IF FI{B}.

Циклам отвечает конструкция

DO OUT OD.

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

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

и т.д. до бесконечности. Условие правильности k шагов цикла обозначим через . Цикл корректен, если

├

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

Основой для логики вывода правильных программ служат аксиомы Хоара (правила верификации). Они допускают интерпретации в терминах программных конструкций.

Сформулируем аксиомы Хоара, которые определяют предусловия как достаточные условия, гарантирующие, что исполнение соответствующего оператора при успешном завершении приведет к желаемым постусловиям.

1. аксиома присваивания: { (х|е)}х := е{ }

2.

3.

4.

5. правило для условного оператора (краткая форма)

6. правило для условного оператора (краткая форма)

7. предусловия и постусловия цикла until (до) удовлетворяют правилу:

63. Многозначные логики. Трёхзначная логика Я.Лукасевича. m-значная логика Э.Поста.

Многозначные логики - тип формальной логики, характерный наличием более чем двух возможных истинностных значений (истинности и ложности)

Я. Лукасевичем была предложена трехзначная логика, основанная на предположении, что высказывания бывают истинными, ложными и возможными, или неопределенными. К последним были отнесены высказывания наподобие: <Я буду в Москве в декабре будущего года>. Событие, описываемое этим высказыванием, сейчас никак не предопределено ни позитивно, ни негативно. Значит, высказывание не является ни истинным, ни ложным, оно только возможно.

Все законы трехзначной логики Лукасевича оказались также законами и классической логики; обратное, однако, не имело места. Ряд классических законов отсутствовал в трехзначной логике. Среди них были закон противоречия, закон исключенного третьего, законы косвенного доказательства и др. То, что закона противоречия не оказалось в трехзначной логике, не означало, конечно, что она была в каком-то смысле противоречива или некорректно построена.

Первыми примерами конечнозначных логик явились трехзначная логика Лукасевича, которая порождается функциями 1-x, min(1,1-x1+x2), где x1, x2 принимают значения 0,1/2,1 и m-значная логика Поста, которая порождается функциями x1+1 (mod m), max(x1, x2), где x1, x2 принимают значения 0,1, ..., m-1. 

Исходя из связи 3-решеток с булевой алгеброй, мы определяем n-арную решетку Ln(B) над булевой алгеброй B как множество возрастающих цепей из n–1 элементов B с покомпонентным порядком. Множество постоянных цепей, все элементы которых равны, образуют в Ln(B) булеву подалгебру, изоморфную B; ее элементы называются булевыми. Эквивалентным образом можно определить n-арные решетки как универсальные алгебры (дистрибутивные решетки с n нульарными и n унарными операторами), удовлетворяющие некоторым тождествам, т.е. как многообразие Поста. n-арная решетка над простейшей булевой алгеброй имеет n элементов и содержится в любой n-арной решетке. Решётка в теории множеств — частично упорядоченное множество, в котором каждое двухэлементное подмножество имеет как точную верхнюю (sup), так и точную нижнюю (inf) грани.

На n-арной решетке определяются n модальных функций – все они, кроме инверсии, суть эндоморфизмы обычной решетки, имеющие булевы значения; для n = 3 это – функции «необходимо» и «возможно». Относительно инверсии они не гомоморфизмы, за исключением k-ой при n=2k. Интервал между наименьшим и наибольшим модусом назовем модальным интервалом элемента x; таким образом, любой элемент вместе со всеми своими модусами принадлежит своему модальному интервалу. Введенные модальные функции порождают так наз. модальный моноид мощности 2n (при n>2), все элементы которого суть эндоморфизмы или антиэндоморфизмы решетки. При n=2 модальный моноид содержит не 4, а 2 функции и есть группа.