[Date Index] [Thread Index] [FOM Postings] [FOM Home]

*To*: fom@math.psu.edu*Subject*: FOM: NYC panel discussion/Separating Conjectures*From*: Harvey Friedman <friedman@math.ohio-state.edu>*Date*: Tue, 28 Dec 1999 12:11:14 -0500*Sender*: owner-fom@math.psu.edu

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.

[Date Prev] [Date Next] [Thread Prev] [Thread Next]

[Date Index] [Thread Index] [FOM Postings] [FOM Home]