# 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. – rus9384 Sep 26 '17 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. – Yuval Filmus Sep 26 '17 at 10:09
• To emphasize Yuval Filmus' statement, you can formalize typical computer science concepts in formal systems far weaker than ZFC. – Derek Elkins left SE Sep 26 '17 at 11:07
• Far, far, far weaker in fact. – Andrej Bauer Sep 26 '17 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. – Andrej Bauer Sep 29 '17 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. – Daniel Gratzer Sep 26 '17 at 18:27
• How are types "iffy"? For me, they are right at the core of CS "feels". – Raphael Sep 26 '17 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 – jmite Sep 26 '17 at 21:13
• I think it's quite clear that HoTT belongs in Math, CS and Philosophy. – Andrej Bauer Sep 26 '17 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. – Andrej Bauer Sep 26 '17 at 21:33