[FOM] Alternative foundations?

[Panu Raatikainen]

henk <henk at cs.ru.nl>:

> Now a FOM has as task to be able to represent proofs, so that others
> can check them. Set theory is a very awkward theory to represent  
> computations. ... as proofs involving serious computing  become  
> unreadable. In short: set theory doesn't contain a convenient  
> computational model.

This may be true about the official language of set theory (with only  
membership and identity), but surely we in practice extend the  
language with the help of definitions. And I can't see how this is  
problem in that case.
Or am I missing something?


On 22 Feb 2014 09:59, "Hendrik Boom" wrote:

> Subsuming logic into the type theory has been around since  
> Martin-Lof's intuitionistic type theory.   What's interesting about
> homotopy type theory appears to be the treatment of equality types.

At least Martin-Löf's type theory is essentially based on the idea of  
"propositions-as-types" (a proposition is identified with the type of  
its proofs) - which in turn presupposes the intuitionistic notion of  
absolute provability. (And I, for one, have always found that notion  
deeply unclear...) Inasmuch as HoTT is founded on the same idea, I am  
not too convinced... (Is it?)


Best

Panu


-- 
Panu Raatikainen

Ph.D., Adjunct Professor in Theoretical Philosophy

Theoretical Philosophy
Department of Philosophy, History, Culture and Art Studies
P.O. Box 24  (Unioninkatu 38 A)
FIN-00014 University of Helsinki
Finland

E-mail: panu.raatikainen at helsinki.fi

http://www.mv.helsinki.fi/home/praatika/