Does there exist a set theory Twhich has not yet been proved to be inconsistentand in which one can prove the existence of (1) the empty set (2) sets that are singletons and (3) sets which have nonempty proper subsets. T has no axiom of infinity butas with Quine's NFone can prove in T the existence of a universal set (i.e a set of all sets). Howeverunlike Quine's NFthe universal set of T should be finite. One can think of T as being formalized in the classical first order predicate calculus, using the same language as ZF. My motive in seeking a set theory such as T is to find out whether there exist set theories that might be acceptable to an ultrafinitist (as conforming to the principles of that viewpoint), while still allowing a certain amount of arithmetic to be carried out in them.

Perhaps I have misunderstood your requirements, but it seems that the following trivial theory has all your desired properties. Namely, let $T$ be the theory asserting
This theory is clearly consistent, since we can write down a finite model, with three elements. In fact, this is the only model of $T$. But meanwhile, it has all your properties, since it asserts that $E$ is empty and that $P$ is a singleton and that $V$ has a nonempty proper subset, namely, $P$. Finally, $V$ is finite, since it has exactly three elements. (One quibble, you said in (2) that you wanted "sets" and not just a set that was a singleton. In this case, please add another set $Q$ to the theory that has only $P$ as a member, and also make $Q$ an element of $V$.) I suspect that you may have in mind that the theory should also include additional unstated settheoretic principles. 


I have been studying a theory I call Modular Arithmetic (MA). MA has the same axioms as first order Peano Arithmetic (PA) except Ax( ~S(x)=0 ) is replaced with Ex( S(x)=0 ). MA is consistent because it has arbitrarily large finite models base on modular arithmetic. The upward Löwenheim–Skolem theorem proves MA must have infinite models. MA can be made into an ultrafinite theory by adding an axiom like Ax( x=0 or x=S(0) or ... or x=Sn(0) ) where Sn(0) is some finite number of applications of successor to 0 (a numeral). Coming up with a set theory based on MA is problematic. It is simple to show MA is omega inconsistent. The predecessor of 0 must be nonstandard (not a numeral) in any infinite model of MA. If the predecessor of 0 is standard we can prove the model is finite using induction. This means Ax( ~S(x)=0 ) is true for all standard natural numbers in any infinite model. A set theory based on MA can't be well ordered or well founded, either. (x =< y) <> Ez( x+z=y ) is trivially true for any x and y. Using S(x) = x U {x} as a definition of successor is inconsistent with the axioms of MA. In ZF, even the Axiom of Pairing allows the construction of arbitrarily large sets. Assuming we could come up with a set theory for MA, it would have the properties you ask for. One way to do this would be to encode sets as binary expansions of natural numbers. Element x is a member of the set if the x'th bit of the expansion is true. This would allow us to have sets of size log2(n) where n is the size of the universe. We can equate 0 with the empty set. We can define singleton sets for "small" elements of the universe. We could also define sets with subsets. We could do a reasonable amount of arithmetic by choosing n large enough. We could have sets and do math on sets as large as 100 by having a universe of size 2^100. 


If there is such a theory, I doubt that an ultrafinitist would like it. The universal set V has to contain itself as an element, and that means you can have chains of unlimited length of the form $x \in y \in \ldots \in z$. But an ultrafinitist doesn't want objects of infinite size, and V smells very much like an object of infinite size (depth). Depending on the exact interpretation of your axiom #2, and what you mean by set equality, I don't think such a set theory exists. If #2 is meant to say that for any set, there is a singleton containing that set as its member, then we have the existence of $\emptyset$, {$\emptyset$}, {{$\emptyset$}}, ... and all of these are elements of V. If set equality means what people usually take it to mean, then these are all unequal, so V is infinite. [EDIT: more material added below] If, on the other hand, the meaning of your axiom #2 is as assumed in JDH's answer, and not as assumed in mine, then there is no generic machinery in your axioms for building new sets out of old ones. This raises the question of the specific meaning of "a certain amount of arithmetic." In JDH's answer, the objects P and Q can be identified with the numbers 1 and 2, and we can clearly make models where this process extends up to some larger integer, such as 387. Then you have a theory with enough objects in it to name the first 387 integers. Is this enough arithmetic? To make this a compelling realization of what we have in mind for a set theory, I think you would want to describe things like "the set of all odd integers less than 153," but your axioms don't have enough machinery in them to generate anything like that. I think the basic problem here is that if we're going to be ultrafinitists and only admit the existence of integers up to some size $n$, then any set theory that can describe the existence of all sets made out of those integers is going to have a number of sets much, much larger than $n$  unless we don't provide enough machinery to generate a rich universe of sets out of these integers, in which case it won't feel like a compelling realization of what we have in mind when we talk about a set theory. This problem is bad enough without the universal set. The universal set just makes it infinitely bad. 


It appears to me that meaningful ultrafinitist arithmetic is possible, but it has limitations e.g. cannot include functions growing too fast such as exponentiation to a variable power. Proving the existence of $x \mapsto 2^x$ would require a stronger form of induction than accepted by some ultrafinitists. This MO question seems relevant: Is there any formal foundation to ultrafinitism? 

