Category: Review/overview

Naive Set Theory summary

I’ve almost finished reading Paul Halmos’ Naive Set Theory. The book is highly technical, therefore it may not be suitable for everyone. I wanted to dig deeper into the technicalities, so that’s the main reason I chose to work through it.

I recommend reading Daniel Velleman’s How To Prove It before tackling this one. How To Prove It is a book about mathematical proofs, but it involves proving properties about sets so you learn both proofs and sets on the way.

Here’s a quick summary of my thoughts on the book and set theory in general.

Introduction

What is a set? A set is a collection of objects. That’s all it is! As simple as that sounds, sets are very important in mathematics. This simplicity is what sparked interest for me.

In fact, (almost) all of mathematics is built upon sets! Set Theory is one of the widely accepted foundations of mathematics. There are also some other theories, but we won’t get into that.

Different mathematical ideas usually need an apparatus to be described. Very often this apparatus is Set Theory.

Examples

Example 1: Consider Probability Theory as a branch of mathematics. To represent a sample space of, for example a dice roll, we usually say \Omega = \{ 1, 2, 3, 4, 5, 6 \}. So \Omega is a set which contains all the possible outcomes. Rolling an even number is represented by some other set, A, where A = \{ 2, 4, 6 \} but also note that A \subseteq \Omega. There’s a relation between A and \Omega, and this relation is “subset”, as we have observed. Relations needn’t necessarily be always a subset, but we digress a little. What’s the probability to roll an even number, given the sample space? It’s simply \frac{|A|}{|\Omega|} = \frac{3}{6} = 0.5. We just used set theory to calculate the probability of rolling an even number of a 6-sided dice!

If you don’t quite understand the notation in the previous paragraph, don’t worry. It’s really simple, and I have already covered it in a previous post, Abstractions with Set Theory.

Example 2: So Probability was one example, but it goes farther than that. Turing Machines (the computation model that your computer/phone/etc uses) can also be described through set theory. Any computation can be represented through sets, which is really awesome.

Example 3: Another interesting example is natural numbers. They can be represented as: 0 = \{ \}, i.e. the empty set, 1 = \{ \{ \} \} i.e. a set containing the empty set, 2 = \{ \{ \{ \} \} \}, well, you get the idea 😀

Example 4: As we noted earlier, there was a relation between two sets, namely the “subset” relation. Relations can be generalized further, and are used to describe some shared property between objects. For example, \leq may be a valid relation on some set, for example, the natural numbers.

Example 5: Abstraction goes further with Algebraic Structures. For example, a Magma represents a set together with some binary operation (it can be anything!). An example, natural numbers with operation plus makes a Magma.

Conclusion

As you can see, there are too many abstractions! What’s the point in generalizing all of this and introducing all these weird names like Magma, etc? Well, it’s similar to what we do with code. Think about how we generalize some calculations in a large software project and we put them in a function with its own name. We don’t care about the details, we only want to look at it and use it from a different abstraction level. This function has its own properties and behavior which can be observed while we code (e.g. it accepts some specific arguments, or returns either an array or int, etc). Same with mathematics!

Recursion Theorem

Meta: As I mentioned, this book is highly technical. Note this is a 100-page book and I spent almost a year on it – on and off. The thing is, you don’t read it like a storybook. Think of it more like a Sudoku puzzles book. When I’m in the mood, I sit down and “solve” some puzzles. Sometimes, even for myself, some of the technical explanations are hard to understand. But I don’t give up – I re-read them a lot of times. When it clicks, I get a very good feeling. Like when you learn a new trick. It’s a very similar feeling to programming. Try to think of some task that you worked on and you learned a new cool trick. It feels good, and you can’t wait to apply this trick again and again until it gets boring. 🙂

So we can conclude that Set Theory is a really powerful apparatus. I hope these examples sparked some interest for you too!

Dafny – programming language for formal specifications

Dafny is an imperative compiled language that supports formal specification through preconditions, postconditions, loop invariants.

I found out about it from The Great Theorem Prover Showdown, while reading Hacker News one day.

It only seems to target C#, but can automatically prove properties about functions nevertheless.

I finished Dafny Tutorial and it was pretty straight-forward. The tutorial should be easy to follow for anyone with basic knowledge with the C programming language (and mathematical logic). The examples for the Dafny tutorial can be ran from the browser so you do not have to install it locally to go through it.

The reason why I like this programming language is because it seems much simpler than e.g. Coq or Idris that are based on dependent types / Calculus of Constructions (however, note that it still shares some stuff such as algebraic data types, or inductive types).

The tutorial starts with functions, pre-post conditions and assertions, and then proceeds with loop invariants. It proves basic properties for abs/max, etc.

For example, abs takes an integer and produces an integer greater than or equal to zero. Here’s the proof for that:

method Abs(x: int) returns (y: int)
ensures 0 <= y
{
y := 0;
}

With ensures we set the post-conditions (alternatively, requires is for pre-conditions). Pretty simple and neat, right? 🙂

Like pre- and postconditions, an invariant is a property that is preserved for each execution of the loop. Here’s an example for an invariant:

method m(n: nat)
{
var i := 0;
while i < n
invariant 0 <= i
{
i := i + 1;
}
}

However if you go through the tutorial you will see by the exercises that the challenge in picking a good loop invariant is finding one that is preserved with each loop execution, but also one that lets you prove what you need.

Finally, example for quantifiers:

method m()
{
assert forall k :: k < k + 1;
}

The tutorial takes only a couple of hours to finish, and for anyone interested in programming languages like this I highly recommend you go through it 🙂

The conclusion paragraph of the tutorial states it well:

Even if you do not use Dafny regularly, the idea of writing down exactly what it is that the code does is a precise way, and using this to prove code correct is a useful skill. Invariants, pre- and post conditions, and annotations are useful in debugging code, and also as documentation for future developers. When modifying or adding to a codebase, they confirm that the guarantees of existing code are not broken. They also ensure that APIs are used correctly, by formalizing behavior and requirements and enforcing correct usage. Reasoning from invariants, considering pre- and postconditions, and writing assertions to check assumptions are all general computer science skills that will benefit you no matter what language you work in.

For all the tutorial exercises, you can check out my Dafny Git repository.

Metamath

During my research on various theorem provers, today I stumbled upon Metamath.

To me, what was interesting about it was its simplicity. You start by defining a formal system, i.e. variables, symbols, axioms, inference rules. Then you build new theorems based on the formal system.

The core concept behind Metamath is substitution, and it’s using RPN notation to build hypothesis on the stack and then rewrite them using the inference rules to reach conclusion.

The program is written in C, and I compiled it on both OS X and my Android phone. It’s pretty light-weight and compiles in a few milliseconds, and it’s also interesting that you can take it anywhere you want on your phone.

Metamath has no special syntax. It will tokenize a file that we give to it, and tokens that start with $ are Metamath tokens, while everything else are user-defined tokens.

Here is a list of built-in Metamath tokens:

  • To define constants, use the $c token.
  • To define variables, use the $v token.
  • To define types of variables, use the $f token.
  • To define essential hypothesis, use the $e token.
  • To define axioms, use the $a token.
  • To define proofs, use the $p token.
  • To start proving in $p statement, use the $= token.
  • To end the statements above, use the $. token.
  • To insert comments, use the $( and $) tokens.
  • To define a block (has effect on scoping), use the ${ and $} tokens. Note that only $a and $p tokens will remain outside the scope.

That’s basically it. The package has included demo example and an example for the MU puzzle as well. There are other systems as well (Peano, Set).

There are some basic rules as well:

  • A hypothesis is either a $e or a $f statement
  • For every variable in $e, $a or $p, we must have a $p assertion, i.e. every variable in an essential hypothesis/axiom/proof must have a floating hypothesis (type)
  • A $f, $e, or $d statement is active from the place it occurs until the end of the block it occurs in. A $a or $p statement is active from the place it occurs through the end of the database.

For the complete syntax you can refer to the Metamath book.

Now for the example we’ll use, start by creating a test.mm file. We’ll define a formal system and demonstrate the usage of modus ponens to come up with a new theorem, based on our initial axioms.

$( Declare the constant symbols we will use $)
$c -> ( ) wff |- I J $.

$( Declare the variables we will use $)
$v p q $.

$( Specify properties of the variables, i.e. they are wff formulas $)
wp $f wff p $.
wq $f wff q $.

$( Define "mp", for the modus ponens inference rule $)
${
mp1 $e |- p $.
mp2 $e |- ( p -> q ) $.
mp  $a |- q $.
$}

$( Define our initial axioms. I and J are well-formed formulas,
we have a proof for I and we have conditional for I -> J $)
wI  $a wff I $.
wJ  $a wff J $.
wim $a wff ( p -> q ) $.

$( Prove that we can deduce J from the initial axioms. Note how we use
block scope here, since we don't want the hypothesis proof_I and
proof_I_imp_J to be visible outside of this scope. $)
${
$( Given I and I -> J $)
proof_I $e |- I $.§
proof_I_imp_J $e |- ( I -> J ) $.

$( Prove that we can deduce J $)
proof_J $p |- J $=
wI  $( Stack: [ 'wff I' ] $)
wJ  $( Stack: [ 'wff I', 'wff J' ] $)

$( Note that we had to specify wff for I and J before using mp,
since the types have to match, as set on line 8 and 9 $)

proof_I       $( Stack: [ 'wff I', 'wff J', '|- I' ] $)
proof_I_imp_J $( Stack: [ 'wff I', 'wff J', '|- I', '|- ( I -> J )' ] $)

mp  $( Stack: [ '|- J' ] $)
$.
$}

To verify our file, we run ./metamath 'read test.mm' 'verify proof *' exit.

Note how we had to separate wff from |-. Otherwise, if we just used |-, then all well formed formulas would be proven to be true, which doesn’t make much sense.

In addition to this, the reason why we have implication -> and turnstile provable assertion |- is that the former is a wff (i.e. statement in the object language) and works on propositions, while the latter is not a wff but rather a statement in the meta language and works on proofs.

The arrow -> is usually used to denote an “internalization” of the meaning of turnstile, into the object language. This allows us, in some sense (depending on the meaning ascribed to ->) to represent the relationships between hypotheses and conclusions in the object language, whereas without it it becomes difficult to reason about on a higher-order level (e.g. most systems do not allow A, (A |- B) |- B).

For more complete examples, you can check out:

  • logic.mm – where I define a basic logical system that contains definitions for and-elim and and-intro and proves some theorems.
  • peano.mm – where I define successor for natural numbers and prove some theorems about ordering of them.

Due to its minimalistic design, when compared to Coq it has no Calculus of Constructions, Inductive Types, etc.

To conclude, I think it’s a fun program to play with, but since it has no “real” framework, I don’t think it’s as industry ready as Coq.