The Coq mailing list

["Russell O'Connor" <roconnor AT Math.Berkeley.EDU>]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

[To: 
coq-club AT pauillac.inria.fr]

On Mon, 6 Jan 2003, Pierre Courtieu wrote:

> That is a work around, but you can't be absolutly sure that no paradox
> have been used unless you typecheck everything globally with no axiom
> (that said, the probability that you use paradox is low). But of
> course you can do global typing (if possible) only from time to time.

Exactly what kind of paradox are we talking about that would require this
global check, and for which using axioms instead of theorems would be
inadequate?

- -- 
Russell O'Connor            <http://www.math.berkeley.edu/~roconnor/>
``[Law enforcement officials] suggested that the activists were stopped
not because their names are on the list, but because their names resemble
those of suspected criminals or terrorists.'' -- SFGate.com
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.2.1 (SunOS)

iQCVAwUBPhnRP00+aO5oRkNZAQJDWwQAhtvHHJwad2C9FIUAX15KwLPeCtzZPnBF
+D61OM9fIbKxyiKI9KA9pYoJbGL9O/Mht+fCK13jhg1mOdQ6W0OpYvE2gQ8JXcir
1ZVq/9PKF2joGr8yArDD/XmTfRF3IXGQn+5wyb0sQ7siHXUB3R1g1EvNLtgmthRg
Gp73qPXkyMk=
=KO2O
-----END PGP SIGNATURE-----