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

Computer Science Asked by TomR on November 8, 2020

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 (that λx.Φ(x) is true for all values of argument, all values of x) 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 is correct way to express, using quantifier, that expression λx.Φ(x) is true for all values of x?

Generally my concern (and therefore – my question) is valid. Let’s consider F(x,y)=λx.λy.Φ(x, y). In that case ∀F is ambigous (there is big difference between ∀x.F(x, y) and ∀y.F(x, y)) and ∀∀F and would be even more ambigous for functions with argument count n>=3. So, ∀ should mention argument explicitly. But I guess – noone can refer to some argument explicitly for the function that is written in anonymous form (with λ) or am I wrong? I am so confused about this notation – how to refere the argument of anonymous function which is referred by ∀?

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?

## Related Questions

### Solving the Knapsack problem in $O(n^2P)$, where P is the maximum weight of all items

1  Asked on November 28, 2021 by user2207686

### Number of words of length n for special language

0  Asked on November 28, 2021

### Intuition for Church-Turing thesis for Turing machines

2  Asked on November 28, 2021

### Global-input-local-output p-time algorithms

0  Asked on November 25, 2021

### Does a regular expression exist for any number that contains no more than two 5s and no 6 twice in a row?

2  Asked on November 25, 2021 by hish

### Is $EVEN-SAT$ $NP$-hard?

2  Asked on November 23, 2021 by zur-luria

### Proof of the undecidability of compiler code optimization

5  Asked on November 23, 2021 by stephen-mwangi

### Counting circuits with constraints

1  Asked on November 23, 2021 by judy-l

### Uncurrying and Polymorphism

3  Asked on November 21, 2021

### Algorithm suggestion to order data with specific condition

0  Asked on November 21, 2021 by user3862410

### If $A$ is context-free then $A^*$ is regular

1  Asked on November 21, 2021

### Which is the best approach to solve Turing machines exercises?

2  Asked on November 17, 2021 by ocram

### What is the reason for writing parallel programs?

1  Asked on November 17, 2021 by user123521

### Are all Recursively Enumerable languages which are not Recursive also Undecidable?

1  Asked on November 17, 2021 by dshri

### Is English Turing-complete?

3  Asked on November 15, 2021

### If factor isn’t found in P-1 algorithm, should upper bound be increased linearly (i.e. +1)

0  Asked on November 13, 2021 by northerner

### Can map-reduce speed up the count-min-sketch algorithm?

1  Asked on November 11, 2021 by pragya

### Maximization problem on finite collection of finite sets

1  Asked on November 11, 2021 by yuezato

### Do there exist fast multiplication algorithms for two integers with one of them being static?

1  Asked on November 8, 2021 by john-flemin

### Convert the given NFA to DFA

2  Asked on November 5, 2021 by vinay-varahabhotla