| Home | Blog index | Previous | Next | About | Privacy policy |
If the proof of a mathematical result is very complicated, there might be doubts about whether the proof is complete and correct. Issues like this could be resolved immediately if it was practical to present, alongside research articles, proofs of the mathematical results written in a language for which the reasoning could be checked by computer.
The foundations of the necessary language were laid by Aristotle around 350 BC, and the remaining ingredients were introduced by Gottlob Frege in 1879. Frege's system used a cumbersome two-dimensional notation and was more general than needed, and the key part of the system was isolated and simplified to a one-dimensional notation by Bertrand Russell and others. It is called Lower Predicate Calculus, abbreviated to LPC, or First-Order Predicate Calculus.
In his Ph.D. thesis, completed in 1929, Kurt Gödel proved that everything that can be proved in LPC, can be proved using just a handful of basic principles of reasoning. This result, called the Completeness Theorem, was published in 1930, the year before the appearance of Gödel's famous Incompleteness theorems about axioms for arithmetic.
Gödel's Completeness Theorem means that computer programs for facilitating and checking reasoning in LPC can usefully be divided into two modules. The first module will detect and report all errors of reasoning in proofs that use only the basic principles of reasoning. Its source code will evolve towards a steady state, and a person who wants to be sure that proofs are valid only needs to check the source code of this module. The second module will make available an ever-growing range of more sophisticated principles of reasoning, that will in due course start to include steps of reasoning used in research papers, and will replace each use of a sophisticated principle by a sequence of steps using only the basic principles.
The remaining prerequisites for a practical system for producing computer-checkable proofs of the mathematical results in research articles are a built-in framework for defining and using abbreviations, and a large and growing knowledge base of useful definitions and results that can be referred to.
In its traditional form, LPC is a little awkward to work with. One effect of this is that part of the way through the chapter on set theory in a well-known textbook, "Introduction to Mathematical Logic," by Elliott Mendelson, the author substantially gives up presenting proofs in LPC, and starts presenting them in English instead.
Part of the problem is that statements in the traditional form of LPC resemble mathematical formulae. But research papers in mathematics are not usually sequences of formulae: they are usually written in English, interspersed with formulae. This suggests that alternative forms of LPC might exist, that are equivalent to the traditional form, but flow more like a natural language.
Such alternative forms of LPC, that resemble a natural language, do indeed exist. One of them is called Verish, which is a blend of the words "Verify" and "English". It has the advantage that a program of the above structure for facilitating and checking reasoning is freely available for it, and a start has been made on the knowledge base.
In the remainder this post I would like to give you a self-contained introduction to LPC, in the shape of Verish, and then show you the proof of Gödel's Completeness Theorem, in a simplified form due to Leon Henkin.
Because Verish resembles a natural language, I'll describe its grammar using the grammatical terms used for natural languages, rather than the terms traditionally used for describing LPC. When a grammatical term is used in a sense that differs slightly from its usual meaning, I'll write it with an initial capital.
To make Verish as convenient as possible, its Letters are the 94 non-blank displayable ASCII characters usually found on computer keyboards. ASCII characters that are not Letters, for example blanks and carriage returns, have no significance, and may be included or omitted without any restrictions.
Eight of the Letters have special functions and are called Capitals, and the remaining 86 Letters are called Formatives. The eight Capitals are:
= - ( )
equivalent not and or
+ / [ ]
the of every somewhere the approximate English equivalent of each Capital has been written underneath it.
It might seem strange to see parentheses and square brackets used to represent
"and", "or", "every", and "some". But parentheses and square brackets are not
needed for their usual purposes in Verish, and their use as above reflects the
reciprocal relations between "and" and "or", and between "every" and "some".
The traditional symbols for "and" and "or" are 
and 
, and if these are rotated
90° to the left, in the same way as an image of a person's face is rotated to
obtain the Internet "smileys", they become the chevrons < and >. However using
the chevrons as Capitals would not be convenient for using Verish with html, so
the corresponding parentheses are used instead.
The traditional LPC symbol for "some" is a capital E written backwards, 
, and
if the middle bar is removed from this, it resembles the Verish symbol for
"some". And similarly, if the middle bar is removed from the first letter of
Every, it resembles the Verish symbol for "every". Furthermore, "and" is related
to "every", because if a statement is true for everything, then it is true for
the first thing and for the second thing and for the third
thing, and so on, and
similarly, "or" is related to "some", because if a statement is true for
something, then it is true either for the first thing or for the
second thing or
for the third thing, and so on. These relations between "and" and "every", and
between "or" and "some", are reflected by the last two columns of the above
table.
An additional help for remembering the Capitals is that + resembles the first letter of "the".
The parts of speech of Verish are now defined by a generative grammar, of the form studied by Noam Chomsky.
A Noun consists of the Capital +, followed by one or more Formatives.
A Preposition consists of the Capital +, followed by one or more Formatives, followed by one or more occurrences of the Capital /.
An Adverb consists of either the Capital [, or the Capital ], followed by one or more Formatives.
A Conjunction is either the Capital = or the Capital ( or the Capital ).
The Negation is the Capital -.
A Word is either a Noun or a Preposition or an Adverb or a Conjunction or the Negation. Thus a Word always begins with one of the seven Capitals = - ( ) + [ or ]. These seven Capitals are called Initials.
A Phrase is either a Noun, or a Preposition followed by a number of Phrases, one for each Capital / in the Preposition.
A Sentence is either a Phrase, or an Adverb or the Negation followed by a Sentence, or a Conjunction followed by two Sentences. Thus a Sentence is a series of Words, and each way of producing a bigger Sentence out of previously existing Sentences introduces exactly one additional Word, and this additional Word occurs at the beginning of the new Sentence. Furthermore, each Word in a Sentence after its first Word is the first Word of a uniquely defined smaller Sentence.
For any sequence of Letters, the Scope of any occurrence of an Initial in the sequence is defined as follows. Starting with a count of +1 at the immediate left of the Initial concerned, we move rightwards, adding +1 for each Conjunction or Capital / passed, and -1 for each Capital + passed. The Scope begins at the immediate left of the Initial concerned, and ends at the first point where the count is 0 and the next Letter, if there is one, is an Initial. If the sequence ends before the count reaches 0, the Scope is considered incomplete.
The above definitions imply that the Scope of the first Initial of a Sentence is precisely the whole Sentence, and the Sentences that occur during the formation of a larger Sentence, by the above rules, are precisely the Scopes of the Initials in the larger Sentence. A Sentence always contains at least two Letters, and a sequence of Letters is a Sentence if and only if the following six conditions are all satisfied.
To prove that a sequence of Letters that satisfies these six conditions is a Sentence, we note that a sequence of Letters that contains exactly one Initial, and satisfies the first three conditions, is a Noun, and by considering the first Initial in a sequence of Letters that contains two or more Initials, and satisfies the six conditions, we confirm that if every sequence of Letters that contains a smaller number of Initials, and satisfies the six conditions, is a Sentence, then the sequence of Letters under consideration is also a Sentence.
The Subjects of a Word in a Sentence are the Sentences that consecutively follow that Word, until the end of the Sentence that begins with that Word. Thus a Noun has no Subjects, a Preposition has as many Subjects as the number of Capitals / in the Preposition, an Adverb and the Negation each have one Subject, and a Conjunction has two Subjects. The Subjects of a Sentence are the Subjects of the first Word of the Sentence.
An occurrence of a Noun or a Preposition, in a Sentence, is called a Verb occurrence, if it is not part of the Subject of any Preposition in the Sentence, and an Object occurrence, if it is part of the Subject of some Preposition in the Sentence. A Phrase in a Sentence is called a Verb Phrase of the Sentence if its first Word is a Verb occurrence of that Word, and an Object Phrase of the Sentence if its first Word is an Object occurrence of that Word.
An Adverb and a Noun are said to Agree, if they are the same apart from their Initials. An Object occurrence of a Noun in a Sentence is said to be a Governed occurrence, if it is part of the Subject of an Adverb that Agrees with that Noun.
A Clause of a Sentence is an Adverb or a Preposition or a Noun of that Sentence, together with its Subjects, that is not part of the Subject of any Adverb or Preposition. Thus the Clauses of a Sentence are disjoint, and a Sentence is built from its Clauses, using only Conjunctions and the Negation.
The grammar of Verish also includes a built-in framework for defining and using abbreviations, which is essential for its practical utility, but to keep this post as short as possible, I'll omit any discussion of that.
A Meaning of a Sentence is a specification that includes:
Given a Meaning of a Sentence that begins with an Adverb, a Related Meaning is a Meaning of the Subject of the Sentence that is identical to the given Meaning, except that the Meanings can differ on whether a thing is specified for the Noun that Agrees with that Adverb, and if both Meanings specify a thing for that Noun, they can specify different things for it.
A Sentence is determined to be true or false, for a given Meaning, by the following rules:
From these rules, a Sentence of the form ) - A B, where A and B are Sentences, means that A implies B, for it is true provided that B is true if A is true.
Verish documents are organized into sequences of three or more Sentences called Paragraphs. The first Sentence of a Paragraph is a Noun called the Title. For this post, where we're omitting any discussion of definitions and abbreviations, I'll only consider Statement Paragraphs. The last Sentence of a Statement Paragraph is called the Statement, and for this post, I'll call a Statement a Fact if it is true for all its Meanings. The Sentences between the Title and the Statement are Phrases called Briefs that contain at most one Preposition. They indicate the justification of the Statement.
This is the point where Kurt Gödel's Completeness Theorem comes to our assistance. The reasoning checking module of the Verish program recognizes just six principles of reasoning, one of which is used for introducing or removing abbreviations that have already been defined, and won't be discussed in this post, and the other five are by the Completeness Theorem sufficient to prove every Fact. Thus if you check the C++ source code of the reasoning checking module of the Verish program to satisfy yourself, once and for all, that the program will detect all errors of reasoning, and the author of a research paper takes the trouble to produce a parallel version of the paper with the proofs in Verish, which the utilities module of the Verish program is intended to facilitate, you can then usefully study the paper sufficiently to pick up the gist of the arguments, and if you want to know whether you can depend on the results, but are too busy to check the proofs in fine detail, you can simply put the parallel Verish version of the paper through the reasoning checking module to check it. The reasoning checking module is now in a fairly stable form, and is contained in a C++ source code file that is currently 2104 lines long, plus a header file that is currently 110 lines long, so checking the source code might perhaps take you a few days.
I'll now briefly summarize the five principles of reasoning recognized by the reasoning checking module that are not specifically concerned with introducing or removing abbreviations, and then show you the proof of Gödel's Completeness Theorem, that these five principles are sufficient to prove every Fact that does not involve abbreviations. These five principles are called Tabulate, Example, Generalize, Focus, and Some, and the specific principle used to justify the Statement in a Statement Paragraph is indicated by the Brief, called the Reason, that immediately precedes the Statement. The Subjects of the Reason, if any, are the Titles of any earlier Statement Paragraphs that the justification relies on. Any Briefs between the Title and the Reason are called Methods, and they can indicate the use of more sophisticated principles of reasoning that have been expanded by the utilities module into sequences of Paragraphs that use the basic principles of reasoning, or simply be used to enhance the organization of long proofs.
The Reason is either +Tb, or a Brief whose first Word is a Preposition whose Initial and Formatives are +Tb.
Every assignment of either true or false, independently, to the distinct Clauses in the present Statement and any specified previous Statements is tested. If the present Statement is true for every assignment which is consistent with the specified previous Statements, if any, being Facts, then the present Statement is also a Fact.
The Reason is +Ex.
The Statement has the form ) - A B C, where A is an Adverb that begins with [, B is a Sentence, and C is obtained from B by replacing every Object occurrence that is not Governed, of the Noun that Agrees with A, by a Phrase D, such that no Noun in D becomes Governed, when D replaces an occurrence in B of the Noun that Agrees with A.
For any Meaning of the Statement, all the occurrences of D in C, that have replaced occurrences in B of the Noun that Agrees with A, correspond to the same thing, so from the rules that determine whether a Sentence is true or false for a given Meaning, C is true if the Sentence A B is true. So the Statement is a Fact.
The Reason is a Brief whose first Word is +Gn/.
The Statement has the form A B, where A is an Adverb that begins with [ and B is the Statement specified by the Reason.
The Statement A B is true for all its Meanings if the specified previous Statement B is true for all its Meanings, because every Related Meaning of a Meaning of the Statement A B is also a Meaning of the Statement B.
The Reason is a Brief whose first Word is +Fc/.
The specified earlier Statement has the form A ) B C, where A is an Adverb that begins with [, and B and C are Sentences such that the Noun that Agrees with A has no Object occurrence in B that is not Governed, and the Statement has the form ) B A C.
For any Meaning of A ) B C, and any Meaning of ) B C that is Related to that Meaning, B is true for the Related Meaning if and only if it is true for the original Meaning. If B is true for the original Meaning, then ) B A C is true for that Meaning. If B is false for the original Meaning, then A ) B C is true if C is true for every Related Meaning, and false otherwise, and ) B A C is also true if C is true for every Related Meaning, and false otherwise. Thus if A ) B C is true for a given Meaning, then ) B A C is also true for that Meaning.
The Reason is a Brief whose first Word is +Sm/.
The Statement and the specified earlier Statement are related by the replacement of one occurrence of three consecutive Words of the form - A - in one of the Statements, where A is an Adverb that begins with [, by B in the other Statement, where B is the Adverb obtained from A by replacing its [ by ].
Every Meaning of either Statement is also a Meaning of the other Statement, and for every Meaning of the Statements, each of the Statements is true for that Meaning if and only if the other Statement is true for that Meaning, so the new Statement is a Fact if the earlier Statement is a Fact.
I'll now show you the proof of Kurt Gödel's Completeness Theorem, that Tabulate, Example, Generalize, Focus, and Some are sufficient to prove every Fact whose Statement does not contain abbreviations. The following proof is adapted from the proof sketched in Chapter 1 of the 1966 book, "Set Theory and the Continuum Hypothesis," by Paul J. Cohen.
The idea of the proof of the Completeness Theorem is that if S is a Statement that has no proof, we will construct a Meaning of S in which S is false. This will be done by constructing a collection of Statements that includes - S, and possibly also other Statements that are derived from S but might have fewer Adverbs than S, such that there is no proof of the negation of the conjunction with ( of any finite number of the Statements in the collection, or in other words, such that there is no proof of any Sentence of the form - ( T1 ( T2 ( T3 ... ( Tn - 1 Tn, where T1, T2, ... , Tn are any finite number of Statements in the collection. We will then use the Statements in the collection that contain no Adverbs to construct a Meaning of all the Statements in the collection, in which all the Statements in the collection, including - S, are true.
The first step is to prove that if T is any Sentence that contains an Adverb, we can construct another Sentence U that begins with an Adverb and has the same total number of Adverbs as T, such that we can prove U is equivalent to T, or in other words, such that we can prove the Statement:
= T U
To do this, we'll first prove that if A and B are any Sentences, +c is any Noun, +d is any Noun such that +d has no Object occurrences in A or B that are not Governed, and no Object occurrence of +c in A that is not Governed lies in the Scope of any Adverb that Agrees with +d, and E is the Sentence obtained from A by replacing all Object occurrences of +c in A that are not Governed, by +d, then we can prove the following two Statements:
= ( [c A B [d ( E Band
= ) [c A B [d ) E B
The proof of the first of these is:
+1 +Ex ) - [d ( E B ( E B
+2 +Tb/ +1 ) - [d ( E B E
+3 +Gn/ +2 [d ) - [d ( E B E
+4 +Fc/ +3 ) - [d ( E B [d E
+5 +Ex ) - [d E A
+6 +Gn/ +5 [c ) - [d E A
+7 +Fc/ +6 ) - [d E [c A
+8 +Tb/// +1 +4 +7 ) - [d ( E B ( [c A B
+9 +Ex ) - [c A E
+10 +Tb/ +9 ) - ( [c A B ( E B
+11 +Gn/ +10 [d ) - ( [c A B ( E B
+12 +Fc/ +11 ) - ( [c A B [d ( E B
+13 +Tb// +8 +12 = ( [c A B [d ( E B
The proof of the second is:
+1 +Ex ) - [d ) E B ) E B
+2 +Tb/ +1 ) ) - [d ) E B B E
+3 +Gn/ +2 [d ) ) - [d ) E B B E
+4 +Fc/ +3 ) ) - [d ) E B B [d E
+5 +Ex ) - [d E A
+6 +Gn/ +5 [c ) - [d E A
+7 +Fc/ +6 ) - [d E [c A
+8 +Tb// +4 +7 ) - [d ) E B ) [c A B
+9 +Ex ) - [c A E
+10 +Tb/ +9 ) - ) [c A B ) E B
+11 +Gn/ +10 [d ) - ) [c A B ) E B
+12 +Fc/ +11 ) - ) [c A B [d ) E B
+13 +Tb// +8 +12 = ) [c A B [d ) E B
Next, we note that by writing - A, - B, and - E, for A, B, and E respectively, in the above results, and using Tabulate, we obtain:
= ) - [c - A B - [d ( - E - Band
= ( - [c - A B - [d ) - E - B
We also have:
+1 +Ex ) - [d ( - E - B ( - E - B
+2 +Tb/ +1 ) - [d ( - E - B - ) E B
+3 +Gn/ +2 [d ) - [d ( - E - B - ) E B
+4 +Fc/ +3 ) - [d ( - E - B [d - ) E B
+5 +Ex ) - [d - ) E B - ) E B
+6 +Tb/ +5 ) - [d - ) E B ( - E - B
+7 +Gn/ +6 [d ) - [d - ) E B ( - E - B
+8 +Fc/ +7 ) - [d - ) E B [d ( - E - B
+9 +Tb// +4 +8 = - [d ( - E - B - [d - ) E Band by an analogous proof, also:
= - [d ) - E - B - [d - ( E B
From these and the preceding two results, we obtain, by Tabulate:
= ) - [c - A B - [d - ) E Band
= ( - [c - A B - [d - ( E B
And from these, we obtain, by Some:
= ) ]c A B ]d ) E Band
= ( ]c A B ]d ( E Bunder the same conditions on A, B, +c, +d, and E, as before.
We next note that if A is any Sentence, and +c is any Noun, we have:
+1 +Ex ) - [c A A
+2 +Tb/ +1 ) - [c A - - A
+3 +Gn/ +2 [c ) - [c A - - A
+4 +Fc/ +3 ) - [c A [c - - A
+5 +Tb/ +4 ) - [c A - - [c - - A
+6 +Sm/ +5 ) - [c A - ]c - A
+7 +Ex ) - [c - - A - - A
+8 +Tb/ +7 ) - [c - - A A
+9 +Sm/ +8 ) ]c - A A
+10 +Gn/ +9 [c ) ]c - A A
+11 +Fc/ +10 ) ]c - A [c A
+12 +Tb// +6 +11 = - [c A ]c - A
So we have:
= - [c A ]c - AAnd by a very similar proof, we also have:
= - ]c A [c - A
We next note that if F and G are any Sentences, then by Tabulate, the following Statement is a Fact:
= = F G ( ) - F G ) F - GFor ) - F G is true provided that G is true if F is true, and ) F - G is true provided that F is true if G is true. So
( ) - F G ) F - Gis true if F and G are either both true or both false, and false otherwise, and is thus equivalent to = F G.
If T is a Sentence that contains an Adverb, and we want to construct another Sentence U that begins with an Adverb and has the same total number of Adverbs as T, such that we can prove U is equivalent to T, we first use Tabulate to obtain an equivalent Sentence V in which all sub-Sentences of T that begin with = have been replaced by equivalent sub-Sentences that don't begin with =, as in the above example. This is done starting with the smallest sub-Sentences of T that begin with = and working upwards through the hierarchy of sub-Sentences, so that the equivalent Sentence V that we obtain at the end of this process has no occurrences of =.
We next note that if V contains an Adverb, then at least one of its Clauses must begin with an Adverb, because a Clause that starts with + is a Phrase and does not contain any Adverb. So if V has just a single Clause then it already starts with an Adverb, so let's now assume that V has at least two Clauses.
We now choose a Clause that begins with an Adverb, for example, the first such Clause. Since V contains at least two Clauses and has no occurrences of =, our chosen Clause must be a Subject of an ( or an ) or a -. If our chosen Clause is the Subject of a -, then we use Tabulate, together with one of the equivalences we obtained here, to find a Sentence V1 equivalent to V, such that V1 has the same number of Adverbs as V, and the same number of Clauses as V, but one fewer - outside all Clauses than V. And if our chosen Clause is the Subject of an ( or an ), we use Tabulate, together with one of the equivalences we obtained above, or here, to find a Sentence V1 equivalent to V, such that V1 has the same number of Adverbs as V, and the same number - outside all Clauses as V, but one less Clause than V.
If V1 has more than one Clause, we now carry on in the same way, obtaining a sequence of Sentences V2, V3, ... , such that each is proved equivalent to the previous one, and thus also to V and to T, and has the same number of Adverbs as T, and the sum of the number of Clauses plus the number of - outside all Clauses is reduced by one for each successive Sentence. Thus we eventually obtain a Sentence U that is proved equivalent to T and has the same number of Adverbs as T but has just one Clause, and thus begins with an Adverb, as required.
If S is a Statement that has no proof, we will now construct a a collection of Statements that includes - S, and possibly also other Statements that are derived from S but might have fewer Adverbs than S, such that there is no proof of any Sentence of the form - ( T1 ( T2 ( T3 ... ( Tn - 1 Tn, where T1, T2, ... , Tn are any finite number of Statements in the collection, in the following way.
We start by putting the Sentence - S into the collection, as the first Statement in the collection. And if S does not contain any Noun that has an Object occurrence in S that is not Governed, we choose a Noun +a that does not Agree with any Adverb in S, for use in the following steps.
We now repeat the following sequence of three steps, a possibly infinite number of times, stopping only if a complete pass through the sequence does not add any new Statements to the collection.
The reason it might be necessary to repeat this sequence of steps an infinite number of times is that any new Nouns introduced at the third step in one pass can lead, at the second step of the next pass, to the addition to the collection of new Statements derived from any Statement of the form [b C that is already in the collection, and these new Statements might have any number of Adverbs up to one less than the number of Adverbs in S. These new Statements can then lead, at the first step of the pass after that, to the addition to the collection of new Statements of the form ]f G, which then lead to the introduction of more new Nouns at the third step of that pass, and so on.
To show that there is no proof of any Sentence of the form - ( T1 ( T2 ( T3 ... ( Tn - 1 Tn, where T1, T2, ... , Tn are any finite number of Statements in the collection, we note, first, that by assumption, there is no proof of S, and thus no proof of - - S, so there is no proof of a Statement of the above form, when the only Statement in the collection is -S. I will now show that if there is no proof of a Statement of the above form before any particular new Statement is added to the collection in the above sequence of steps, then there is also no proof of a Statement of the above form after that new Statement is added to the collection. The second step of the above sequence of three steps might involve the addition of an infinite number of new Statements to the collection at each pass, but these can still be added one by one, so the following arguments will show that there is never, at any stage, a proof of any Statement of the above form, formed from a finite number of Statements in the collection.
Firstly, if there is a proof of a Statement of the above form after adding a new Statement to the collection at the first of the above three steps, then since the new Statement has been proved equivalent to a Statement that is already in the collection, Tabulate shows that there was already a proof of a Statement of the above form, before the new Statement was added.
Secondly, if there is a proof of a Statement of the above form after adding a new Statement to the collection at the second of the above three steps, then if there was no proof of such a Statement before adding the new Statement to the collection, the Statement of the above form, of which there is now a proof, must be equivalent to a Statement of the form
- ( T1 ( T2 ( T3 ... ( Tn - 1 ( Tn D,
where D is the new Statement that was added at the second of the above three steps. The above Statement is, by Tabulate, equivalent to the Statement:
) - T1 ) - T2 ) - T3 ... ) - Tn - 1 ) - Tn - D.
If there is a proof of this Statement, then by Tabulate, there is also a proof of the Statement:
) - T1 ) - T2 ) - T3 ... ) - Tn - 1 ) - Tn ) - [b C - D,
where [b C is the Statement, already in the collection, from which the new Statement D was derived, at the second of the above steps. However by Example, the following Statement is also a Fact:
) - [b C DHence by Tabulate, the following Statement is also a Fact:
= ) - [b C - D - [b CFor if [b C is true, then D is true, by the previous result, so ) - [b C - D is false if - [b C is false, and if - [b C is true, then ) - [b C - D is also true, regardless of whether D is true or false. Thus by Tabulate, there is also a proof of the Statement:
) - T1 ) - T2 ) - T3 ... ) - Tn - 1 ) - Tn - [b C,
and thus also a proof of the Statement:
- ( T1 ( T2 ( T3 ... ( Tn - 1 ( Tn [b C.
But this is a Statement of the above form, formed from Statements that were already in the collection before the addition of D, and thus, by assumption, it has no proof.
And thirdly, if there is a proof of a Statement of the above form after adding a new Statement to the collection at the third of the above three steps, then if there was no proof of such a Statement before adding the new Statement to the collection, the Statement of the above form, of which there is now a proof, must be equivalent to a Statement of the form
- ( T1 ( T2 ( T3 ... ( Tn - 1 ( Tn I,
where I is the new Statement that was added at the third of the above three steps. The above Statement is, by Tabulate, equivalent to the Statement:
) - T1 ) - T2 ) - T3 ... ) - Tn - 1 ) - Tn - I.
If there is a proof of this Statement, then by Tabulate, there is also a proof of the Statement:
) - T1 ) - T2 ) - T3 ... ) - Tn - 1 ) - Tn ) - ]f G - I,
where ]f G is the Statement, already in the collection, from which the new Statement I was derived, at the third of the above steps. So by Tabulate again, there is also a proof of the Statement:
) ) - T1 ) - T2 ) - T3 ... ) - Tn - 1 ) - Tn - ]f G - I.
So by Generalize, there is a proof of the Statement:
[h ) ) - T1 ) - T2 ) - T3 ... ) - Tn - 1 ) - Tn - ]f G - I,
where +h is the new Noun that replaced all Object occurrences of +f in G, that are not Governed in G, in order to form I from G, at the third of the above three steps. So by Focus, there is a proof of the Statement:
) ) - T1 ) - T2 ) - T3 ... ) - Tn - 1 ) - Tn - ]f G [h - I.
However, we also have:
+1 +Ex ) - [h - I - G
+2 +Gn/ +1 [f ) - [h - I - G
+3 +Fc/ +2 ) - [h - I [f - G
+4 +Tb/ +3 ) - [h - I - - [f - G
+5 +Sm/ +4 ) - [h - I - ]f G
+6 +Ex ) - [f - G - I
+7 +Sm/ +6 ) ]f G - I
+8 +Gn/ +7 [h ) ]f G - I
+9 +Fc/ +8 ) ]f G [h - I
+10 +Tb// +5 +9 = - ]f G [h - IThus by the preceding result, and Tabulate, there is also a proof of the Statement:
) - T1 ) - T2 ) - T3 ... ) - Tn - 1 ) - Tn - ]f G,
and thus also a proof of the Statement:
- ( T1 ( T2 ( T3 ... ( Tn - 1 ( Tn ]f G.
But as in the previous case, this is a Statement of the above form, formed from Statements that were already in the collection before the addition of I, and thus, by assumption, it has no proof.
Thus there is no proof of any Sentence of the form - ( T1 ( T2 ( T3 ... ( Tn - 1 Tn, where T1, T2, ... , Tn are any finite number of Statements in the collection.
We'll now construct a Meaning for all the Statements in the collection, including - S, in the following way.
Firstly, the non-empty collection of things specified by the Meaning consists of the Noun +a, if we introduced it at the start, plus every Noun that has an Object occurrence in any Statement in the collection that is not Governed in that Statement, plus every Phrase that can be formed from Prepositions that have Object occurrences in S, together with these Nouns. This collection of things is certainly non-empty, because we introduced +a if S does not contain any Noun that has an Object occurrence in S that is not Governed.
We now specify that for every Noun that has an Object occurrence in a Statement in the collection of Statements that is not Governed in that Statement, the thing in the collection of things that corresponds to that Noun is that Noun itself. And for every combination of a Preposition that has an Object occurrence in a Statement in the collection of Statements, and a list of things in the collection of things as the Subjects of that Preposition, the thing in the collection of things that corresponds to that combination is the Phrase formed from that Preposition, with the Phrases corresponding to those things in the collection of things, as its Subjects.
We complete the specification of the Meaning, by choosing a specification, for every Noun that has a Verb occurrence in a Statement in the collection of Statements, of either true or false, and a specification, for every combination of a Preposition that has a Verb occurrence in a Statement in the collection of Statements, and a list of things in the collection as the Subjects of that Preposition, of either true or false, in the following way.
We note, first, that due to the above specification of the things in the collection of things, and the above specification of the things in the collection of things that correspond to Object occurrences of Nouns and Prepositions, these specifications of true or false consist of a specification, for every Sentence that is a Phrase, and whose Verb, or in other words, whose first Word, has a Verb occurrence in some Statement in the collection of Statements, and thus in S, and whose Subjects are formed from Prepositions that have an Object occurrence in some Statement in the collection of Statements, and thus in S, and Nouns that have an Object occurrence in some Statement in the collection of Statements, that is not Governed in that Statement.
We now form an augmented collection of Statements, by taking, one by one, each of these Sentences that are Phrases, and for which we have to specify either true or false in order to complete the specification of the Meaning, and adding either that Sentence P or its negation - P to the collection of Statements, according to the following rule: if there is no proof of any Statement of the form
- ( T1 ( T2 ( T3 ... ( Tn - 1 ( Tn P,
where T1, T2, ... , Tn are any finite number of Statements that are already present in the augmented collection of Statements, and contain no Adverbs, then we add P as a new Statement to the augmented collection of Statements. And if there is a proof of any such Statement, then we add - P as a new Statement to the augmented collection of Statements, instead.
We now observe that there can never be both a proof of a Statement of the above form, and also a proof of a Statement of the form
- ( R1 ( R2 ( R3 ... ( Rm - 1 ( Rm - P,
where R1, R2, ... , Rm are any finite number of Statements that are already present in the augmented collection of Statements, and contain no Adverbs. For if there were proofs of both the above Statements, then by Tabulate, there would also be a proof of the Statement:
- ( T1 ( T2 ( T3 ... ( Tn - 1 ( Tn ( R1 ( R2 ( R3 ... ( Rm - 1 Rm.
This is a Statement of the above form, formed from Statements that were already in the augmented collection before the addition of whichever of P and - P is added. So by the proof above, there is no proof of any such Statement, formed from Statements from the original collection of Statements that contain no Adverbs, before we started adding the additional Statements to form the augmented collection. And the above rule for which of P and - P we add to the augmented collection implies that if there is no proof of any such Statement, formed from Statements from the augmented collection of Statements that contain no Adverbs, before we add either P or - P to the augmented collection of Statements, for another of the Sentences P that are Phrases and for which we have to specify either true or false to complete the specification of the Meaning, then there is also no proof of any such Statement, after we have added either P or - P to the augmented collection of Statements for that Sentence P.
Thus there is no proof of any Sentence of the form
- ( T1 ( T2 ( T3 ... ( Tn - 1 Tn,
where T1, T2, ... , Tn are now any finite number of Statements in the augmented collection of Statements, that contain no Adverbs.
We now complete the specification of the Meaning, by specifying that for each of the Sentences P that are Phrases, and for which we have to specify either true or false in order to complete the specification of the Meaning: P is true if P occurs in the augmented collection of Statements, and P is false if - P occurs in the augmented collection.
This implies that for the Meaning that we have now specified, every Statement in the augmented collection of Statements, that contains no Adverbs, is true. For each such Statement is either a Statement in the original collection of Statements that contains no Adverbs, or is either P or - P for one of the Sentences that are Phrases, and for which we had to specify either true or false in order to complete the specification of the Meaning. In the latter case, the Statement is true as an immediate consequence of the above specification of whether P is true or false.
In the former case, the first four of the above rules for determining whether a Sentence is true or false in a given Meaning determine whether the Statement is true or false in the Meaning we have just specified. If the Statement was false for this Meaning, then by Tabulate, there would be a proof of the Statement
- ( T ( Q1 ( Q2 ... ( Qn - 1 Qn,
where T is the Statement from the original collection of Statements that contains no Adverbs, and Q1, Q2, ... , Qn are those Statements added to the original collection of Statements in the augmented collection, such that either Q1 or - Q1, either Q2 or - Q2, ... , and either Qn or - Qn, are the Clauses of T. For the above Statement is by Tabulate equivalent to the Statement
) - T ) - Q1 ) - Q2 ... ) - Qn - 1 - Qn.
And if T is false when Q1, Q2, ... , Qn are all true, then this Statement is true for all assignments of either true or false, independently, to its distinct Clauses, or in other words, to whichever of Q1 or - Q1, Q2 or - Q2, ... , and Qn or - Qn, are the Clauses of T. So this Statement is proved by Tabulate. Thus since we showed above that there is no proof of a Statement of the above form, T must be true for the Meaning that we specified above.
We now find, from the fifth and sixth of the above rules for determining whether a Sentence is true or false in a given Meaning, that all the Statements in the original collection of Statements that contain exactly one Adverb, and which begin with that Adverb, are true for the Meaning that we specified above, and hence, since every Statement in the original collection of Statements that contains exactly one Adverb is equivalent to one of these Statements, that all the Statements in the original collection of Statements that contain exactly one Adverb are true for that Meaning. And from this, using again the fifth and sixth of the above rules, we find that every Statement in the original collection of Statements that contains exactly two Adverbs, and begins with an Adverb, is true for that Meaning, and hence, that every Statement in the original collection that contains exactly two Adverbs is true for that Meaning. And in the same way, we find in succession that all Statements in the original collection of Statements that contain three, four, or more Adverbs are true for that Meaning. Thus - S, which is one of the two Statements in the original collection of Statements that contain the largest number of Adverbs, and is the one that does not start with an Adverb, is true for that Meaning.
Thus we have proved Kurt Gödel's Completeness Theorem: any Statement that contains no abbreviations, and can not be proved to be a Fact by using only Tabulate, Example, Generalize, Focus, and Some, has a Meaning in which it is false, and is therefore not a Fact.
The software on this website is licensed for use under the Free Software Foundation General Public License.
Page last updated 4 May 2023. Copyright (c) Chris Austin 1997 - 2023. Privacy policy