- •Раздел 4. Математическая логика и формальные системы.
- •4.1. Введение в формальные системы
- •4.2. Принципы построения формальных теорий.
- •4.3. Исчисление высказываний. Аксиомы и правила вывода.
- •2) Правило заключения (Modus Ponens). Если u и u β – выводимые формулы, то β выводима:
- •4.4. Исчисления предикатов и теории первого порядка.
- •3. Аксиомы исчисления предикатов делятся на две группы:
- •1) Аксиомы исчисления высказываний ( можно взять любую из систем или );
- •2) Две следующие предикатные аксиомы:
- •4.Правила вывода:
- •3) Правило - введения:
- •4.5.Предмет математической логики
- •4.6. Аксиоматический метод
- •1.4 Такое число m единственно.
- •1.20 Если k ј m и m ј n, то k ј n.
- •4.7. Логика высказываний
- •2.1 Укажите два примера множества строк: одно замкнутое, другое не замкнутое относительно правил построения.
- •2.2 Множество формул замкнуто относительно правил построения.
- •2.3 Является ли формулой ¬(p & q)?
- •2.4 Является ли формулой (p)?
- •2.10 Найдите формулу f такую, что (3) – единственная интерпретация, при которой f истинна.
- •2.11 Для любых формул f1,...,Fn (n і 1) и любой интерпретации I
- •2.12 Сформулируйте и докажите подобный факт для дизъюнкции f1 ъ ··· ъ Fn.
- •2.13 Для любой интерпретации I существует формула f такая, что I – единственная интерпретация, при которой f истинна.
- •2.15 Покажите, что для атомов p и q
- •2.22 Предполагая, что p и q – атомы, определите
- •2.23 G влечёт f тогда и только тогда, когда g и { ¬f } не выполнимо.
- •2.24 Определить, какие из следующих формул являются тавтологиями: (p й q) ъ (q й p), ((p й q) й p) й p, ((p є q) є r) є (p є (q є r)).
- •2.25 Для любых формул f, g1,...,Gn (n і 1) : f следует из { g1,..., Gn } тогда и только тогда, когда (g1 & ··· & Gn) й f – тавтология.
- •2.26 Найдите вывод q & p из p & q.
- •2.29 Найдите вывод p й r из p й q и q й r.
- •2.43 Правило удаления отрицания корректно.
- •2.44 Правило введения отрицания корректно.
- •2.45 Правило противоречия корректно.
- •2.52 Оба правила введения дизъюнкции корректны.
- •2.53 Правило удаления дизъюнкции корректно.
- •3.1 Является ли " X формулой?
- •3.2 Если формула содержит квантор, тогда она содержит переменную. Верно или нет ?
- •3.3 Если формула содержит квантор, тогда она содержит скобки. Верно или нет ?
- •3.4 Найдите свободные переменные и связанные переменные формулы
- •3.5 Все простые числа больше чем X.
- •3.10 Найдите результат подстановки константы a вместо X в формулу из задачи 3.4.
- •3.11 Если V не является свободной переменной f(V), тогда f(t) равно f(V).
- •V не является свободной переменной формулы Kw f.
- •3.12 Терм, не содержащий ни одной связанной переменной формулы f, является подстановочным в f для любой переменной.
- •3.23 Каждый терм содержит объектную константу или объектную переменную. Верно или нет ?
- •3.38 Модель арифметики первого порядка (7) стандартна.
- •3.39 G непротиворечива.
- •3.40 Арифметика первого порядка имеет нестандартную модель.
3.23 Каждый терм содержит объектную константу или объектную переменную. Верно или нет ?
В логике первого порядка существуют три типа атомарных формул:
пропозициональные константы,
строки вида R(t1, ... , tn) где R – предикатная константа арности n (n > 0) и t1, ..., tn – термы,
строки вида (t1 = t2), где t1, t2 – термы.
Взяв в качестве множества атомарных формул данное множество, мы получаем, что определение формул (первого порядка) совпадает с определением предикатных формул в начале этой части.
Для любых термов t1 и t2, t1 № t2 обозначает формулу ¬(t1 = t2).
Выводы в логике первого порядка
Определение вывода в логике предикатов с функциональными константами и равенством включает новый тип аксиом и два новых правила вывода. Правила, как и раньше, содержат метапеременные, служащие для обозначения формул и термов.
Новые аксиомы выражают рефлексивность равенства и имеют вид Ж |– t = t , где t – произвольный терм. Новые правила вывода – правила замены:
|
|
|
G |– t1 = t2 G |– F(t1) |
|
G |– t1 = t2 G |– F(t2) |
|
(З=) |
|
|
| |
|
|
G |– F(t2) |
G |– F(t1) |
где t1 и t2 свободные для v в F(v).
Для каждой из следующих формул найдите вывод из пустого множества посылок.
3.27 x = y Й f(x, y) = f(y, x).
3.28 " x $ y (y = f(x)).
3.29 $ y (x = y & y = z) Й x = z.
3.30 $ x (x = a & P (x)) є P (a).
Теории первого порядка
Теория первого порядка сигнатуры s определяется с помощью аксиом. Интерпретация, при которой истинны все аксиомы теории первого порядка G, называется моделью G. Если теория первого порядка G выполнима, мы также говорим что она непротиворечива. Логические следствия теории первого порядка называется её теоремами. Доказательство предложения F в теории первого порядка G есть вывод F из подмножества аксиом из G.
Теоремы корректности и полноты выполняются для логик предикатов с функциональными символами и равенством и могут быть сформулированы в рамках теорий первого порядка следующим образом. В соответствие с теоремой корректности, если существует доказательство предложения F в теории первого порядка G, тогда F является теоремой G. В соответствие с теоремой полноты Гёделя, обратное также верно: для любой теоремы F теории первого порядка G, существует доказательство F в G. Однако, добавление правил вывода для кванторов второго порядка ведёт к формальной системе которая корректна, но не полна.
Арифметика первого порядка
Мы будем упрощать запись формул сигнатуры арифметики первого порядка (6) введением следующего обозначения: a будет записываться как 0, s(t) как t' , f(t1, t2) как t1+t2, и g(t1, t2) как t1 · t2. Аксиомы арифметики первого порядка являются универсальным замыканием следующих формул:
x' № 0.
x'= y'Й x = y.
(F(0) & " v (F(v) Й F(v'))) Й " v F(v) для любой формулы F(v).
x + 0 = x.
x + y'= (x + y)'.
x · 0 = 0.
x · y'= x · y + x.
Интерпретация (7) является моделью этой теории. Арифметика первого порядка имеет также другие модели, и некоторые из них совсем не похожи на систему натуральных чисел (задача 3.40).
В следующих формулах 1 обозначает терм 0', 2 – 0'', и 4 – 0''''. Через t1 Ј t2 мы обозначаем формулу $ v(t2 = t1 + v), где v – первая объектная переменная, которая не встречается в t1, t2.
В каждой из следующих задач найдите доказательство данной формулы в арифметике первого порядка.
3.34 2 № 4.
3.35 x' № x.
3.36 x'= x + 1.
3.37 x Ј x.
Нестандартные модели арифметики
Термы 0, 0', 0'', ... называются цифрами. Модель M арифметики первого порядка стандартна, если для каждого c О |M| существует цифра t такая, что tM = c.