[FOM] MK |- CON(ZF) ?

[Richard Heck]

On 05/16/2016 12:09 PM, Chris Scambler wrote:
> Thanks for this; I wonder if you could hint at the way in which Pi_1^1
> comprehension is used here? I had thought one could make do with
> Sigma_1^1 separation for sets (one needs to prove the existence of the
> set of natural numbers n for which there is a satisfaction class for
> each Sigma_n formula, which features a second-order existential
> quantifier), but perhaps I'm wrong or missing something.

The sort of construction you describe is "bottom up", and it seems to
correspond in some ways to what's described in the blog post to which
the original question linked. For all I know, principles other than
\Pi^1_1 comprehension can be used here.

Tarski's construction, in any event, is "top down". Basically, what
Tarski does is to describe what we would now call an axiomatic theory of
satisfaction (and so of truth), but he thinks of it as a recursive
*definition* of satisfaction (much confusion has been caused by this),
and he then uses the usual techniques (due to Dedekind and Frege) for
converting a recursive definition into an explicit one.

For the benefit of anyone not familar with those techniques, consider
the following simple example. The recursion equations for addition are:

(i) a + 0 = a
(ii) a + Sb = S(a + b)

We can think of these as constituting a recursive definition of
addition. But we can also use them to produce an explicit definition of
the relation "z = x + y". Say that a relation R is "additive" if
satisfies the following two conditions:

(i') for all x: R(x,0,x)
(ii') If R(x,y,z), then R(x,Sy,Sz)

Now define:

Sum(x,y,z) iff, for all R, if R is additive, then R(x,y,z)

Note that this formula is is \Pi_1^1. (It amounts to taking the
intersection of all the additive relations.) One can easily show that
Sum is itself additive, i.e., it satisfies the recursion equations. That
proof does not actually need comprehension. But if you want to show,
e.g., that Sum is total (unique, etc), then you need \Pi_1^1
comprehension. This is because you need to run an induction on something
like:

    For some z, Sum(x,y,z)

and the definition of Sum is \Pi_1^1.

In the case of satisfaction, in place of (i) and (ii) we have things like:

Sat(*A & B*, s) iff Sat(*A*, s) & Sat(*B*, s)

But the same method works and yields an explicit \Pi_1^1 definition of
Sat. And, as with addition, *the recovery of the recursive clauses* (the
"Tarski commutation conditions") does not need \Pi_1^1 comprehension.
The definition of satisfaction can be given in a purely predicative
theory, such as ACA_0 or GB, and the Tarski clauses proven in such
theories. (There is much work by Albert Visser exploring the general
case here. See e.g. "The Predicative Frege Hierarchy" and "Can We Make
the Second Incompleteness Theorem Co-ordinate Free?")

It's for the proof of consistency that we need \Pi_1^1 comprehension.
This is because we need to run an inductive proof on something like:

If x is (the Goedel number of a) proof, then the universal closure of
the last line of x is true

And this will be \Pi_1^1, since the definition of truth is \Pi_1^1.

Richard

PS Note that I am talking about all of this from a broadly axiomatic
point of view, i.e., as concerning what can be done in certain formal
theories. There are also ways of talking about it from a more
model-theoretic point of view, but that is not something I know a lot about.


-- 

-----------------------
Richard G Heck Jr
Professor of Philosophy
Brown University

Website:   http://rgheck.frege.org/
Blog:      http://rgheck.blogspot.com/
Amazon:    http://amazon.com/author/richardgheckjr
Google+:   https://plus.google.com/108873188908195388170

Check out my books "Reading Frege's Grundgesetze"
  http://tinyurl.com/ReadingFregesGrundgesetze
and "Frege's Theorem":
  http://tinyurl.com/FregesTheorem
or my Amazon author page:
  amazon.com/author/richardgheckjr

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160516/c5e97fa3/attachment-0001.html>