Верещагин Н.К., Шень А. - Языки и исчисления (1076783), страница 16
Текст из файла (страница 16)
Значит, ϕ входитв S 0 и по индуктивному предположению формула ϕ ложна в (R0 , S 0 ).(¬S ) Пусть формула ¬ϕ входит в S. Тогда пара (R ∪ {ϕ}, ∅) непротиворечива (если из R и ϕ выводится противоречие, то из R вы-[п. 4]Интуиционистская пропозициональная логика71водится ¬ϕ). Расширив её до полной, получаем высший мир (R0 , S 0 ),в котором формула ϕ истинна (по индуктивному предположению).Следовательно, формула ¬ϕ ложна в мире (R, S).Лемма 3 доказана. Она завершает доказательство теоремы 26.Напомним ещё раз его схему.
Пусть формула ϕ не выводима в интуиционистском исчислении высказываний. Тогда пара (∅, {ϕ}) непротиворечива. Фиксируем множество F всех подформул формулы ϕ.Расширим нашу непротиворечивую пару до полной (относительноF ). Эта полная пара будет одним из миров шкалы Крипке (в которой мирами являются полные пары). Именно в этом мире и будетложной формула ϕ. 36.
Покажите, что если формулы P и Q ложны в некоторых мирахнекоторых шкал Крипке, то можно построить шкалу Крипке и мир в ней,для которого формула P ∨ Q будет ложной. (Указание: соединим шкалы,в которых ложны формулы P и Q, в одну, добавив новый мир, которыйменьше миров, где P и Q ложны.)Из этой задачи и из теоремы о полноте вытекает такое следствие:если дизъюнкция двух формул выводима в интуиционистском исчислении высказываний, то хотя бы одна из формул тоже выводима.Это свойство выполнено для многих интуиционистских исчисленийи соответствует начальной идее: доказать A ∨ B означает доказатьодну из формул A или B.
Подобные свойства можно доказывать исинтаксически, используя генценовские варианты интуиционистскихисчислений.37. (а) Покажите, что формула ¬¬(ϕ ∨ ¬ϕ) выводима в интуиционистском исчислении высказываний. (б) Покажите, что если формулы ¬¬ϕ 謬(ϕ → ψ) выводимы в интуиционистском исчислении высказываний, тои формула ¬¬ψ выводима в интуиционистском исчислении высказываний.(в) Докажите, что если формула ϕ выводима в классическом исчислениивысказываний, то формула ¬¬ϕ выводима в интуиционистском исчислении высказываний (теорема Гливенко) (г) Покажите, что для формул, содержащих лишь конъюнкцию и отрицание, разницы между классическими интуиционистским исчислениями нет: из классической выводимости следует интуиционистская (теорема Гёделя).38.
Покажите, что интуиционистское исчисление высказываний разрешимо: существует алгоритм, который по произвольной формуле определяет, выводима ли она в интуиционистском исчислении высказываний.(Указание: оцените мощность контрмодели Крипке; можно обойтись и безэтого, заметив, что и множество выводимых формул, и множество формул, имеющих конечные контрмодели, перечислимы.)3. Языки первого порядкаПомимо логических связок, в математических рассуждениях часто встречаются кванторы «для любого» (∀) и «существует» (∃). Например, определение непрерывности начинается словами «для любого положительного ε найдётся положительное δ, для которого .
. . ».А одна из аксиом теории групп (существование обратного элемента)записывается так: ∀x∃y((xy = 1) ∧ (yx = 1)).Можно сформулировать различные логические законы, включающие в себя кванторы. Например, высказывание «существует такоеx, что A» (где A — некоторое свойство объекта x) логически эквивалентно высказыванию «не для всех x верно ¬A».Мы будем записывать такого рода законы с помощью формул,дадим определение истинности формул (при данной интерпретациивходящих в них символов) и исследуем, какого рода свойства можновыражать с помощью формул и какие нельзя.3.1.
Формулы и интерпретацииНачнём с примера. Пусть M — некоторое непустое множество, аR — бинарное отношение на нём, то есть подмножество декартовапроизведения M × M . Вместо hx, yi ∈ R мы будем писать R(x, y).Рассмотрим формулу∀x ∃y R(x, y).Эта формула выражает некоторое свойство бинарного отношения R(для любого элемента x ∈ M найдётся элемент, находящийся с нимв отношении R) и может быть истинна или ложна. Например, еслиM есть множество натуральных чисел N, а R — отношение «строгоменьше» (другими словами, R есть множество всех пар hx, yi, длякоторых x < y), то эта формула истинна.
А для отношения «строгобольше» (на том же множестве) эта формула ложна.Вопрос о том, будет ли истинна формула∃y R(x, y)для данного множества M и для данного бинарного отношения R нанём, не имеет смысла, пока не уточнено, каково значение переменнойx. Например, если M = N и R(x, y) есть x > y, то эта формулабудет истинной при x = 3 и ложной при x = 0. Для данных M и Rона задаёт некоторое свойство элемента x и тем самым определяетнекоторое подмножество множества M .[п. 1]Формулы и интерпретации73Перейдём к формальным определениям. Пусть M — непустоемножество. Множество M k состоит из всех кортежей (последовательностей) hm1 , .
. . , mk i длины k, составленных из элементов множества M . Назовём k-местной функцией на множестве M любоеотображение M k в M (определённое на всём M k ). Синонимы: «функция k аргументов», «функция валентности k», «функция местностиk» и даже «функция арности k» (последнее слово происходит от слов«унарная» для функций одного аргумента, «бинарная» (операция)для функций двух аргументов и «тернарная» для трёх аргументов).Назовём k-местным предикатом на множестве M любое отображение M k в множество B = {И, Л}. Такой предикат будет истинным на некоторых наборах hm1 , .
. . , mk i множества M и ложнымна остальных наборах. Поставив ему в соответствие множество технаборов, где он истинен, мы получаем взаимно однозначное соответствие между k-местными предикатами на M и подмножествамимножества M k . Говоря о предикатах, также употребляют термины«валентность», «число аргументов» и др.Мы будем рассматривать также функции и предикаты валентности нуль. Множество M 0 одноэлементно (содержит единственнуюпоследовательность длины 0). Поэтому функции M 0 → M отождествляются с элементами множества M , а нульместных предикатовровно два — истинный и ложный.Естественно, что в формулы будут входить не сами функции ипредикаты, а обозначения для них, которые называют функциональными и предикатными символами. В качестве символов можно использовать любые знаки.
Важно лишь, что каждому символу приписана валентность, которая определяет, со сколькими аргументами онможет встречаться в формуле. Произвольный набор предикатных ифункциональных символов, для каждого из которых указано неотрицательное число, называемое валентностью, мы будем называтьсигнатурой.Остаётся определить три вещи: что такое формула данной сигнатуры, что такое интерпретация данной сигнатуры и когда формулаявляется истинной (в данной интерпретации).Фиксируем некоторый набор символов, называемых индивидными переменными. Они предназначены для обозначения элементовмножества, на котором определены функции и предикаты; обычнов таком качестве используют латинские буквы x, y, z, u, v, w с индексами.
В каждой формуле будет использоваться конечное числопеременных, так что счётного набора переменных нам хватит. Мы74Языки первого порядка[гл. 3]предполагаем, что переменные отличны от всех функциональных ипредикатных символов сигнатуры (иначе выйдет путаница).Определим понятие терма данной сигнатуры. Термом называется последовательность переменных, запятых, скобок и символовсигнатуры, которую можно построить по следующим правилам:• Индивидная переменная есть терм.• Функциональный символ валентности 0 есть терм.• Если t1 , . . . , tk — термы, а f — функциональный символ валентности k > 0, то f (t1 , . . . , tk ) есть терм.В принципе можно было не выделять функциональные символывалентности 0 (которые также называют константами) в отдельную группу, но тогда бы после них пришлось писать скобки (как этоделается в программах на языке Си).Если A — предикатный символ валентности k, а t1 , .
. . , tk — термы, то выражение A(t1 , . . . , tk ) считается атомарной формулой. Кроме того, любой предикатный символ валентности 0 считается атомарной формулой.Формулы строятся по таким правилам:• Атомарная формула есть формула.• Если ϕ — формула, то ¬ϕ — формула.• Если ϕ и ψ — формулы, то выражения (ϕ ∧ ψ), (ϕ ∨ ψ), (ϕ → ψ)также являются формулами.• Если ϕ есть формула, а ξ — индивидная переменная, то выражения ∀ξ ϕ и ∃ξ ϕ являются формулами.Во многих случаях в сигнатуру входит двуместный предикатныйсимвол =, называемый равенством.
По традиции вместо = (t1 , t2 )пишут (t1 = t2 ).Итак, понятие формулы в данной сигнатуре полностью определено. Иногда такие формулы называют формулами первого порядкаданной сигнатуры, или формулами языка первого порядка с даннойсигнатурой.Наш следующий шаг — определение интерпретации данной сигнатуры. Пусть фиксирована некоторая сигнатура σ. Чтобы задатьинтерпретацию сигнатуры σ, необходимо:[п. 1]Формулы и интерпретации75• указать некоторое непустое множество M , называемое носителем интерпретации;• для каждого предикатного символа сигнатуры σ указать предикат с соответствующим числом аргументов, определённыйна множестве M (как мы уже говорили, 0-местным предикатным символам ставится в соответствие либо И, либо Л);• для каждого функционального символа сигнатуры σ указатьфункцию соответствующего числа аргументов с аргументамии значениями из M (в частности, для 0-местных функциональных символов надо указать элемент множества M , с ними сопоставляемый).Если сигнатура включает в себя символ равенства, то среди её интерпретаций выделяют нормальные интерпретации, в которых символ равенства интерпретируется как совпадение элементов.Приведём несколько примеров сигнатур, используемых в различных теориях.Сигнатура теории упорядоченных множеств включает в себя двадвуместных предикатных символа (равенство и порядок) и не имеетфункциональных символов.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
