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

Математическая логикаЛектор:Подымов Владислав Васильевичe-mail:valdus@yandex.ru2017, весенний семестрЛекция 11Формальная арифметикаЯвные логические определенияТеорема Гёделя о неполнотеАксиомы равенстваАрифметика ПресбургераНапоминаниеЛекция 10 начиналась с такого примера:выполняется ли предложение ϕв естественной арифметической интерпретации Iar ?(например, ϕ : 2 × 2 = 4,или ϕ — произвольное предложение логики предикатов)Если удастся построить теорию, адекватно описывающуюинтерпретацию Iar , то можно будет описывать (и даже иногдарешать) арифметические задачи логическими методамиПопробуем выбрать небольшой, но при этом достаточновыразительный фрагмент арифметики, и построить для негоадекватную теорию TarОстановимся на таком фрагменте:арифметика целых неотрицательных чиселсо сложением, умножением и равенствомФормальная арифметикаСигнатура формальной арифметики: σar = {0} , +(2) , ×(2) , S(1) , =(2)Арифметическая интерпретация Iar символов сигнатуры σarзадаётся так:I предметная область: N0 = {0, 1, 2, 3, .

. .}I 0 = 0,S(d) = d + 1I +, ×, = — сложение, умножение и равенство чиселФормальная арифметика — это любая теория,более-менее адекватно описывающая интерпретацию IarПеред исследованием того, как такая теория может выглядеть,попробуем оценить, насколько выразителен выбранныйфрагмент арифметикиПроверка соотношения Iar |= ϕ — этообоснование/опровержение арифметического утверждения,записанного в виде формулы ϕОпределимость σar = {0} , +(2) , ×(2) , S(1) , =(2)Некоторые арифметические понятия можно явно определить,используя только понятия сигнатуры σarСодержательные примеры:I 1 = S(0)I n = S(S(.

. . S(0) . . . ))| {z }(n ∈ N)n разII2x =x×xx≥y ⇔∃z (x = y + z)Рассмотрим сигнатуру σ и содержащийся в ней символ s:константу, функциональный символ или предикатный символσ−s — это сигнатура, получаемая из σ удалением символа s0σ+s= σ, если σ 0 = σ−sОпределимостьОпределение константы1 c (в сигнатуре σ−c ) —это формула вида ϕ(xc ) (сигнатуры σ−c )Определение функционального символа1 f (n) —это формула вида ϕ(xf , exn )1(n)Определение предикатного символа P —это формула вида ϕ(exn )Примеры определений в сигнатуре σar дляI константы 1:x1 = S(0)I функционального символа ·2(1) :x·2 = x1 × x1I предикатного символа ≥(2) :∃y (x1 = x2 + y)1Более точное название такого определения — явное определение:“А — это Б (не зависящее от А)”ОпределимостьЕсли ϕ(xc ) — определение c, то аксиома ϕ {xc /c}определяет константу cЕсли ϕ(xf , exn ) — определение f, то аксиома ∀exn (ϕ {xf /f(exn )})определяет функциональный символ f (n)Если ϕ(exn ) — определение P, то аксиома ∀exn (P(exn ) ↔ ϕ)определяет предикатный символ P(n)Примеры аксиом, определяющих(в сигнатуре σar )I константу 1:1 = S(0)I функциональный символ ·2 :∀x1 (x1 2 = x1 × x1 )I предикатный символ ≥:∀x1 ∀x2 (x1 ≥ x2 ↔ ∃y (x1 = x2 + y))ОпределимостьТеорема о разрешимости доопределения теорииЕсли теория T сигнатуры σ разрешима, то теорияT ∪ {ϕ} сигнатуры σ+s , где ϕ — аксиома, определяющаясимвол s, также разрешимаДоказательство.Сведём проблему (T ∪ {ϕ})-общезначимости формул сигнатурыσ+s к проблеме T -общезначимости формул сигнатуры σПокажем, как можно преобразовать формулу ψ сигнатуры σ+s вформулу ψ 0 сигнатуры σ, такую что|=T ∪{ϕ} ψ ⇔ |=T ψ 0Для этого, в числе прочего, потребуется формула D,I равносильная определению, используемому в аксиоме ϕ, иI не содержащая связанных переменных, встречающихся в ψОпределимостьТеорема о разрешимости доопределения теорииЕсли теория T сигнатуры σ разрешима, то теорияT ∪ {ϕ} сигнатуры σ+s , где ϕ — аксиома, определяющаясимвол s, также разрешимаДоказательство.Устранение предикатного символа s = P(n)Каждый атом P(t1 , .

. . , tn ) заменяется на формулуD {x1 /t1 , . . . , xn /tn }Например:(D : ∃u (x1 = x2 + u))∀x ∃y ((x + 1)2 ≥ y);∀x ∃y ∃u ((x + 1)2 = y + u)ОпределимостьТеорема о разрешимости доопределения теорииЕсли теория T сигнатуры σ разрешима, то теорияT ∪ {ϕ} сигнатуры σ+s , где ϕ — аксиома, определяющаясимвол s, также разрешимаДоказательство.Устранение константы s = cВсе вхождения константы c в формулу ψ заменяются на “свежую”переменную y, и полученная формула χ заменяется на∀y (D {xc /y} → χ)Например:(D : x1 = S(0))2∀x ∃y ∃u ((x + 1) = y + u);∀v (v = S(0) → ∀x ∃y ∃u ((x + v)2 = y + u))ОпределимостьТеорема о разрешимости доопределения теорииЕсли теория T сигнатуры σ разрешима, то теорияT ∪ {ϕ} сигнатуры σ+s , где ϕ — аксиома, определяющаясимвол s, также разрешимаДоказательство.Устранение функционального символа s = f (n)Пока это возможно,I выбирается атом A с входящим в него термом f(t1 , .

. . , tn )I выбранный терм заменяется в атоме на “свежую”переменную yI полученный атом A0 заменяется на формулу∀y (D {xf /y, x1 /t1 , . . . , xn /tn } → A0 )ОпределимостьТеорема о разрешимости доопределения теорииЕсли теория T сигнатуры σ разрешима, то теорияT ∪ {ϕ} сигнатуры σ+s , где ϕ — аксиома, определяющаясимвол s, также разрешимаДоказательство.Устранение функционального символа s = f (n)(D : x·2 = x1 × x1 )∀v (v = S(0) → ∀x ∃y ∃u ((x + v)2 = y + u));∀v (v = S(0) → ∀x ∃y ∃u ∀w (w = (x + v) × (x + v) → w = y + u))Например:ОпределимостьТеорема о разрешимости доопределения теорииЕсли теория T сигнатуры σ разрешима, то теорияT ∪ {ϕ} сигнатуры σ+s , где ϕ — аксиома, определяющаясимвол s, также разрешимаДоказательство.И что же осталось для обоснования теоремы?Показать, что для любой формулы ψ до преобразования исоответствующей ей формулы ψ 0 после преобразования верно|=T ∪{ϕ} ψ ⇔ |=T ψ 0Можете попробовать доказать это самостоятельноHОпределимостьТеорема о разрешимости доопределения теорииЕсли теория T сигнатуры σ разрешима, то теорияT ∪ {ϕ} сигнатуры σ+s , где ϕ — аксиома, определяющаясимвол s, также разрешимаТеперь можно по умолчанию считать, что помимомаленького набора понятий, указанного в сигнатуре σ,теорией описываетсянамного больший набор понятий s:все те предметы, функции и отношения,которые можно явно определитьна основе имеющихся в σФормальная арифметикаПримеры определений и предложений в сигнатуре σarIопределение натурального числа n:xn = S(S(.

. . S(0) . . . ))| {z }n разIIIопределение чётности числа (Even(1) ):∃y (x1 = y × 2)определение простоты числа (Prime(1) ):∀y ∀z (x1 = y × z → y = 1 ∨ z = 1)гипотеза Гольдбаха:∀x (Even(x) & x ≥ 4 →∃y ∃z (Prime(y) & Prime(z) & x = y + z))(и это далеко не всё, на что способна формальная арифметика)Формальная арифметикаЧтобы была хоть какая-нибудь возможность анализироватьистинность предложений в естественной интерпретации Iarлогическими методами, необходимо иметь теорию Tar ,адекватно описывающую эту интерпретацию:I Iar |= TarI теория Tar полнаСуществует ли такая теория Tar ?Да, например, элементарная теория интерпретации IarНо наличие такой теории никак не поможет в логическоманализе арифметических высказываний: чтобы описатьэлементарную теорию, необходимо решить проблему, дляисследования которой эта теория описываетсяА можно ли описать систему аксиом попроще и попонятнее?Теорема Гёделя о неполнотеЛюбая рекурсивно перечислимая1 теория в сигнатуреформальной арифметики, моделью которой являетсяинтерпретация Iar , неполнаНабросок доказательстваДокажем более простое утверждение:любая конечная теория с моделью Iar неполнаОт противного предположим, что существует конечная полнаятеория T , такая что Iar |= TДокажем, что в любой такой теории T необходимо присутствуетпарадокс лжеца:существует предложение,утверждающее, что это предложение ложно1Существует алгоритм, перечисляющий аксиомы одну за одной;останавливаться алгоритм не обязанТеорема Гёделя о неполнотеНабросок доказательстваПредметы интерпретации Iar — целые неотрицательные числа,поэтому начнём доказательство с сопоставления каждойформуле такого числа1Сопоставим натуральное число каждому символу алфавитасигнатуры σar :IIII1g (0) = 1, g (+) = 2, g (×) = 3, g (=) = 4g (() = 5, g (,) = 6, g ()) = 7g (&) = 8, g (∨) = 9, g (→) = 10, g (¬) = 11,g (∀) = 12, g (∃) = 13g (x1 ) = 14, g (x2 ) = 15, g (x3 ) = 16, .

. .То есть с описания нумерации ГёделяТеорема Гёделя о неполнотеНабросок доказательстваСопоставим формуле ϕ натуральное число (код формулы)g (ϕ[1])g (ϕ[2])g (ϕ[|ϕ|])g (ϕ) = p1× p2× · · · × p|ϕ|ЗдесьI pi — i-е простое числоI ϕ[i] — i-й символ в записи формулы ϕI |ϕ| — размер записи формулы ϕУтверждениеСуществует алгоритм, проверяющий, является ли числоi, i ∈ N0 , кодом формулы(здесь и дальше “алгоритм” — это машина Тьюринга,с алфавитом ленты {0, 1, Λ},работающая с двоичными кодами чисел)Теорема Гёделя о неполнотеНабросок доказательстваИспользуя тот же приём со степенями простых чисел, можноопределить кодI конечной последовательности формулI конечной семантической таблицыI конечного табличного выводаВ теореме полноты табличного вывода был описан алгоритмпостроения успешного вывода Tab(ϕ) для таблицы h T | ϕ i, гдеϕ — произвольная T -общезначимая формулаУтверждениеСуществует алгоритм, останавливающийся тогда итолько тогда, когда на вход подан код какой-либообщезначимой формулы ϕ, и выдающий в ответ кодвывода Tab(ϕ)Теорема Гёделя о неполнотеНабросок доказательстваИ как существование всех этих алгоритмов нам поможет всооружении парадокса лжеца?Вычислимая функция — это частично определённоеотображение f : N0 → N0 , такое что существует реализующийего алгоритм(предполагаю, что понятие вычислимой функции вам знакомо,поэтому подробнее на нём не останавливаюсь)График функции f : N0 → N0 — это множество всех пар чисел(i, j), таких что значение f (i) определно и равно jТеорема Гёделя о неполнотеНабросок доказательстваОтношение R ⊆ Nn0 арифметизуемо, если существует формулаϕ(exn ) в сигнатуре формальной арифметики, такая чтоIar |= ϕ(exn )[den ]⇔(den ) ∈ RУтверждениеГрафик любой вычислимой функции арифметизуем(это утверждение непростое,но доказывать его долго и сложно)Как следствие, арифметизуемым будет график такой функции: g (Tab(g −1 (i))), если i — кодT -общезначимой формулыft (i) =не определено, иначеТеорема Гёделя о неполнотеНабросок доказательстваЭто означает, что существует формула Proof (x, y), такая чтоIar |= Proof (x, y)[d1 , d2 ]⇔d2 — код табличного вывода Tab(ϕ),где ϕ — формула, кодом которой является число d1Рассмотрим такую формулу Val(x):∃y (Proof (x, y) ∨ Proof (neg (x), y))(neg (x) — терм, описывающий код формулы ¬g −1 (x))Что означает формула Val?Iar |= Val[d]⇔d — код формулы, истинной в IarМы выразили свойство истинности формул арифметики наязыке самой арифметики, и теперь наконец-таки можемпопытаться формализовать парадокс лжецаТеорема Гёделя о неполнотеНабросок доказательстваЛемма о диагоналиДля любой арифметической формулы ϕ(x) существуетарифметическое предложение ψ, такое чтоIar |= (ψ ↔ ϕ(x))[g (ψ)](это второе нетривиальное утверждение,которое приведено без доказательства)Применим лемму о диагонали к формуле ϕ = ¬Val:Существует предложение ψ, такое чтоIar |= (ψ ↔ ¬Val(x))[g (ψ)]И что же это означает?Предложение ψ истинно в Iar ⇔ оно ложно в IarHАксиомы равенстваПредикатный символ =(2) нередко используется в “реальных”теориях с одинаковым смыслом: равенство предметовАксиомы, используемые для придания символу =(2) смысларавенства, также оказываются похожими в разных теорияхМножество аксиом равенства произвольной сигнатуры σ,содержащей предикатный символ =(2) , состоит из:I всех аксиом теории равенства T=I аксиом∀exn ∀eyn (x1 = y1 & .