# A concrete piece of evidence for incompleteness

On Thursday, the 25th of March 2015, Venanzio Capretta gave a Theory Lunch talk about Goodstein’s theorem. Later, on the 9th of March, Wolfgang Jeltsch talked about ordinal numbers, which are at the base of Goodstein’s proof. Here, I am writing down a small recollection of their arguments.

Given a base $b \geq 2$, consider the base-$b$ writing of the nonnegative integer

$n = b^m \cdot a_m + b^{m-1} \cdot a_{m-1} + \ldots + b \cdot a_1 + a_0$

where each $a_i$ is an integer between $0$ and $b-1$. The Cantor base-$b$ writing of $n$ is obtained by iteratively applying the base-$b$ writing to the exponents as well, until the only values appearing are integers between $0$ and $b$. For example, for $b = 2$ and $n = 49$, we have

$49 = 32 + 16 + 1 = 2^{2^2 + 1} + 2^{2^2} + 1$

and also

$49 = 27 + 9 \cdot 2 + 3 + 1 = 3^3 + 3^2 \cdot 2 + 3 + 1$

Given a nonnegative integer $n$, consider the Goodstein sequence defined for $i \geq 2$ by putting $x_2 = n$, and by constructing $x_{i+1}$ from $x_i$ as follows: Continue reading

# Limit languages of cellular automata

At today’s Theory Lunch I discussed limit languages of cellular automata, and Lyman Hurd’s example of a CA whose limit language is not regular. I wrote about this on my other blog.

# Proving the beauty of a mind

In the previous Theory Lunch talk we introduced the notion of Nash equilibrium for games in normal form. Today, we went through the proof of Nash’s theorem of existence of mixed strategy Nash equilibria for finite games in normal form.

Let us recall the basic notions. In a game in normal form we have: Continue reading

# Playing with a beautiful mind

Today’s talk’s topic is an idea so important in game theory, and with so many applications in different fields including computer science, that it earned its discoverer, together with Reinhard Selten and John Harsanyi, the 1994 Nobel Memorial Prize in Economic Sciences.

To introduce this idea, together with other basic game-theoretic notions, we resort to some examples. Here goes the first one: Continue reading

# Many choices from few parameters

At the end of March I gave a talk about how to obtain a wide range of Bernoulli distributions with as few parameters as possible. This originates from the needs of simulations of complex systems with cellular automata machine. The solution I described comes from Mark Smith’s doctoral thesis, performed under the supervision of Tommaso Toffoli.

I wrote a post on this on my blog on cellular automata.

# Transgressing the limits

Today, the 14th of January 2014, we had a special session of our Theory Lunch. I spoke about ultrafilters and how they allow to generalize the notion of limit.

Consider the space $\ell^\infty$ of bounded sequences of real numbers, together with the supremum norm. We would like to define a notion of limit which holds for every $\{x_n\}_{n \geq 0} \in \ell^\infty$ and satisfies the well known properties of standard limit: Continue reading

# Natural numbers with addition form a monoid

The other day I gave a very short introductory talk on formalising mathematics in Agda to a highly mathematically literate but otherwise quite general audience. I presented this example.

In Agda, proofs and programs are the same thing, types are sets are propositions. These sets contain values of that type, or equally they contain proofs of that proposition.
Agda is a very expressive language so very little is built in and most things can be defined in a library. We will define some of those things now to see how they work.

module talk where


Natural numbers (0,1,2,3,…) can be seen as being defined by either zero or the successor (+1) suc of another natural number.

data Nat : Set where
zero : Nat
suc  : Nat → Nat


Addition _+_ takes two natural numbers and returns another. It can be defined by recursion (induction) on the first argument. If it is zero we return n and if it is successor we can make a recursive call to (m + n) and apply the successor to the result. The recursive call (inductive hypothesis) is valid as m is structurally smaller than suc m.

_+_ : Nat → Nat → Nat
zero  + n = n
suc m + n = suc (m + n)


Having defined one function we now want to prove something about it. One can think of this as an exercise in formal verification. I want to prove that _+_ satisfies some equations. There is an equals sign in the definition above but this is not the one I should use to state my equations. The = is the definitional equality symbol and denotes equations that the computer can see are true. I want to prove some things that the computer isn’t able to see for itself.

The notion we need is propositional equality which is a relation we will define now. In another language one might expect a relation to have type like Nat → Nat → Bool which might return true if the natural numbers were equal. In Agda we would use Set instead of Bool and the set would be inhabited if the relation holds. We can define propositional equality _≅_ once and for all for any set A which we write as an implicit parameter {A : Set}. Remarkably this set has only one canonical inhabitant refl which is inhabits the type of equations between really identical (definitionally equal) values. This may seem strange but one can prove (derive) the other properties, such as symmetry and transitivity.


-- propositional equality
data _≅_ {A : Set} : A → A → Set where
refl : ∀{a} → a ≅ a


We could prove useful lemmas such as symmetry now but for this post I will only need cong – that functions preserve equality. Given any function f : A → B and two equal elements of A the function should return equal results.
The lemma is very easy to prove as when we pattern match on the proof that the elements are equal then the only possible pattern is refl which forces a and a' to be equal, replacing, say, a' with a which reduces our task to showing that f a ≅ f a. This is easily proved using refl.

-- lemma: functions preserve equality
cong : {A B : Set} → (f : A → B) → {a a' : A} → a ≅ a' → f a ≅ f a'
cong f refl = refl


The lemma is very useful for proving equations that have the same function (such as suc) on both sides. We can use it to reduce our task to proving that what is underneath the function on both sides is equal.

One can define an algebraic structure like a monoid as a record (named tuple/struct/etc.) in Agda. It contains fields for the data and also for the laws. A monoid has a carrier set M a distinguished unit element e and a binary operation op. The three laws state that op has e as its left and right unit and it is associative. The monoid record Mon lives in Set1 as it contains a Set(0).

-- Monoid
record Mon : Set1 where
-- data
field M     : Set
e     : M
op    : M → M → M
-- laws
lunit : ∀ m → op e m ≅ m
runit : ∀ m → op m e ≅ m
assoc : ∀ m n o → op (op m n) o ≅ op m (op n o)


The goal is to define a monoid where M = Nat, e = zero and op = _+_. Let’s go ahead and prove the laws. The first law which would be (zero + n) ≅ n doesn’t require proof as it holds definitionally (it is the first line of the definition of _+_). The second law does require proof as here the _+_ doesn’t compute as the first argument is the variable n.

+runit : ∀ n → (n + zero) ≅ n
+runit zero    = refl
+runit (suc n) = cong suc (+runit n)


We prove the second law +runit by induction on n. When proving a property of a program as we are doing here it’s a good idea to follow the same pattern in the proof as in the program. Here _+_ is defined by recursion on its first argument so it makes sense to carry out the proof by induction on the first argument too. This makes things compute nicely. The first case is zero + zero ≅ zero which Agda computes to zero ≅ zero by applying the definition of _+_. This is easily proved by refl. The second case computes to suc (n + zero) ≅ suc n. First we observe that there is a function suc on both sides so we type cong suc ?. This reduces our problem to proving that n + zero ≅ n which follows from the inductive hypothesis +runit n

+assoc : ∀ m n o → ((m + n) + o) ≅ (m + (n + o))
+assoc zero    n o = refl
+assoc (suc m) n o = cong suc (+assoc m n o)


The proof for associativity proceeds analogously. We pattern match on the first argument m which gives two cases. The first case computes to n + o ≅ n + o and the second computes to suc ((m + n) + o) ≅ suc (m + (n + 0)). As before the first case follows by reflexivity and the second case by congruence of suc and inductive hypothesis.

Having done all the hard work we can now define a monoid for Nat, _+_, and zero:

-- natural numbers with addition form a monoid
NatMon : Mon
NatMon = record {
M     = Nat;
e     = zero;
op    = _+_;
lunit = λ _ → refl; -- this one doesn't require proof
runit = +runit;
assoc = +assoc}