HOL = функциональный подход + конструктивная логика
логика второго порядка - формальная система, расширяющая логику первого порядка возможностью квантификации общности и существования не только над аргументами, но и над самими предикатами
для перехода к высшему порядку сами предикаты рассматриваются как "изменяемые объекты", а не условия, которые просто кем-то как-то когда-то откуда-то свыше "даны". такой "предикат" может менять свои показания даже при одном и том же значении "аргумента" - ну, например, обладать "памятью" обращений к нему (при этом должно строго выполняться одно условие: всякая информация о былом состоянии должна быть недоступна никому, кроме самого предиката)
в логике высокого порядка как объекты трактуются сами отношения и функции, рассматриваемые в логике предикатов. это позволяет формировать утверждения обо всех отношениях, например, если потребуется точно определить, что означает понятие транзитивного отношения. логика высокого порядка является строго более выразительной, чем логика предикатов, в том смысле, что некоторые весьма полезные высказывания логики высокого порядка не могут быть выражены с помощью любого конечного количества высказываний логики предикатов
в логике второго порядка квантификация допустима как в отношении переменных, так и в отношении предикатов или функций от переменных
предположим, что мы хотим выразить некий факт о структуре арифметики Пеано, выраженной сигнатурой:
{ N ; 0, S, <, +, × }
используя кванторы ∀ и ∃
мы можем сформулировать предложение
∀x (x < S x)
которое отражает тот факт, что каждое последующее число больше предыдущего. но трудность возникает, когда мы захотим выразить отношение строгого порядка на множестве натуральных чисел: а именно, что любое непуcтое множество натуральных чисел имеет минимальный элемент
если P является одноместным предикатом, тогда мы можем записать наличие элемента, для которого предикат "быть минимальным" выполняется:
∃x Px → ∀y (Py → y = x)эта формула верна в языке первого порядка, но у нас нет возможности записать такую же формулу с первым квантором общности
но если мы добавим квантор общности к предикату P:
∀P [ ∃x Px → ∀y (Py → y = x) ]то сразу же получим желаемое свойство, но в логике высшего порядка
используя логику второго порядка мы можем сказать, что рассматриваемый универсум бесконечен, просто выразив обязательное наличие транзитивного отношения для любого элемента к другому, но не к самому себе:
∃R [ ∀x ∀y ∀z (xRy Λ yRz → xRz) Λ ∀x (¬ xRx Λ ∃y xRy) ]здесь квантор второго поряка ∃R выражает существование бинарного отношения в универсуме
в логике второго порядка мы можем выразить индукцию натуральных чисел как:
∀P [ (P0 Λ ∀y(Py → PSy)) → ∀y Py ]
для множества действительных чисел мы можем выразить отношение B "быть least-upper-bound" с помощью высказывания:
∀B [ ∃y ∀z (Bz → z ≤ y) Λ ∃z Bz → ∃y ∀y′(∀z (Bz → z ≤ y′) ↔ y ≤ y′) ]
хорошо известен пример из области лингвистики, предложенный Джорджем Булем:
“есть критики, которые ценят только друг друга”это предложение предполагает существование людей с особым свойством, но оно не влечет суждения, что два таких человека ценят только друг друга и больше никого
в классической трактовке теории множеств не делается различия между абстрактными объектами и объектами, существование которых можно подтвердить построением - на бесконечные множества экстраполировали свойства и законы конечных совокупностей
"all xs are ys" - "X = Y" "some xs are ys" - "XY = V" , V - nonempty class "no xs are ys" - "XY = 0" , 0 - empty class
Аксиома Выбора - "для любого семейства попарно непересекающихся непустых множеств можно создать по меньшей мере одно множество, содержащее по одному (и только одному) элементу из каждого из множеств семейства"
но что значит "выбрать из множества"? выбрать какой-то элемент - значит ли это определить этот элемент так, чтобы не было сомнения, что все имеют в виду один и тот же элемент?
Гёдель доказал, что Аксиома Выбора не противоречит аксиомам теории множеств, если эти последние сами непротиворечивы, а Коэн доказал, что отрицание Аксиомы Выбора не противоречит заранее непротиворечивым аксиомам теории множеств