|
Logic, especially in the field of proof theory, considers theorems as statements (called formulas or well formed formulas) of a formal language. The statements of the language are strings of symbols and may be broadly divided into nonsense and well-formed formulas. A set of deduction rules, also called transformation rules or rules of inference, must be provided. These deduction rules tell exactly when a formula can be derived from a set of premises. The set of well-formed formulas may be broadly divided into theorems and non-theorems. However, according to Hofstadter, a formal system often simply defines all its well-formed formula as theorems.[14][page needed] Different sets of derivation rules give rise to different interpretations of what it means for an expression to be a theorem. Some derivation rules and formal languages are intended to capture mathematical reasoning; the most common examples use first-order logic. Other deductive systems describe term rewriting, such as the reduction rules for λ calculus. 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. This diagram shows the syntactic entities that can be constructed from formal languages. The symbols and strings of symbols may be broadly divided into nonsense and well-formed formulas. A formal language can be thought of as identical to the set of its well-formed formulas. The set of well-formed formulas may be broadly divided into theorems and non-theorems. A theorem may be expressed in a formal language (or "formalized"). A formal theorem is the purely formal analogue of a theorem. In general, a formal theorem is a type of well-formed 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 formulas 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 that 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. Syntax and semantics Main articles: Syntax (logic) and Formal semantics (logic) The concept of a formal theorem is fundamentally syntactic, in contrast to the notion of a true proposition, which introduces semantics. Different deductive systems can 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, e.g. in classical propositional logic validities are tautologies. A formal system is considered semantically complete when all of its tautologies are also theorems. Derivation of a theorem Main article: Formal proof The notion of a theorem is very closely connected to its formal proof (also called a "derivation"). To illustrate how derivations are done, we will work in a very simplified formal system. Let us call ours \mathcal{FS} Its alphabet consists only of two symbols { A, B } and its formation rule for formulas is: Any string of symbols of \mathcal{FS} that is at least three symbols long, and is not infinitely long, is a formula. Nothing else is a formula. The single axiom of \mathcal{FS} is: ABBA. The only rule of inference (transformation rule) for \mathcal{FS} is: Any occurrence of "A" in a theorem may be replaced by an occurrence of the string "AB" and the result is a theorem. Theorems in \mathcal{FS} are defined as those formulae that have a derivation ending with that formula. For example ABBA (Given as axiom) ABBBA (by applying the transformation rule) ABBBAB (by applying the transformation rule) is a derivation. Therefore "ABBBAB" is a theorem of \mathcal{FS} \,. The notion of truth (or falsity) cannot be applied to the formula "ABBBAB" until an interpretation is given to its symbols. Thus in this example, the formula does not yet represent a proposition, but is merely an empty abstraction. Two metatheorems of \mathcal{FS} are: Every theorem begins with "A". Every theorem has exactly two "A"s. Interpretation of a formal theorem Main article: Interpretation (logic) Theorems and theories Main articles: Theory and Theory (mathematical logic) |
About us|Jobs|Help|Disclaimer|Advertising services|Contact us|Sign in|Website map|Search|
GMT+8, 2015-9-11 21:58 , Processed in 0.284821 second(s), 16 queries .
