No es obvio que la mayoría de los axiomas de ZFC son constructivas en este sentido, por ejemplo, la sustitución del esquema tiene muchas oraciones que involucran $\phi$ con los no-constructiva cuantificadores existenciales. La única axiomas que parecen obvias intervenciones constructivas son de emparejamiento y extensionality. Aún así, creo que es plausible que ZFC+V=L puede ser axiomatized utilizando sólo constructivo frases. Voy a esbozar un enfoque posible:
Empezar con extensionality y el emparejamiento. Definir $``x \neq \emptyset"$ $\exists! b \forall a(a \not \in b \wedge b \neq x)$ (tomado de Dap de la respuesta).
Definir $x \not \subset y$ $\exists! z(\forall a (a \in z \leftrightarrow (a \in x \wedge a \not \in y))\wedge z \neq \emptyset).$
Definir $\alpha \in Ord$ $\forall \beta \in \alpha (\forall \gamma \in \beta (\gamma \in \alpha)) \wedge \forall S(S \not \subset \alpha \vee S=\emptyset \vee \exists!\beta \in S(\forall \gamma \in S(\beta = \gamma \vee \beta \in \gamma))).$
Creo que la base de la teoría de los números ordinales (y funciones) debe ser constructiva axiomatizable. Debemos ser capaces de estado $V=L$ usando el auxiliar Jensen jerarquía de $S_{\alpha}$ (que es bastante complicado de definir, ver Schindler del libro de texto). En particular, debemos ser capaces de definir de manera constructiva en la idea de un "$S$-secuencia", es decir, un transfinito de la secuencia de la forma $\langle (S_{\alpha}, <_{\alpha}): \alpha<\beta \rangle,$ donde $<_{\alpha}$ es la canónica bien de la orden en cada una de las $S_{\alpha}.$ necesitamos para construir el bien de orden, simultáneamente, debido a que la definición de los sucesivos $S_{\alpha}$'s utiliza la noción de unión, y creo que debemos usar el bien-el fin de definir de manera constructiva la unión de un conjunto.
Ahora podemos decir $V=L$ como la afirmación de que para cada una de las $x,$ hay un único, $S$- secuencia cuyo final $S_{\alpha}$ es el primero que ha $x$ como un elemento. Ahora podemos de manera constructiva del estado de los otros axiomas de ZFC señalando $\exists \phi(x)$ es equivalente a que exista un único $<_L$-mínimo $x$ satisfacción $\phi.$
Addendum: he Aquí una posible contraejemplo a la sugerencia de que una teoría de decidir todas las constructivas frases es necesariamente completa. Definir un poset $(P,<)=(\mathbb{Z} \cup \{\infty, \infty'\},<),$ donde $<|_{\mathbb{Z}}$ es el estándar de orden y $\infty$ $\infty'$ son ambos máximo de elementos.
Considere dos modelos en el lenguaje de un solo predicado binario $<,$ es decir $(M_1,<), (M_2,<),$ donde $M_1=\mathbb{N} \times P$ $M_2=M_1 \cup (\{-1\} \times \mathbb{Z}).$ En cada uno, se definen $(a,b)<(c,d)$ fib $a=c$ $b<d.$ tengo la fuerte sospecha de $(M_1,<)$ $(M_2,<)$ tienen el mismo constructivo verdades, pero claramente no son de primaria equivalente.
