Credentials Modus operandi Prices Testimonials Contact/Payment Math Home Logic Workplace Math Math Mini-Courses Mind-Crafts Home  Note.  I also offer a 10-Session Live Online Mini-Course which presents a more in-depth treatment of Gödels Incompleteness Theorems without requiring any special background in math or logic. It is intended for enjoyment, as an intellectual pastime, and can also be approached as a more systematic accompaniment to Hofstadter's "Gödel, Escher, Bach" or to Smullyan's Gödelian puzzle books.

#### Gödels Incompleteness Theorems - A Brief Introduction

Over the course of its history, mathematics, as a field of endeavour, has increasingly distanced itself from its empirical roots to become an axiomatic science - i.e. a science whose objects of study are certain systems of mutually interrelated conceptual constructs, formally defined and delimited by means of axioms. This historical development of mathematics is intertwined with, and paralleled by, a change in the nature and role of axioms and axiomatization. Originally understood as the articulation of self-evident, generally agreed-upon propositions pertaining to the external objects, phenomena and principles under study, axiomatization has evolved into the activity of structuring a field of knowledge as a purely deductive system whose objects of study are intellectual constructs fully defined by the propositions put forth as the axioms of the field. Thus, for example, the axiom system of Euclidean geometry has evolved from a set of presumably self-evident certainties concerning a realm of external objects such as points, straight lines and angles, to a set of propositions intended as complete definitions of the concepts of "point", "straight line", "angle", etc., and aimed at recasting the study of geometric objects as a purely deductive pursuit.

This effort to recast mathematics as a network of axiomatic, deductive disciplines had as its main aims the increase in the precision and unequivocality of mathematical discourse, and the freeing of mathematical practice from appeals to intuition and from subjective factors such as being influenced, in judging the correctness of mathematical arguments, by how convincing they are. The crucial question, however, is whether through such a recasting anything is irretrievably lost - i.e. whether in pursuing a purely axiomatic approach to a given discipline the researcher can retain unhampered access to all the relevant properties of the objects under study. In other words, the crucial issue is whether an axiom system is, or can be made, fully adequate to the field of which it is meant to give an account. To be adequate in this sense, the axiom system must not state - or imply - any properties the objects under study do not have, and must give complete access to those relevant properties which the objects do possess.

It is important to understand that within mathematics all projects of axiomatization presuppose an underlying logical framework which constitutes a formalized account of the permissible mathematical reasoning, and which supplies the formal deductive machinery whereby new conclusions will be derived from the selected axioms. In the context of the axiomatization of arithmetic which is the focus of Gödel's Theorems, this underlying deductive framework is the system known as First-Order Predicate Calculus or First-Order Logic. This system regards an elementary proposition - or elementary thought - as consisting in predicating a property or relationship of one or more objects. All more complex propositions are built up from elementary propositions by means of the operations of conjunction ("and"), disjunction ("or"), implication ("if... then..."), negation, and universal and existential quantification ("... holds for all objects", "... holds for some object"). The deductive apparatus consists of a number of specific propositional patterns which are selected as logical axioms, and a number of rules of inference which govern the drawing of conclusions from given premises. Of crucial importance are the following two facts:

• The deductive apparatus of First-Order Logic is deductively sound, in the sense that the logical axioms are universally valid - i.e. true under every interpretation - and none of the rules of inference ever lead from true premises to false a conclusion.
• The system of First-Order Logic is deductively adequate, in the sense that every proposition which is universally valid - i.e. true under every interpretation - can be proven within it.
An example of a universally valid proposition is "For any x and y, if x has property P and x stands in relationship R to y, then x has property P". This proposition is true irrespective of the universe of discourse from which we draw our x's and y's, and irrespective of the interpretation of the predicates P and R. In contrast, the proposition "For any x and y, if x has property P and x stands in relationship R to y, then y has property P" is true under some interpretations of the variables and predicates, and false under others. For example, if we are talking about people, and we take P to mean "is tall" and R to mean "is of the same height as", then the proposition is true. If, on the other hand, we are talking about whole numbers, and we take P to mean "is even" and R to mean "is greater than", then the proposition is false.

Gödel's two Incompleteness Theorems constitute a critical juncture in the process of grappling with the issue of adequate axiomatizations. Their particular focus is the axiomatization of elementary arithmetic, i.e. the possibility of selecting a manageable set of statements A which adequately define the concept of natural numbers (positive integers) and the operations upon them, so that the entirety of arithmetic could be recast as a purely deductive endeavor founded entirely upon the axioms in A. The gist of the Incompleteness Theorems, in the most general terms, is that it is not possible to find a totally adequate set of axioms for arithmetic.

More specifically and more precisely, let us assume that A is a candidate axiom system for arithmetic - i.e., A is a set of statements formulated in the language of First-Order Arithmetic (i.e., a language that includes numeric constants, the relationship of equality, the operations "next number", addition and multiplication, and the logical apparatus of First-Order Logic), and A is manageable, in the sense that the statements of A are either finite in number or can be usefully enumerated in some fashion.

We can then state Gödel's two Incompleteness Theorems as follows:

1st Theorem (Semantic Version):
Assuming that the axiom system A is arithmetically sound - i.e. all the axioms in A are true sentences of arithmetic - it is possible to construct a sentence G which is a true sentence of arithmetic but is not provable from A.

1st Theorem (Syntactic Version):
Assuming that the axiom system A has the following two properties:
• A is sufficiently strong to be a plausible candidate for an axiom system for arithmetic; in particular, it is at least strong enough to permit the derivation, by correct reasoning, of any true elementary arithmetic statement involving the operations of addition, multiplication and successor-taking, and incorporates the principle of natural induction;
• A is consistent - i.e. it is not possible to deduce from it a contradiction;
it is possible to construct, within the language of First-Order Arithmetic, a sentence G such that
- G is not provable from A
- if, in addition, A has a property called omega consistency (see below) then the negation of G is also not provable from A.

In other words, assuming that A is sufficiently strong, and is consistent and omega-consistent, one can construct an arithmetic sentence G which is not decidable from A - in the sense that neither G nor its negation can be deduced from A .

2nd Theorem:
If the axiom system A fulfills the conditions of the Syntactic Version of the 1st Theorem (see above) - i.e. A is sufficiently strong and consistent - then the consistency of A is not provable from A. More precisely, it is possible to formulate, within the language of First-Order Arithmetic, a proposition which in effect expresses the consistency of A - in fact, this can be done in many different ways. Any such proposition will not be provable from A. And if, in addition, A has a property called omega consistency (see below) then the negation of any such proposition will also not be provable from A.

In other words, under the same conditions which govern the undecidablity of the sentence G referred to in the Syntactic Version of the 1st Theorem, any sentence which expresses the consistency of A within the language of First-Order-Arithmetic will, too, be undecidable from A.

The property of omega consistency referenced above is defined as follows: A set of statements S of arithmetic is said to be omega consistent if it is not possible both to prove from S some existential sentence of the form "there exists an x such that P(x)" and also prove, for each specific number n, the negation of P, i.e. the sentence "not P(n)". Omega consistency is stronger than consistency (in the sense that omega consistency implies consistency but not vice versa) and weaker than arithmetic soundness (in the sense that arithmetic soundness implies omega consistency but not vice versa). And it is certainly a condition that we would want any reasonable axiom system for arithmetic to fulfill.

Let us clarify a bit the terms "semantic" and "syntactic", as used above. The propositions from among which the axioms of A are chosen are linguistic strings such as "For all x, x * 0 = 0" or "There exists an x such that x + 2 = x". The logical operation of inference, as it is formalized by First-Order Logic, depends purely on the syntactic structure of propositions: for example, from a proposition of the form "A and B", where A and B are propositions, one is permitted to infer "A" and also to infer "B", and from a proposition of the form "For all x, P(x)", irrespective of what the predicate "P" may be, one is permitted to infer any proposition of the form "P(a)", where a is any constant-symbol. Any notion that can be articulated by invoking solely First-Order proof procedures and the linguistic structure of propositions is a syntactic notion. In particular, the notion of logical consistency of an axiom system - which is defined as the impossibility of deducing from the system both a proposition and its negation - and the notion of omega consistency defined above, are both syntactic notions.

On the other hand, the truth or falseness of a proposition are semantic properties - the proposition becomes true or false only under a specific interpretation of the proposition's components (the predicate symbols, variables and constants which appear in the proposition). As we saw above, the same syntactic entity can be true under one interpretation and false under another. Similarly, validity is a semantic property - even though the fact, mentioned above, that valid propositions coincide with those that are provable from the axioms of First-Order Logic alone, establishes a strict duality between the semantic property of validity and the syntactic property of being a theorem of First-Order Logic. And the arithmetic soundness of an axiom system for arithmetic is a semantic property as well - it has to do with the truth of the axioms under the specific interpretation in which the universe of discourse is taken to be the set of natural numbers with the standard operations of succession, addition, and multiplication.

Note that the notion of an axiom system being sufficiently strong engages, at one and the same time, both syntax and semantics - since it requires the provability from the axioms of a collection of statements expressing basic truths about natural numbers.

Of the two versions of the First Incompleteness Theorem, the Semantic Version is - both in its statement and its proof - more direct, simpler, and more immediately impressive. The Syntactic Version, on the other hand, can be expressed (in a sense which will be explained below) by a formula of arithmetic (which the Semantic version can not), and this formula, moreover, can be proved within arithmetic itself from the chosen axiom system A. This latter fact, in turn, becomes the cornerstone of the proof of the Second Incompleteness Theorem.

##### The Common Framework for the Incompleteness Theorems: Constructing the Gödel Sentence
Both Incompleteness Theorems, whether formulated in semantic or syntactic terms, have as their common object of investigation a set A of propositions (or statements, or formulas - we use these terms interchangeably) intended to serve as an axiom system for the arithmetic of the natural numbers. This axiom system is assumed to be manageable in the sense that its statements are either finite in number or can be usefully enumerated in some fashion - so that it is possible to distinguish, by some reasonable procedure, between what does and what does not belong to our axiom set.

To begin to outline the reasoning behind these theorems, let us consider what is needed in order to construct such a defining set of statements for the natural numbers. First of all, we need an adequate set of symbols. Since we want to talk about numbers and operations on them, we need symbols for the individual numbers themselves - for example, Arabic numerals - as well as for operations on numbers, comparisons between numbers, and all the usual operations of First-Order Predicate Calculus. Thus, our alphabet will consist of

the digits 0 - 9
symbols for variables
+, -, *, =, >
implies-that
it-is-not-the-case-that
or
and
there-exists-a-number such-that
for-every-number
(, )         [for delimiting and grouping phrases]
With this equipment, we can build formulas such as
```(1)      2 + 22 = 24
```
or
```(2)     it-is-not-the-case-that
there-exists-a-number x such-that  x > 2030546.
```
To express the idea that z is a prime number, we could say
```(3)     for-every-number x
for-every-number y
z = x * y  implies-that  either  x = 1  or  y = 1.
```
and to express the idea that y is an even number, we could say
```(4)     there-exists-a-number  x  such-that   x * 2 = y.
```
Notice that unlike in the case of (1), which is true, and (2), which is false, the truth of (3) depends on the value substituted for "z", and the truth of (4) depends on the value substituted for "y". We say that (3) and (4) contain free variables - "z" in the case of (3), and "y" in the case of (4). Substituting numeric constants - i.e. numerals - for the free variables in each formula yields a true or false arithmetic sentence. Thus, for instance, substituting the numeral "375" for "y" in (4) yields
```(5)     there-exists-a-number  x  such-that   x * 2 = 375,
```
which, under the standard arithmetic interpretation, falsely states that 375 is divisible by 2.

Building upon these simpler elements, we can express more complex ideas such as "Every even number is the product of two primes" or "There is no largest prime number".

Such an extreme formalization of the vocabulary is not usually adopted in everyday mathematical practice. Mathematicians, like all scientists, employ a wide vocabulary of formal and less-formal terms that have sufficiently precise, agreed-upon meanings and can be used freely without the danger of hidden error or misunderstanding. An uncompromisingly formal and rigorous approach is needed only when either such a danger becomes a paramount concern, or when the investigation focuses on the capabilities and limits of mathematical practice - as is the case with Gödel's Theorems. To embark on this kind of investigation, it is highly useful to posit the language employed in this practice as built up from a limited number of simple building blocks from which all more complex linguistic practices can be constructed by some set of rigorous rules. The exact number and scope of the selected building blocks is not relevant; what matters is their manageability, the precise rules of their usage, and their joint expressive power.

The common thread of Gödel's Incompleteness Theorems is that arithmetic, understood as a branch of mathematics whose goal is to investigate actual properties of the natural numbers, cannot be fully axiomatized. However carefully we choose our axioms, and however many we select, if the axiom set is manageable - so that we can know by some simple procedure what is and what is not an axiom - there will always be actual properties of the natural numbers that we will not be able to "get at" from these axioms through a purely deductive procedure - i.e. statements which must in actuality hold, but which cannot be proved from the chosen axiom system. Notice that the concept of manageability is crucial. We could say, for instance: "Let's simply take as our axioms all true statements about the natural numbers." Such an axiom system would be complete and consistent: one could, in principle, prove every true statement, and no false ones. In practice, however, faced with a complex arithmetic statement, we would have no way of recognizing whether or not it was an axiom, and the system would therefore be actually useless for proving or disproving anything.

This intuitive notion of "manageability", and its relationship to arithmetic itself - specifically the fact that it can be translated very precisely into purely arithmetic concepts - lies at the very heart of Gödel's proofs. The crux of the argument is that if our linguistic means are to be adequate for arithmetic, they have to be expressive enough to permit us to talk about things like divisibility, decomposition into prime numbers, etc. However, if the system possesses that level of expressiveness (which is the least we would expect of it), it turns out to be powerful enough to also "talk", in a certain sense which we will make clearer below, about anything that is "manageable" - in particular, about any useful axiom system we may construct within it, as well as about the proof procedures that constitute "correct reasoning". And this very potential for self-referentiality on the part of the system makes it possible to construct within the system sentences which, one might say, outstrip the system's own deductive capabilities.

The main trick in the proofs of the Incompleteness Theorems is to assign to every statement of arithmetic a natural number. This mapping allows us then to construct statements which, while talking about numbers - as is proper for arithmetic - can be interpreted as "talking" about statements themselves. Not any numbering is equally useful here. The numbering should permit an elegant and invertible translation between the kinds of things one does with linguistic symbols in a deductive system and operations on natural numbers.

The most basic operation on linguistic symbols is stringing them together, concatenating them. Thus, the desirable kinds of numberings should effect a simple rule for forming the number corresponding to the concatenation of two linguistic strings. If, for example, the basic alphabet of our language consisted of only ten symbols, we could propose the following numbering:

• Assign the digits 0 - 9 to the basic symbols

• If S1 and S2 are two strings in our arithmetic language, and N1 and N2 are their corresponding numbers, assign to the concatenation S1S2 the number whose corresponding Arabic numeral consists of the Arabic numeral for N1 followed by the Arabic numeral for N2.
Thus, for example, if N1 and N2 - i.e. the numbers assigned to S1 and S2 - were those expressed, respectively, by the Arabic numerals "23341" and "763", then S1S2 would have corresponding to it the number whose Arabic-numeral expression is "23341763".

Observe that this concatenation rule has a relatively simple expression in the language of arithmetic. The number expressed by "23345763" is obtained from our N1 and N2 by multiplying N1 by 1000 (10 to the power 3 - 3 being the length of the string S2) and adding N2 to the result.

A similar numbering can be devised for the arithmetical alphabet described above, even though it has more than ten symbols. Instead of using base 10, as we do in daily life, we can use a base equal to the number of symbols in our arithmetical alphabet. This requires the invention of a few new digits, but preserves the above type of relatively simple rule for concatenation.

The requirement that the selected numbering scheme should yield an arithmetically graceful rule for mapping concatenation has very powerful repercussions. Not surprisingly, our notions of what constitutes a well-formed formula, a formula with free variables, or a proof from a given set of axioms, can all be expressed as rules for how symbols are stringed together, i.e. as rules of concatenation. And at the same time, the requirement that our axiom system for arithmetic be "manageable" implies, as it turns out, that one can formulate an arithmetically cogent characterization of the set of numbers corresponding to the linguistic strings selected as axioms. Thus, once we have a proper numbering for the elements of the language (we will refer to such a numbering as as a Gödel numbering, or a G-numbering for short), and as long as our axiom system A is manageable in the sense indicated above, the following numerical properties all turn out to be expressible within arithmetic itself:

• x is the G-number of an arithmetical formula.
• x is the G-number of the formula obtained by substituting y for all free variables in the formula with G-number z
• x is the G-number of one of the axioms in A
• x is the G-number of a formula which is provable from A.

We will now use these facts to perform a construction which is the heart of all the Incompleteness Theorems - the construction of the Gödel sentence for A. In view of the expressibility of the properties and relations listed above, it is possible to construct a formula of arithmetic with two free variables which can be "encapsulated" as

```
(A)    y is the G-number of the formula obtained by substituting x
for all free variables in the formula whose G-number is x.
```
as well as a formula of arithmetic with one free variable which can be "encapsulated" as
```
(B)    for-every-number z
if  z is the G-number of the formula obtained by substituting x
for all free variables in the formula whose G-number is x
then z is not the G-number of a formula provable from A.
```
[By the term "encapsulation", as we just used it above, we mean a summary rendering, in English, of the salient semantic content of an arithmetical formula.]

Remembering that (B) can be treated as a formula of pure arithmetic, let us, for the sake of clarity, express the same idea more understandably. What (B) says, can be formulated as

```
(C)   There is no proof from A for the formula obtained by substituting x
for all free variables in the formula whose G-number is x.
```
The formula for which (B) and (C) are shorthands is a formula of arithmetic containing one free variable, "x". Since it is a formula of arithmetic, it itself has a G-number. If we had taken the trouble to spell out (C) in all its gory arithmetic detail, and to give a precise description of our G-numbering, we could in fact calculate this number (which would, undoubtedly, turn out to be quite large). In lieu of this calculation, let us call this number c. Thus, c is the G-number of the (fully spelled out) formula (C).

Let us substitute c for "x" in (C). This gives us, for A, the formula known as the Gödel sentence:

```
(GSentA)   There is no proof from A for the formula obtained by substituting c
for all free variables in the formula whose G-number is c.
```
GSentA is a formula of arithmetic. It states that a certain formula of arithmetic is not provable from A. But which formula is that? The one obtained by substituting c for all free variables in the formula whose G-number is c, i.e. the one obtained by substituting c for x in (C). But the formula obtained by substituting g for x in (C) is GSentA itself. Thus, GSentA basically says "There is no proof from A for the formula GSentA", or "I AM NOT PROVABLE FROM A".

Note that since the Gödel sentence, when fully spelled out as a formula of arithmetic, has to contain a spelled-out expression of the property "x is the G-number of one of the axioms in A", it will be a different sentence for different choices of A. So although the construction of the Gödel sentence always proceeds along the same lines, its exact formal content will depend not only on the selected Gödel numbering, but also on the actual axiom system under consideration. This is why we have subscripted its shorthand name GSent with "A".

##### Gödels First Incompleteness Theorem - Semantic Version
The 1st Incompleteness Theorem, in its semantic formulation, can be stated as follows:
Assume that A is a manageable (in the sense indicated above) set of arithmetic statements that is also arithmetically sound - i.e. such that if we reason correctly using only A as our starting point, we will never arrive at any conclusion that does not actually hold in the realm of the natural numbers. Then it is possible to construct an arithmetical sentence which is actually true in the realm of natural numbers but cannot be proved from A.
To sketch the proof of the theorem, we note that we can construct for A the Gödel sentence GSentA, as outlined above. GSentA is a formula of arithmetic which, when understood as per the mediation of the chosen G-numbering, states that the formula GSentA is not provable from A.

Is GSentA provable from A? If it is, then what it states is false, and so we have a false formula which can be proved. Since, however, we have assumed that A is arithmetically sound - so that we cannot prove from it any arithmetically false proposition - we are forced to conclude that GSentA is in fact not provable. And since this non-provability is exactly what GSentA asserts, GSentA is true. So we have indeed constructed a sentence which, although arithmetically true, cannot be proved from A.

What would happen if we simply enlarged our axiom system A by adding the sentence GSentA to it as another axiom? Would the resulting axiom system now permit us to prove all true statements about the natural numbers? Well, since this new axiom system - which we might call A' - has GSentA as one of its axioms, it would certainly permit us to prove GSentA itself - in addition, of course, to everything that we could already prove from A. However, we can now construct a new Gödel sentence, GSentA', for A'. Since A' is different from A, the sentence GSentA' will be different from GSentA; but by the same argument we just used above, it will, in turn, be a true sentence of arithmetic which is unprovable from A'.

##### Gödels First Incompleteness Theorem - Syntactic Version
The Syntactic Version of the 1st Incompleteness Theorem can be stated as follows:
Assume that A is a manageable (in the sense indicated above) set of arithmetic statements that is also sufficiently strong (in the sense that it permits us to prove any true elementary arithmetical statement involving the operations of addition, multiplication and successor-taking, and it incorporates the principle of natural induction) and consistent - i.e. it is not possible to deduce from A a contradiction. Then it is possible to construct an arithmetical sentence which is not provable from A and such that, under the additional assumption that A is omega consistent, the negation of this sentence is also not provable from A. Thus, if A is omega-consistent, it is possible to construct a sentence of arithmetic which can neither be proved nor disproved from A.
In order to outline the proof of the Syntactic Version, we need to introduce the notion of a formula of arithmetic capturing a property of the natural numbers. It is best to present this notion of capturing in comparison and contrast to the notion of expressing which we have been using loosely in the previous argument. Let us define this notion more precisely:
A formula of arithmetic F with one free variable expresses a property P of the natural numbers if the following holds for any natural number n:

- If n has property P, then F(n) is true.
- If n does not have property P, then the negation of F(n) is true.

We can now define the notion of capturing:
A formula of arithmetic F with one free variable captures a property P of the natural numbers relative to an axiom system A if the following holds for any natural number n:

- If n has property P, then F(n) is provable from A.
- If n does not have property P, then the negation of F(n) is provable from A.

This definition of "capturing" can be extended, in an obvious manner, from properties of single numbers to numeric relations between two or more numbers (in which case the formula F would need to have two or more free variables).

Note that whether or not a property can be expressed by a formula of arithmetic has to do exclusively with the power of the language, whereas the question of whether or not it can be captured has to do, in addition, with the power of the selected axiom system. Thus, for example, the formula

```      there-exists-a-number  z  such-that   x * z = y.
```
is a formula with two free variables which expresses the relation "y is divisible by x"; but if we choose a very weak axiom system - for example, one consisting only of the axiom "0 + 1 = 1" - the property "y is divisible by x" will not be captured by this (or any other) formula.

In the context of the Syntactic Version of the 1st Incompleteness Theorem, the crucial result concerning capturability is the following: if our axiom system A is manageable and sufficiently strong in the sense defined above, then, given a G-numbering, the following numerical properties all turn out to be capturable relative to A:

• x is the G-number of an arithmetical formula.
• x is the G-number of the formula obtained by substituting y for all free variables in the formula with G-number z
• x is the G-number of one of the axioms in A
• x is the G-number of a proof, from A, of the formula with G-number y.
We can now outline the proof of the Syntactic Version of the 1st Theorem. Let us assume that our chosen axiom system A has the properties postulated in the Syntactic Version. We select a G-numbering and construct, for our A, a Gödel sentence GSentA. We will show that GSentA is the sentence whose existence is asserted by the Syntactic Version - i.e. that under the assumption that A is consistent, GSentA is not provable from A, and under the assumption that A is omega-consistent the negation of GSentA is not provable from A.

Thus, the proof has two parts:

1. If A is consistent, then GSentA is not provable from A.

Let us imagine, to the contrary, that GSentA is provable from A, and let p be the G-number of its proof. Let us denote by g the G-number of GSentA. As we said above, there is a formula of arithmetic - call it Proof(x,y) - that expresses and captures the relationship "x is the G-number of a proof, from A, of the formula with G-number y". Thus we can encapsulate this formula as:

```(Proof(x,y))     x is the G-number of a proof, from A,
of the formula with G-number y.
```
Since the formula Proof(x,y) captures the relation it expresses, every true specific instance of Proof(x,y) is provable from A. In particular, by our assumption that p is the G-number of a proof of GSentA, we have to conclude that the true formula
```(Proof(p,g))     p is the G-number of a proof, from A,
of the formula with G-number g
```
which is an instance of Proof(x,y), is provable from A.

At the same time, GSentA, which states that GSentA is not provable from A, can be encapsulated as

```(GSentA)   for-every-number x
it-is-not-the-case-that x is the G-number of a proof, from A,
of the formula with G-number g.
```
If this is provable from A - as we have assumed it is - then, by the inference rules governing universal quantification in First-Order Logic, so is the formula
```(GSentA-for-p)   it-is-not-the-case-that
p is the G-number of a proof, from A,
of the formula with G-number g
```
which is a specific instance of the universal-quantifier formula GSentA.

But GSent-for-p is the negation of Proof(p,g) - and yet we have had to conclude that both are provable from A. Thus our experimental assumption of the provability, from A, of GSentA, has led us to the conclusion that there exists a sentence which can be both proved and refuted from A, contradicting the assumption that A is consistent. Hence, if A is consistent, GSentA is not provable from A.

2. If A is omega-consistent, then the negation of GSentA is not provable from A.

Let us imagine, to the contrary, that the negation of GSentA is provable from A. If, once again, we denote by g the G-number of GSentA, we can write this negation as

```(neg-GSentA)   there-exists-a-number x such-that
x is the G-number of a proof, from A,
of the formula with G-number g.
```
Since omega-consistency is stronger than consistency, A is consistent, and we can apply to the present case the conclusion we arrived at in the first part of the proof of the Syntactic Version: GSentA is not provable from A. Since the relationship "x is the G-number of a proof, from A, of the formula with G-number y" is capturable in A, there is a formula of arithmetic with one free variable which can be encapsulated as
```(proves-GSentA)   x is the G-number of a proof, from A,
of the formula with G-number g
```
which captures the relation it expresses and which is false for every specific natural number. Consequently, for each natural number n, the formula
```(neg-n-proves-GSentA)   it-is-not-the-case-that
n is the G-number of a proof, from A,
of the formula with G-number g
```
obtained by substituting n for the free variable in the negation of proves-GSentA, must be provable from A. We are thus led to conclude that one can prove from A both the formula neg-GSentA, which states the existence of a natural number having a certain property, and, for each specific natural number n, the formula neg-n-proves-GSentA which states that n does not posses that same property. This contradicts the assumption that A is omega-consistent. We have to conclude, therefore, that our experimental assumption of the provability, from A, of the negation of GSentA, is untenable: if A is omega-consistent, the negation of GSentA must be unprovable from A. This concludes the proof of the Syntactic Version of the 1st Incompleteness Theorem.
##### Gödels Second Incompleteness Theorem
The Second Incompleteness Theorem can be stated as follows:
Assume that A is a manageable (in the sense indicated above) set of arithmetic statements that is also sufficiently strong (in the sense that it permits us to prove any true elementary arithmetical statement involving the operations of addition, multiplication and successor-taking, and it incorporates the principle of natural induction) and consistent - i.e. it is not possible to deduce from A a contradiction. Then it is not possible to prove from A its own consistency. More precisely, if ConsA is any formula of arithmetic that expresses the consistency of A, then ConsA is not provable from A. Furthermore, if, in addition, A is omega consistent, then the negation of ConsA is also not provable from A. Thus, if A is omega-consistent, ConsA is undecidable - it can neither be proved nor disproved from A.
The assumptions of the 2nd Incompleteness Theorem are identical to those of the Syntactic Version of the 1st Theorem, and the proof of the unprovability of ConsA is intimately tied to the proof of Part 1 of the Syntactic Version, which we outlined above: that if our axiom system A is consistent, then the Gödel sentence GSentA is not provable from A. What is of crucial importance about this proof is that it can actually be formalized within A itself. In other words, if ConsA is a formula of arithmetic which expresses the fact that A is consistent, and which can thus be encapsulated as
```(ConsA)   The axiom system A is consistent.
```
then we can construct a formula of arithmetic - call it SyntVer1A - which expresses the statement of Part 1 of the Syntactic version of the 1st Incompleteness Theorem, and can thus be encapsulated as
```(SyntVer1A)   ConsA implies-that (GSentA is not provable from A)
```
and such that SyntVer1A is provable from A.

Note that since the statement "GSentA is not provable from A" is equivalent to GSentA itself, we can rephrase the above encapsulation of SyntVer1A to simply say

```(SyntVer1A)   ConsA implies-that GSentA.
```
And - just to repeat ourselves for emphasis - the above formula SyntVer1A is provable from A.

Our earlier discussion gives some general idea of what GSentA, as a fully spelled-out formula of arithmetic, may actually contain; but what would be the actual arithmetic contents of ConsA? There are many alternative ways of formulating, within arithmetic, the idea that A is consistent. Perhaps the simplest is to utilize the fact that, by the rules governing the operation of implication in First-Order Predicate Logic, a contradiction implies any proposition; consequently, if an axiom system is inconsistent, any proposition whatsoever can be proved from it. In particular, if the axiom system is inconsistent - and only if it is inconsistent - it is possible to prove from it the negation of one of its own axioms. Thus, given our axiom set A, all we have to do is to form the negation of any of its axioms - let's denote the selected axiom by As, and the G-number of its negation by neg-as - and then construct an arithmetic formula which in effect says "There is no proof, from A, for the formula with G-number neg-as". This formula can then serve as our ConsA.

We can now outline the proof of the Second Incompleteness Theorem. The proof, once again, has two parts:

1. If A is consistent, then ConsA is not provable from A.

Let us imagine, to the contrary, that the formula ConsA is provable from A. As we discussed above, the formula SyntVer1A is also provable from A. But SyntVer1A is an if-then sentence that has ConsA as its "if" clause and GSentA as its "then" clause. It is one of the inference rules of First-Order Logic - a rule called Modus Ponens - that if an if-then statement and its "if" clause have both been deductively established, we are permitted to deduce the "then" clause. Consequently, if we could prove from A both SyntVer1A and ConsA, we could use Modus Ponens to deduce GSentA, and it , too, would be provable from A - in contradiction to the Syntactic Version of the First Incompleteness Theorem. Thus our experimental assumption of the provability of ConsA is not tenable, and we are obliged to conclude that ConsA is not provable from A.

2. If A is omega-consistent, then the negation of ConsA is not provable from A.

Let us imagine, to the contrary, that the negation of ConsA is provable from A. To fix attention, let us work with the specific version of ConsA that we discussed above, i.e.

```(ConsA)   There is no proof, from A, for the formula with G-number neg-as.
```
The negation of ConsA can then be encapsulated as
```(neg-ConsA)   there-exists-a-number x such-that
x is the G-number of a proof, from A,
of the formula with G-number neg-as.
```
Since omega-consistency is stronger than consistency, A is consistent, and therefore it is in fact not possible to prove from A the negation of one of its axioms - in particular, axiom As. Since the relationship "x is the G-number of a proof, from A, of the formula with G-number y" is capturable in A, there is a formula of arithmetic with one free variable which can be encapsulated as
```(proves-neg-AsA)   x is the G-number of a proof, from A,
of the formula with G-number neg-as.
```
which captures the relation it expresses and which is false for every specific natural number. Consequently, for each natural number n, the formula
```(neg-n-proves-neg-AsA)   it-is-not-the-case-that
n is the G-number of a proof, from A,
of the formula with G-number neg-as
```
obtained by substituting n for the free variable in the negation of proves-neg-AsA, must be provable. We are thus led to conclude that one can prove from A both the formula neg-ConsA, which states the existence of a natural number having a certain property, and, for each specific natural number n, the formula neg-n-proves-neg-AsA which states that n does not posses that same property. This contradicts the assumption that A is omega-consistent. We have to conclude, therefore, that our experimental assumption of the provability, from A, of the negation of ConsA, is untenable: if A is omega-consistent, the negation of ConsA is unprovable from A. This concludes the proof of the Second Incompleteness Theorem.