[FOM] Why not this theory be the foundational theory of mathematics?
Patrik Eklund
peklund at cs.umu.se
Sat Mar 30 07:42:00 EDT 2019
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
More information about the FOM
mailing list