Как понять квантор без предикации «∀(λφ.(φ x m→ φ y))»?

Question

Я читаю о встраивании/автоматизации модальной логики в классическую логику высшего порядка (http://page.mi.fu-berlin.de/cBenzmueller/papers/C46.pdf), и доказательство Гёделя существования Бога является ярким примером здесь. https://www.isa-afp.org/entries/GoedelGod.html (как закодировано для Изабель/HOL).

Это вложение имеет вложение равенства Лейбница для индивидов:

abbreviation mLeibeq :: "μ ⇒ μ ⇒ σ" (infixr "mL=" 90) where "x mL= y ≡ ∀(λφ. (φ x m→ φ y))"

и этот тип равенства уже используется для первой аксиомы:

A1a: "[∀(λΦ. P (λx. m¬ (Φ x)) m→ m¬ (P Φ))]"

который можно записать без лямбда-выражений как:

A1a: ∀φ[P(¬φ)↔¬P(φ)]

У меня вопрос - как понять выражение ∀(λφ. (φ x m→ φ y)), потому что обычно у нас есть ∀x.P(x)?Т.е.Квантор универсальности ожидает аргумент (x) и предикат (P(x)), но в этом выражении содержится неизвестно что?целый (λφ. (φ x m→ φ y)) и аргумент x или предикат P(x)?Что здесь можно опустить, какое здесь соглашение?

Answer 1

А $х$ в $\forall x .P(x)$ является нет Аргумент.Это связанная переменная указывая, в какой переменной находится квантифер.

Сравним ситуацию с определенным интегралом, для конкретики уже с $0$ к $1$.Вот пример:$$\int_0^1 x^2 + 3 x \, dx$$Это очень архаичный способ записи математических выражений, которого любят придерживаться математики.В общем (и игнорируя детали о неинтегрируемых функциях) определенный интеграл сам по себе является функцией:это принимает функцию $f$ в качестве аргумента, например $f(x) = x^2 + 3x$ и возвращает число (площадь под кривой).Поэтому мы могли бы просто написать $I$ для «интегрировать из $0$ к $1$", а затем интеграл от $f$ это просто$$I(ф)$$(Или, если вы хотите, чтобы границы интеграции были видимыми, напишите $I_0^1(ф)$, но я не буду).Аргумент $f$ это не обязательно должен быть символ, это может быть сложное выражение:$$I(x \mapsto x^2 + 3 x)$$Обратите внимание, как "$dx$" выше изменено на "$x \mapsto$".В $\лямбда$-обозначение исчисления, мы бы написали это как$$I(\лямбда х .х^2 + 3 х).$$В архаичных обозначениях люди иногда чувствуют себя неловко при написании.$$\int_0^1 f$$и поэтому они всегда отображают $dx$ написав$$\int_0^1 f(x) \, dx$$хотя на самом деле в этом нет необходимости, потому что $\int_0^1$ это функция высшего порядка который отображает вещественные функции в действительные числа.Если вы хотите заставить традиционного математика чувствовать себя неловко, вам следует написать$$\int_0^1 (x \mapsto x^2 + 3 x)$$на своих досках

Если это ясно, то нетрудно увидеть, что квантор универсальности $\forall$ похожа на интеграцию, за исключением того, что она требует пропозициональная функция (одно сопоставление с истинностными значениями вместо чисел) и возвращает истинностное значение.Архаичные обозначения$$\forall x .(х^2 + 3 х > -3)$$можно заменить, как и для интегралов, на$$А(ф).$$Здесь $А$ является квантором всеобщности, и $f$ его аргумент, который представляет собой функцию, отображающую набор в значения истинности.Примером такой функции является $f(x) = (x^2 + 3 x > -3)$.И снова мы можем встроить сложное выражение, чтобы получить$$A(\лямбда х .(x^2 + 3 x > -3))$$Теперь просто замените $А$ с $\forall$ в память о старых добрых временах:$$\forall(\lambda x .(x^2 + 3 x > -3)).$$Вот как это нравится компьютерам.Обозначения общие, поэтому можно написать просто $\forall f$ вместо $\forall x .е(х)$, и это раскрывает $\forall$ для чего это:а более высокого порядка функция, которая отображает пропозициональную функцию в истинностные значения.