[FOM] Why not this theory be the foundational theory of mathematics?
José Manuel Rodriguez Caballero
josephcmac at gmail.com
Fri Mar 29 07:05:12 EDT 2019
"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.
Sent from my iPhone
More information about the FOM