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

[Patrik Eklund]

Dear José,

> 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?

I can try.

Concerning the quantifiers it is indeed more tricky, and some remarks 
were given from my side in a recent posting.

---

Concerning the lambda symbol and lambda terms, I can refer to our 
unpublished

   http://glioc.com/files_glioc/ModernEyesOnLambdaCalculus.pdf

the content of which was presented at the International Workshop on 75 
Years of the lambda-Calculus,
St Andrews (Scotland), 15 June 2012. The three-level signature 
construction also appears in our Fuzzy Terms

   https://www.sciencedirect.com/science/article/pii/S0165011413000997

---

Here a brief outline of the idea. Given a signature (S,Omega) we have 
the first level of terms, and then we create a "second level signature" 
with 'type' as the only type, and all types in S as constant operators 
of type 'type'. We add one binary operator => : type x type -> type to 
the second level set of operators, and this the terms on level two are 
all "simple types" (types from S and all function types created from 
types in S). This terms set of ground terms on level two we use as types 
on a level three signature. For any two types s1 and s2 on the third 
level, we add an app_{s1,s2} operator which corresponds to the 
application in lambda calculus. Operators from level one and transformed 
down to level three. See page 5 in St Andrews paper where a omega 
transforms to a lambda^omega. Clearly we do not need the lambda symbol 
at all, and in fact, there is not one one all-purpose lambda symbol. The 
point is that omega "owns its abstraction", i.e. there is now 
general-purpose lambda as an abstractor. De Bruijn went a bit in this 
direction, but we drive it far enough to make considerations of "free 
and bound" obsolete.

Barendregt during that my presentation at St Andrews still defended the 
traditional notation because it is "elegant", and it is, but it leads to 
trouble, because renaming and such things must be handled well. We avoid 
renaming as pointed out down on p. 6.

The implementational efficiency, e.g. thinking about Isabelle and HOL, 
of what we do surely is not as for the traditional one, but this, we 
claim, creates lambda terms in a way that "avoids trouble" that must be 
fixed in one way or another.

---

On pp. 7-12 in the St Andrews paper you also what happens when we 
explain Schönfinkel, Curry and Church in this presence of the 
three-level signature approach.

---

The motivation of doing this does not stop there.

In logic we are generally interested in many-valued logic, and when we 
adopt that third level lambda term functor e.g. over Goguen's category 
Set(Q), where could be a quantale, we are getting fuzzy lambda calculus 
(entirely different from Vilem Novak's approach). We also see how 
description logic, also as a many-valued logic, in fact can be seen as a 
lambda-calculus, and not as something sub to first-order. This is 
detailed in the Fuzzy Terms paper.

All this can be generalized over monoidal closed categories, which 
brought us to the algebraic foundations of many-valuedness as presented 
in our book from last year

   https://www.springer.com/us/book/9783319789477

Non-commutativity comes into play.

---

Applications are interesting for us.

Many-valuedness in these algebraic senses appear almost anywhere, and 
health care terminologies has been one of my favourites.

---

Best,

Patrik



On 2019-03-29 13:05, José Manuel Rodriguez Caballero wrote:
> 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