11. Формальная арифметика. Явные логические определения. Теорема Гёделя о неполноте. Аксиомы равенства. Арифметика Пресбургера (1131927), страница 2

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 2)

. . & xn = yn → f(x1 , . . . , xn ) = f(y1 , . . . , yn ))Iдля всех функциональных символов f (n) сигнатуры σаксиом∀exn ∀eyn (x1 = y1 & . . . & xn = yn → (P(x1 , . . . , xn ) ↔ P(y1 , . . . , yn )))для всех предикатных символов P(n) сигнатуры σ,кроме =(2)Арифметика ПресбургераА есть ли нетривиальный фрагмент арифметики, которыйвсё-таки можно адекватно описать “хорошей” системой аксиом?Исключим умножение из рассмотренного фрагментаарифметики: σpa = {0}, +(2) , S(1) , =(2)Ipa — это интерпретация, получаемая из Iar удалением оценкифункционального символа ×Каковы выразительные возможности такого фрагментаарифметики?Можно ли предоставить “хорошую” систему аксиом, адекватноописывающую интерпретацию Ipa ?Так как ответы на эти вопросы давно известны, начнёмнепосредственно с системы аксиомАрифметика Пресбургера σpa = {0}, +(2) , S(1) , =(2)Арифметика Пресбургера — это теория Tpa сигнатуры σpa ,состоящая изI аксиом равенстваI аксиом, определяемых схемой математической индукцииIIϕ(x) {x/0} & ∀x (ϕ(x) → ϕ(x) {x/S(x)}) → ∀x ϕ(x)ещё четырёх аксиом:IIII∀x ¬(S(x) = 0)∀x ∀y (S(x) = S(y) → x = y)∀x (x + 0 = x)∀x ∀y (x + S(y) = S(x + y))Утверждение.

Ipa |= TpaДоказательство. Очевидно?Теорема разрешимости арифметики ПресбургераТеория Tpa разрешимаДоказательство.Введём несколько сокращений:(α ∈ N, β ∈ N0 , x ∈/ Vart1 ∪ Vart2 )I α — это S(S(. . . S(0) . . . ))| {z }α разIβt — это |t + t +{z· · · + }tβ разIIIt1 > t2 — это ∃x (t1 = t2 + x & ¬(x = 0))t1 ≡α t2 — это ∃x (t1 + αx = t2 ) ∨ ∃x (t2 + αx = t1 )все отношения, обратные к >, ≡α , =, введём как отрицанияэтих отношенийБудем в доказательстве считать α и βt термами, а остальныесокращения — атомамиДоказательство разрешимости арифметики ПресбургераРефлексивность равенства: |=Tpa 0 = 0Симметричность равенства и аксиома ∀x S(x) 6= 0:(α ∈ N0 )|=Tpa S(α) 6= 0 и |=Tpa 0 6= S(α)Аксиомы равенства и ∀x ∀y (S(x) = S(y) → x = y):(β ∈ N0 )|=Tpa S(α) = S(β) ⇔ |=Tpa α = βНепротиворечивость теории:6|=Tpa 0 6= 0, 6|=Tpa S(α) = 0 и 6|=Tpa 0 = S(α)Значит, |=Tpa α = β ⇔ Ipa |= α = βАналогично (хотя и технически сложнее) можно показать, что|=Tpa α > β ⇔ Ipa |= α > β|=Tpa α ≡γ β ⇔ Ipa |= α ≡γ βБескванторная формула — это формула, не содержащаякванторовИтог: для любого бескванторного предложения ϕ верно|=Tpa ϕ ⇔ Ipa |= ϕДоказательство разрешимости арифметики ПресбургераА как быть с произвольной формулой ϕ(exn )?Шаг 1: перейти к предложению ψ: ∀exn ϕ(очевидно, |=Tpa ϕ⇔|=Tpa ψ)Шаг 2: преобразовать ψ в бескванторное предложение χ,такое что|=Tpa ψ ⇔ |=Tpa χШаг 3: общезначимость предложения χ проверяется легко: этобулева формула над высказываниями о равенстве, равенстве помодулю и неравенстве целых неотрицательных чиселОсталось показать, как преобразуется формула на шаге 2На некоторое время забудем о теории Tpa :|=Tpa ψ ⇔|=Tpa χIpa |= ψ ⇔ Ipa |= χДоказательство разрешимости арифметики ПресбургераКаждый шаг преобразования состоит из нескольких этапов:I заменим все кванторы ∀ на ∃: ∀x ϕ ≈ ¬∃x ¬ϕI рассмотрим подформулу ∃x ϕ(x, exn ),где ϕ — бескванторная формулаI преобразуем ϕ в ДНФ, используя законы булевой алгебрыI вынесем за квантор ∃x слагаемые, не содержащие x:∃x (ϕ(exn ) ∨ ψ(x, exn )) ≈ ϕ(exn ) ∨ ∃x ψ(x, exn )I перенесём квантор ∃x под каждое слагаемое:∃x (K1 ∨ · · · ∨ Kn ) ≈ ∃x K1 ∨ · · · ∨ ∃x KnI каждую формулу ∃x Ki преобразуем в бескванторную ссохранением её значения в IpaФормула Ki (x, exn ) трактуется в Ipa каксистема (не)равенств над N0Покажем, как исключить x из произвольной системы ссохранением проекции множества решений на exnДоказательство разрешимости арифметики ПресбургераКаждое (не)равенство системы можно привести к одной изследующих форм:(t1 , t2 не зависят от x)αx + t1 = t2αx + t1 < t2αx + t1 ≤ t2αx + t1 ≡β t2αx + t1 6= t2αx + t1 > t2αx + t1 ≥ t2αx + t1 6≡β t2A ≡β B + 1 A ≡β B + 2A=BA 6≡β B ⇔ A≥B ⇔ ...A>BA ≡β B + (β − 1)A 6= B⇔A>BA<BA≤B ⇔A=BA<BЗначит, достаточно рассмотреть системы только над такими(не)равенствами:αx + t1 = t2αx + t1 < t2αx + t1 ≡β t2αx + t1 > t2Доказательство разрешимости арифметики ПресбургераЕсли система содержит хотя бы одно равенство =, тоисключить x можно так: t1 ≡α t2αx + t1 = t2t2 ≥ t1⇔(exn )S(exn )S(exn ) αx + t1 = t2 αx + t1 = t2βx + t3 ≷ t4 ⇔αt3 + βt2 ≷ αt4 + βt1....

. . αx + t1 = t2 αx + t1 = t2βx + t3 ≡γ t4 ⇔αβx + αt3 ≡αγ αt4...... αx + t1 = t2αt3 + βt2 ≡αγ αt4 + βt1⇔...Пусть теперь система не содержит равенств =Доказательство разрешимости арифметики ПресбургераВо всех строгих неравенствах системы можно получитьодинаковые левые части: αx + t1 ≷1 t2 αβx + βt1 + αt3 ≷1 βt2 + αt3βx + t3 ≷2 t4 ⇔αβx + βt1 + αt3 ≷2 αt4 + βt1......Если система содержит много строгих неравенств (в однусторону ) с одинаковыми левыми частями, то можно исключитьx из всех неравенств, кроме одного:  αx + t ≷ t1αx+t≷t  t1 R t21αx + t ≷ t2 ⇔αx + t ≷ t2...t2 ≷ t1...Доказательство разрешимости арифметики ПресбургераРавенства по модулю разных чисел можно привести кравенствам по модулю одного числа: αx + t1 ≡γ t2 αδx + δt1 ≡γδ δt2βx + t3 ≡δ t4 ⇔βγx + γt3 ≡γδ γt4......Итог: осталось показать, как исключить x из системы,содержащейI не более одного неравенства αx + t > t1 ,I не более одного неравенства αx + t < t2 с той же левойчастью иI произвольное число равенств βi x + t i ≡γ t i по одинаковому34модулю γДоказательство разрешимости арифметики ПресбургераКак исключить x из неравенства>:αx + t > t1αx + t < t2βx + t3 ≡γ t4...Если t > t1 , то неравенство выполненоДля каждого решения системы, такого что t ≤ t1 , найдётсярешение, отличающееся только значением x:αx + t ∈ {t1 + 1, .

. . , t1 + αγ}Значит, неравенство αx + t > t1 можно заменить насовокупностьt > t1 αx + t = t1 + 1 αx + t = t1 + 2 ...αx + t = t1 + αγДоказательство разрешимости арифметики ПресбургераКак исключить x из < и ≡γ , когда он исключён из >: [αx + t < t2 ]βx + t3 ≡γ t4...  [t < t2 ]  t3 ≡γ t4  ...  [α + t < t2 ]β + t3 ≡γ t4⇔  ... ...   [α(γ − 1) + t < t2 ]β(γ − 1) + t3 ≡γ t4...Доказательство разрешимости арифметики ПресбургераИ причём здесь теория Tpa ?Сохранение Tpa -(не)общезначимости формулы на каждомэлементарном шаге преобразования системы (не)равенств,записанном как преобразование формулы, обосновываетсяаналогично тому, как обосновывалось точное арифметическоеосмысление бескванторных предложений в началедоказательстваПримеры таких элементарных шагов:I перестановка слагаемыхI вынесение переменной x в каждой частиI добавление [вычитание] равных чисел к частям [из частей](не)равенстваI умножение (не)равенства на число (для (не)равенства помодулю — с домножением основания на то же число)I ...Доказательство разрешимости арифметики ПресбургераВопрос на понимание:А где в доказательстве применяетсясхема математической индукции?HАрифметика ПресбургераТеорема полноты арифметики ПресбургераАрифметика Пресбургера полнаТеорема о выразительности арифметики ПресбургераСуществует формула ϕ(exn ) сигнатуры σpa ,выполняющаяся в интерпретации Ipa в точности нанаборах предметов множества D⇔Существует совокупность систем линейных(не)равенств вида =, 6=, >, <, ≥, ≤, ≡α , 6≡α над N0 смножеством решений DАрифметика ПресбургераДоказательство теорем полноты и выразительности.Внимательно изучив доказательство теоремы разрешимости,можно убедиться, чтоI каждую формулу ϕ(exn ) можно преобразовать вбескванторную формулу ψ(exn ) над сигнатурой,расширенной всеми требуемыми (не)равенствами,имеющую тот же арифметический смыслI формула ψ(exn ) имеет в интерпретации Ipa смыслсовокупности систем линейных (не)равенств над N0I если ϕ — предложение, то ψ — бескванторное предложение,для которого верно либо |=Tpa ψ, либо |=Tpa ¬ψHКонец лекции 11.

Характеристики

Список файлов лекций