A critical step in Godel’s proof is his construction of “the Godel sentence” which, when interpreted, means “this statement cannot be derived within this formal system”. The formal system in which he constructed this statement is one that deals with the natural numbers, first order logic, and elementary arithmetic such as the successor function.

How in the world, then, did he express such a statement? It is certainly not obvious that it’s possible. After all, it is not true that any formal system can express any statement, so the ability to write down a formula that has the above meaning is not a given. It takes a lot of work to demonstrate that such a statement can be expressed.

We’re not going to demonstrate how Godel expressed this statement in this post, but rather talk about the notion of expressibility in general. We want to know, precisely, what it means to be able to express something in a formal system, as well as the stronger property of capturing (or representing1).

First, let’s recall statements that cannot be expressed within particular formal systems. We’ve seen examples of this already. In the Add system, we could not express (true) statements of addition that dealt with negative numbers. When discussing first vs second order logic, we noted that first order logic could not quantify over sets. So, first order logic would not be able to express the statement “there exists a property \(P\) that has 3 elements”.

Now let’s see a few examples of formulas that do express familiar properties:

Evenness

\[\exists v (2 \times v = x)\]

The above formula is an open formula that expresses the property of being even. A formula is open when there are one or more variables that are not bound. In this case, \(v\) is bound by the quantifier \(\exists\), but \(x\) is not. So this formula has one free variable: \(x\). This open formula expresses the property of being even because for any number \(x\), this formula is true iff \(x\) is even. Put another way, this open formula has the set of even numbers as its extension.

Primeness

\[(x \neq 1 \land \forall u \forall v (u \times v = x \supset (u = 1 \lor v = 1)))\]

The above open formula expresses the property of being prime. In words, it says that \(x \neq 1\) and for all two numbers \(u\) and \(v\), if \(u \times v = x\) then either \(u = 1\) or \(v = 1\).

Definition

An open formula \(\varphi(x)\) can express a property \(P\) iff, for any \(n\):

  • if \(n\) has the property \(P\), then \(\varphi(\bar{n})\) is true, and
  • if \(n\) does not have the property \(P\), then \(\lnot \varphi(\bar{n})\) is true.

This definition can be extended to many-place relations (not just one-place properties) in the obvious way.

Capturing Relations

There is a stronger version of expressing a property (or relation) which is capturing a property (or relation).

A formal system \(T\) can capture a property \(P\) by the open formula \(\varphi(x)\) iff, for any \(n\):

  • if \(n\) has the property \(P\), then \(T \vdash \varphi(\bar{n})\), and
  • if \(n\) does not have the property \(P\), then \(T \vdash \lnot \varphi(\bar{n})\)

This definition can be extended to many-place relations (not just one-place properties) in the obvious way.

Expressing a property with a formula \(\varphi(x)\) means that the \(\varphi(x)\) is true iff \(x\) has the relevant property, capturing a property means that \(\varphi(x)\) is derivable in the formal system iff \(x\) has the relevant property.

Expressing is to truth as capturing is to derivability.

  1. In another example of Naming Is Hard™, the notion of capturability goes by other names, most notably representability (which is used by GEB). ↩