Is there a decidable set theory?

[Demystifier]

The Godel theorem shows that the standard Peano axiomatization or arithmetic is undecidable. However, there is an alternative Presburger's axiomatization of arithmetic, which is decidable.

Similarly, the standard ZFC axiomatization of set theory is undecidable. For instance, the continuum hypothesis is undecidable in ZFC. Is there an alternative axiomatization of set theory which is decidable?

 

[mathman]

Presburger's is decidable, but it is too weak to do ordinary arithmetic. I suspect that if it exists a decidable set theory would be too weak to do ordinary set theory.

 

[Demystifier]

By Presburger arithmetic you cannot state certain general theorems, but I think you can still do arithmetic in a practical sense. (For instance, you can compute concrete products such as $2\times 6=12$. Any 7 year old kid can do it without knowing Peano axioms.) Perhaps something similar might be true with decidable set theory.

 

[TeethWhitener]

Is there an alternative axiomatization of set theory which is decidable?

Somewhat trivially, any inconsistent theory is decidable (since all formulae in the theory follow from the inconsistency by the principle of explosion).

Also:
https://en.wikipedia.org/wiki/Decidable_sublanguages_of_set_theory

 

[SSequence]

While this does not answer the actual technical part of your question, it is probably of some (tangential) relevance (because of being related to decidability and proof length).

The somewhat trivial (and non-technical) observation is that consider all well-formed statements (that are suppose to have true or false values) of length n that can be formed in some "reasonable" reasoning system. Also suppose that all the well-formed statements are also decidable in the system (using some agreed and/or given rules of inference as part of the reasoning system).

For some statement S, suppose we define the minimum proof-length as the length of the shortest proof of S. Let T(n) denote the maximum value among the minimum proof-lengths for all statements of length n or less. Then T(n) has to be strictly bounded by some recursive function.

For example, think of example of Presburger arithmetic mentioned above. Then I am pretty sure there is a recursive function that would bound the minimum proof-lengths (as mentioned in previous paragraph) for a given length of statements cast in the system (as questions with truth values). And I would suspect that recursive function wouldn't really grow that much faster than much of elementary functions encountered in normal math (possibly hovering somewhere little above or below (more likely below) ackermann function).

So the inability of a "reasonable" reasoning system (PA should count I think because it can't answer some of its own questions) to cast questions that it itself can't answer can also be seen in this way ... The reasoning system should fail to prove certain statements of length n or less (that it can cast as questions) because it would completely stop proving "any" statement of length n or less after f(n) number of steps (where f is some recursive function). I don't have any good idea what that function would be for PA though.

 

[SSequence]

So the inability of a "reasonable" reasoning system (PA should count I think because it can't answer some of its own questions) to cast questions that it itself can't answer can also be seen in this way ... The reasoning system should fail to prove certain statements of length n or less (that it can cast as questions) because it would completely stop proving "any" statement of length n or less after f(n) number of steps (where f is some recursive function). I don't have any good idea what that function would be for PA though.

Sorry I think this particular part can't be assumed beforehand (under the more generic assumption of theorems being recursively enumerable).