Page last updated 17 Nov 2020
Representability is a notion employed by many incompleteness proofs. Informally, we can say that the notion is that, given a formal system, and an expression A that is not an expression of that system, then provided certain conditions are satisfied, there is an expression B of the formal system that represents the “meaning” of the original non-system expression A. In effect, the assumption of representability is the assumption that there exists an algorithm (Footnote: Such an algorithm would be in a meta-language; there would be two sub-languages, one for the expression A and one for the expression B. ) that can precisely translate the expressions of one mathematical language to expressions of another mathematical language.
In any incompleteness proof that I have seen that uses the notion of representability, no actual proof of this representability is presented, it is simply assumed to be correct. Why such an assumption is considered acceptable in proofs that should rely only on accepted axioms is a mystery. This is particularly so in the case of proofs that are claimed to be entirely proved by computer but are in fact reliant on the assumption of representability. In such proofs you will never see an algorithm that will translate from one mathematical language to another mathematical language - which is what the assumption of representability assumes. It is not surprising that you will never encounter such an algorithm, since all such incompleteness proofs rely on the use of a Gödel numbering function, and it can be proved that there can be no algorithm that can precisely translate an expression that includes the Gödel numbering function to an expression in a purely number-theoretic language. See The Impossibility of Representation of a Gödel Numbering Function by a Formula of the Formal System for an exposition of this proof.
Gödel, in the first ever published incompleteness proof, ushered in the philosophy that when writing an incompleteness proof, one can simply throw in an unproven assumption along the way, rather than actually proving it. The result of his proof relies completely on his Proposition V, which is a proposition that makes numerous assumptions - including the assumption of representability. The result is a crucial confusion of the different levels of language involved in the proof (this confusion is proved in the paper The Fundamental Flaw in Gödel’s Proof of his Incompleteness Theorem).
The notion of representability is dealt with in more detail below; first we will deal with the substitution of a variable by a value that is defined to not belong to the variable’s domain.
Substitution of Variables
In many incompleteness proofs, there is an assumption that one can always substitute a variable that has a given domain by a function provided its range of values are the same as the domain of the variable. But this assumption can conceal essential details.
Consider this expression of a purely number-theoretic language system:
n + 2 > 0
Now, given a function GN(s), whose range is natural numbers, and where s is a variable whose domain is a given set of symbol strings that are not numbers, suppose that we now substitute the n by GN(s) to give the expression: (Footnote: Since GN(s) is any function whose domain is symbol strings and whose range is natural numbers, it can be a Gödel numbering function. )
GN(s) + 2 > 0
This is a common mathematical operation, but what is actually being done is that this is being used a convenient shortcut to the more formal expression:
For all s as symbol strings, there exists a natural number n, such that n = GN(s), and n + 2 > 0.
The crucial point here is that this is an expression where its overall language is not confined to objects that are only natural numbers (i.e., it is not a number-theoretic expression), but within this overall expression n + 2 > 0 has not changed, and it remains a purely number-theoretic expression. Hence the convenient shortcut that is:
GN(s) + 2 > 0
is actually an expression that makes an illegal substitution of a variable of a purely number-theoretic expression. This is so since GN(s) is not itself a natural number, and it does not satisfy the definition of the domain of the variable s. And there is no reason to assume that simply because n + 2 > 0 has a particular property that GN(s) + 2 > 0 will also have that property.
As noted, such a substitution is an extremely common mathematical operation. But the fact that the convenient shortcut usually works without any ensuing problem does not mean that certain properties of the expression n + 2 > 0, in particular that it is a number-theoretic expression, and that n has the domain of natural numbers, can always be ignored. The convenient shortcut usually works without any problem simply because in most cases the substitution does not conceal any crucial detail. In cases that involve only numbers, the function that is being substituted is a function which itself is a number-theoretic function whose objects are natural numbers, and whose variables have the domain of natural numbers. As an example, if we use the same purely number-theoretic expression as was used above:
n + 2 > 0
and given a purely number-theoretic function f(x), where x is a variable whose domain is natural numbers, and we now substitute the n by f(x)to give the expression:
f(x) + 2 > 0
Again, this is a convenient shortcut to the more formal expression:
For all x, there exists n, such that n = f(x), and n + 2 > 0.
But here, in stark contrast to the previous case, the overall expression remains as a purely number-theoretic expression. Hence in this case, the convenient shortcut conceals no important details. And in this case, we do not need to specify the domains of n and x since every variable in the language is already specified as having the domain of natural numbers.
For more details on the substitution of variables by values outside their domain, see the addendum in the paper An Error in a Computer Verified Proof of Incompleteness by Russell O’Connor.
The above describes composite functions that are derived from two pre-existing functions. Now, if one function has the property of being purely number-theoretic, and if the second function does not, why would anyone assume that the resultant composite function is purely number-theoretic? That is an absurd assumption, yet it is assumed in many incompleteness proofs.
As a trivial example of the fallacy involved, consider a purely number-theoretic function - the identity function:
I[x] = x
Now substitute the x by a function GN(s), and assert in the meta-language that:
I[GN(s)] = GN(s)
where GN(s) is a function where the domain of s is symbol strings, and the range of values of the function are natural numbers.
Superficially that might appear to be a valid statement, where the purely number-theoretic property of the identity function is ignored. However, simply because for the function I[x] there are also limitlessly many purely number-theoretic expressions that, given a specific value substituted for x, give the value of I[x] - it does not follow that the composite function I[GN(s)] has any corresponding expression in purely number-theoretic terms, and which evaluates the value of GN(s) given a value s. This cannot be the case, since s and its domain cannot be expressed in a purely number-theoretic system.
Does it matter?
But does it matter?
Yes, it does matter.
The reason why it matters is because many incompleteness proofs rely on the notion of “Representability”. Informally, the principle of “Representability”, as is commonly used in many incompleteness proofs is that, instead of generating an actual expression of the formal system, an expression is generated in another language instead, and then it is claimed by the notion of “Representability” that there is an expression in the formal system that states essentially the same thing as the original expression.
To be more specific, if the original expression expresses a certain function whose only objects are natural numbers and whose variables only have the domain of natural numbers, then there is an expression in the formal system that expresses precisely that same function - provided certain other conditions are satisfied. That is, when the free variables of the expression in the formal system are substituted, the resultant value of the expression is the same numerical value as that given by the original expression when its variables are substituted by the same numerical values.
Similarly, if the original expression expresses a certain relation between natural numbers and variables whose domain is natural numbers, then (provided certain other conditions are satisfied) there is an expression in the formal system that expresses precisely that same relation between natural numbers and variables whose domain is natural numbers. (Footnote: For more details on representability see the addendum in the paper An Error in a Computer Verified Proof of Incompleteness by Russell O’Connor. )
Clearly, if that is the case, then the inverse also applies, that is, given an expression of a number-theoretic number formal system, then there is also a number-theoretic expression that can be expressed and which uses different symbols (and more symbols) than the formal system uses. Furthermore, for both expressions, it must be the case that the objects are natural numbers, and the variables have the domain only of natural numbers.
Obviously, to be able to claim Representability, the expression of the other language must have certain properties. So what are those properties? Well, obviously, there must be some relationship between those properties and the properties of expressions of the formal system. So it is instructive to first examine the properties of expressions of the formal system.
Substitution in the formal system
A number-theoretic formal system consists of objects that are natural numbers, and variables whose domain is the objects of the system, i.e., natural numbers (in the format of the system). Hence expressions of the system only make statements about natural numbers, and not about any other things. So, given an expression of the formal system:
- Natural numbers in the format of the formal system (e.g., symbol strings of the format 0, f0, ff0, fff0, …) may be substituted for a variable in such an expression of the formal
And depending on the rules of the particular system, it is also the case that:
- A valid expression of the system can also be produced by replacing a variable x in the expression by a different variable y of the system, providing certain conditions are observed (such as the new variable name not conflicting with variables already in the expression). This is basically just a name change.
- A valid expression of the formal system can also be produced by replacing a variable x in an existing expression A of the system by another existing expression B of the system, providing certain conditions are observed (such as there may not be variables in the substituted expression B that conflict with variables already in the expression A). For example, if the free variable of a number-theoretic expression is substituted by a number-theoretic function, the resultant expression is also a number-theoretic expression.
Now, given such a formal system, if there is an expression C which is not an expression of the formal system, but is an expression in another language whose objects are also natural numbers, and whose variables also have the domain of natural numbers, then (providing other certain conditions are observed) we might assert that there can be an expression D of the formal system that states the same relationship between natural numbers as that expression C. This assumption is called the “representability” of the expression in the formal system.
In such a definition of “Representability”, any included assumptions must be logically reasonable and acceptable. For that to be the case, then the expression which is to be “representable” must also conform to the three rules above.
Otherwise if, for example, we produce an expression K by substituting a variable x in an existing expression L by an expression which includes a variable whose domain is not natural numbers, then that expression K does not conform to Condition 3 above, and thus there can be no logical reason to suppose that the expression K is “representable” in the formal system.
Type Theories and Computer Proofs
It can be noted that many type theories operate on the substitution assumption as described above in the section Substitution and Variables. Many computer based proof systems use types and generally they also incorporate the same assumption. And as noted above, many proofs that are carried out in such systems do not require a strict delineation of number-theoretic expressions and non-number-theoretic expressions, and so they operate without any problems.
However, in proofs of incompleteness that involve the use of expressions that must be purely number-theoretic, it is crucial that the property of being number-theoretic is always strictly observed. But the substitution assumption precludes there being a strict delineation of number-theoretic expressions and non-number-theoretic expressions, unless additional code is used to enforce such strict delineation. The result is almost inevitable - there is a confusion of number-theoretic expressions and non-number-theoretic expressions, and this produces an erroneous result.
I have now added an extension to my paper An Error in a Computer Verified Proof of Incompleteness by Russell O’Connor on a computer proof by Russell O’Connor, showing that the proof, although supposedly fully checked by computer, actually relies on untenable assumptions regarding representability that are implicit in O’Connor’s definitions in his proof. O’Connor claims, among other things, that his computer proof proves that the formal system can express certain expressions - but if one actually looks at the computer code, one will see that it only proves that these certain expressions satisfy a definition made by O’Connor and which he calls “representability”- and then simply assumes that this is the same as the computer actually proving that these certain expressions can be expressed by the computer system. While I would not wish to accuse O’Connor of any deliberate dishonesty, to call such a proof a fully computer checked proof is a gross misrepresentation of the truth. This also may make you wonder how many other implicit assumptions are included in other claims of fully computer checked proofs. See also the page computer-checked proofs.
O’Connor appears to set great importance upon the fact that his ‘proof ’ has been ‘verified’ by a computer program. The uninitiated might accept O’Connor’s apparent claim that a proof that is step by step checked by a computer program must always be infallibly correct. While it is true that such a computer program will always follow the instructions it has been given, to accept the infallibility of a claim of “computer-checked proof” is to rely on the assumption that the creators of the program have not made any mistakes; this includes both the creators of the underlying system and the creators of any specific proof that uses that system.
Furthermore, there is the question of the interpretation of the complete code. The claim of “computer verified proof” on its own can never assure us that there is no error in the overall reasoning, which is the formalization itself and the interpretation that we put on that formalization. And the more complex the formalization, the more difficult it is to be sure that we have applied the correct interpretation to it. While the interpretation of a proof that deals only with, for example, natural numbers can be straightforward, in proofs that involve more complex concepts such as a meta-language that makes statements about another language, this is not the case, as illustrated above by the failure to understand the assumptions involved in the concept of representability.
Substitution according to type
One person suggested a counter-argument to the above, and claimed that O’Connor’s proof was correct because the proof was based on a theory of types; his argument was as follows:
Using the type term “nat” for natural numbers, if natural numbers, variables whose domain is natural numbers, and functions whose range are natural numbers are all assigned the type “nat” then one can substitute a type “nat” variable by a type “nat” function.
The person asserted to me that, although the expression n + 2 > 0 is defined as a purely number-theoretic expression, it is perfectly valid to say that the variable n can be substituted by an expression such as GN(s), where s is a variable whose domain is a given set of symbol strings that are not numbers. The reason he gave was that to me that GN(s) is of type “nat”, and since n is defined in the proof as type “nat”, the substitution is correct. He also said that there are computer codes that check that all substitution is made according to the type rules and therefore, he claimed, there could not be any substitution error.
But the reality is that, in fact, GN(s) itself isn’t a natural number. This is obvious, since it has no numerical value. If GN(s) itself had a numerical value, then that would mean that there is some symbol string, let’s call it abc, such that GN(s) = GN(abc). Now, GN(s) is any arbitrary function, so that means if it is a bijection (i.e., gives a one-to-one correspondence) that must mean that the variable s is equal to the symbol string abc, which means that they are interchangeable. But that is absurd, since s is a variable, and abc is not a variable
The above simply demonstrates that the type “nat” that is so defined does not actually represent precisely the same concept as natural number. A natural number is an entity for which the Peano axioms (Footnote: The Peano axioms were formulated by the Italian mathematician Giuseppe Peano. They constitute a formal definition of the fundamental properties of natural numbers. See for example, The Peano Axioms at Wolfram. ) apply, but GN(s) itself isn’t a natural number. And a purely number-theoretic expression is an expression in which the objects of the language are natural numbers for which the Peano axioms apply.
Applying an alternative definition such as type “nat” does not change pre-existing fundamental mathematical definitions pertaining to natural numbers. A variable whose domain is natural numbers is defined as substitutable by a natural number. That is a fact that isn’t going to ever change, regardless of any playing around with alternative terminologies.
When both natural numbers and functions whose range is natural numbers are simply lumped together under a single type term “nat”, all that does is to paper over the fact that there actually is a difference between a natural number and a function whose range is natural numbers.
The Evaluation of a Function
When I pointed this out to the person mentioned above, he changed tack, and then said that, provided the function GN(s) evaluates as a natural number, then the substitution is valid and the computer code checking is correct.
But again, I had to point out that GN(s) does not evaluate as a natural number. And then the person changed tack again, and replied that what he actually meant was that when a valid value is substituted for the variable s that there is an evaluation. So what he was in fact saying was:
For all s, GN(s) is a valid substitution for the variable n in n + 2 > 0.
which means that he is claiming that, for example, GN(abc) is a valid substitution for the variable n in n + 2 > 0, which gives GN(abc) + 2 > 0. Well, as was described earlier, this is simply a shortcut for the more formal statement:
For all s as symbol strings, there exists a natural number n, such that n = GN(s), and n + 2 > 0.
and this implies the particular instance for abc, which is:
For the symbol string abc, there exists a natural number n, such that n = GN(abc), and n + 2 > 0.
As in the analysis in the section Substitution and Variables above, this expression is an expression where its overall language is not confined to objects that are only natural numbers (i.e., it is not a number-theoretic expression), but within this overall expression, n + 2 > 0 has not changed, and it remains a purely number-theoretic expression. And the convenient shortcut that is:
GN(abc) + 2 > 0
is actually an expression that conceals the fact that there has been an illegal substitution of a variable in an expression that is defined as being purely number-theoretic. The fact that GN(abc) evaluates as a natural number does not of itself mean that it is a valid substitution for a purely number-theoretic variable.
And, as pointed out in my paper on O’Connor’s proof, this gives rise to a problem - O’Connor assumes that because one expression is “representable” on account of it being a purely number-theoretic expression, then an expression that has been derived by the sort of substitution indicated above is assumed to be also “representable”. This is of course absurd because the derived expression is not a number-theoretic expression.
Encodings of expressions
Some people fail to discern the distinction between an expression of a formal number-theoretic system that corresponds to a relationship between non-numerical quantities, and an expression of a formal number-theoretic system that is claimed to actually state a relationship between non-numerical quantities.
The fact is that there can indeed be an expression of a formal number-theoretic system that corresponds to a certain relationship between non-numerical quantities (subject to certain conditions). But in order to generate that formal number-theoretic expression, some sort of coding function is needed that converts those non-numerical quantities into numerical quantities. And there can be such encoding systems, whereby the formal system together with the encoding system form a compound system that can make statements regarding non-numerical entities. In such a case, it is crucially important to recognize that the formal system alone does not make any statements regarding non-numerical entities. The information about the relationship between the non-numerical quantities is not contained within the expression of the formal system – it is only the combination of that expression and the inverse of the encoding function that allows one to retrieve that information.
Furthermore, since there are infinitely many encoding systems, for any given encoding system and a formula of the formal system that together make a proposition A about given entities, then there can also be another encoding system that, together with precisely the same formula of the formal system, that together make the negation of the very same proposition A. This demonstrates that one cannot simply select some formula of the formal system, and select some encoding system, and then claim that that formula itself is making a proposition about non-numerical entities, for then one could select that same formula, and a different encoding system, and then claim that that formula is making the negation of the very same proposition. That would be a straightforward contradiction.
This demonstrates that to select a formula of a formal system, and then claim that that formal system expression, by itself, is making a statement about non-numerical entities is clearly absurd. Of course, if a compound system is being used, it may be convenient to omit any mention of the encoding system, and simply use the statements of the formal system, but it must be remembered that that is only a convenience. In order to prevent any ambiguity, it must always be clear that a compound system is being used, and which includes one specific encoding function.
Of course, the Gödel numbering system is itself an encoding system that encodes strings of symbols as natural numbers. Common to all incompleteness proofs is the claim that there are expressions of the formal system that actually are making statements about expressions of the formal system. But, as noted above, for any such statement of the formal system that is claimed to be making an assertion about expressions of the formal system, there will also be an encoding such that the very same expression of the formal system is making the negation of the claimed assertion about expressions of the formal system. This, of course, is absurd.
The origin of such absurd claims can always be traced back to the erroneous claim that an expression of the formal system can actually express a function that encodes that very formal system. But the coding function must have a variable that has the domain of the symbols of the non-numerical expressions. And it is clear that no purely number-theoretic expression has such a variable. It follows that the coding function is external to the number-theoretic formal system, and is defined in a language that is a meta-language to the formal system. It further follows that given a purely number-theoretic expression, it is impossible to derive any such coding function from the purely number-theoretic expression alone.
To claim that the formal system is referring to its own expressions by using some encoding function is rather like me claiming that I can understand Chinese - but when somebody makes a detailed inquiry, they discover that what I really meant is that I can’t actually understand Chinese, but that I can understand any Chinese expression if it has already been encoded into English – so that my claim that I can understand Chinese would be a complete travesty of the actual situation.
Representability does not use encoding
On the other hand, given a purely number-theoretic expression that states some relationship, one can express that relationship as an expression of the formal system without any encoding function, since all the objects are natural numbers, both in the original expression and in the formal expression. And given an expression of the formal system, one can present that information in different formats or languages without the need for an inverse of an encoding function. All you need is the knowledge of the formats of natural numbers in the two systems.
Primitive Recursive relations
In many incompleteness proofs, the point of determining that a relation is a primitive recursive number-theoretic relation (i.e., an expression whose only objects are numbers) has two purposes:
- the relation can be expressed in the formal system, because the formal system can express number-theoretic relations, and
- since the relation is primitive recursive, then that means that there is always a finite means of determining whether the relation applies or does not apply for any specific values that are substituted for its free variables.
These are two quite separate purposes. The crucial point is that for any claim that a function/relation is expressible in the formal system because the function/relation is primitive recursive necessarily entails that the function/relation must be purely number-theoretic.
As site owner I reserve the right to keep my comments sections as I deem appropriate. I do not use that right to unfairly censor valid criticism. My reasons for deleting or editing comments do not include deleting a comment because it disagrees with what is on my website. Reasons for exclusion include:
Frivolous, irrelevant comments.
Comments devoid of logical basis.
Comments with excessive number of different points.
Questions about matters that do not relate to the page they post on. Such posts are not comments.
Comments with a substantial amount of mathematical terms not properly formatted will not be published unless a file (such as doc, tex, pdf) is simultaneously emailed to me, and where the mathematical terms are correctly formatted.
Reasons for deleting comments of certain users:
Bulk posting of comments in a short space of time, often on several different pages, and which are not simply part of an ongoing discussion. Multiple anonymous usernames for one person.
Users, who, when shown their point is wrong, immediately claim that they just wrote it wrong and rewrite it again - still erroneously, or else attack something else on my site - erroneously. After the first few instances, further posts are deleted.
Users who make persistent erroneous attacks in a scatter-gun attempt to try to find some error in what I write on this site. After the first few instances, further posts are deleted.
Difficulties in understanding the site content are usually best addressed by contacting me by e-mail.
Note: a password enables editing of comments, an email enables notification of replies