[FOM] Constructivism and physics; Absolute truth vs. relative meaning

[joeshipman@aol.com]

Friedman's and Sazonov's posts are remarkably thought-provoking.

Friedman says:

11. Let me be more specific. I do not know of a single interesting 
theorem
of mathematics that is proved without extensive use of abbreviation 
power.

12. So if you start with a theory T with the usual very spartan 
primitives
common in f.o.m., and you wish to prove theorem A, which lives in the
language of T, you have a problem right away. We can expect all existing
mathematical proofs of A to be riddled with abbreviations that go well
beyond the language of T. Furthermore most commonly, even to *state* A, 
we
require in practice that we immediately expand the language of T. This
compounds the problem of seriously talking about cut free proofs in T.

Sazonov gives a concrete example of a formal system where the theorem 
"FALSE" (that is, an inconsistency) has no feasible proof in  a system 
which excludes the "cut rule", but has a short proof using cuts.


I would like to see much more exploration of the phenomenon of 
abbreviations and new proof techniques shortening the proofs of real 
theorems.  One good place to start might be the following:

I recently found a straightforwardly computable necessary and 
sufficient condition for implications between "degree axioms" in field 
theory to be true in all fields.  Let [n] denote the sentence "all 
polynomials of degree n have a root". This is straightforwardly 
expressible in the language of field theory, by a sentence whose size 
is linear in n (assuming all variables are assigned unit size; if we 
insist on measuring sentence length in terms of characters in a finite 
alphabet, then ANY sentence involving a linear number of variables must 
be have "size" at least O(n log n), but this has no relation to the 
number of steps necessary in a proof).

For example, the sentence [4] is expressed in the first order language 
of fields as follows:

Forall x0 Forall x1 Forall x2 Forall x3 Thereexists x4 
(x0+(x4*(x1+(x4*(x2+(x4*(x3+x4)))))) = 0)

The work of Cardano and Ferrari in the 16th century showed, in effect, 
that the implication ([2]&[3])-->[4] was true in all fields. In 
particular, if AF denotes the conjunction of the first-order axioms for 
fields, then (AF&[2]&[3])-->[4] is a logical tautology.

What I proved is that (AF&[i1]&[i2]&...&[i_m])-->[n] is a logical 
tautology (and therefore provable in pure first-order logic) iff the 
following condition holds:

For every subgroup G of Sn which acts without fixed points on 
{1,2,?,n}, the additive semigroup generated by the indexes in G of its 
proper subgroups contains one of the i?s.

The subgroups of the symmetric group S4 which act without fixed points 
on {1,2,3,4} are  S4, the alternating group A4, various dihedral groups 
D4, various cyclic groups C4, and various Klein Four groups K. These 
have subgroups of index 2,3,2,2, and 2 respectively, so the condition 
holds for i1=2, i2=3, n=4.

For n>4, the alternating group An has no proper subgroups of index <n, 
which means that any implication between degree axioms with n on the 
right-hand side must have one of the i's on the left-hand-side be >=n.

What is interesting to me is that any one of these finite implications 
between degree axioms could have been discovered at any time in the 
last couple of centuries, by completely elementary reasoning involving 
only the first-order language of fields. But how long would the proofs 
have to be?

For example, one can demonstrate the sentence

([2]&[15])-->[6]

by specializing to the case m=6 one of Gauss's proofs of the 
fundamental theorem of algebra, which reduced the case of polynomials 
of degree m = (2^k)*r, for r odd, to the case of polynomials of degree 
r(r-1)/2, which has one fewer power of 2, with the base case handled by 
the fact from analysis that odd-degree real polynomials have roots.

But does this really translate into the first-order language of fields 
in a feasible way, in the general case? It seems possible, given the 
size of permutation groups of degree n and the number of different such 
groups that must be considered, that any first-order proof must have 
size exponential in n (which would, of course, be double-exponential in 
the amount of space it takes to state the  implication in the notation 
I used above).

On the other hand, in ZFC, and using results from the theory of 
permutation groups and the Classification of Finite Simple Groups, it 
appears that one can define an algorithm to identify valid "degree 
implications" whose running time is affected most severely by the 
difficulty of factoring integers, and which is sublinear in the length 
of the corresponding first-order tautologies.

-- JS