[FOM] A Foundational Path via Elementary PRA constructions

Rex Butler rexbutler at hotmail.com
Thu May 4 15:51:55 EDT 2006

>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 

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 

Rex Butler

More information about the FOM mailing list