Decidability of equality of two set-theoretical terms constructed without replacement or specification Define the set of NS-terms (NS is for "no schemes") to be the smallest
set of terms satisfying the following rules :


*

*$\emptyset,\omega$ are NS-terms.

*if $x$ and $y$ are NS-terms, then so are 
$x\cup y, x\cap y, x\setminus y,\lbrace x,y\rbrace,\bigcup(x),\bigcap(x)$
and ${\cal P}(x)$.


Thus the NS-terms are the terms that can be constructed using all axioms
of ZFC except replacement and specification (the "schemes").
Perhaps those terms already have a name in the literature ?
I have two closely related questions about this set $T$ of NS-terms.
Question 1. For $t,t' \in T$, is it always true that either ZFC proves $t=t'$ or ZFC proves $t\neq t'$ ?
Question 2. Let $f: T^2 \to \lbrace true,false \rbrace$ be the map
defined as follows : $f(t,t')$ is true iff ZFC proves $t=t'$. Is $f$
computable ?
EDIT : since there are several variants used for the axiom of infinity, I explain which one I use here. I define $\omega$ to be the "set of all integers", where (as is standard) a set $x$ is an integer iff it is an ordinal all of whose elements are successor ordinals or zero(=the empty set). Then my axiom of infinity states that $\omega$ exists (it is necessarily unique by extensionality).
EDIT 07/27 : as user nombre noted, there is a definition problem with the value to assign to $\bigcap(\emptyset)$. Let us decide that $\bigcap(\emptyset)=\emptyset$, which is as good a convention as any other (and probably does not change the answer to the question ; solvers are welcome to attribute another value to $\bigcap(\emptyset)$ if it leads to a solution).
 A: This is not an answer but a clarification of a few points, I can delete it tomorrow if you like:
First, let's say that NS-terms are words, more precisely:
$V_0$ is the set of words $\{\varnothing;\omega\}$. $\forall n \in \mathbb{N}, V_{n+1} = \{x;\bigcup (x); \bigcap (x); \mathcal{P}(x); \{x;y\};x - y; x \cup y; x \cap y \ | \ x,y \in V_n\}$, and the set of all NS-terms is $V_{\omega_0} = \bigcup \limits_{n \in \mathbb{N}} V_n$.
Since $ZFC \vdash \forall x,y(x \cup y = \bigcup (\{x;y\}) \wedge x \cap y = \bigcap (\{x;y\}))$, the symbols $\cup$ and $\cap$ can be disregarded.
NS-terms are all defininable in a natural way:
Just set $F_{\varnothing}[x]$ as $"\forall y(y  \notin x)"$, and $F_{\omega}$ as "$x$ is the set of finite ordinals". Then for instance, $F_{\{t;t'\}}[x]$ is $"\forall y(y \in x \longleftrightarrow F_t[y] \vee F_{t'}[y])"$. The special case is $F_{\bigcap (t)}[x]$ because we want to avoid the terms interpreted by proper classes. But we can fix this by setting $F_{\bigcap (t)}[x]= "t$ and $x$ are empty or $\forall y(y \in x \longleftrightarrow \forall z,w((F_t[w] \wedge z \in w) \rightarrow y \in z)))$".
Then if $t,t'$ are NS-terms the statement $"t = t'"$ is an abreviation for $\forall x(F_t[x] \longleftrightarrow F_{t'}[x])$.
(it is wuite crucial to agree on the formulas $F_t[x]$ before thinking about the problems)

All this is just to specify the context. As for the question 1, I haven't found a way to answer it.
I think a suitable first step would be proving by induction that if $\mathcal{M}$ is a model of ZFC,  $t$ is a NS-term, and $n$ is the least integer such that $t \in V_n$, then:
$\mathcal{M} \vDash t = \varnothing$ iff $\forall t' \in V_{\max(0,n-1)}, \mathcal{M} \vDash (t' \notin t)$.
But I didn't get near to doing that. Though it seems to be a good induction hypothesis at some points, it doesn't seem to be enough at others.
