[FOM] A Foundational Path via Elementary PRA constructions

[Rex Butler]

>Since part B talks about PRA proving things about A, B, ~, and f,  these 
>four entities should presumably be primitive recursive  definitions of two 
>predicates, a relation, and a function, not simply  the predicates, 
>relation, and function themselves.
>
>Andreas Blass

Thanks for that correction.  Hopefully I was more clear on this issue in the 
short note (in pdf) I linked to, which was the main purpose of my post.  I 
intended the rest of the message only for context.  This I did, as text is 
not exactly a suitable medium for  commutative diagrams.

In the note I used set and category theoretic notations, hoping that their 
intended translations into PRA would be clear.  I also used the word 
morphism instead of function is most places.  There all constructions are 
represented by ordered tuples of PRA function symbols, subject to some PRA 
conditions.

There is another issue that needs clearing up.  I intended 'there exists' 
statements in the note (whether referenced explicitly or implicitly) to be 
interpreted as "we can construct (in  an intuitively primitive recurisve 
fashion)".

Rex Butler