Formal theorem: Wikis

Note: Many of our articles have direct quotes from sources you can cite, within the Wikipedia article! This article doesn't yet, but we're working on it! See more info or our list of citable articles.

Encyclopedia

Updated live from Wikipedia, last check: June 02, 2012 01:29 UTC (42 seconds ago)

From Wikipedia, the free encyclopedia

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.^[1]

A theorem is one of the most fundamental concepts in logic and mathematics. 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 theorem is a type of formula or proposition 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 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 tautologies. A tautology is a formula that is true under any possible interpretation. A formal system is considered semantically complete when all of its tautologies are also theorems.

1 Syntax and semantics
- 1.1 Derivation of a theorem
- 1.2 Interpretation of a theorem
  - 1.2.1 Example
2 Relation to theories
3 See also
4 Notes
5 References

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

Relation to theories

Main articles: Theory, Theory (mathematical logic), and Scientific theory

A theory is a collection of theorems. The main broad distinction to be made among different types of theories is whether or not their theorems are intended to be interpreted as representing a true proposition which is empirical or non-empirical. If every theorem of a theory is empirical, then it is a scientific theory (also called an empirical theory). If there is even one non-empirical theorem in the theory, it is a non-empirical theory.

Theorems in mathematics and logic are non-empirical because they have no content until given an interpretation. This is precisely why theorems of mathematics and logic are useful. They can be applied to any subject matter no matter what its content. If the content of a theory consists entirely of theorems whose interpretations are statements about observation and sense data, than it is a scientific theory.

It is not correct to say that a scientific theory is either true or false as its theorems may be. A theory is taken as a whole as strongly or weakly supported by the facts. A key attribute of a scientific theory is that it is falsifiable, that is, it makes predictions about the natural world that are testable by experiments. Any disagreement between prediction and experiment demonstrates the incorrectness of the scientific theory, or at least limits its accuracy or domain of validity. Mathematical theorems, on the other hand, are purely abstract formal statements: the proof of a theorem cannot involve experiments or other empirical evidence in the same way such evidence is used to support scientific theories.

Notes

^ Godel, Escher, Bach: An Eternal Golden Braid, Douglas Hofstadter

References

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

Logic

History and core topics

History	General · Chinese · Greek · Indian · Islamic

Core topics	Reason · Philosophical logic · Philosophy of logic · Mathematical logic · Metalogic · Logic in computer science

Key concepts and logics

Reasoning	Deduction · Induction · Abduction

Critical thinking and Informal	Proposition · Inference · Argument · Validity · Cogency · Explanation · Term logic · Fallacies · Syllogism · Argumentation theory

Philosophy of logic	Platonic realism · Logical atomism · Logicism · Formalism · Nominalism · Fictionalism · Realism · Intuitionism · Constructivism · Finitism

Mathematical	Formal language · Formation rule · Formal system · Deductive system · Formal proof · Interpretation · Formal semantics · Well-formed formula · Set · Element · Class · Axiom · Rule of inference · Relation · Theorem · Logical consequence · Consistency · Soundness · Completeness · Decidability · Satisfiability · Independence · Set theory · Axiomatic system · Proof theory · Model theory · Recursion theory · Type theory · Syntax

Propositional	Boolean functions · Monadic predicate calculus · Propositional calculus · Logical connectives · Quantifiers · Truth tables

Predicate	First-order · Quantifiers · Predicate · Second-order

Modal	Alethic · Axiologic · Deontic · Doxastic · Epistemic · Temporal

Other Non-classical logics	Computability · Fuzzy · Linear · Relevance · Non-monotonic

Controversies

Paraconsistent logic · Dialetheism · Intuitionistic logic · Paradoxes · Antinomies · Is logic empirical?

Key figures

Alfarabi · Algazel · Alkindus · Al-Razi · Aristotle · Averroes · Avicenna · Boole · Cantor · Carnap · Church · Dharmakirti · Dignāga · Frege · Gentzen · Kanada · Gödel · Gotama · Hilbert · Ibn al-Nafis · Ibn Hazm · Ibn Taymiyyah · Kripke · Leibniz · Mozi · Nagarjuna · Pāṇini · Peano · Peirce · Putnam · Quine · Russell · Skolem · Suhrawardi · Tarski · Turing · Whitehead · Zadeh

Lists

Topics	Outline of logic · General · Basic · Mathematical logic · Boolean algebra · Set theory

Other	Logicians · Rules of inference · Paradoxes · Fallacies · Logic symbols

Portal · Category · WikiProject · Logic stubs · Mathlogic stubs · Cleanup · Talk · changes

Hidden categories: Articles to be merged from November 2009 | All articles to be merged

The Full Wiki

Search:

More info on Formal theorem

Related topics