[FOM] syntactic power

[Harvey Friedman]

We start with a carefully formulated standard formal language LST for
set theory.

Let S,T be two set theories. We say that S ># T if and only if

the shortest sentence not decided in S is longer than the shortest
sentence not decided in T.

How does ># come out with various important pairs of set theories S and T? E.g,

ZFC + CH ># ZFC + notCH?
ZFC + nonCH ># ZFC + CH?

Or maybe first address

ZFC + CH ># ZFC?
ZFC ># ZF?
ZFC + V = L ># ZFC?

How much does this depend on the exact choice of LST, assuming that it
is not in any way rigged?

Ask the same questions within the language of second order arithmetic.

Maybe less interesting is to ask this for the language of arithmetic,
but perhaps still interesting? Maybe more interesting in fragments of
real closed fields or axiomatic geometry?

Harvey Friedman