FOM: NYC panel discussion/Separating Conjectures

[Harvey Friedman]

Simpson 10:55PM 12/26/99 wrote:

>Harvey Friedman focused his opening remarks on a provocative,
>long-range conjecture that he has recently formulated.  The thrust of
>the conjecture is that we are going to discover a completely
>coding-free and base-theory-free way of calibrating the strength of
>mathematical statements and groups of statements.  I know that this
>summary does not do justice to Harvey's vision, so I call on Harvey to
>elaborate here on FOM.

Actually, this has little to do with my opening remarks, although it was
indeed about
"a provocative, long-range conjecture that he [Friedman] has recently
formulated. "

I have reworked these conjectures and plan to discuss them in more detail
in my numbered postings, but I will give some versions of them here.

1. S_1 is the set of formulas in first order predicate calculus with
equality where the universal closure is satisfiable.

2. S_2 is the set of all schemes in first order predicate calculus with
equality where the set of universal closures of the substitution instances
is satisfiable.

3. S_3 is the set of all quantifier free formulas in first order predicate
calculus with equality where the universal closure is satisfiable.

4. S_4 is the set of all finitely axiomatized equational theories with a
model with more than one element.

Let | | count the number of symbols except commas and parentheses in any
formula in first order predicate calculus with equality or scheme in first
order predicate calculus with equality or in any finite set of formulas in
first order predicate caluclus with equality. Symbols to be counted include
connectives, constant, relation, function symbols, forall, therexists,
variables, =.

Note that in each case, for any n >= 1, there are finitely many x in S with
|x| <= n up to a meaning preserving  change of variables.

It is obvious that for any consistent r.e. theory T, there exists x in S
such that T does not prove x in S.

We write #(S_i,T) for the greatest n such that for all x in S_i, if |x| <=
n then T proves "x in S_i."

Let T_1 - T_9 be the theories PA, Z_2, ZC, ZFC, ZFC + weakly compact
cardinal, ZFC + measurable cardinal, ZFC + supercompact cardinal, ZFC +
rank into rank, ZF + V into V.

FIRST CONJECTURE i,j. #(S_i,T_j) < #(S_i,T_j+1).

SECOND CONJECTURE i,j. There exists x in S_i, |x| = #(S_i,T_j)+1, where
RCA_0 proves "x in S_i if and only if Con(T_j)."

THIRD CONJECTURE i,j. Let |x| <= #(S_i,T_j). Then "x in S" or "x notin S"
has a proof in T_j with at most
1,000,000 symbols (with abbreviations allowed).

The first amounts to 32 conjectures. The second and third amount to 36
conjectures each.

I call these Separating Conjectures because they concern the separation of
9 important levels of the logical universe.