[FOM] A Foundational Path via Elementary PRA constructions.

Rex Butler rexbutler at hotmail.com
Mon May 1 12:14:00 EDT 2006

I wrote the note linked below specifically for posting on FOM email list.
Please pardon any naivete, etc.  I must admit a fascination with PRA and its
constructions, though I have little formal training in the foundations of
mathematics.  Comments?

See:  http://www.math.utah.edu/~rbutler/PRA/PRA.pdf

Here is a sketch of the preliminary idea:

A Foundational Path:

1.  Using natural language, define primitive recursive arithmetic (PRA).

2.  A. Define a primitive to be a pair (A,~) where A is a primitive 
    predicate and ~ is a primitive recursive equivalence relation.

    B. Define a function between two primitives (A,~) and (B,~) to be a
    primitive recursive function f: N --> N such that PRA proves

        If x in A then f(x) in B and
        If x,y in A and x ~ y  then  f(x) ~ f(y).

    With these statement proved, we write f: (A,~) --> (B,~), etc...
    Equality of functions will be as provable in PRA.

    [Here we use Godel coding as a method of construction rather than merely
    as a method of representation.]

3.  Introduce computability and enumerability as follows:

    A.  Define an primitive type A = A_THM to be a function
    pi_A : A_PROOF --> A_PROP. between primitives.  We write x in A_THM if 
    proves x is in the image of pi_A. The image of the function  pi_A is 
    and we now define Sigma_1 sets to be sets of such form.  Thinking
    foundationally, we may consider such primitive types as elementary
    protological systems.  For example, we may present any recursively
    axiomatizable theory (such as PRA itself) in this form.  Thinking
    geometrically, we may visualize pi_A as a projection and rename A_PROOF 
    A_COVER and A_PROP as A_BASE, as we do below:

    B.  Define a function between primitive types A and B to be a function
    f_COVER: A_COVER --> B_COVER between their enumerating primitives such
    that PRA proves

        For x,y in A_COVER,
            pi_A(x) ~ pi_A(y) in A_BASE implies
            pi_B(f(x)) ~ pi_B(f(y)) in B_BASE

    This induces a effectively computable (partial) function f: A_BASE --> 
    We now define partial recursive functions to be those functions of such 

    We now have a Brouwer-Heyting-Kolomogorov semantics of some sort, a
    proposition being a pair (a,A) where A = (A_COVER,pi_A,A_BASE) is a
    primitive type and a is an element of A_BASE.  A proposition (a,A) is
    'true' if PRA proves pi_A(q) = a for some explicit q in A_COVER.

    C.  Extend the construction by allowing both the image of pi_A and
    the equality defined thereon to be Sigma_1 by providing explicit
    presentations by primitive recursive parameterization.

4.  Within PRA and via the use of these constructions, proceed with
    foundational studies as usual or according to preference.  Present 
    axiomatizable theories such as ZFC, etc... as primitive types, 
    all mathematical explorations within these theories as they are 
    in PRA.

    Intuitively, we consider further foundational theories by 'descent' 
    PRA instead of 'ascent' out of PRA.  Thus PRA and it's constructions are
    viewed as the elemental foundational system of mathematics, the language 
    constructive mathematics within which nonconstructive mathematical
    systems are defined.

Rex Butler
Graduate Student
Department of Mathematics
University of Utah

More information about the FOM mailing list