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

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

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

·  Наличие конечного алфавита (словарь). Количество символов, которым мы будем оперировать.

·  Правило построений формул. Формулы не могут быть неправильно построенными, но могут быть неверными, но правильно построенными.

·  Должно быть задано конечное число аксиом (или выделено конечное число формул, которые мы не доказываем). Аксиома – это формула, считающейся истинной без доказательства.

·  Правила вывода. Позволяют выводить теоремы из аксиом или других теорем. Теорема – формула, истинность которой доказана с помощью правил вывода из аксиом или других теорем.

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

Для описания грамматики языка используется метаязык. Алфавит этого языка содержит классы метасимволов. Формальные языки могут быть линейные и графовые. Линейные языки состоят из строк, то есть линейный язык – это множество строк. Строка рассматривается как вектор символов.

Одни строки могут являться подстроками других. Если для любого элемента одной строки объединение всех пересечений одноэлементного множества этого элемента с элементами другой строки не равно пустому множеству, то первая строка является подстрокой второй строки.

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

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

2.  Составляющие формальной системы. Аксиомы и аксиомные схемы, примеры. Соотношение между мощностью множества аксиом и мощностью множества правил вывода, правило подстановки.

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

·  Наличие конечного алфавита (словарь).

·  Правило построений формул.

·  Должно быть задано конечное число аксиом.

·  Правила вывода. Позволяют выводить теоремы из аксиом или других теорем.

Аксиома – это формула, считающейся истинной без доказательства. С помощью аксиомных схем задаются аксиомы. Отличие аксиомной схемы от аксиомы в том, что аксиомная схема записывается на некотором метаязыке, формулы которого содержат метапеременные. Любая аксиома может быть получена путем одновременной замены каждой метапеременной во всех ее вхождениях в аксиомную схему на конкретную формулу языка.

Например, аксиомные схемы, задающие правила для введения и удаления логических связок по отношению к формулам, являющимся подформулами этих аксиом:

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

Множество аксиом может быть бесконечным (в этом случае задается при помощи аксиомных схем), и множество правил вывода содержать только одно правило вывода, или – множество аксиом может быть пустым, а множество правил вывода может содержать несколько правил вывода.

Результат подстановки t вместо v в атомарную формулу F получается из F одновременной заменой всех вхождений v на t, где v – переменная, t – формула языка.

3.  Составляющие формальной системы. Множество правил вывода (метааксиом отношения выводимости), примеры. Отношение выводимости () в классических формальных теориях, свойства.

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

·  Наличие конечного алфавита (словарь).

·  Правило построений формул.

·  Должно быть задано конечное число аксиом.

·  Правила вывода. Позволяют выводить теоремы из аксиом или других теорем.

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

На лекциях Ij обозначалось |=, кроме вышеприведённого свойства отношение вывода является транзитивным отношением и обладает следующим свойством:

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

4.  Понятие формального вывода формулы в формальной теории. Отношение непосредственной выводимости. Гипотезы, теоремы формальной теории.

Под формальным (логическим) выводом формулы β из множества посылок G понимается вектор (последовательность) логических формул, каждый i-й компонент которого является аксиомой или элементом множества G, либо – формулой, которая выводима (получена путём применения правила вывода) из множества формул, состоящего из всех таких формул и только таких формул, которые являются k-ми компонентами этого вектора, где (k<i), а формула β является последним компонентом этого вектора.

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

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

5.  Семантика формальной теории, модель. Алгебраические системы, алгебры классической логики. Высказывание, предикат, логические связки.

Алгебраическая система или алгебраическая структура — множество G (носитель) с заданным на нём набором операций и отношений (сигнатура), удовлетворяющим некоторой системе аксиом. Непустое множество M, рассматриваемое вместе с интерпретацией на нем всех символов сигнатуры называется алгебраической системой сигнатуры Ω и обозначается Т = (М. Ω). Множество M называют носителем алгебраической системы (M, Ω). Мощностью алгебраической системы называется мощность ее носителя.

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

Простейшая логическая формула может задавать некоторое высказывание. Высказывание – это некоторая сущность, относительно которой можно сказать, истинна она или ложна.

Предикат (n-арный) — это функция с областью значений {0,1} , определённая на n-й декартовой степени множества M. Таким образом, каждую n-ку элементов M он характеризует либо как «истинную», либо как «ложную». Предикат можно связать с математическим отношением: если n-ка принадлежит отношению, то предикат будет возвращать на ней 1.Предикат называют тождественно-истинным и пишут: если на любом наборе аргументов он принимает значение 1. Предикат называют тождественно-ложным и пишут: если на любом наборе аргументов он принимает значение 0. Предикат называют выполнимым, если хотя бы на одном наборе аргументов он принимает значение 1.