Formal theorem

Formal theorems constructed in a formal language are a subset of the language's formulas. The set of formulas may be broadly divided into theorems and non-theorems. However, quite often, a formal system will simply define all of its formulas as theorems.

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 $\vdash$ $S$ is often used to indicate that $S$ 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

Main articles: Syntax (logic) and Formal semantics

Derivation of a theorem

Main article: Formal proof

The notion of a formal theorem is deeply intertwined with its derivation. Given a particular very simple formal system (we shall call ours ${\mathcal {FS}}$) whose alphabet α consists only of two symbols { $\triangle$, $\square$ } and whose formation rule for formulas is:

'Any string of symbols of ${\mathcal {FS}}$ which is at least 3 symbols long, and which is not infinitely long, is a formula of ${\mathcal {FS}}$. Nothing else is a formula of ${\mathcal {FS}}$.'

The single axiom of ${\mathcal {FS}}$ is:

'$\triangle$ $\square$ $\square$ $\triangle$'

The transformation rule for ${\mathcal {FS}}$ is:

'Any occurrence of '$\triangle$' in a formula of ${\mathcal {FS}}$ may be replaced by an occurrence of the string '$\triangle$ $\square$' and the result is a formula (wff) of ${\mathcal {FS}}$.'

Theorems in ${\mathcal {FS}}$ are defined as those formulae in ${\mathcal {FS}}$ of which a derivation can be constructed, the last line of which is that formula.

1) $\triangle$ $\square$ $\square$ $\triangle$ (Given as axiom)

2) $\triangle$ $\square$ $\square$ $\square$ $\triangle$ (by applying the transformation rule)

3) $\triangle$ $\square$ $\square$ $\square$ $\triangle$ $\square$ (by applying the transformation rule)

Therefore '$\triangle$ $\square$ $\square$ $\square$ $\triangle$ $\square$' is a theorem of ${\mathcal {FS}}$. The string '$\triangle$ $\square$ $\square$ $\square$ $\triangle$ $\square$' 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 ${\mathcal {FS}}$ are:

'Every theorem of ${\mathcal {FS}}$ begins with '$\triangle$' '

'Every theorem of ${\mathcal {FS}}$ has exactly two triangles.'

Interpretation of a formal theorem

Main article: Interpretation (logic)

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 ${\mathcal {FS'}}$) whose alphabet α consists only of three symbols { $\blacksquare$, $\bigstar$, $\blacklozenge$ } and whose formation rule for formulas is:

'Any string of symbols of ${\mathcal {FS'}}$ which is at least 6 symbols long, and which is not infinitely long, is a formula of ${\mathcal {FS'}}$. Nothing else is a formula of ${\mathcal {FS'}}$.'

The single axiom schema of ${\mathcal {FS'}}$ is:

" $\blacksquare$ $\bigstar$ * $\blacklozenge$ $\blacksquare$ * " (where " * " is a metasyntactic variable standing for a finite string of " $\blacksquare$ "s )

A formal proof can be constructed as follows:

(1) $\blacksquare$ $\bigstar$ $\blacksquare$ $\blacklozenge$ $\blacksquare$ $\blacksquare$

(2) $\blacksquare$ $\bigstar$ $\blacksquare$ $\blacksquare$ $\blacklozenge$ $\blacksquare$ $\blacksquare$ $\blacksquare$

(3) $\blacksquare$ $\bigstar$ $\blacksquare$ $\blacksquare$ $\blacksquare$ $\blacklozenge$ $\blacksquare$ $\blacksquare$ $\blacksquare$ $\blacksquare$

In this example the theorem produced " $\blacksquare$ $\bigstar$ $\blacksquare$ $\blacksquare$ $\blacksquare$ $\blacklozenge$ $\blacksquare$ $\blacksquare$ $\blacksquare$ $\blacksquare$ " 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

• Metatheorem
• List of theorems
• Inference

References

• Geoffery Hunter, Metalogic
• Douglas Hofstadter, Godel Esher Bach
• Benson Mates, Elementary Logic