# Set theory and computer science

It's said that in Zermelo–Fraenkel set theory (ZFC) one can develop all of mathematics. How about computer science?

Is it possible to define algorithms as a first step? More specifically, how to define "if x = 1 then y else z"? How about loops?

• Well, it's kinda misleading to say that ZFC allows to develop all of mathematics. There can be a consistent set theory $A: A\land ZFC$ is inconsistent. Commented Sep 26, 2017 at 8:56
• You can define the semantics of programming languages in systems weaker than ZFC. I suggest picking up a textbook on programming language semantics. Commented Sep 26, 2017 at 10:09
• To emphasize Yuval Filmus' statement, you can formalize typical computer science concepts in formal systems far weaker than ZFC. Commented Sep 26, 2017 at 11:07
• Far, far, far weaker in fact. Commented Sep 26, 2017 at 21:25
• Very briefly: here is coding of natural numbers in set theory, here is coding of ordered pairs, functions are sets of ordered pairs, integers are sets of ordered pairs of natural numbers, rationals are sets of ordered pairs of integers, reals are sets of rationals (Dedekind cuts). So the sign function is the set $\{(x,y) \mid (x < 0 \land y = -1) \lor (x = y = 0) \lor (x > 0 \land y = 1) \}$. I got rid of if-then-else, I think. Commented Sep 29, 2017 at 9:34

It all depends what you consider "computer science."

For what I would call "classical computer science" i.e. the theory of Algorithms, Turing Machines, etc. it can all be modelled in set theory.

A Turing Machine is just a tuple (which can be modelled using sets): a set of states, a tape-alphabet set, a transition function, etc. All of these are set-theoretic constructs, and even with nondeterminism, we replace the transition function with a relation, which is again set theoretic.

Similarly, we can define the semantics of programming languages using sets. Usually this just boils down to a big-step or small-step operational semantics, which again, is just defining relations.

Where things get iffy is with the so-called "alternate foundations of mathematics". This includes things like:

They provide alternate sets of axioms from which mathematics can be built up. For example, the usually discard excluded middle and axiom of choice. Homotopy type theory, for example, introduces the Univalence Axiom.

These systems tend to be heavily oriented towards computation through the Curry-Howard Correspondence, so that a proof can "run" on a computer. So they don't quite fit into ZFC, but are generally considered part of computer science.

• I mean it's absolutely possible to develop all of these with set theory as the metatheory, so there's not really a conflict here. Commented Sep 26, 2017 at 18:27
• How are types "iffy"? For me, they are right at the core of CS "feels". Commented Sep 26, 2017 at 19:54
• @Raphael they're iffy in the sense that it's unclear whether something like HoTT belongs in Math, CS, or Philosophy, and unclear whether they are separate from ZFC (since they're an alternate foundation) or can be expressed in it Commented Sep 26, 2017 at 21:13
• I think it's quite clear that HoTT belongs in Math, CS and Philosophy. Commented Sep 26, 2017 at 21:26
• What I am trying to say is that is very well understood how type theory and set theory are related. There is no mystery. Commented Sep 26, 2017 at 21:33