[FOM] Formalization Thesis
wojtek at cs.cornell.edu
Fri Jan 4 19:11:43 EST 2008
On Fri, 4 Jan 2008, Andrej Bauer wrote:
> And just a quick comment: Timothy picked ZFC as an example. People who
> actually work on formalization know that having powerful type-theoretic
> infrastructure is absolutely necessary to keep things organized (imagine
> having 3000 lemmas...). So they use type theory instead. For example,
Infrastructure is orthogonal to whether one uses type theory or set
theory. Mizar's dealing with the number of lemmas pretty fine.
> Because most modern proof asistants (Coq, Isabelle) can
> easily encode ZFC, as well as ZFC + your favorite large cardinals, as
> well as intuitionistic mathematics, temporal logic, etc., it would be
This is simply not true, unless by "encode ZFC" you mean encode *both* the
logic and the axioms, in which case the claim is somewhat vacous, as
then you can "encode ZFC" in any programming language.
> theories. I am just pointing out that the practice of formalization
> requires a great deal of "logic engineering" (that logicians are not
> used to) that is invisible in ZFC.
In type theory as well. These issues do not depend much on underlying
More information about the FOM