[FOM] Constructivism and physics; Absolute truth vs. relative meaning
joeshipman@aol.com
joeshipman at aol.com
Fri Feb 10 09:27:24 EST 2006
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
More information about the FOM
mailing list