G10. Expressibility and Capturability
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
Now let’s see a few examples of formulas that do express familiar properties:
Evenness
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,
Primeness
The above open formula expresses the property of being prime. In words, it says that
Definition
An open formula
- if
has the property , then is true, and - if
does not have the property , then 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
- if
has the property , then , and - if
does not have the property , then
This definition can be extended to many-place relations (not just one-place properties) in the obvious way.
Expressing a property with a formula
Expressing is to truth as capturing is to derivability.