Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

One "application" (in quotes because honestly for all the fanfare I haven't come across something that was worked out to be usable by non-specialists) is automatic differentiation, see http://blog.sigfpe.com/2006/09/practical-synthetic-different...

Generally speaking, the ability to extended intuionistic mathematics by new axioms that are classically inconsistent is a bit of a misnomer. The real power is that these "axioms" allow you to easily and immediately specialize the generic language of intuionistic mathematics into a domain-specific language for various areas.

So that

1. adding the continuity axiom gives you a domain-specific language which can only describe continuous functions and no others

2. adding the differentiation axiom gives you a domain-specific language called synthetic differential geometry in which you can only talk about differentiable functions

3. adding the computability axiom gives you a domain-specific language in which you can only talk about computable functions.

4. adding the law of the excluded middle gives you the domain-specific language of classical mathematics.

Now, each of the first three can also be interpreted within classical mathematics (which is how we know the extensions are consistent with classical mathematics), but that's analogous to writing an interpreter in C versus merely adding new syntax to an existing language (e.g. how DSLs can be implemented in LISP).



Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: