FOM: conservative extensions

[Stephen G Simpson]

Robert Tragesser writes:
 > The notion "conservative extension" has acquired the reality of
 > centrality and powerful significance in logical investigations in
 > the foundations of mathematics.

I wouldn't phrase it in exactly this way, but yes, I agree.  The
notion of conservative extension does seem to pop up a lot in f.o.m.,
and for very good reasons.

First, the definition: If T and T' are formal systems and T' is an
extension of T, we say that T' is conservative over T for a class of
sentences S if every S-sentence provable in T' is already provable in
T.  In the special case where S is the class of *all* sentences in the
language of T, we say simply that T' is conservative over T.

This notion ought to be part of everyone's training in f.o.m.  It can
be used to state a great many logical results which are of
f.o.m. significance.  You can get an idea of the scope by searching
through the FOM archive for "conservative".  Here are some favorite
conservative extension results:

  RCA_0 is conservative over PRA for Pi^0_2 sentences.
  
  WKL_0 is conservative over RCA_0 for Pi^1_1 sentences.
  
  ACA_0 is conservative over PA.
  
  Sigma^1_1-AC_0 is conservative over ACA_0 for Pi^1_2 sentences.

  ATR_0 is conservative over IR for Pi^1_1 sentences.
  
  Sigma^1_2-DC_0 is conservative over Pi^1_1-CA_0 for Pi^1_3 sentences.
  
  ZFC + V=L is conserative over ZF for Pi^1_2 sentences.
  
  ZFC + GCH (actually ZFC + V=L(r) for some real r) is conservative over
  ZF for Pi^1_3 sentences.
  
  ZFC + GCH is conservative over ZFC (actually over ZF + a well ordering
  of the reals) for Pi^2_1 sentences.
  
  VNBG set-class theory is conservative over ZF set theory.
  
  VNBG plus global choice is conservative over ZFC.

Tragesser continues:
 > Could someone explain/expose something of the history and more
 > particularly something approaching the full sheaf of various
 > "implications" of this "property" [as a foundational concept]?

Let me take a stab at it.  I think the key word here is
"instrumentalism".  (I heard this word recently from Alexander
Ignjatovic.)

If we show that T' is conservative over T for S-sentences, then that
result can be interpreted as saying that the primitives and/or axioms
that are present in T' but not in T can be "eliminated" or, viewing it
the other way round, these primitives and/or axioms can be "harmlessly
introduced" on top of T, i.e. they can be viewed as mere instruments
which we introduce artificially in order to make it easier or more
convenient for us to prove S-sentences, without increasing our
ontological commitments beyond what is already in T.

As an example, consider Hilbert's program.  We can state Hilbert's
program in modern terms as follows: to show that ZFC is conservative
over PRA for Pi^0_1 sentences.  In other words, to show that the
transfinite machinery of higher set theory is only a superstructure
that we erect for our own convenience; to show that all of the
concrete, universal, number-theoretic statements that are provable
with the aid of such machinery could have been proved finitistically,
without such machinery.

This turns out to be false, but that's far from the end of the story
with respect to finitistic reductionism.  See my paper on partial
realizations of Hilbert's program, on-line at
http://www.math.psu.edu/simpson/papers/hilbert/.

-- Steve