Элементы математической логики. Фролов И.С. - 40 стр.

UptoLike

ВУЗ: 

СГАУ | Самара

Составители: 

Рубрика: 

B
i
(1 6 i 6 m) — либо аксиома, либо получается из предыдущих
формул последовательности по правилу MP.
Формула B называется доказуемой формулой, или теоремой, ес-
ли существует ее доказательство; этот факт обозначается ` B.
Пример 3. Построим доказательство для A ⇒ A.
1. A ⇒ ((A ⇒ A) ⇒ A) (аксиома 1).
2. (A ⇒ ((A ⇒ A) ⇒ A)) ⇒ ((A ⇒ (A ⇒ A)) ⇒ (A ⇒ A))(акс.2).
3. (A ⇒ (A ⇒ A)) ⇒ (A ⇒ A) (MP, 1, 2).
4. A ⇒ (A ⇒ A) (аксиома 1).
5. A ⇒ A (MP, 4, 3).
Теорема 1. ` A ⇒ A для любой формулы A.
/ Действительно, в приведенном выше выводе A может быть заме-
нена на любую формулу. .
Сделаем несколько замечаний.
I. Выводы и доказательства в формальной теории проводятся не на языке
этой теории, а на так называемом метаязыке: если символами формальной теории
являются атомы P, Q, R, связки ⇒, ¬, ∧, ∨, и т.д., то в метаязыке используются ме-
тапеременные A, B, C, обозначающие произвольную формулу, Γ, ∆, обозначающие
списки формул, символ `, обозначающий выводимость и т.д. Термин «теорема» (а
также «доказательство», «вывод» и т.д.) имеет двоякое значение: в формальной тео-
рии это — доказуемая логическая формула, при изучении формальной теории это
— утверждение об объектах формальной теории, формулируемое и обосновываемое
на метаязыке.
II. В определенном нами исчислении высказываний имеется бесконечное чис-
ло аксиом, получаемых путем подстановок различных формул в конечное множе-
ство схем аксиом.
Иногда задают другие множества аксиом: например, считают, что в языке
исчисления имеются только связки ⇒, ¬, ∧, ∨, и удаляют последние три схемы ак-
сиом. Если же вновь потребуется связка ⇔, то запись A ⇔ B обычно вводят как
сокращение для формулы (A ⇒ B) ∧ (B ⇒ A).
III. Следует различать запись |= A («формула A общезначима», т.е. истинна
при любой интерпретации входящих в нее атомов — это проверяется с помощью таб-
лиц истинности или проведением эквивалентных преобразований) и ` A («формула
A доказуема»— это можно проверить, только построив доказательство). Интересен
вопрос: как связаны между собой отношения общезначимости и доказуемости на
множестве всех логических формул?
Отметим некоторые свойства понятия выводимости.
Теорема 2. Пусть A, B — произвольные формулы, Γ, ∆ — мно-
жества формул. Тогда
1) если A ∈ Γ, то Γ ` A (рефлексивность);
2) если Γ ⊂ ∆ и Γ ` A, то ∆ ` A (утончение);
3) если Γ ` A
i
для всех A
i
∈ ∆ и ∆ ` B, то Γ ` B (транзитив-
ность).
39

Страницы