[FOM] Wiki: type theoretic fnds

[Patrik Eklund]

Harvey,

Here is a simple reason why category theory can be supportive.

If you look at classical terms, we say "Constants and variables are 
terms, and if omega is an operator with t1,...,tn as terms, then 
omega(t1,...,tn) is also a terms. These are the only terms."

This definition can be formalized to appear as a term monad, but it adds 
nothing as such, many say. However it adds in applications, since with 
that underlying term functor we can compose with other functors, and 
also view the functor over other categories than just the category of 
sets.

For "lambda terms" the situation is different. Traditionally we say 
"Variables are \-terms. If M is a \-term, then so is \x.M. If MN are 
\-terms, then so is MN.". This is seens as an "elegant" definition by 
computer scientists, even if they at the same time acknowledge, that the 
definition brings in undesirable \-terms. Tricks are needed to fix it.

Here is where Church again comes into play. Church said that '\' is an 
informal symbol, and we have formalized the construction of \-terms so 
that '\' is not an "abstractor" of operators or terms, but the operator 
itself takes care of its own abstraction. Some detail you see in the 
paper

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

and attached also our Fuzzy Terms paper with the formal and categorical 
term construction in both cases.

As one example we show how the informal treatment of "description logic" 
(the logic in web ontology, Google) can be formalized, and indeed 
extended with composition and being over other categories, which opens 
up perspectives for applications.

Curry and Howard were always cautious about these things since they knew 
something was fishy, but apparently they could never put their fingers 
on it. Martin-Löf showed no scruples and simply started to "reformalize 
foundations" with similarly sloppy symbolism. Computer scientists and 
secondhand logicians followed him like bankvoles. Today if you hear HoTT 
fanatics explain their content, you will not understand it, because even 
they don't. There is simply nothing to understand. As I often say, if 
something in their theory becomes questionable, they bring in stuff from 
the outside, so as to say.

You could also say that their approach hides things, and this makes it 
very hard to analyze. A bit like Turing machines. Recursion is hidden 
and never really brought up front. This is the reason why the 
Church-Turing thesis remains a mystery, since Church-Kleene-Gödel keeps 
all of recursion within the machinery, where Turing's approach hides it 
an it becomes "algorithm".

To conclude, type theory stays deliberately informal, and they can 
therefore continue to attract "algorithm" believers. But for 
foundations, it's no good. Similarly, I am concerned with set theory as 
being untyped, and quantifier symbols being similarly informal as 
compared to the lambda symbol. The FOM community is also stubborn, and 
this is the reasoin why I am a bit allergic against "wisdom".

There is no moderation of these things, and very few think in these 
directions. For us it is not just important formalization, but it helps 
us develop more elaborate applications, e.g. in conerning logic as 
potentially to be used in health care. Evidence-based medicine is awful. 
We need logic-based medicine.

And so on and so forth.

Sorry for spamming you, but your mail correlates with some thoughts I 
tried to present last year, but my postings were indeed rejected. I am 
therefore happy to continue to read your postings, as I have been also 
in the past, even if not replying to them earlier.

Similar type theory debates have taken place under the categories 
mailing list, where my postings have been accepted. I have been openly 
very critical against the type theory communities. Some understand, but 
the categorical machinery is quite heavy, so those not well versed in 
it, will reject it.

Best,

Patrik



On 2016-03-30 23:20, Harvey Friedman wrote:
> I looked some at
> 
> https://en.wikipedia.org/wiki/Univalent_foundations
> 
> https://en.wikipedia.org/wiki/Homotopy_type_theory
> 
> As I expected, I could not find a single example of any of the 
> following:
> 
> 1. Some issue in f.o.m. that is not being addressed by the usual f.o.m.
> 2. Some issue in f.o.m. that is being addressed by type theoretic 
> f.o.m.
> 
> I see some new algebraic/topological type interpretations of type
> theories, and the like.
> 
> Although it wasn't clear from these articles, I could imagine that
> there is some kinds of type theories for which it is not at all
> obvious that one has any mathematical model, or even that one has any
> model at all in any reasonable sense.
> 
> So the impression one inevitably gets is that this stuff is
> 
> a. A framework for doing some new kinds of abstract categorical
> algebra/topology that is exciting to very abstractly minded
> mathematicians.
> b. A complicated solution in search of a foundational problem.
> 
> So I repeat my suspicion and therefore my challenge.
> 
> Anything that can be done with this kind of "foundations" can be done
> much more simply and much more powerfully and much more effectively by
> sugaring the usual f.o.m.
> 
> But I can't start backing this up, and others cannot really challenge
> me, until they state a crystal clear foundational issue that they
> think is not or cannot be addressed in standard f.o.m., and that is
> addressed in this exotic f.o.m.
> 
> One thing that does not seem to be in doubt, correct me if I am wrong.
> This exotic f.o.m. is much more complicated than standard f.o.m.
> 
> Perhaps we should start with a simpler question.
> 
> What foundational issue is addressed by even ML type theory - no
> univalence axiom - that cannot be more simply and better addressed by
> standard f.o.m.?
> 
> Let me close with a methodological question.
> 
> What standards should be applied by proposing to replace an existing
> system with another system that is massively more complicated?
> 
> My answer of course as you see, is to ask for careful generally
> understandable explanations as to what is to be gained. There also
> needs to be a major effort made to see if the existing much simpler
> system already can be used to address the issues, whatever they are,
> adequately, or maybe even better.
> 
> Harvey Friedman
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Fuzzy Terms reprint.pdf
Type: application/pdf
Size: 494260 bytes
Desc: not available
URL: </pipermail/fom/attachments/20160331/14c6ce2c/attachment-0001.pdf>