TITLE: Boolean logic as an alternate, minimalist foundation for arithmetic
QUESTION [2 upvotes]: Arithmetic, and math in general, is typically formalized in first-order ZFC set theory. Since there are no urelements, the closest thing we have to an "atom" is the empty set. Sets are built up gradually from sets containing sets containing... the empty set. We can construct the natural numbers via the Von Neumann construction, where $0=\{\}$, $1={0}=\{\{\}\}$, $2=\{0,1\}=\{\{\},\{\{\}\}\}$, and so on. From here we can develop arithmetic (and more) by defining tuples, relations, functions and so on. The empty set and the containment relation is all we need.
Meanwhile, in the practical world, we appear to have a completely different "de facto" foundation for much of math: Boolean logic. Rather than building everything up from the empty set, we build everything up from bits, which are our new "atoms." We can build up the natural numbers from bits via the base 2 representation. From here we can develop arithmetic (and more) by creating Boolean circuits for addition, multiplication, and so on. Bits and NAND gates are all we need.
Despite the obvious connections, I have never seen an attempt to formalize arithmetic in a parsimonious, reductionist way using only bits and logic gates as primitives. This is obviously possible since basically every computer is doing it.
In theory, it might even be possible to build set theory on a foundation of bits and logic gates, as Boolean algebra and set theory are intimately connected on a few different levels. Stone's representation theorem is an isomorphism between Boolean algebras and fields of sets, so there should be a proper class-sized Boolean algebra that is a model of ZFC (or close enough to get somewhere). Boolean logic is basically equivalent to classical propositional logic due to the completeness theorem, so "bits" are equivalent to classical propositions. I suppose one could think of sets themselves as related to Boolean-valued models of propositional logic.
Does anyone know of such an approach? If not, how could one accomplish this?

REPLY [2 votes]: I'm not that familiar with Stone's representation, but to me it seem that the existence of multiplicative unity corresponds to the existence of an universe which is non-existant in ZF set theory. A question is if Stone's representation works if we drop the requirement of the unity?
Furthermore it look's like the Stone's representation does not automatically guarantees the existence of power set and infinite set. Those axioms or equivalent are needed in order to build real arithmetics (we need both infinite sets and even larger sets).