[FOM] Monsieur, x^p = x (mod p), donc Dieu existe. Repondez !

[Daniel Mehkeri]

A FOM editor points out that systems without exponentiation,
and lengths of proofs in these systems, are well-known, and asks
that I relate my remarks to these. Simultaneously, less well-known
systems have been brought to my attention, along with the suggestion
that they might provide an ultrafinitary proof of Fermat's little
theorem. (Some relevant public discussion is on dialinf.wordpress.com)
There are, I'm sure, lots of ways to go about ultrafinitism. I will
write briefly about some examples, after which I will state some
general considerations.

The line between ultrafinitism and other forms of constructivism
is succinctly characterised in the passage of Troelstra and van
Dalen I originally quoted: can we, 'in principle', view a large
number as a sequence of units?

EXAMPLE 1. Q + IDelta_0.

In the language of Robinson's Q, numbers on the order of 2^2^10 can
be given as terms in a few thousand symbols. IDelta_0 is induction
for formulas with any number of bounded quantifiers.

So if P is a bounded formula, and I can prove P(0), and also that
P(n) implies P(n+1), then I can conclude P(n). This particularises
to give a deduction of P(2^2^10) of feasible size. By allowing
induction in this way, we are treating 2^2^10 as a sequence of
units.

EXAMPLE 2. Buss' Bounded Arithmetic (S_2^1).

This is the system I referred to in my original message on this
thread, and I will give some more detail here. It is also based on Q,
but here we have "binary" induction instead (the inductive step goes
from n to 2n+1 and 2n+2, rather than to n+1 in the "unary" version;
see e.g. http://www.math.ucsd.edu/~sbuss/ResearchWeb/BAthesis/). BA
allows us to express large numbers without obviously treating it as
a sequence of units, instead treating it as a binary representation.

Now consider:
   FOR ANY x,p    [[ such that x^p =/= x (mod p) ]],
   THERE EXISTS d [[ such that d is a non-trivial factor of p ]].
I put it in this form because the parts in [[ ]] are computable and
so definable in Q at most Sigma_1, meaning this is Pi_2. BA has a
metamathematical property that its Pi_2 sentences are witnessed by
computable functions having running times which are polynomial in the
lengths of their arguments. So from a proof of Fermat's little
theorem we would extract a PTIME method to factor p whenever
x^p =/= x (mod p). No such algorithm is known.

EXAMPLE 3. Sazonov's arithmetic over a finite row

Sazonov describes some related systems not based on Q. I attempt to
summarise some of them here, see e.g. "A logical approach to the
problem 'P=NP?'" http://www.csc.liv.ac.uk/~sazonov/papers.html

Here, the successor operation eventually stops at the last number,
designated by []. We have the finite row of numbers from 0 to [] to
which unary induction applies, and we have some alternate ways of
representing numbers up to 2^[] as binary strings.

The provably total functions of this system have running time
polynomial in []. Fermat's little theorem may well be provable up to
[], but if it were provable up to 2^[] then as above we would
extract a PTIME factoring algorithm.

EXAMPLE 4. Boucher's second-order arithmetic

This is in the same spirit as Sazonov's arithmetic with box, but
using second-order variables to represent the binary strings. For
details see "Arithmetic without the Successor Axiom",
http://www.andrewboucher.com/papers/

This does in fact prove Fermat's little theorem for the first-order
variables. But these are explicitly being treated as sequences of
units. It may also be provable for the second-order variables. But
without suitable restrictions on induction and comprehension, some
unary induction seems to become derivable for the second-order
variables as well, so they are also being treated as sequences of
units.

END OF EXAMPLES.

Now to the general considerations here. I repeat the sentence from
the discussion of BA:
   FOR ANY x,p    [[ such that x^p =/= x (mod p) ]],
   THERE EXISTS d [[ such that d is a non-trivial factor of p ]].
the parts in [[ ]] are efficiently testable by modern computers,
for binary representations on the order of 2^2^10, and in fact
somewhat larger. In particular, for the RSA-2048 challenge number
that I quoted originally, 2^p =/= 2 (mod p).

To the constructivist or intuitionist there is no problem: there are
indeed algorithms to factor p. They are not practical, but given
enough time and space, they would work.

"Given enough time and space" is of course not an excuse available
to the ultrafinitist. An infeasible computation does not count as a
proof of anything: "really" it doesn't terminate at all, since the
running time is a large number, and cannot be viewed as a sequence
of units.

I do realise that PTIME is only asymptotic feasibility. I realise
we can't PROVE there are no good algorithms for factoring. I realise
that there are many other variations on ultrafinitary systems
besides these that I haven't explicitly covered. But, modern
computers can easily do modular exponentiation with quite large
numbers, while factoring numbers of this size is so far not feasible
in ANY sense, not even probabilistically. So we do seem to have a
quite general obstacle here.

At least, I hope the FOM editors and readers are now satisfied that I
do not need to pre-emptively address further proposals. Maybe instead
this will provoke the ultrafinitists, or those wishing to argue on
their behalf, to prove Fermat's little theorem, up to at least the
relevantly sized numbers, and argue that their assumptions do not
treat numbers of this size as sequences of units, despite the above
considerations. Or maybe it will prove them to argue against this
characterisation of ultrafinitism. Or maybe to provide an
ultrafinitary alternative to Fermat's little theorem that suffices
for modern cryptography.


Daniel Mehkeri
--