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.

2$\begingroup$ The general goal of this question seems interesting to me, regardless of the merits of this specific proposed set of axioms. People who want a universal set are generally people who are interested in claiming the existence of the biggest infinities they can name without having inconsistency. Ultrafinitists want exactly the opposite. If someone could make a model that did both at once, and its properties were sufficiently compelling, it would probably cause some serious indigestion on both sides, like Skolem's reaction to Skolem's paradox. $\endgroup$– Ben CrowellSep 23 '12 at 21:14

3$\begingroup$ What was Skolem's reaction to Skolem's paradox? $\endgroup$– Garabed GulbenkianSep 24 '12 at 19:59
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
 There are exactly three distinct objects: $E$, $P$ and $V$.
 $E$ has no members.
 $P$ has only $E$ as a member.
 Everything is a member of $V$, including $V$.
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.

$\begingroup$ The issue we need to get the OP to clarify is whether #2 means that (a) at least one singleton set exists, or (b) for every set, a singleton exists containing only that set. If a, then your model works. If b, then as I argued in my answer, no model exists. $\endgroup$ Sep 23 '12 at 21:49

3$\begingroup$ Another point to think about is why we would consider your example trivial. It feels trivial because it's only got 3 members, but would it be any less trivial if it had 4 members, or too many members to describe within the length limit that MO sets for posts? Remember, the goal is to make a finite universe of sets. $\endgroup$ Sep 23 '12 at 21:55

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.

$\begingroup$ Perhaps the requirement should be that the universal class is finite? $\endgroup$– CharlesSep 23 '12 at 20:52

$\begingroup$ @Charles: I don't think the argument in my second paragraph depends on any assumption that V is a set rather than a proper class. $\endgroup$ Sep 23 '12 at 20:59

2$\begingroup$ I don’t think ultrafinitists would accept the arguments in your first two paragraphs: they’re essentially the same as the argument that from 0 and S, one obtains infinitely many natural numbers; and this is exactly the kind of induction instance that ultrafinitists reject. In particular, “$V \in V$” seems no worse than “$0 \leq 0$”, which I’m pretty sure ultrafinitists accept. $\endgroup$ Sep 24 '12 at 2:43

$\begingroup$ @Peter LeFanu Lumsdaine: In the second paragraph, I'm sketching an argument within ZFC, not within an ultrafinitist theory. The OP asked (if I'm understanding correctly) whether there are models of his/her axioms within ZFC that are finite. In other words, when the OP says, "the universal set of T should be finite," I think this has to be understood as a statement within ZFC, to be proved within ZFC, about a model of the axioms in ZFC. I don't think "finite" has a definition within the theory the OP was proposing. $\endgroup$ Sep 25 '12 at 18:54
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?

$\begingroup$ Thanks to you all for your insightful comments. Joel, that is a really neat little model which certainly satisfies my requirements and you are right that I am going to need additional axiomsonly it is not at all clear to me what those should be. I would like to be able to carry out Nelson's arithmetic in T and also to have 2^x not defined for all sets x (just as Nelson does when x is a number variable). The existence of a universal class is probably not needed and may make things more complicated. $\endgroup$ Sep 24 '12 at 19:25