Note. I also offer a 10Session Live Online MiniCourse which presents a more indepth 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 selfevident, generally agreedupon 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 selfevident 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 FirstOrder Predicate Calculus or FirstOrder 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 FirstOrder 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 FirstOrder 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 FirstOrder 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 FirstOrder 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 successortaking, 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 FirstOrder 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 omegaconsistent, 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 FirstOrder 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 FirstOrderArithmetic 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 FirstOrder 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 constantsymbol. Any notion that can be articulated by invoking solely FirstOrder 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 FirstOrder Logic alone, establishes a strict duality between the semantic property of validity and the syntactic property of being a theorem of FirstOrder 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 FirstOrder
Predicate Calculus. Thus, our alphabet will consist of
the digits 0  9
symbols for variables
+, , *, =, >
impliesthat
itisnotthecasethat
or
and
thereexistsanumber suchthat
foreverynumber
(, ) [for delimiting and grouping phrases]
With this equipment, we can build formulas such as
(1) 2 + 22 = 24
or
(2) itisnotthecasethat
thereexistsanumber x suchthat x > 2030546.
To express the idea that z is a prime number, we could say
(3) foreverynumber x
foreverynumber y
z = x * y impliesthat either x = 1 or y = 1.
and to express the idea that y is an even number, we could say
(4) thereexistsanumber x suchthat 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) thereexistsanumber x suchthat 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 lessformal terms
that have sufficiently precise, agreedupon 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 selfreferentiality 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 S_{1} and S_{2} are two strings in our arithmetic language,
and N_{1} and N_{2} are their corresponding numbers,
assign to the concatenation S_{1}S_{2} the number whose corresponding Arabic
numeral consists of the Arabic numeral for N_{1} followed
by the Arabic numeral for N_{2}.
Thus, for example, if N_{1} and N_{2}  i.e. the numbers assigned
to S_{1} and S_{2} 
were those expressed, respectively, by the Arabic numerals
"23341" and "763", then S_{1}S_{2} would have corresponding to it the number whose
Arabicnumeral 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 N_{1} and N_{2} by multiplying N_{1} by 1000 (10 to the power 3  3 being
the length of the string S_{2}) and adding N_{2} 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 wellformed 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 Gnumbering 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 Gnumber of an arithmetical formula.

x is the Gnumber of the formula obtained by substituting y for
all free variables in the formula with Gnumber z

x is the Gnumber of one of the axioms in A

x is the Gnumber 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 Gnumber of the formula obtained by substituting x
for all free variables in the formula whose Gnumber is x.
as well as a formula of arithmetic with one free variable which can be "encapsulated" as
(B) foreverynumber z
if z is the Gnumber of the formula obtained by substituting x
for all free variables in the formula whose Gnumber is x
then z is not the Gnumber 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 Gnumber 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 Gnumber.
If we had taken the trouble to spell out (C) in all its gory
arithmetic detail,
and to give a precise description of our Gnumbering, 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 Gnumber 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:
(GSent_{A}) There is no proof from A for the formula obtained by substituting c
for all free variables in the formula whose Gnumber is c.
GSent_{A} 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
Gnumber 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 GSent_{A} itself. Thus, GSent_{A} basically says "There is no proof from A for the formula GSent_{A}", 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 spelledout expression of the property "x is the Gnumber 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 GSent_{A}, as outlined above. GSent_{A} is a formula of arithmetic which, when understood as per the mediation of the chosen Gnumbering, states that the formula GSent_{A} is not provable from A.
Is GSent_{A} 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 GSent_{A} is in fact
not provable. And since this nonprovability is exactly what GSent_{A}
asserts, GSent_{A} 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 GSent_{A} 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 GSent_{A} as one of its axioms, it would certainly permit us to prove GSent_{A} itself  in addition, of course, to everything that we could already prove from A. However, we can now construct a new Gödel sentence, GSent_{A'}, for A'. Since A' is different from A, the sentence GSent_{A'} will be different from GSent_{A}; 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 successortaking, 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 omegaconsistent, 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
thereexistsanumber z suchthat 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 Gnumbering, the following numerical properties all
turn out to be capturable relative to A:

x is the Gnumber of an arithmetical formula.

x is the Gnumber of the formula obtained by substituting y for
all free variables in the formula with Gnumber z

x is the Gnumber of one of the axioms in A

x is the Gnumber of a proof, from A, of the formula with Gnumber 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 Gnumbering and construct, for our A, a Gödel sentence GSent_{A}. We will show that GSent_{A} is the sentence whose existence is asserted by the Syntactic Version  i.e. that under the assumption that A is consistent, GSent_{A} is not provable from A, and under the assumption that A is omegaconsistent the negation of GSent_{A} is not provable from A.
Thus, the proof has two parts:
1. If A is consistent, then GSent_{A} is not provable from A.
Let us imagine, to the contrary, that GSent_{A} is provable from A, and let p be the Gnumber of its proof. Let us denote by g the Gnumber of GSent_{A}. As we said above, there is a formula of arithmetic  call it Proof(x,y)  that expresses and captures the relationship "x is the Gnumber of a proof, from A, of the formula with Gnumber y". Thus we can encapsulate this formula as:
(Proof(x,y)) x is the Gnumber of a proof, from A,
of the formula with Gnumber 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 Gnumber of a proof of GSent_{A}, we have to conclude that the true formula
(Proof(p,g)) p is the Gnumber of a proof, from A,
of the formula with Gnumber g
which is an instance of Proof(x,y), is provable from A.
At the same time, GSent_{A}, which states that GSent_{A} is not provable from A, can be encapsulated as
(GSent_{A}) foreverynumber x
itisnotthecasethat x is the Gnumber of a proof, from A,
of the formula with Gnumber g.
If this is provable from A  as we have assumed it is  then, by the inference rules governing universal quantification in FirstOrder Logic, so is the formula
(GSent_{A}forp) itisnotthecasethat
p is the Gnumber of a proof, from A,
of the formula with Gnumber g
which is a specific instance of the universalquantifier formula GSent_{A}.
But GSentforp 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 GSent_{A}, 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, GSent_{A} is not provable from A.
2. If A is omegaconsistent, then the negation of GSent_{A} is not provable from A.
Let us imagine, to the contrary, that the negation of GSent_{A} is provable from A. If, once again, we denote by g the Gnumber of GSent_{A}, we can write this negation as
(negGSent_{A}) thereexistsanumber x suchthat
x is the Gnumber of a proof, from A,
of the formula with Gnumber g.
Since omegaconsistency 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: GSent_{A} is not provable from A. Since the relationship "x is the Gnumber of a proof, from A, of the formula with Gnumber y" is capturable in A, there is a formula of arithmetic with one free variable which can be encapsulated as
(provesGSent_{A}) x is the Gnumber of a proof, from A,
of the formula with Gnumber g
which captures the relation it expresses and which is false for every specific natural number. Consequently, for each natural number n, the formula
(negnprovesGSent_{A}) itisnotthecasethat
n is the Gnumber of a proof, from A,
of the formula with Gnumber g
obtained by substituting n for the free variable in the negation of provesGSent_{A}, must be provable from A. We are thus led to conclude that one can prove from A both the formula negGSent_{A}, which states the existence of a natural number having a certain property, and, for each specific natural number n, the formula negnprovesGSent_{A} which states that n does not posses that same property. This contradicts the assumption that A is omegaconsistent. We have to conclude, therefore, that our experimental assumption of the provability, from A, of the negation of GSent_{A}, is untenable: if A is omegaconsistent, the negation of GSent_{A} 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 successortaking, 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 Cons_{A} is any formula of arithmetic that expresses the consistency of A, then Cons_{A} is not provable from A. Furthermore, if, in addition, A is omega consistent, then the negation of Cons_{A} is also not provable from A. Thus, if A is omegaconsistent, Cons_{A} 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 Cons_{A} 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 GSent_{A} 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 Cons_{A} is a formula of arithmetic which expresses the fact that A is consistent, and which can thus be encapsulated as
(Cons_{A}) The axiom system A is consistent.
then we can construct a formula of arithmetic  call it SyntVer1_{A}  which expresses the statement of Part 1 of the Syntactic version of the 1st Incompleteness Theorem, and can thus be encapsulated as
(SyntVer1_{A}) Cons_{A} impliesthat (GSent_{A} is not provable from A)
and such that SyntVer1_{A} is provable from A.
Note that since the statement "GSent_{A} is not provable from A" is equivalent to GSent_{A} itself, we can rephrase the above encapsulation of SyntVer1_{A} to simply say
(SyntVer1_{A}) Cons_{A} impliesthat GSent_{A}.
And  just to repeat ourselves for emphasis  the above formula SyntVer1_{A} is provable from A.
Our earlier discussion gives some general idea of what GSent_{A}, as a fully spelledout formula of arithmetic, may actually contain; but what would be the actual arithmetic contents of Cons_{A}? 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 FirstOrder 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 A_{s}, and the Gnumber of its negation by nega_{s}  and then construct an arithmetic formula which in effect says "There is no proof, from A, for the formula with Gnumber nega_{s}". This formula can then serve as our Cons_{A}.
We can now outline the proof of the Second Incompleteness Theorem. The proof, once again, has two parts:
1. If A is consistent, then Cons_{A} is not provable from A.
Let us imagine, to the contrary, that the formula Cons_{A} is provable from A. As we discussed above, the formula SyntVer1_{A} is also provable from A. But SyntVer1_{A} is an ifthen sentence that has Cons_{A} as its "if" clause and GSent_{A} as its "then" clause. It is one of the inference rules of FirstOrder Logic  a rule called Modus Ponens  that if an ifthen 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 SyntVer1_{A} and Cons_{A}, we could use Modus Ponens to deduce GSent_{A}, 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 Cons_{A} is not tenable, and we are obliged to conclude that Cons_{A} is not provable from A.
2. If A is omegaconsistent, then the negation of Cons_{A} is not provable from A.
Let us imagine, to the contrary, that the negation of Cons_{A} is provable from A. To fix attention, let us work with the specific version of Cons_{A} that we discussed above, i.e.
(Cons_{A}) There is no proof, from A, for the formula with Gnumber nega_{s}.
The negation of Cons_{A} can then be encapsulated as
(negCons_{A}) thereexistsanumber x suchthat
x is the Gnumber of a proof, from A,
of the formula with Gnumber nega_{s}.
Since omegaconsistency 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 A_{s}. Since the relationship "x is the Gnumber of a proof, from A, of the formula with Gnumber y" is capturable in A, there is a formula of arithmetic with one free variable which can be encapsulated as
(provesnegA_{s}_{A}) x is the Gnumber of a proof, from A,
of the formula with Gnumber nega_{s}.
which captures the relation it expresses and which is false for every specific natural number. Consequently, for each natural number n, the formula
(negnprovesnegA_{s}_{A}) itisnotthecasethat
n is the Gnumber of a proof, from A,
of the formula with Gnumber nega_{s}
obtained by substituting n for the free variable in the negation of provesnegA_{s}_{A}, must be provable. We are thus led to conclude that one can prove from A both the formula negCons_{A}, which states the existence of a natural number having a certain property, and, for each specific natural number n, the formula negnprovesnegA_{s}_{A} which states that n does not posses that same property. This contradicts the assumption that A is omegaconsistent. We have to conclude, therefore, that our experimental assumption of the provability, from A, of the negation of Cons_{A}, is untenable: if A is omegaconsistent, the negation of Cons_{A} is unprovable from A.
This concludes the proof of the Second Incompleteness Theorem.
Copyright © 2006 Malgosia Askanas. All rights reserved.