Copyright © James R Meyer 2012 - 2017 www.jamesrmeyer.com
A formal language is a language in which everything is precisely defined, so that there cannot be any ambiguity about any expression in that language. A formal language will have:
And there are rules concerning combinations of these symbols. All formal languages must have:
In addition, in logic or mathematics, there will also be a precise definition of how a sentence can be said to be proved in the formal language, and this consists of:
The initial axiomatic sentences are sentences that are taken to be proved, without actually having to be proved by the proof rules. These are statements that form the basis from which propositions are proved. Commonly it is stated that it is given that the axiomatic sentences are ‘true’. See also the axioms of the formal system.
The proof rules are rules that determine what sentences can be proved from other sentences. A valid proof will consist of a set of sentences, which always has at least one axiomatic sentence. Every sentence in the proof is proved according to the proof rules by one or more proof steps from the axiomatic sentences, so that the proof of every sentence in the proof can be traced back to the axiomatic sentences. See also the rules of inference. The formal language, its alphabet, together with the axioms and the rules of inference, is often referred to as a formal system. See also Formal Language Systems in the simplified explanation of Gödel’s incompleteness proof.
A consistent formal system is a formal system:
A formal system that is not consistent is called inconsistent.
The standard meaning of the term ‘completeness’ as applied to a formal language system is that the formal system is called ‘complete’ if, for every valid proposition of the language, either that proposition is provable, or its negation is provable. (Footnote: Note that another uncommon interpretation of the term ‘completeness’ is that even if there are valid propositions for which neither the proposition nor its negation is provable, a formal system is said to be complete if there is no other possible way of proving the proposition nor its negation to be true by some other consistent system.) That means that if we have a valid proposition of the language that cannot be proved, then its negation must be provable.
The converse of completeness is ‘incompleteness’, and a formal system is called ‘incomplete’ if there is at least one proposition of the language that cannot be proved, and neither can its negation.
You might think that it’s rather a big deal whether a language system is complete or not. And you would be right. But some people believe that if a language system is incomplete, it is incomplete because there is something lacking in the definition of the language system, and that for the propositions for which neither they or their negation can be proved, there can exist a proof by some other means.
All right, you might say, if it can be proved by other means, then you simply have to add some more definitions to your language system. These definitions can only be for more axiomatic sentences or rules of inference, since the question of incompleteness only applies to propositions that can be validly constructed using the alphabet and the rules of grammar.
A statement in a formal language system is simply a set of symbols that can be arranged according to the rules of the system. Statements in such a system have no innate ‘truth’ value. For example, we might have a statement such as ‘3 + 4 = 7’. Is this true or false? Most people will say that it is true. But in doing so, they are including the assumption that it is to be taken as a statement of our standard mathematics. But it could also be a statement of a formal language system where the symbols ‘3’, ‘4’, ‘=’, and ‘7’ have the same connotation as our standard mathematics, but where ‘+’ indicates subtraction. In this system, the statement ‘3 + 4 = 7’ is incorrect.
So, you might wonder, if a formal system is incomplete, and there is a certain statement of that system that the formal system cannot prove (or its negation), how could that statement be either ‘true’ or ‘false’ - since the ‘truth’ or ‘falsity’ of the statement surely depends on the definition of the formal system that the statement belongs to - so where could such ‘truth’ or ‘falsity’ come from?
The answer to that is that it there is no reason to suppose that it has any ‘truth’ or ‘falsity’. Unless you are a Platonist and have a faith in ‘real’ mathematical things but which have no material existence. Platonists believe that such mathematical statements refer to ‘real’ things, so that ‘3’ and ‘4’ refer to ‘real’ things, things that are ‘real’ even though they have no physical existence. And if believe that, then you can also believe that statements that refer to these ‘real’ things must have a ‘true’ or ‘false’ value. But if you aren’t a Platonist, then you have no reason to suppose that the ‘truth’ or ‘falsity’ of a statement of a formal system can arise from anything other than the definition of that formal system.
So what does Gödel’s incompleteness theorem say about formal language and formal systems?
It says that for every consistent formal language system that includes numbers there will always be at least one valid proposition of that system for which that proposition cannot be proved, and nor can its negation - regardless of how many axiomatic sentences and rules of inference that you add to the system. And Gödel’s proof also claims that the proposition can be proved by a non-formal language system (that it is ‘true’).
This non-formal language system must have an alphabet. This language must have rules of grammar - the propositions that Gödel makes should be grammatically correct.
So far, we have, in principle, in this ‘non-formal’ language, the essentials of a formal language:
- so that the only difference in this ‘non-formal’ system and a formal system must be a difference in the axiomatic sentences and the rules of inference.
This non-formal language makes certain assumptions. While some of those assumptions are implied, they should all be capable of being clearly defined. For if the assumptions made in Gödel’s proof cannot be clearly defined, then how can it be asserted that the proof is logically acceptable?
Gödel claims that his reasoning is correct. That means that it must be the case that every proposition that he makes must follow logically from the previous propositions, even if some of those steps are implied rather than explicitly stated (otherwise the proof can’t be considered to be logically acceptable).
So, if we assume for a moment that Gödel’s proof is logically valid, what is the difference in principle between Gödel’s ‘non-formal’ system and a formal system?
The answer is that, in principle, there is no difference whatsoever. The obvious conclusion is that Gödel’s result relies on some assumption that is logically unacceptable. And this is indeed the case.
This is a good question.
In simple terms, a proposition is a sentence that may be said to make a claim or an assertion.
In traditional terminology, a proposition is said to be a sentence that is either ‘true’ or ‘false’. Unfortunately this is not a great definition, since the terms ‘true’ and ‘false’ are not precisely defined.
A better definition might be that a proposition is a valid sentence of the formal language that can be shown to follow from another valid sentence of the formal language by the rules of inference. This does not mean that the proposition is proved, since we have not shown that the other sentence can be proved. This definition requires that the formal system is sufficiently defined to enable a decision to be definitely made for any sentence as to whether it is a proposition or not, without any reference to its meaning.
Obviously, a sentence that is not a proposition cannot be provable, nor can its negation (provided the system is logically coherent).
Some propositions certainly are provable. And for some propositions, the negation is provable.
Diverse opinions and criticisms are welcome, but messages that are frivolous, irrelevant or devoid of logical basis will be blocked (comments will be checked before appearing on this site). Difficulties in understanding the site content are usually best addressed by contacting me by e-mail. Note: you will be asked to provide an e-mail address - this will only be used to notify you of replies to your comments - it will never be used for any other purpose, will never be displayed and does not require verification. Comments are common to the entire website, so please indicate what section of the site you are commenting on.
If you cannot see any comments below, it may be that a plug-in on your browser is blocking Disqus comments from loading. Avast anti-virus in particular is known to do this, especially with Internet Explorer and Safari. See Disqus Browser plug-in/extension conflicts or Why isn’t the comment box loading?.
Please wait for comments to load …
There is now a new page on Lebesgue measure theory and how it is contradictory.
There is now a new page Halbach and Zhang’s Yablo without Gödel which demonstrates the illogical assumptions used by Halbach and Zhang.
It has come to my notice that, when asked about the demonstration of the flaw in his proof (see A Fundamental Flaw in an Incompleteness Proof by Peter Smith PDF), Smith refuses to engage in any logical discussion, and instead attempts to deflect attention away from any such discussion. If any other reader has tried to engage with Smith regarding my demonstration of the flaw, I would be interested to know what the outcome was.
I found that making, adding or deleting footnotes in the traditional manner proved to be a major pain. So I developed a different system for footnotes which makes inserting or changing footnotes a doddle. You can check it out at Easy Footnotes for Web Pages (Accessibility friendly).
I have now added a new section to my paper on Russell O’Connor’s claim of a computer verified incompleteness proof. This shows that the flaw in the proof arises from a reliance on definitions that include unacceptable assumptions - assumptions that are not actually checked by the computer code. See also the new page Representability.
There is now a new page on Chaitin’s Constant (Chaitin’s Omega), which demonstrates that Chaitin has failed to prove that it is actually algorithmically irreducible.
For convenience, there are now two pages on this site with links to various material relating to Gödel and the Incompleteness Theorem
– a page with general links:
– and a page relating specifically to the Gödel mind-machine debate:
All pages on this website are printer friendly, and will print the main content in a convenient format. Note that the margins are set by your browser print settings.
Comments on this site are welcome, please see the comment section.
Please note that this web site, like any other is a collection of various statements. Not all of this web site is intended to be factual. Some of it is personal opinion or interpretation.
If you prefer to ask me directly about the material on this site, please send me an e-mail with your query, and I will attempt to reply promptly.
Feedback about site design would also be appreciated so that I can improve the site.
Copyright © James R Meyer 2012 - 2017