Axiom of Strong Negation of Undefinable Choice

The questions on this topic have been first exposed in: Overleaf: Axiom of Strong Negation of Undefinable Choice.

$ZF⊢Finite$ $Choice$

In this section I resemble the proof of Finite Choice from the axioms of $ZF$ by following the Discussion.

Here I recap Andreas Blass’s answer: We are given the existential statement, “There is an element in $x$.” What should be noticed in addition is that what we want to prove is also an existential statement, “There is a choice function.” We have an explicit construction, which I’ll call $C$, that will convert any element of $x$ into a choice function, namely sending any $y$ to $\{(x,y)\}$. If we can’t explicitly define any particular $y$, then we won’t be able to define any particular choice function either, but the problem doesn’t require us to explicitly define a choice function; we need only prove that one exists. And that follows, thanks to $C$, from the existence of elements in $x$.

Then, I shall distinguish two axioms: Axiom of Finite Choice ($AFC$) and Axiom of Finite Definable Choice ($AFDC$), and from the answer above I note $ZF⊢AFC$. Now, meanwhile $AFC$ can clearly be written within the object language ${\mathcal{L}}_{ϵ}$, it might not be the case with $AFDC$, in fact this axiom should entail the predicate “being ${\mathcal{L}}_{ϵ}$-definable” which cannot clearly be written in the same language since it depends on it.

Question: Is there a way to express $AFDC$ in ${\mathcal{L}}_{ϵ}$? A candidate but possibly way to complex method would be to change the logic behind the existential quantifier "${\exists }_x\phi (x)$" might be true only if you can present an $x$ s.t. $\phi (x)$, this would be a more radical version of intuitionistic mathematics (here I mean the one excluding $AC$ and not necessarily $A\vee \neg A$). In fact one would, in such a logic, not admit any proof of existence that cannot present a definable example, this can clearly be stated in the semantical definition of the quantifiers of a classical (or intuitionistic, in the sense that rejects $A\vee \neg A$) logic.

Otherwise, one might simply add a predicate $\delta$ to ${\mathcal{L}}_{ϵ}$, call it ${\mathcal{L}}_{ϵ,\delta }$, s.t. $\delta (x)$ iff. there is a formula $\phi \in {\mathcal{L}}_{ϵ}$ s.t. ${\forall }_y\phi (y)\leftrightarrow \phi (x)$. Since there is an existential on formulae, this is a metalinguistic definition, which is not a problem since all syntax is traditionally defined metalinguistically (i.e. $a\wedge b$ iff $a$ and $b$). Note that the definition of $\delta$ is not recursive because it runs over formulae in the language without $\delta$ itself.

In ${\mathcal{L}}_{ϵ,\delta }$ we can write $AFDC$ and consider both $ZF+AFDC$ and $ZF+\neg AFDC$ which will both probably be consistent, since $ZF$ is written in ${\mathcal{L}}_{ϵ}$ only. One might proceed by adding axioms to $ZF$ s.t. they result consistent with $SNUC$ as expressed in the $\text{LATEX}$ file above.

Question: Could we have an axiom $X$ in ${\mathcal{L}}_{ϵ,\delta }$ s.t. $ZF+X⊢ADC$, i.e. the Axiom of Definable Choice? Is $X$ needed? That is an axiom that allows to pick definable elements. Perhaps this axiom might not even be needed if we are in ${\mathcal{L}}_{ϵ,\delta }$.

Question: Can we finally prove $con(ZF) \Rightarrow con(ZF + AFDC)