uzluga.ru
добавить свой файл
1 2 ... 9 10

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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



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

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

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

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

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

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

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

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

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

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



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





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

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

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

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







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

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

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

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

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

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



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

Квантор — общее название для логических операций, ограничивающих область истинности какого-либо предиката. Чаще всего упоминают квантор всеобщности (обозначение: , читается: «для всех…», «для любого…» или «любой…») и квантор существования (обозначение: , читается: «существует…» или «найдется…»). В математической логике приписывание квантора к формуле называется связыванием квантора.В логике предикатов, большое значение имеют 2-е операции называемые:

1) Квантор "Существования"

2) Квантор "Общности"

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

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

Терм — выражение формального языка (системы), является формальным именем объекта или именем формы. Понятие терма определяется индуктивно. Термом называется символьное выражение: t(X1, X2, … , Xn), где t — имя терма, называемая функтор или «функциональная буква», а X1, X2, … , Xn — термы, структурированные или простейшие.В логике первого и второго порядков терм определяется рекурсивно следующим образом:

  • всякая индивидная константа есть терм;

  • всякая свободная переменная есть терм;

  • если fi — і-местная фунциональная константа и t1, t2, …, ti — термы, то fi(t1,t2,...,ti) также есть терм;

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

  1. Дистрибутивность и ассоциативность кванторов.

Квантор — общее название для логических операций, ограничивающих область истинности какого-либо предиката. Чаще всего упоминают квантор всеобщности (обозначение: , читается: «для всех…», «для любого…» или «любой…») и квантор существования (обозначение: , читается: «существует…» или «найдется…»). В математической логике приписывание квантора к формуле называется связыванием квантора.В логике предикатов, большое значение имеют 2-е операции называемые:

1) Квантор "Существования"

2) Квантор "Общности"

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



Ассоциативность.




Высказывание означает, что область истинности предиката P(x) совпадает с областью значений переменной x.

Высказывание означает, что область истинности предиката P(x) непуста.

  1. Нормальные формы логических формул: КНФ, ДНФ. Предварённая нормальная форма. Сколемовская стандартная форма.

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

Элементарная конъюнкция – формула, подформулами которой являются только конъюнктивные формулы, либо – атомарные формулы, либо отрицания атомарных формул.

Элементарная дизъюнкция – формула, подформулами которой являются только дизъюнктивные формулы, либо – атомарные формулы, либо отрицания атомарных формул.

ДНФ – формула, подформулами которой являются дизъюнктивные формулы, либо элементарные конъюнкции.

КНФ – формула, подформулами которой являются конъюнктивные формулы, либо – элементарные дизъюнкции.

Предварённой нормальной конъюнктивной (дизъюнктивной) формой называется формула, в которой нет некванторной подформулы, которая имеет кванторную подформулу, и в которой присутствует в качестве подформулы КНФ (ДНФ), которая не является подформулой формулы, не являющейся кванторной формулой или КНФ (ДНФ). Другими словами, предварённая нормальная форма – это формула, у которой все кванторы записаны слева, а оставшаяся подформула является КНФ(ДНФ), не включающей кванторов.

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

Пример: формула принадлежит классу , формула принадлежит классу , а формула вообще не находится в предваренной нормальной форме.

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



следующая страница >>