[FOM] Alternative foundations?

[Harvey Friedman]

Henk Barendregt wrote:

Now a FOM has as task to be able to represent proofs, so that others
can check them. Set theory is a very awkward theory to represent
computations.

********************

Can't we simply prove outright that all formalisms, including ZFC with
abbreviation power, represent large computations awkwardly? If so,
awkwardness of representing computations would not be a credible
consideration in choice of foundations.

Perhaps you mean something other than "awkwardness of representation of
computations"?

Another question I would like to add to my list I questions I posted in my
first email on Alternative Foundations.

The standard way that people get convinced that an alternative foundation
is sound, at least in the sense that it is internally consistent, is to
interpret it in set theory, or a fragment of set theory. Does anybody
object to this continued practice? In particular, does somebody propose to
use an alternative foundation A for this purpose? I.e., judge the
consistency of alternative foundations B - including set theory - according
to whether B tis interpretable in A? Or is the issue of consistency and
interpretation to be rejected?

Harvey Friedman
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20140221/93637b24/attachment.html>