Comment comprendre quantificateur sans prédication “ ∀(λφ.(φ x m→ φ y))”?

Question

Je lis à propos de l'incorporation de l'automatisation des logiques modales classiques d'ordre supérieur logique (http://page.mi.fu-berlin.de/cbenzmueller/papers/C46.pdf) et Goedels la preuve de l'existence de Dieu est l'exemple le plus marquant ici https://www.isa-afp.org/entries/GoedelGod.html (comme encodé pour Isabelle/HOL).

Cette incorporation a l'incorporation de l'égalité de Leibniz pour les particuliers:

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

et ce type de euqality est utilisé pour la première axiome déjà:

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

qui peut être écrit sans lambdas comme:

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

Ma question est - comment comprendre l'expression ∀(λφ. (φ x m→ φ y)), car habituellement, nous avons ∀x.P(x)?I. e.quantificateur universel attend de l'argument (x) et le prédicat (P(x)), mais cette expression contient ne sais quoi?est ensemble (λφ. (φ x m→ φ y)) et l'argument x ou Prédicat P(x)?Ce qui peut être omis ici, ce qui est la convention utilisée ici?

Answer 1

L' $x$ dans $\forall x .P(x)$ est pas un argument.C'est un variable liée indiquant la variable qui le quantifer est en allant sur.

Laissez-nous comparer la situation de l'intégrale, pour nos résultats concrets juste de $0$ pour $1$.Voici un exemple:$$\int_0^1 x^2 + 3 x \, dx$$ C'est un très archaïques de la manière d'écrire des expressions mathématiques que les mathématiciens aiment s'en tenir.En général (et en ignorant les détails au sujet de la non-intégrable fonctions) l'intégrale est lui-même une fonction:elle prend une fonction $f$ comme argument, comme $f(x) = x^2 + 3x$ et renvoie un nombre (l'aire sous la courbe).Donc, on pourrait simplement écrire $I$ pour "l'intégration de $0$ pour $1$"et puis l'intégrale de $f$ est tout simplement $$I(f)$$ (Ou si vous voulez garder l'intégration des limites visibles écrire $I_0^1(f)$, mais je ne veux pas).L'argument $f$ n'a pas besoin d'être un symbole, il peut être une expression complexe:$$I(x \mapsto x^2 + 3 x)$$ Remarquez comment "$dx$"au-dessus changé "$x \mapsto$".Dans $\lambda$-calcul de la notation de nous écrire ce que $$I(\lambda x .x^2 + 3 x).$$ Dans archaïque notation parfois, les gens se sentent mal à l'aise à l'écrit $$\int_0^1 f$$ et de sorte qu'ils finissent toujours l'affichage $dx$ par la rédaction $$\int_0^1 f(x) \, dx$$ même si il n'y a vraiment pas besoin de le faire, parce que $\int_0^1$ est un fonction d'ordre supérieur les cartes valeurs réelles fonctions de nombres réels.Si vous voulez faire traditionnel mathématicien mal à l'aise, vous devez écrire $$\int_0^1 (x \mapsto x^2 + 3 x)$$ sur leurs tableaux

Si c'est beaucoup plus clair, alors il devrait être facile de voir que le quantificateur universel $\forall$ c'est comme l'intégration, sauf qu'elle prend un la fonction propositionnelle (une cartographie de la vérité des valeurs plutôt que des numéros) et renvoie un valeur de vérité de.La notation archaïque $$\forall x .(x^2 + 3 x > -3)$$ peut être changé, tout comme pour les intégrales, à $$A(f).$$ Ici $A$ est le quantificateur universel, et $f$ son argument, qui est une fonction de mappage à partir d'un jeu de la vérité des valeurs.Un exemple d'une telle fonction est $f(x) = (x^2 + 3 x > -3)$.Et encore une fois, nous pouvons inline l'expression complexe à obtenir $$A(\lambda x .(x^2 + 3 x > -3))$$ Maintenant, il suffit de remplacer $A$ avec $\forall$ pour le bon vieux temps l'amour:$$\forall(\lambda x .(x^2 + 3 x > -3)).$$ Ce son comment les ordinateurs comme elle.La notation est général, donc on peut écrire simplement $\forall f$ au lieu de $\forall x .f(x)$, et il expose $\forall$ pour ce qu'il est:un d'ordre supérieur la fonction que les cartes de fonction propositionnelle à la vérité des valeurs.