[FOM] Why not this theory be the foundational theory of mathematics?

[José Manuel Rodriguez Caballero]

Patrik wrote: 
"The tricky thing happens when we add quantifiers as characters 
and treat them as formal symbols (unlike lambda which Church said was an 
informal symbol). Then we similarly create "formulas" by putting symbols 
in sequence, using natural language to say how and how not these 
characters can be legoed together. Category has been successful in 
dealing with lambda terms, but dealing with formulas involving 
quantifiers is tricky."

Could you illustrate this criticism of symbolic use of quantifies in the particular case of the (traditional) epsilon-delta formulation of the limit of a function f(x) at a given point? Which are the consequences of your criticism in the foundations of Classical Analysis? How does this criticism affects the formalization of classical analysis in a proof assistant, e.g., Isabelle/HOL?

At least in my case, I find concrete examples useful in order to understand the abstract argument.

Kind Regards,
Jose M

Sent from my iPhone