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

Метод доказательства от противного применяется также и в других формах. Например, вместо импликации X → У доказывают равносильную ей импликацию (X ^ Y) → X, т. е. предполагая, что истинны утверждения Х и У, выводят истинность утвержде­ния X в противоречие с предположением. На основании равно­сильности Х→ Y≡ (X ^ Y) → X. Сделается вывод об истинности импликации X → Y. Вторая равносильность Х→ Y≡ (X ^ Y) → Y дает возможность заменить доказательство импликации X → Y доказательством импликации (X ^ Y) → Y, т. е. предположив, что истинны утверждения X и Y, вывести отсюда истинность утверждения К в противоречие с предположением. Наконец еще одна форма этого метода, являющаяся также одной из форм мето­да приведения к абсурду, основа­на на равносильности X → Y≡ (X ^ Y) → (Z ^ Z) Предполагая, что истинны утверждения Хи Y, выводим из них некоторое ут­верждение и его отрицание.

Метод доказательства от противного имеет две модификации: метод приведения противоположного утверждения к абсурду и метод приведения данного утверждения к абсурду.

Первый метод состоит в следующем. Пусть требуется доказать утверждение Х. Допускается противоположное ему утверждение Х и из него выводятся два противоречащих друг другу утверждения Y и Y: X → Y и X → Y. Из этого делается вывод о том, что справедливо исходное утверждение Х. Оправданием этому методу служит тавтология:. (X→Y) → ((X→Y)→X).

Второй метод состоит в следующем. Пусть требуется опровергнуть Х, т. е. доказать Х. В этом случае два противоречащих друг другу утверждения Y и Y выводятся не из утверждения Х, а из самого данного утвреждения Х: Х→Y и X→Y. Из этого делается вывод о том, что справедливо! Х, т. е. данное утверждение Х опровергнуто. Оправданием этому методу служит тавтология: (X→Y) → ((X→Y)→X).

18.  Исчисление предикатов первого порядка. Аксиоматика.

Предикат – высказывательная функция, определенная на некотором множестве М, т. е. такая n-местная функция Р, которая каждому упорядоченному набору <a1,a2, …, an> элементов множества М сопоставляет некоторое высказывание, обозначаемое P(a1,a2, …, an).

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

Здесь формула α, имеющая свободное вхождение переменной χ, обозначена как α(χ). Формула α(χ) не имеет свободных вхождений τ. Формула α(τ) получена заменой свободных вхождений переменной χ на τ.

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

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

Названия этих аксиомных схем следующие: «аксиомная схема введения импликации», «аксиомная схема удаления импликации», «аксиомная схема введения конъюнкции» и т. д.

19.  Исчисление предикатов первого порядка. Правила вывода.

Предикат – высказывательная функция, определенная на некотором множестве М, т. е. такая n-местная функция Р, которая каждому упорядоченному набору <a1,a2, …, an> элементов множества М сопоставляет некоторое высказывание, обозначаемое P(a1,a2, …, an).

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

Есть два правила вывода, называемые правилами Бернайса. Если переменная не является параметром формулы , то правила Бернайса разрешают такие переходы:

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

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

Используя первое правило Бернайса, легко установить допустимость правила обобщения

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

Правило (Gen) (от Generalization — обобщение) кодифицирует стандартную практику рассуждений: мы доказываем какое-то утверждение со свободной переменной , после чего заключаем, что мы доказали , так как было произвольным.

Второе правило Бернайса также вполне естественно: желая доказать в предположении , мы говорим: пусть такое существует, возьмем его и докажем (то есть докажем со свободной переменной ).

20.  Теорема о доказуемых формулах исчисления предикатов. Теорема об общезначимых предикатных формулах (Теорема Гёделя).

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

Здесь речь идёт о правилах доказательства (MP, CondP, Contr, Gen, Part). Точнее говорить о том, что эта система правил, позволяющих доказать любую тавтологию, то есть "абсолютный логический закон", верный при любой интерпретации входящих в него символов. О том, что любое содержательное доказательство можно представить как вывод некоторой тавтологии.