Re: [mizar] [gmane.comp.science.types.announce] [Agda] CFP: Dependently Typed Programming (FI Special Issue)

[Robert Boyer <boyer@cs.utexas.edu>]

> Why do people bother with various type theories when
> set theory is available?  What is the expected gain?

I am weak in history, but I think that the
Whitehead-Russell type theory of Principia Mathematica
was invented to support the formal development of some
of mathematics with a reduced risk of hitting another
paradox, like Russell's paradox, which might prove that
the chosen set theory was inconsistent.  I think one
set theory of Quine was proved inconsistent.

The type theories of folks like Martin Lof, de Bruijn,
and Gerard Huet are even constructive.  Huet does not
like the first order theorem:

    For some x, P(x) or not P(x).

('Why is there something rather than nothing?'
Heidegger once asked.)

Paul Lorenzen did not like the theorem:

    not not p -> p

So some type theories permit one to do lots of very
constructive mathematics without depending upon a
possibly inconsistent set theory, or even on a possibly
dubious first order logic, whose semantics are
generally based on set theory.

Primitive recursive arithmetic (PRA), and the reverse
mathematics program, is another way to get by with
less.  Small is beautiful, you know, at least to some.
Others say size matters.  PRA goes back to Skolem's
idea for avoiding the inconsistencies of set theory by
avoiding quantification over infinite domains.

Frege once remarked something like, 'What is all this
concern with consistency?  Just because it is
consistent that God exists and that He is good does not
mean that a Good God Exists.'  I'm not sure yet what I
would have replied to him.

Bob

P. S. Corrections by any real masters of the subject
out there most solicited.  As Socrates says, the best
sort of thing that can happen to you is to find out
that you're wrong about something!