[FOM] Formalization Thesis

[Wojtek Moczydlowski]

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 
logic.

Wojtek Moczydlowski