[FOM] A Foundational Path via Elementary PRA constructions.

[Rex Butler]

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 
recursive
    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 
PRA
    proves x is in the image of pi_A. The image of the function  pi_A is 
Sigma_1,
    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 
as
    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 --> 
B_BASE.
    We now define partial recursive functions to be those functions of such 
form.

    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 
recursively
    axiomatizable theories such as ZFC, etc... as primitive types, 
performing
    all mathematical explorations within these theories as they are 
formalized
    in PRA.

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


Rex Butler
Graduate Student
Department of Mathematics
University of Utah