What really algorithm are? Can we define algorithm as functions or in terms of set theory Can we reconvert proof using algorithm in set theory concept.For example,

Theorem: A function defined on closed and bounded interval [a, b] be continuous. And if f(a).f(b)<0 then there exist c in (a, b) such that f(c) = 0 Proof: Outline of proof using an algorithmic approach is: wee take midpoint d of [a, b] if f(d) = 0 then we are done. If not we look at sign of f(d) and define [a1, b1] such that one of a1 or b1 is d and such that f(a1)f(b1)<0 and again we look at midpoint and procced as above. And in the end we use nested interval theorem if process does not terminate. I think you get outline of proof.

But question: Is it possible to write same proof in set theory terms?(And there is proof of theorem using connected metric space concept which does not use algorithm but am just consult with above proof)

Summary of Questions: 1. What is proof by recursion? 2. Can every theorem which is proved by a 'proof by recursion' be proved without 'proof by recursion'?

  • $\begingroup$ What exactly do you mean by "writing a proof in set theoretic terms"? $\endgroup$ Oct 10, 2014 at 5:29
  • 2
    $\begingroup$ This question seems a bit confused and vague.. $\endgroup$ Oct 10, 2014 at 8:01
  • $\begingroup$ @AndresCaicedo Writing proof in set theoretic terms I mean to say that 'facts' and 'terms' used in proof are proved and defined from set theory respectively. $\endgroup$
    – Sushil
    Oct 10, 2014 at 17:27
  • $\begingroup$ Any formal concept in mathematics can be stated in set theoretic terms, if that is what you are after. You formalize algorithms via Turing machines, and perhaps this is really the key term for you to investigate. Anyway, Turing machines are functions. Set theoretically, functions are sets of ordered pairs, and ordered pairs are special kinds of sets. So any reasoning about algorithms can be formalized as a set theoretic argument. (I do not know what the particular advantage of doing this would be here, but this is the standard approach.) $\endgroup$ Oct 10, 2014 at 19:15
  • $\begingroup$ @AndresCaicedo Ok thanks so basically I have to look at Turing Machines. Can you please give some good reference for this. $\endgroup$
    – Sushil
    Oct 10, 2014 at 20:15

1 Answer 1


Recursion is a powerful, well-defined concept in set theory. The Recursion Theorem (or its generalization) can be applied whenever a deterministic recursive algorithm can be used.

Here is a proof sketch of an equivalent formulation of the Intermediate Value Theorem, using recursion in the set theoretic context.


Let $f : [a, b] \to \mathbb R$ be a continuous function, where $a \le b$ is a pair of real numbers such that $f(a) \cdot f(b) \le 0$. Then, there exists a $c \in [a, b]$ such that $f(c) = 0$.

Proof Sketch

We shall first represent the midpoint procedure as a set-theoretic function $g$, whose domain and range shall be the set $S$ of closed subintervals of $[a, b]$. For instance, $g : S \to S$ can be defined as:

$$ g\left([p, q]\right) = \begin{cases} \left[ p, \frac{p+q}{2} \right] & \text{if}\mathrel{} f(p) \cdot f\left(\frac{p+q}{2}\right) \le 0 \\ \left[ \frac{p+q}{2}, q \right] & \text{otherwise} \end{cases} $$

By invoking the recursion theorem on $g$, we obtain a unique function $G : \mathbb N \to S$ such that $G(0) = [a, b]$ and that $G(n+1) = g\bigl(G(n)\bigr)$.

It can be verified that $\langle G(0), G(1), G(2) \ldots \rangle$ is an infinite sequence of closed, nested intervals whose lower and upper bounds converge to a single point $c \in [a, b]$.

It can further be verified (by properties of $g$ and by continuity of $f$) that $f(c) \cdot f(c) \le 0$, whence $f(c) = 0$.


A small generalization—the Axiom of Dependent Choice—can be used to obtain a proof of the intermediate value theorem from a nondeterministic recursive algorithm.

To do so, one can represent the nondeterministic algorithm as a relation $R$ on the nonempty set $\big\{ [p, q] \subseteq [a, b] \bigm| f(p) \cdot f(q) \le 0 \bigr\}$.

For instance, suppose we only cared that each subsequent interval was a subinterval whose size was half or less:

$$ [p, q] \mathrel R [s, t] \Longleftrightarrow [s, t] \subseteq [p, q] \mathrel{}\text{and}\mathrel{} t-s \le \frac{q-p}{2} $$

Then, it is straightforward to verify that $R$ is an entire relation, whence the axiom of dependent choice can be used to obtain an infinite sequence $$ [a_1, b_1] \mathrel R [a_2, b_2] \mathrel R [a_3, b_3] \mathrel R [a_4, b_4] \mathrel R \ldots $$ with the required properties.

  • $\begingroup$ Yeah that is exactly I was searching. Now the question is that: Can every proof using algorithm like above be formulated as functions like this. Or How we define proof using algorithms. One comment I got says to study Turing Machines(which seems reasonable to me). Any comment you would like to add to it. $\endgroup$
    – Sushil
    Oct 12, 2014 at 15:07
  • $\begingroup$ @Sushil: Since years ago, I have learned about the Curry-Howard correspondence. It is essentially a bidirectional dictionary to translate proofs into algorithms, conjectures into types, and proven theorems into inhabited types. Every proof of a theorem can indeed be formulated as a deterministic function that inhabits a specific lambda type! (Caveat: the lambda type encodes each assumption of a proof as an additional parameter. This includes any variant of axiom of choice) $\endgroup$
    – Moh
    Sep 17, 2023 at 19:50

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .