This page is keyboard accessible:
• Use Tab, Shift + Tab keys to traverse the main menu. To enter a sub-menu use the Right Arrow key. To leave a sub-menu use the Left Arrow or the Escape key.
• The Enter or the Space key opens the active menu item.
• To skip the menu and move to the main content, press Tab after the page loads to reveal a skip button.
• To get back to the top of the page anytime, press the Home key.
• For more information, click here: Accessibility   Close this tip.

Note: Full functionality of this web page requires JavaScript to be enabled in your browser.

Formal language


What is a formal language?

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:

  • a definition of the symbols that make up the alphabet of the language
  • a definition of the symbols used for punctuation

And there are rules concerning combinations of these symbols. All formal languages must have:

  • a definition of the rules of grammar - these are rules which determine which combinations of symbols are valid combinations (valid words) and which sentences are valid sentences and which are not

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:

  • a definition of a set of initial axiomatic sentences, usually called axioms
  • a definition of a set of proof rules, commonly called the ‘rules of inference’

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:

  • which includes the concept of negation, where one proposition can be defined as the negation of the other, and
  • where there are no sentences where that sentence and its negation can both be proved in that formal system. In other words, you cannot prove in a consistent system that 2 = 2 and that 2 ≠ 2

 A formal system that is not consistent is called inconsistent.


Completeness and Incompleteness

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.


Incompleteness and ‘Truth’

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.


For more on Platonism see Platonism, The Myths of Platonism and Platonism’s Logical Blunder.


Gödel’s Incompleteness Theorem and Formal Language

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:

  • a definition of the symbols that make up the alphabet of the language
  • a definition of the symbols used for punctuation
  • a definition of the rules of grammar

- 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.


What is a Proposition?

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.

section divider


section divider



Diverse opinions and criticisms are welcome, but messages that are frivolous, irrelevant or devoid of logical basis will be blocked. 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 - any address will do, it does not require verification. Your e-mail will only be used to notify you of replies to your comments - it will never be used for any other purpose and will not be displayed. If you cannot see any comments below, see Why isn’t the comment box loading?.

section divider

The Lighter Side


Paper on the diagonal proof

There is now a paper that deals with the matter of language and the diagonal proof, see On Considerations of Language in the Diagonal Proof.

section divider

Other recently added pages

The Myths of Platonism


Goodman’s Paradox


The Platonist Rod paradox


The Balls in the Urn Paradox


section divider

Lebesgue Measure

There is now a new page on a contradiction in Lebesgue measure theory.

section divider

Easy Footnotes

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).

section divider

O’Connor’s “computer checked” proof

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.

Previous Blog Posts

Moderate Platonism

Descartes’ Platonism

The duplicity of Mark Chu-Carroll

A John Searle Inanity

Man versus Machine

Fake News and Fake Mathematics

Ned Block’s Blockhead

Are we alone in the Universe?

Good Math, Bad Math?

Bishops Dancing with Pixies?

Artificial Intelligence

Cranks and Crackpots

The Chinese Room


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:

Gödel Links


– and a page relating specifically to the Gödel mind-machine debate:

Gödel, Minds, and Machines

Printer Friendly

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.

Note: for some browsers JavaScript must be enabled for this to operate correctly.


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 - 2018