[FOM] consistency of NF? + equiconsistency of Map Theory

[Klaus Ebbe Grue]

> Just to be clear, with respect to what are they showing consistency of NF?
> What is the strongest system known to be consistent conditional on 
> consistency of NF?
> And while I'm on the subject of alternative foundations, what is the 
> status of Grue's "Map Theory"? Is it decisively equi-consistent with ZFC?
> Best,
> Cody

First of all: I look forward to the release of Holmes proof of the consistency
of NF. I have worked quite some time on the consistency of NF without
much luck and look forward to see how Holmes did it.

Concerning the equi-consistency of Map Theory (MT) versus ZFC:

Short answer: It depends on the definition of equi-consistent.

Long answer: As pointed out by Chantal Berline, and as far as I
remember, the problem is: To prove one axiomatic system A to
be stronger than another system B one proves Con(B) in A. That
makes sense in theories which build on top of first order predicate
calculus. One has to be careful, though, concerning how exactly
Con(B) is defined.

Now MT does not build on first order predicate calculus. And it has three
truth values: true, false, and bottom. So one at least has to go through
the definition of "equi-consistent" to see if it still makes sense.

Now to what can be done:

(1) Every formula of ZFC can be translated to a formula of MT. Every
proof in ZFC can be translated to a proof in MT. Thus, every theorem
of ZFC is a theorem of MT. Maybe MT can prove more than ZFC.
But not too much more since MT is consistent (which is provable in
ZFC+SI).

That suggests (modulo the definition of "equi-consistent" and "stronger
than") that MT is equi-consistent or stronger than ZFC. And that MT
is weaker than ZFC+SI.

(2.1) One can define a model Z of ZFC in MT. The model Z has
what one could call "the size of a class".

(2.2) One can (of course) represent formulas of ZFC by Godel numbers
in MT. For simplicity, however, it is convenient to represent formulas
by well-founded maps rather than restricting to numbers.

(2.3) On can define a "notion of truth" function f in MT such that f(x) =
true in MT iff x is the Godel number of a ZFC formula which is true in Z.

(2.4) One can prove in MT that f(x) is true or false (and, thus, not
bottom) for all well-founded x.

(2.5) One can prove in MT that f(x) is true for some formulas x
(e.g. take some axiom of ZFC) and false for some formulas y (e.g.
take the negation of some axiom).

(2.6) One can (of course) represent all proofs of ZFC by Godel
numbers in MT. For convenience, we again use well-founded
maps instead of numbers.

(2.7) One can (of course) define Bew(p,x) such that Bew(p,x) =
true iff p is a proof of x.

(2.8) One can prove in MT that Bew(p,x) is true or false for all
well-founded p and x.

(2.9) One can prove [Bew(p,x) \implies f(x)] for well-founded p
and x. (In MT this is done by induction in the length of p).

(2.10) From the above one can prove [\forall p : \neg Bew(p,y)]
in MT for some y (e.g. take y to be the negation of an axiom).
Above, \forall of MT is a universal quantifier which ranges
over all well-founded p.

That suggests (modulo the definition of "stronger than") that
MT is stronger than ZFC.

Point (1) above has been worked out in detail and published
(in my 1992 paper on MT). Point (2.1-2.10) have not been
worked out in detail. But I consider them straightforward
given the published work on (1).

But that leaves us with a question: How to compare the
strength of MT and ZFC? Or, more generally, how to
compare two arbitrary formal theories, not just theories
based on first order predicate calculus? Maybe the answer
is trivial. Maybe someone has already answered it.
Unfortunately, I have never managed to get back to
this question.

Cheers,
Klaus