So verstehen Sie den Quantor ohne Prädikation „ ∀(λφ.(φ x m→ φ y))“?

Question

Ich lese über die Einbettung/Automatisierung modaler Logiken in die klassische Logik höherer Ordnung (http://page.mi.fu-berlin.de/cbenzmueller/papers/C46.pdf) und Goedels Beweis der Existenz Gottes ist hier ein herausragendes Beispiel https://www.isa-afp.org/entries/GoedelGod.html (wie für Isabelle/HOL kodiert).

Diese Einbettung hat Einbettung zur Leibniz-Gleichstellung für Einzelpersonen:

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

und diese Art von Gleichheit wird bereits für das erste Axiom verwendet:

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

was ohne Lambdas geschrieben werden kann als:

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

Meine Frage ist: Wie ist der Ausdruck zu verstehen? ∀(λφ. (φ x m→ φ y)), denn normalerweise haben wir das ∀x.P(x)?D.h.Der universelle Quantor erwartet das Argument (x) und das Prädikat (P(x)), aber dieser Ausdruck enthält niemand weiß was?ist ganz (λφ. (φ x m→ φ y)) und Argumentation x oder Prädikat P(x)?Was kann hier weggelassen werden, welche Konvention wird hier verwendet?

Answer 1

Der $x$ In $\forall x .P(x)$ Ist nicht ein Argument.es ist ein gebundene Variable Gibt an, über welche Variable sich der Quantifer erstreckt.

Vergleichen wir die Situation mit dem bestimmten Integral, um die Konkretheit zu gewährleisten $0$ Zu $1$.Hier ist ein Beispiel:$$\int_0^1 x^2 + 3 x \, dx$$Dies ist eine sehr archaische Art, mathematische Ausdrücke zu schreiben, an der sich Mathematiker gerne orientieren.Im Allgemeinen (und abgesehen von Details zu nicht integrierbaren Funktionen) ist das bestimmte Integral selbst eine Funktion:es braucht eine Funktion $f$ als Argument, wie z $f(x) = x^2 + 3x$ und gibt eine Zahl zurück (die Fläche unter der Kurve).Wir konnten also einfach schreiben $I$ für „integrieren aus“. $0$ Zu $1$" und dann das Integral von $f$ ist einfach$$I(f)$$(Oder wenn Sie die Integrationsgrenzen sichtbar halten möchten, schreiben Sie $I_0^1(f)$, aber ich werde nicht).Das Argument $f$ muss kein Symbol sein, es kann ein komplexer Ausdruck sein:$$I(x \mapsto x^2 + 3 x)$$Beachte wie "$dx$„ oben geändert in „$x \mapsto$".In $\lambda$-Kalkül-Notation würden wir dies schreiben$$I(\lambda x .x^2 + 3 x).$$In der archaischen Notation fühlen sich die Menschen beim Schreiben manchmal unwohl$$\int_0^1 f$$und so werden sie am Ende immer angezeigt $dx$ durch Schreiben$$\int_0^1 f(x) \, dx$$auch wenn das eigentlich nicht nötig ist, denn $\int_0^1$ ist ein Funktion höherer Ordnung die reelle Funktionen auf reelle Zahlen abbildet.Wenn Sie möchten, dass sich der traditionelle Mathematiker unwohl fühlt, sollten Sie schreiben$$\int_0^1 (x \mapsto x^2 + 3 x)$$auf ihren Whiteboards

Wenn so viel klar ist, sollte es leicht zu erkennen sein, dass es sich um den universellen Quantor handelt $\füralle$ ist wie Integration, nur dass es einen braucht Satzfunktion (eine Abbildung in Wahrheitswerte anstelle von Zahlen) und gibt a zurück Wahrheitswert.Die archaische Notation$$\forall x .(x^2 + 3 x > -3)$$kann, genau wie bei Integralen, in geändert werden$$A(f).$$Hier $A$ ist der universelle Quantor und $f$ sein Argument, das eine Funktionsabbildung von einer Menge auf die Wahrheitswerte ist.Ein Beispiel für eine solche Funktion ist $f(x) = (x^2 + 3 x > -3)$.Und wieder können wir den komplexen Ausdruck einbinden, um ihn zu erhalten$$A(\lambda x .(x^2 + 3 x > -3))$$Jetzt einfach austauschen $A$ mit $\füralle$ Um der guten alten Zeiten willen:$$\forall(\lambda x .(x^2 + 3 x > -3)).$$So mögen es Computer.Die Notation ist allgemein, wir können also einfach schreiben $\forall f$ anstatt $\forall x .f(x)$, und es entlarvt $\füralle$ für das, was es ist:A Auftrag von oben Funktion, die Aussagenfunktionen auf Wahrheitswerte abbildet.