Математическая логика и теория алгоритмов 3


Чтобы посмотреть этот PDF файл с форматированием и разметкой, скачайте его и откройте на своем компьютере.
Математическая логика
и теория алгоритмов

Первухин Михаил Александрович

Исчисление
высказываний

Лекция 3

Определение
формального исчисления


Будем

говорить,

что

формальное

исчисление



определено,

если

выполняются

четыре

условия
.


1
.

Имеется

некоторое

множество

А

символов

2

алфавит

исчисления


.

Конечные

последовательности

символов

называются

словами

или

выражениями

исчисления


.

Обозначим

через

S

множество

всех

слов

алфавита

исчисления


.


2
.

Задано

подмножество



ܵ
,

называемое

множеством

формул

исчисления


.

Элементы

множества

F

называются

формулами
.

Определение
формального исчисления


3
.

Выделено

множество








формул,

называемых

аксиомами

исчисления


.


4
.

Имеется

конечное

множество

K

отношений

ܴ
1
,
ܴ
2
,

,
ܴ
݊

между

формулами,

называемых

правилами

вывода,

причем

если

߮
1
,

,
߮
݉
,
߮


ܴ

,

то

߮

называется

непосредственным

следствием

формул

߮
1
,

,
߮
݉

по

правилу

ܴ

.


Итак,

исчисление



есть

четверка

(

,

,
��
,

)
.

Выводом

в

исчислении



называется

последовательность

формул

߮
1
,
߮
2
,

,
߮
݊

такая,

что

для

любого



(
1



݊
)

формула

߮


есть

либо

аксиома

исчисления


,

либо

непосредственное

следствие

каких
-
либо

предыдущих

формул
.


Формула

߮

называется

теоремой

исчисления


,

выводимой

в


,

или

доказуемой

в


,

если

существует

вывод

߮
1
,

,
߮
݊
,
߮
,

который

называется

выводом

формулы

߮

или

доказательством

теоремы

߮
.



Если

существует

алгоритм,

с

помощью

которого

для

произвольной

формулы

φ

через

конечное

число

шагов

можно

определить,

является

ли

φ

выводимой

в

исчислении



или

нет
,

то

исчисление

называется

разрешимым
.



Исчисление

называется

непротиворечивым,

если

не

все

его

формулы

доказуемы
.


Система
аксиом и правил вывода


Используя

понятие

формального

исчисления,

определим

исчисление

высказываний

(ИВ
)
.




Алфавит

ИВ

состоит

из

букв

x
,
y
,
z
,
u
,
v
,

возможно

с

индексами

(которые

называются

пропозициональными

переменными),

логических

символов

(связок)

¬
,

,

,

,

а

также

вспомогательных

символов

(
,
)
.


Множество

формул

ИВ

определяется

индуктивно
:


а)

все

пропозициональные

переменные

являются

формулами

ИВ
;


б)

если

߮
,
߰

-

формулы

ИВ,

то

¬
߮
,
(
߮

߰
)
,
(
߮

߰
)
,
(
߮



߰
)

2

формулы

ИВ
;


в)

выражение

является

формулой

ИВ

тогда

и

только

тогда,

когда

это

может

быть

установлено

с

помощью

пунктов

"а"

и

"б"
.


Таким

образом,

любая

формула

ИВ

строится

из

пропозициональных

переменных

с

помощью

связок

¬
,

,

,

.


Подформулой

߰

формулы

߮

ИВ

называется

подслово

߮
,

являющееся

формулой

ИВ
.


Под

длиной

формулы

߮

будем

понимать

число

символов,

входящих

в

слово

߮
.

Аксиомами

ИВ

являются

следующие

формулы

для

любых

формул

߮
,
߰
,
߯

ИВ
:

1.
߮

(
߰

߮
)
;

2.
(
߮

߰
)

(
(
߮

(
߰

߯
)
)

(
߮

߯
)
)
;

3.
(
߮

߰
)

߮
;

4.
(
߮

߰
)

߰
;

5.
(
߮

߰
)

(
(
߮

߯
)

(
߮

(
߰

߯
)
)
)
;

6.
߮

(
߮

߰
)
;

7.
߮

(
߰

߮
)
;

8.
(
߮

߯
)

(
(
߰


)

(
(
߮

߰
)

߯
)
)
;

9.
(
߮

߰
)

(
(
߮

¬
߰
)

¬
߮
)
;

10.
¬
¬
߮

߮
.


.



Указанные

формулы

называются

схемами

аксиом

ИВ
.

При

подстановке

конкретных

формул

в

какую
-
либо

схему

получается

частный

случай

схемы

аксиом
.


Единственным

правилом

вывода

в

ИВ

является

правило

заключения

(
modus

ponens
)
:

если

߮

и

߮

߰

-

выводимые

формулы,

то

߰

-

также

выводимая

формула
.

Символически

это

записывается

так
:

߮
,
߮

߰
߰
.


Говорят,

что

формула

߮

выводима

в

ИВ

из

формул

߮
1
,

,
߮
݉


(
обозначается

߮
1
,

,
߮
݉

߮
),

если

существует

последовательность

формул

߰
1
,

,
߰

,
߮
,

в

которой

любая

формула

либо

является

аксиомой,

либо

принадлежит

множеству

формул

{
߮
1
,

,
߮
݉
}
,

называемых

гипотезами,

либо

получается

из

предыдущих

по

правилу

вывода
.

Выводимость

формулы

߮

из



(

߮
)

равносильна

тому,

что

߮

-

теорема

ИВ

или

доказуемая

формула

ИП
Σ
.


Пример

Покажем,

что


߮

߮
.




Квазивыводом

в

ИВ

формулы

߮

из

формул

߮
1
,

,
߮
݉

называется

последовательность

формул

߰
1
,

,
߰

,
߮
,

в

которой

любая

формула,

либо

принадлежит

множеству

формул

{
߮
1
,

,
߮
݉
}
,

либо

выводима

из

предыдущих
.


Замечание

1
.

Если

существует

квазивывод

в

ИВ

формулы

߮

из

формул

߮
1
,

,
߮
݉
,


то

߮

выводима

в

ИВ

из

формул

߮
1
,

,
߮
݉
.


Примеры


Покажем
,

что

߮
,
߰

߮

߰
.






Покажем,

что

߮

¬
¬
߮
.


Приложенные файлы

  • pdf 8958314
    Размер файла: 492 kB Загрузок: 0

Добавить комментарий