The axioms of set theory can be divided into three categories :
-The "restrictive" axioms, which impose that set have certain regularity properties (extensionality, foundation).
-The "constructive" axioms, which allow one to form a uniquely defined set from older ones or from nothing (Empty set, pairing, union set, infinity, subset, replacement, power set)
-The "nonconstructive" axiom (choice).
(So for my purposes here it will be convenient to consider the infinity axiom only in the form "The set $\omega$ of all finite ordinals exists" instead of vaguer forms not defining a unique new set). One can create a mini-language of terms representing sets, associating a "constructor" to each constructive axiom : we will then have ${\bf Empty, Infinity}$ with no arguments, ${\bf Union, Power}$ with one argument, ${\bf Pair}$ with two arguments,${\bf Subset}$ with two arguments, the second of which must be a formula in one variable, and ${\bf Replacement}$ with two arguments, the second of which must be a formula in two variables.
So we have a set of seven constructors,
$C=\lbrace {\bf Empty,Infinity,Union,Power,Pair,Subset,Replacement }\rbrace$
For any subset $C’$ of $C$, one may form the language $L(C’)$ of terms formed from constructors in $C’$ only. On $L(C’)$, there is a natural membership relation coming from the interpretation of the terms. Since there are only countably many formulas, $L(C’)$ is effectively countable, so it makes sense to talk about the decidability of the membership relation on $L(C’)$.
Of course, the full language $L(C)$ will be undecidable (unless $ZFC$ is inconsistent). Now I ask : Is membership decidable when $C’=\lbrace{\bf Empty,Infinity,Pair,Union,Subset }\rbrace$ ?