We exhibit canonical middle-inverse Choice maps within categorical
(Free-Variable) Theory of Primitive Recursion as well as in Theory of partial
PR maps over the Theory of Primitive Recursion with predicate abstraction.
Using these choice-maps, defined by mu-recursion, we address the Consistency
problem for a minimal Quantified extension Q of latter two theories: We prove,
that Q's exists-defined mu-operator coincides on PR predicates with that
inherited from theory of partial PR maps.
We exhibit canonical middle-inverse Choice maps within categorical
(Free-Variable) Theory of Primitive Recursion as well as in Theory of partial
PR maps over the Theory of Primitive Recursion with predicate abstraction.
Using these choice-maps, defined by mu-recursion, we address the Consistency
problem for a minimal Quantified extension Q of latter two theories: We prove,
that Q's exists-defined mu-operator coincides on PR predicates with that
inherited from theory of partial PR maps.