[FOM] Finite Analogues of Infinite Structures

[Dmytro Taranovsky]

Every model of arithmetic or set theory is infinite.  However, there is
a sense in which finite structures can satisfy PA or ZFC.

In these quasi-models, not every statement in the language is
meaningful, but every feasible statement is meaningful.  In the model,
every formula with parameters that fill in all free variables--
henceforth called statement--is either true or false or meaningless.
Propositional connectives retain their meaning, and produce meaningful
statements when applied to meaningful statements.  The universal
quantifier is expressed through the existential one, and the existential
quantifier is interpreted as follows:  If (En) phi(n) is meaningful,
then it is true iff there is n such that phi(n).  A partial model
satisfies an axiom schema if it satisfies all meaningful axioms in the
schema.

A particularly canonical specification of meaningfulness is the
following.  The universe consists of natural numbers less than a
particular large integer N.  Predicates in the language are meaningful
(when applied objects in the universe), and functions are treated
through predicates.  Fix a canonical coding phi --> |phi| of statements
by positive integers.  (En) phi(n) is meaningful iff for every m < |(En)
phi(n)|, phi(m) is meaningful.  If meaningful, (En) phi(n) is true iff
there is m < |(En) phi(n)| such that phi(m) iff there is m such that
phi(m) (coherence condition). By the coherence condition, truth values
of meaningful statements can be computed without encountering parameters
out of range of the universe.

Thus, the truth values of feasible statements do not depend on which
statements are meaningful.  A statement m bits long and with quantifier
nesting depth n is meaningful iff roughly 2^(m*2^n) < N.  It is possible
to eliminate the second exponent at the price of arbitrariness in the
definition of meaningfulness, and of independence of truth-values of
meaningful statements from the notion of meaningfulness.  

It is possible to increase the closure properties for the set of
meaningful statements, but some integers in the model do not have a
successor in the model, and (En) phi(n) cannot be meaningfully false
unless phi(m) is meaningful for sufficiently many m.


Given a model of a theory, we can construct a finite quasi-submodel as
follows:  For each n<N, if n+1 = |(Em) phi(m)|, and the model satisfies
(Em) phi(m), but no previously added element satisfies phi, then add x
satisfying phi(x) and assign x to n.  

If a theory has a quasi-model, then it has no inconsistency proof using
only statements that are meaningful in the quasi-model.  Conversely, if
M is sufficiently large relative to N and a theory has no inconsistency
proof shorter than M, then it has a quasi-model of size at least N or a
model of size less than N.

Thus, formal reasoning about set theory can be translated as reasoning
about a finite object--a member of the ninth level, V(9), of the
cumulative hierarchy--that is a quasi-model of true set theory.  Some
statements are not well-defined in the quasi-model, but that should
cause no obstacles since statements longer than, say, 2^65536 bits will
not be used in proofs for the foreseeable future.

Dmytro Taranovsky
http://web.mit.edu/dmytro/www/main.htm