## How to write “∀x.F(x)” for “F(x)=λx.Φ(x)” in one expression (sequel from question about “∀(λφ. (φ x m→ φ y))”?

This question is sequel from How to understand quantifier without predication " ∀(λφ. (φ x m→ φ y))"? which further explains the notation and context.

So – I have anonymous Boolean-valued function `F(y)=λx.Φ(x)` (of course, y and x point to the same variable, I just used different syntactic names, to point out, that x is bound variable) and I would like to write the statement, that `F(x)` is true for all the values of the argument and it can be written `∀x.F(x)`. But `F(x)` is named function, but I would like to write the same expression for the anonymous function that uses lambda, so I am with my suggestion: `∀x.λx.Φ(x)` or `∀x.λy.Φ(y)`? And apparently they both are wrong.

What I am trying to achieve? I just want to build parser for language that is declared in https://www.isa-afp.org/browser_info/current/AFP/GoedelGod/GoedelGod.html. This language contains expressions like `[∀(λΦ. P (λx. m¬ (Φ x)) m→ m¬ (P Φ))]`.

I am using ANTLR grammar for lambda calculus https://github.com/antlr/grammars-v4/blob/master/lambda/lambda.g4 and I understand that the 1) quantifiers; 2) logical connectives; 3) arithmetic functions are just another lambda functions (it is just syntactic sugar that they are written in the specific non-lambda syntax/prefix form etc.) and as such I express them in the existing lambda.g4 grammar https://github.com/antlr/grammars-v4/blob/master/lambda/lambda.g4. So – my first step is to write the cited expressions with the named functions and then I will just replace them with anonymous functions because lambda.g4 has no options to introduce named functions. But it is so confusing to write anonymous function and the quantifier function for the same argument.

Just side question – maybe there is better ANTLR grammar for lambda calculus with syntactic sugar for quantifiers and connectives?

Posted on Categories proxies

## How to understand quantifier without predication ” ∀(λφ. (φ x m→ φ y))”?

I am reading about embedding/automation of modal logics in classical higher order logic (http://page.mi.fu-berlin.de/cbenzmueller/papers/C46.pdf) and Goedels proof of God’s existence is prominent example here https://www.isa-afp.org/entries/GoedelGod.html (as encoded for Isabelle/HOL).

This embedding has embedding for Leibniz equality for individuals:

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

and this type of euqality is used for the first axiom already:

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

which can be written without lambdas as:

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

My question is – how to understand the expression `∀(λφ. (φ x m→ φ y))`, because usually we have `∀x.P(x)`? I.e. universal quantifier expects the argument (`x`) and the predicate (`P(x)`), but this expression contains noone know what? is entire `(λφ. (φ x m→ φ y))` and argument `x` or Predicate `P(x)`? What can be omitted here, what is the convention used here?

Posted on Categories proxies