Система натурального вывода.

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

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

Формализация – даны отправные точки, истинные определения, посылки.
Для аксиоматизации логического высказывания и логики предикатов требуются:

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

2. Указать определение доказательств и доказуемой формулы на основе правила

3. Формулировка формул, правил и доказательств

4. Сформулировать относительно данной системы метод требования

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

6. Разрешимость, непротиворечивость

Формула является разрешимой если у нас есть общий метод доказуемости формул.

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

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

Кванторная теория, в частности логика предикатов – это логическая теория, язык которой позволяет анализировать высказывания и умозаключения с учетом внутренней структуры простых высказываний

Построение начинается с задания алфавита (совокупность исходных символов подразделяются на: нелогические, логические и технические)

Нелогические - термины естественного языка (имена, предикаторы)

Исходные символы:

p, q, r, s, p1... – пропозициональные переменные (символы для обозначения целых повествовательных предложений);

a, b, c, d, a1... – предметные константы (символы для обозначения единичных имен);

x, y, z, x1... – предметные переменные (символы для обозначения общих имен);

P, Q, R, S, P1... – предикатные символы (символы для обозначения свойств и отношений);

логическое отрицание («не» или «неверно, что»); конъюнкция («и»); дизъюнкция («или»); строгая дизъюнкция («либо…, либо…»);É - импликация («если…, то…»); тождество (эквивалентность) («тогда и только тогда, когда…»); квантор всеобщности («все», «каждый»);квантор существования («некоторые», «существуют»);

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

· Все это относится к логике предикатов

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

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

Терм

1. Произвольная предметная константа (напр. a)

2. Произвольная предметная переменная (напр. t1)

3. Если Ф – n-местная, предметно функциональная константа, а t1,t2….tn термы. То выражение Ф(t1,t2….tn) является термом.

4. Ничто иное не является термом

1,2 – простые термы; 3- сложные

! Терм не может начинаться с предикаторной константы в виде P (g(x, a)) и не может начинаться с двухместной константы напр. h(g(x,a). Хотя я не особо понимаю и мне кажется проблема везде в двойной формуле, то сеть g (x, a) – терм

Подформулой атомарной формулы является она сама. Подформулами формулы F являются формула F и все ее подформулы. Подформулами формул F&G, FvG, F→G, F↔G являются они сами и все подформулы формул F и G.

Определение формулы

1. Если П-N местная предикаторная константа, t1,t2….tn-это термы, то выражение П(t1,t2….tn) является формулой

2. Если А- формула, то L(представим что то отрицание)А-формула

3. Если А и В –формулы, то (А^В) и т.п-формулы

4. Если А формула, а а- предметная переменная, то VаА является формулой

5. Ничто иное не является формулой

Формулы типа 1 – элементарные, атомные; другие формулы- сложные, молекулярные

Логическое следование – отношение, существующее между посылками и обосновано выводимыми из них заключениями (напр. Если А, то В)

Понятие модели.

Модель – есть упорядоченная двойка объектов, в которой <D;Y>D – не пустая область объектов, а Y – функция, сопоставляющая дисприктивные выражения языка, некоторые объекты в области D.

 

! Важно то, что они истинные