[FOM] A Foundational Path via Elementary PRA constructions
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.
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
More information about the FOM