Formal proof: Difference between revisions
mNo edit summary |
cite |
||
| Line 1: | Line 1: | ||
{{Unreferenced|date=May 2008}} |
|||
:see also [[Mathematical proof]], [[Proof theory]], and [[Axiomatic system]]. |
:see also [[Mathematical proof]], [[Proof theory]], and [[Axiomatic system]]. |
||
A '''formal proof''' or '''derivation''' is a sequence of [[well-formed formula]]s of a [[formal language]] |
A '''formal proof''' or '''derivation''' is a finite sequence of [[proposition|sentences]] (called [[well-formed formula]]s in the case of a [[formal language]]) each of which is an [[axiom]] or follows from the preceding sentences in the sequence by a [[rule of inference]]. The last sentence in the sequence is a [[theorem]] of a [[formal system]]. The notion of theorem is not in general [[effective method|effective]], therefore there may be no method by which we can always find a proof of a given sentence or determine that none exists. The concept of [[deduction]] is a [[generalization]] of the concept of proof.<ref>The Cambridge Dictionary of Philosophy, ''deduction''</ref> |
||
The theorem is a [[syntactic consequence]] of all the wffs preceding it in the proof. For a wff to qualify as part of a proof, it must be the result of applying a rule of the [[deductive apparatus]] of some formal system to the previous wffs in the proof sequence. |
|||
== Background == |
== Background == |
||
| Line 25: | Line 27: | ||
An ''interpretation'' of a formal system is the assignment of meanings to the symbols, and truth-values to the sentences of a formal system. The study of formal interpretations is called [[formal semantics]]. ''Giving an interpretation'' is synonymous with ''constructing a [[Structure (mathematical logic)|model]]. |
An ''interpretation'' of a formal system is the assignment of meanings to the symbols, and truth-values to the sentences of a formal system. The study of formal interpretations is called [[formal semantics]]. ''Giving an interpretation'' is synonymous with ''constructing a [[Structure (mathematical logic)|model]]. |
||
== References == |
|||
{{reflist}} |
|||
{{logic}} |
{{logic}} |
||
Revision as of 04:21, 13 May 2008
- see also Mathematical proof, Proof theory, and Axiomatic system.
A formal proof or derivation is a finite sequence of sentences (called well-formed formulas in the case of a formal language) each of which is an axiom or follows from the preceding sentences in the sequence by a rule of inference. The last sentence in the sequence is a theorem of a formal system. The notion of theorem is not in general effective, therefore there may be no method by which we can always find a proof of a given sentence or determine that none exists. The concept of deduction is a generalization of the concept of proof.[1]
The theorem is a syntactic consequence of all the wffs preceding it in the proof. For a wff to qualify as part of a proof, it must be the result of applying a rule of the deductive apparatus of some formal system to the previous wffs in the proof sequence.
Background
Formal language
A formal language is an organized set of symbols the essential feature of which is that it can be precisely defined in terms of just the shapes and locations of those symbols. Such a language can be defined, then, without any reference to any meanings of any of its expressions; it can exist before any formal interpretation is assigned to it -- that is, before it has any meaning. Formal proofs are expressed in some formal language
Formal grammar
A formal grammar (also called formation rules) is a precise description of a the well-formed formulas of a formal language. It is synonymous with the set of strings over the alphabet of the formal language which constitute well formed formulas. However, it does not describe their semantics (i.e. what they mean).
Formal systems
A formal system (also called a logical calculus, or a logical system) consists of a formal language together with a deductive apparatus (also called a deductive system). The deductive apparatus may consist of a set of transformation rules (also called inference rules) or a set of axioms, or have both. A formal system is used to derive one expression from one or more other expressions.
Formal interpretations
An interpretation of a formal system is the assignment of meanings to the symbols, and truth-values to the sentences of a formal system. The study of formal interpretations is called formal semantics. Giving an interpretation is synonymous with constructing a model.
References
- ^ The Cambridge Dictionary of Philosophy, deduction
| Major fields |
| ||||
|---|---|---|---|---|---|
| Foundations | |||||
| Lists |
| ||||
