5
$\begingroup$

Starting with $\sf Z$ minus Separation, add to its language a primitive constant $0$ standing for the empty set, and primitive total $(n+1)$-ary functions $f^n_i$ where $i$ is a natural, now let $\varphi_0, \varphi_1, \cdots$ be an enumeration on formulas whose free variables are all and only $(x,y,w_0,..,w_n)$. Add the following axiom schemata (parameters hidden):

Attribution: $[\forall x \exists y : \varphi_i(x,y)] \to \forall x \forall y \, (f_i(x)=y \to \varphi_i(x,y)) \\ [\neg \forall x \exists y: \varphi_i(x,y)] \to \forall x \, (f_i(x) = 0 )$

Now, we come to our scheme:

Functionality: $i=0,1,2, \ldots\\ \forall A \, \exists B: \forall y \, (y \in B \leftrightarrow \exists x \in A: y=f_i(x))$

I'd label this theory as: $\sf Z + Functionality$.

Now, Z + Functionality is ought to prove schemata of Separation and Replacement. Also, Axiom of Choice follows. So, it is at least $\sf ZFC$.

Is the above theory interpretable by $\sf ZFC$?

Improve this question
$\endgroup$
5
  • 1
    $\begingroup$ Your attribution axiom is basically Skolemization, and in ZFC+V=L you have definable Skolem functions. If the $f_i$ are definable, functionality is equivalent to replacement. So this should be interpretable in ZFC+V=L, hence also ZF(C). $\endgroup$ Commented Apr 3 at 13:33
  • $\begingroup$ @Wojowu, the $f_i$s' are not necessarily definable, that's why choice holds. We are primitively extending ZFC by those primitive functions, would that add any strength? $\endgroup$ Commented Apr 3 at 13:43
  • 1
    $\begingroup$ @ZuhairAl-Johar Assuming V=L, there are definable functions satisfying these conditions because there's a definable global well-ordering. $\endgroup$ Commented Apr 3 at 15:23
  • 2
    $\begingroup$ @ZuhairAl-Johar I'm saying that under ZFC+V=L there is a choice of Skolem functions which is definable. For interpretation we only need some choice of Skolem functions, and them being definable makes functionality follows from replacement. $\endgroup$ Commented Apr 3 at 15:44
  • $\begingroup$ @Wojowu, Ah! I see. So, ZFC interprets that. I think this ought to be written as an answer. $\endgroup$ Commented Apr 3 at 16:56

1 Answer 1

Reset to default
5
$\begingroup$

Your attribution property basically means that $f^n_i$ are Skolem functions. By interpreting a theory which has definable Skolem functions, replacement will give us your functionality axiom schema for free.

One such theory is ZFC together with axiom of constructibility $V=L$. The key is that $L$ admits a canonical definable well-ordering $<_L$, so we can define $f_i^n(x)$ as the $<_L$-least element $y$ satisfying $\varphi_i(x,y)$ if one exists, or $0$, depending on if $\varphi_i$ is total.

Since ZFC interprets ZFC+$V=L$, by passing to $L$, your theory is interpretable too.

Improve this answer
$\endgroup$

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.