11.4: Логіка вищого порядку

Template:MathJaxZach

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

На практиці логіка вищого порядку часто формулюється з точки зору функцій замість відносин. (За модулем природних ідентифікацій ця різниця несуттєва.) З огляду на деякі основні «\(A\)сортування»\(B\)\(C\),,,... (які ми зараз будемо називати «типами»), ми можемо створювати нові, обумовлюючи

Якщо\(\sigma\) і\(\tau\) є кінцевими типами, то так і є\(\sigma \to \tau\).

Подумайте про типи як синтаксичні «мітки», які класифікують об'єкти, які ми хочемо в нашій області;\(\sigma \to \tau\) описує ті об'єкти, які є функціями, які приймають об'єкти типу\(\sigma\) до об'єктів типу\(\tau\). Наприклад, ми можемо захотіти мати тип\(\Omega\) істинних значень, «true» і «false», і тип\(\Nat\) натуральних чисел. У такому випадку ви можете думати про об'єкти типу\(\Nat \to \Omega\) як унарні відносини, або підмножини\(\Nat\); об'єкти типу\(\Nat \to \Nat\) - це функції від натуральних чисел до натуральних чисел; а об'єкти типу\((\Nat \to \Nat) \to \Nat\) є «функціоналами», тобто вищими- функції типу, які приймають функції до чисел.

Як і у випадку з логікою другого порядку, можна думати про логіку вищого порядку як різновид багатосортованої логіки, де є свого роду для кожного типу об'єкта, який ми хочемо розглянути. Але зазвичай зрозуміліше просто визначити синтаксис логіки вищого типу з нуля. Наприклад, ми можемо визначити набір скінченних типів індуктивно, наступним чином:

1. \(\Nat\)є кінцевим типом.

2. Якщо\(\sigma\) і\(\tau\) є кінцевими типами, то так і є\(\sigma \to \tau\).

3. Якщо\(\sigma\) і\(\tau\) є кінцевими типами, так і є\(\sigma \times \tau\).

Інтуїтивно\(\Nat\) позначає тип натуральних чисел,\(\sigma \to \tau\) позначає тип функцій від\(\sigma\) до\(\tau\), і\(\sigma \times \tau\) позначає тип пар предметів, один від\(\sigma\) і один від \(\tau\). Потім ми можемо визначити набір термінів індуктивно, наступним чином:

1. Для кожного типу\(\sigma\) існує запас змінних\(x\),\(y\),\(z\),... типу\(\sigma\)

2. \(\Obj 0\)є терміном типу\(\Nat\)

3. \(\Obj S\)(наступник) - термін типу\(\Nat \to \Nat\)

4. Якщо\(s\) є терміном типу\(\sigma\), і\(t\) є терміном типу\(\Nat \to (\sigma \to \sigma)\), то\(\Obj{R}_{st}\) це термін типу\(\Nat \to \sigma\)

5. Якщо\(s\) є терміном типу\(\tau \to \sigma\) і\(t\) є терміном типу\(\tau\), то\(s(t)\) це термін типу\(\sigma\)

6. Якщо\(s\) є терміном типу\(\sigma\) і\(x\) є змінною типу\(\tau\), то\(\lambd[x][s]\) є терміном типу\(\tau \to \sigma\).

7. Якщо\(s\) є терміном типу\(\sigma\) і\(t\) є терміном типу\(\tau\), то\(\tuple{s, t}\) це термін типу\(\sigma \times \tau\).

8. Якщо\(s\) термін типу,\(\sigma \times \tau\) то\(p_1(s)\) це термін типу\(\sigma\) і\(p_2(s)\) є терміном типу\(\tau\).

Інтуїтивно\(\Obj{R}_{st}\) позначає функцію, визначену рекурсивно,\[\begin{aligned} \Obj{R}_{st}(0) & = s \\ \Obj{R}_{st}(x+1) & = t(x, R_{st}(x)),\end{aligned}\]\(\tuple{s, t}\) позначає пару, чиєю першою складовою є,\(s\) а друга складова якої є\(t\),\(p_1(s)\) і\(p_2(s)\) позначають перший і другий елементи («проекції») з\(s\). Нарешті,\(\lambd[x][s]\) позначає функцію,\(f\) визначену\[f(x) = s\nonumber\] для будь-якого\(x\) типу\(\sigma\); тому пункт (6) дає нам форму розуміння, що дозволяє нам визначати функції за допомогою термінів. Формули будуються з тверджень присудків ідентичності\(\eq[s][t]\) між однотипними термінами, звичайними пропозиційними зв'язками та кількісною оцінкою вищого типу. Потім можна прийняти аксіоми системи як основні рівняння, що регулюють терміни, визначені вище, разом із звичайними правилами логіки з кванторами та предикатом ідентичності.

Якщо доповнювати систему скінченного типу типом значень\(\Omega\) істинності, потрібно включити аксіоми, які також регулюють її використання. Насправді, якщо хтось розумний, можна позбутися складних формул цілком, замінивши їх термінами типу\(\Omega\)! Потім доказову систему можна відповідно модифікувати. Результатом є, по суті, проста теорія типів, викладена Церквою Алонзо в 1930-х роках.

Як і у випадку з логікою другого порядку, існують різні версії семантики вищого типу, які можна використовувати. У повній версії змінні типу\(\sigma \to \tau\) змінюються по множині всіх функцій від об'єктів типу\(\sigma\) до об'єктів типу\(\tau\). Як і слід було очікувати, ця семантика занадто сильна, щоб визнати повну, ефективну систему доказів. Але можна розглянути більш слабку семантику, при якій структура складається з наборів елементів\(T_\tau\) для кожного типу\(\tau\), разом з відповідними операціями по застосуванню, проекції тощо Якщо деталі виконані правильно, то можна отримати теореми про повноту для види доказостійких систем, описаних вище.

Логіка вищого типу приваблива тим, що вона забезпечує основу, в якій ми можемо вбудовувати багато математики природним чином: починаючи з\(\Nat\), можна визначити дійсні числа, безперервні функції тощо. Він також особливо привабливий в контексті інтуїціоністичної логіки, оскільки типи мають чіткі «конструктивні» тлумачення. Насправді можна розробити конструктивні варіанти семантики вищого типу (заснованої на інтуїціоністичній, а не класичній логіці), які досить красиво прояснюють ці конструктивні тлумачення, і багато в чому цікавіші, ніж класичні аналоги.