Formal theorem
![]() |
![](http://upload.wikimedia.org/wikipedia/commons/6/62/Formal_languages.png)
In mathematics and logic, a formal theorem is the purely formal analogue of a theorem. There are at least two senses in which the term "theorem" is used. In one sense, we are referring to an idea which is identical to the meaning of the theorem. In another sense, we are referring to, for instance, the ink marks on paper or chalk marks on a board which represent that idea. In general, a formal theorem is a type of formula that satisfies certain logical and syntactic conditions. The notation is often used to indicate that is a theorem.
Formal theorems consist of strings of symbols formed according to both the syntactic rules (also called its formation rules or grammar) of a formal language and the transformation rules of a formal system. Specifically, a formal theorem is always the last formula of a derivation in some formal system each formula of which is a logical consequence of the formulas which came before it in the derivation. The initially accepted formulas in the derivation are called its axioms, and are the basis on which the theorem is derived. A set of theorems is called a theory.
What makes formal theorems useful and of interest is that they can be interpreted as true propositions and their derivations may be interpreted as a proof of the truth of the resulting expression. A set of formal theorems may be referred to as a formal theory. A theorem whose interpretation is a true statement about a formal system is called a metatheorem.
The concept of a formal theorem is fundamentally syntactic, in contrast to the notion of a "true proposition" in which semantics are introduced. Different deductive systems may be constructed so as to yield other interpretations, depending on the presumptions of the derivation rules (i.e. belief, justification or other modalities). The soundness of a formal system depends on whether or not all of its theorems are also validities. A validity is a formula that is true under any possible interpretation. A formal system is considered semantically complete when all of its validities are also theorems.
Syntax and semantics
Derivation of a theorem
The notion of a formal theorem is deeply intertwined with its derivation. Given a particular very simple formal system (we shall call ours ) whose alphabet α consists only of two symbols { , } and whose formation rule for formulas is:
- 'Any string of symbols of which is at least 3 symbols long, and which is not infinitely long, is a formula of . Nothing else is a formula of .'
The single axiom of is:
- ' '
The transformation rule for is:
- 'Any occurrence of '' in a formula of may be replaced by an occurrence of the string ' ' and the result is a formula (wff) of .'
Theorems in are defined as those formulae in of which a derivation can be constructed, the last line of which is that formula.
- 1) (Given as axiom)
- 2) (by applying the transformation rule)
- 3) (by applying the transformation rule)
Therefore ' ' is a theorem of . The string ' ' is not considered to be "true" or "proved," until it is given an interpretation it is merely derived. In this example, the string isn't even a proposition, but only a mere abstraction.
Two metatheorems of are:
- 'Every theorem of begins with '' '
- 'Every theorem of has exactly two triangles.'
Interpretation of a formal theorem
A derivation of a theorem can be interpreted as a proof of the truth of some proposition. To establish a proposition as a theorem, the existence of a line of reasoning from axioms in the system (and other, already established theorems) to the given statement must be demonstrated.
Although the proof is necessary to produce a theorem, it is not usually considered part of the theorem. And even though more than one proof may be known for a single theorem, only one proof is required to establish the theorem's validity. The Pythagorean theorem and the law of quadratic reciprocity are contenders for the title of theorem with the greatest number of distinct proofs.
The definition of formal theorems as elements of a formal language allows for results in proof theory that study the structure of formal proofs and the structure of provable formulas. The most famous result is Gödel's incompleteness theorem; by representing theorems about basic number theory as expressions in a formal language, and then representing this language within number theory itself, Gödel constructed examples of statements that are neither provable nor disprovable from axiomatizations of number theory.
Example
Given a different simple formal system (we shall call this one ) whose alphabet α consists only of three symbols { , , } and whose formation rule for formulas is:
- 'Any string of symbols of which is at least 6 symbols long, and which is not infinitely long, is a formula of . Nothing else is a formula of .'
The single axiom schema of is:
- " * * " (where " * " is a metasyntactic variable standing for a finite string of " "s )
A formal proof can be constructed as follows:
- (1)
- (2)
- (3)
In this example the theorem produced " " can be interpreted as meaning "One plus three equals four." A different interpretation would be to read it backwards as "Four minus three equals one."
See also
Notes
- ^ Godel, Escher, Bach: An Eternal Golden Braid, Douglas Hofstadter
References
- Geoffery Hunter, Metalogic
- Douglas Hofstadter, Godel Esher Bach
- Benson Mates, Elementary Logic