Is there a finitistic set theory, and if there is, is it provably consistent?

Question

ZFC is the mainstream set theory. It has an axiom of infinity which claims that there is at least one infinite set. Now suppose like Aristotle, we object and say that there are no actually infinites in nature, only potentially infinite ones, and so we decide to drop the axiom of infinity, presumably this means that we must drop the axiom of Choice as this becomes irrelevant when there are no infinite sets to work with.

Presumably no other essential modifications need to be made to any other axioms - but considering the answer to this question perhaps one needs an axiom to assert the existence of the empty set.

Now is this fragment of ZFC - which is a theory of finite sets - provably consistent? Or is it likely, that it still embeds PA, and thus Godels incompleteness theorem applies?

Answer 1

V-omega, the set of hereditarily finite sets is a model of the theory you get by taking ZFC and replacing the axiom of infinity with its negation, and it is bi-interpretable with Peano Arithmetic (so indeed, Gödel's incompleteness theorem still applies).

For more, see e.g. https://math.stackexchange.com/questions/107639/what-are-the-consequences-if-axiom-of-infinity-is-negated