11.3: Логіка другого порядку

Template:MathJaxZach

Мова логіки другого порядку дозволяє кількісно оцінювати не тільки область окремих осіб, але і над відносинами в цій області. З огляду на мову першого порядку\(\Lang{L}\), для кожного\(k\) з них додає змінні,\(R\) які варіюються над\(k\) -ary відносини, і дозволяє кількісно оцінити ці змінні. Якщо\(R\) є змінною для\(k\) -ary відношення, і,...\(t_1\),\(t_k\) є звичайними (першого порядку) членами,\(\Atom{R}{t_1,\dots,t_k}\) є атомарною формулою. В іншому випадку набір формул визначається так само, як і у випадку з логікою першого порядку, з додатковими реченнями для кількісної оцінки другого порядку. Зауважте, що у нас є лише присудок ідентичності для термінів першого порядку: якщо\(R\) і\(S\) є змінними відношення однакової арності\(k\), ми можемо визначити,\(\eq[R][S]\) щоб бути абревіатурою для\[\lforall{x_1 \dots}{\lforall{x_k}{(\Atom{R}{x_1, \dots, x_k} \liff \Atom{S}{x_1, \dots, x_k})}}.\nonumber\]

Правила логіки другого порядку просто розширюють правила квантора на нові змінні другого порядку. Тут, однак, потрібно бути трохи обережним, щоб пояснити, як ці змінні взаємодіють з предикатними символами\(\Lang{L}\), і з формулами\(\Lang{L}\) більш загалом. Як мінімум, змінні відношення вважаються термінами, тому один має висновки форми\[A(R) \Proves \lexists{R}{A(R)}\nonumber\] Але якщо\(\Lang{L}\) мова арифметики з символом постійного відношення\(<\), можна також очікувати, що наступний висновок буде дійсним: \[x < y \Proves \lexists{R}{\Atom{R}{x,y}}\nonumber\]або для заданої формули\(A\),\[A(x_1, \dots, x_k) \Proves \lexists{R}{\Atom{R}{x_1,\dots,x_k}}\nonumber\] Більш загалом, ми могли б хотіти дозволити умовиводи форми,\[\Subst{A}{\lambd[\vec x][B(\vec x)]}{R} \Proves \lexists{R}{A}\nonumber\] де\(\Subst{A}{\lambd[\vec x][B(\vec x)]}{R}\) позначає результат заміни кожної атомної формули форми\(\Obj{R}{t_1,\dots,t_k}\) в \(A\)по\(B(t_1, \dots, t_k)\). Це останнє правило еквівалентно наявності схеми розуміння, тобто аксіоми форми\[\lexists{R}{\lforall{x_1, \dots, x_k}{(A(x_1, \dots, x_k) \liff \Atom{R}{x_1, \dots, x_k})}},\nonumber\] один для кожної формули\(A\) в мові другого порядку, в якій не\(R\) є вільною змінною. (Вправа: показати, що якщо\(R\) дозволено відбуватися в\(A\), ця схема непослідовна!)

Коли логіки посилаються на «аксіоми логіки другого порядку», вони зазвичай означають мінімальне розширення логіки першого порядку за правилами квантора другого порядку разом зі схемою розуміння. Але часто цікаво вивчати слабші підсистеми цих аксіом і правил. Наприклад, зауважте, що в повній узагальненості схема аксіоми осмислення є імпредикативною: вона дозволяє стверджувати про існування відношення\(\Atom{R}{x_1, \dots, x_k}\), яке «визначається» формулою з кванторами другого порядку; і ці квантори варіюються над множиною всіх таких відношень—a набір, який включає в\(R\) себе! Приблизно на рубежі двадцятого століття поширеною реакцією на парадокс Рассела було покладання провини на такі визначення, і уникати їх у розробці основ математики. Якщо забороняється використовувати квантори другого порядку у формулі\(A\), то має предикативну форму розуміння, яка дещо слабкіше.

З семантичної точки зору можна вважати структуру другого порядку, що складається з структури першого порядку для мови, поєднаної з безліччю відносин на області, над якою перебувають квантори другого порядку (точніше, для кожного\(k\) існує сукупність відносин арності). \(k\)). Звичайно, якщо розуміння включено в систему доказів, то у нас є додаткова вимога, що в «частині другого порядку» є достатньо відносин, щоб задовольнити аксіом розуміння - інакше система доказів не є звуковою! Один простий спосіб застрахувати, що навколо досить відносин - взяти частину другого порядку, щоб складатися з усіх відносин на частині першого порядку. Така структура називається повною, і, в певному сенсі, дійсно є «передбачуваною структурою» для мови. Якщо ми обмежуємо нашу увагу повними структурами, ми маємо те, що відомо як повна семантика другого порядку. У цьому випадку вказівка структури зводиться до вказівки частини першого порядку, оскільки вміст частини другого порядку випливає з неї неявно.

Підводячи підсумок, існує певна неоднозначність при розмові про логіку другого порядку. З точки зору системи доказів, можна мати на увазі або

1. «Мінімальна» система доказів другого порядку разом з деякими аксіомами розуміння.

2. «Стандартна» система доказів другого порядку, з повним розумінням.

З точки зору семантики, може бути зацікавлений в будь-якому

1. «Слабка» семантика, де структура складається з частини першого порядку, разом з частиною другого порядку, досить великою, щоб задовольнити аксіоми розуміння.

2. «Стандартна» семантика другого порядку, в якій розглядаються тільки повні структури.

Коли логіки не вказують систему доказів або семантику, яку вони мають на увазі, вони зазвичай посилаються на другий пункт у кожному списку. Перевага використання цієї семантики полягає в тому, що, як ми побачимо, вона дає нам категоричні описи багатьох природних математичних структур; в той же час система доказування досить сильна і звучна для цієї семантики. Недоліком є те, що система доказування не є повною для семантики; насправді, жодна ефективно задана система доказів не є повною для повної семантики другого порядку. З іншого боку, ми побачимо, що система доказів є повною для ослабленої семантики; це означає, що якщо речення не є доказовим, то існує якась структура, не обов'язково повна, в якій воно помилкове.

Мова логіки другого порядку досить багатий. Можна ідентифікувати унарні відносини з підмножинами області, і тому, зокрема, ви можете кількісно оцінити над цими множинами; наприклад, можна висловити індукцію для натуральних чисел з однією аксіомою\[\lforall{R}{((\Atom{R}{\Obj{0}} \land \lforall{x}{(\Atom{R}{x} \lif \Atom{R}{x'})}) \lif \lforall{x}{\Atom{R}{x}})}.\nonumber\] Якщо взяти мову арифметики мати символи\(\Obj 0, \Obj \prime, +, \times\) і \(<\), можна додати такі аксіоми, щоб описати їх поведінку:

1. \(\lforall{x}{\lnot x' = \Obj 0}\)

2. \(\lforall{x}{\lforall{y}{(s(x) = s(y) \lif x = y)}}\)

3. \(\lforall{x}{(x + \Obj 0) = x}\)

4. \(\lforall{x}{\lforall{y}{(x + y') = (x + y)'}}\)

5. \(\lforall{x}{(x \times \Obj 0) = \Obj 0}\)

6. \(\lforall{x}{\lforall{y}{(x \times y') = ((x \times y) + x)}}\)

7. \(\lforall{x}{\lforall{y}{(x < y \liff \lexists{z}{y = (x + z')})}}\)

Неважко показати, що ці аксіоми разом з аксіомою індукції вище дають категоричний опис структури\(\Struct{N}\), стандартну модель арифметики, за умови використання повної семантики другого порядку. Враховуючи будь-яку структуру,\(\Struct{M}\) в якій ці аксіоми є істинними, визначте функцію\(f\) від\(\Nat\) до області\(\Struct{M}\) використання звичайної рекурсії на\(\Nat\), так що\(f(0) = \Assign{\Obj 0}{M}\) і\(f(x+1) = \Assign{\prime}{M}(f(x))\). Використовуючи звичайну індукцію\(\Nat\) і той факт, що аксіоми (1) і (2)\(\Struct M\) тримаються, ми бачимо, що\(f\) є ін'єкційним. Щоб побачити, що\(f\) є суб'єктивним,\(P\) Дозволяти бути набір елементів\(\Domain{M}\), що знаходяться в діапазоні\(f\). Так як\(\Struct M\) повний,\(P\) знаходиться в домені другого порядку. За конструкцією\(f\), ми знаємо, що\(\Assign{\Obj 0}{M}\) знаходиться в\(P\), і що\(P\) закрито під\(\Assign{\prime}{M}\). Той факт, що індукційна аксіома тримається в\(\Struct M\) (зокрема, для\(P\)) гарантує, що\(P\) дорівнює всій області першого порядку\(\Struct M\). Це показує, що\(f\) це біекція. Показати, що\(f\) це гомоморфізм, не складніше, використовуючи звичайну індукцію на\(\Nat\) багаторазово.

У теоретичних множині функція - це лише особливий вид відношення; наприклад, унарну функцію\(f\) можна ідентифікувати з двійковим співвідношенням, що\(R\) задовольняє\(\lforall{x}{\lexists{!y}{R(x,y)}}\). Як результат, можна кількісно оцінити і над функціями. Використовуючи повну семантику, потім можна визначити клас нескінченних структур як клас структур,\(\Struct M\) для яких існує ін'єкційна функція від області\(\Struct M\) до власної підмножини себе:\[\lexists{f}{(\lforall{x}{\lforall{y}{(\eq[f(x)][f(y)] \lif \eq[x][y])}} \land \lexists{y}{\lforall{x}{\eqN[f(x)][y]}})}.\nonumber\] заперечення цього речення тоді визначає клас скінченних структур.

Крім того, можна визначити клас порядків, додавши до визначення лінійного впорядкування наступне:\[\lforall{P}{(\lexists{x}{\Atom{P}{x}} \lif \lexists{x}{(\Atom{P}{x} \land \lforall{y}{(y < x \lif \lnot \Atom{P}{y})})})}.\nonumber\] Це стверджує, що кожна непорожня множина має найменший елемент, по модулю ідентифікація «множини» з «одномісним співвідношенням». Для іншого прикладу можна висловити поняття зв'язності для графів, сказавши, що немає нетривіального поділу вершин на роз'єднані частини:\[\lnot \lexists{A}{(\lexists{x}{A(x)} \land \lexists{y}{\lnot A(y)} \land \lforall{w}{\lforall{z}{((\Atom{A}{w} \land \lnot \Atom{A}{z}) \lif \lnot \Atom{R}{w,z})}})}.\nonumber\] Для ще одного прикладу ви можете спробувати як вправу визначити клас скінченних структур, область яких має парний розмір. Більш вражаюче, можна надати категоричний опис дійсних чисел як повне впорядковане поле, що містить раціональні.

Словом, логіка другого порядку набагато виразніше логіки першого порядку. Це хороша новина; тепер для поганого. Ми вже згадували, що не існує ефективної системи доказування, яка б була повноцінною для повної семантики другого порядку. На краще чи на гірше, багато властивостей логіки першого порядку відсутні, включаючи компактність та теореми Левенгейма-Сколема.

З іншого боку, якщо хтось готовий відмовитися від повної семантики другого порядку з точки зору слабшого, то мінімальна система доказування другого порядку є повною для цієї семантики. Іншими словами, якщо ми читаємо\(\Proves\) як «доводить в мінімальній системі» і\(\Entails\) як «логічно означає слабшу семантику», ми можемо показати це коли завгодно\(\Gamma \Entails A\)\(\Gamma \Proves A\). Якщо хтось хоче включити конкретні аксіоми розуміння в систему доказування, потрібно обмежити семантику структурами другого порядку, які задовольняють цим аксіомам: наприклад, якщо\(\Delta\) складається з набору аксіом розуміння (можливо, усіх), ми маємо, що якщо\(\Gamma \cup \Delta \Entails A\), потім\(\Gamma \cup \Delta \Proves A\). Зокрема, якщо не\(A\) є доказовим використанням розглянутих нами аксіом розуміння, то існує модель,\(\lnot A\) в якій ці аксіоми розуміння, тим не менш, тримаються.

Найпростіший спосіб побачити, що теорема повноти має слабшу семантику, - це думати про логіку другого порядку як багато відсортовану логіку, як показано нижче. Один сорт інтерпретується як звичайний домен «першого порядку», а потім для кожного\(k\) ми маємо область «відношення арності»\(k\). Ми приймаємо мову, щоб мати вбудовані символи відношення «\(\Atom{\Obj{true}_k}{R,x_1,\dots,x_k}\)», який призначений стверджувати\(x_1\), що\(R\) тримає\(x_k\),..., де\(R\) змінна роду «\(k\)-ary відношення» і \(x_1\),...,\(x_k\) є об'єктами сорту першого порядку.

При такій ідентифікації слабка семантика другого порядку є, по суті, звичайною семантикою для багатосортованої логіки; і ми вже спостерігали, що багато відсортована логіка може бути вбудована в логіку першого порядку. За модулем переклади вперед і назад, слабша концепція логіки другого порядку насправді є формою логіки першого порядку в маскуванні, де область містить як «об'єкти», так і «відносини», керовані відповідними аксіомами.