HOME

TheInfoList



OR:

In
logic Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from prem ...
and
mathematics Mathematics is an area of knowledge that includes the topics of numbers, formulas and related structures, shapes and the spaces in which they are contained, and quantities and their changes. These topics are represented in modern mathematics ...
, a formal proof or derivation is a finite
sequence In mathematics, a sequence is an enumerated collection of objects in which repetitions are allowed and order matters. Like a set, it contains members (also called ''elements'', or ''terms''). The number of elements (possibly infinite) is called ...
of sentences (called
well-formed formula In mathematical logic, propositional logic and predicate logic, a well-formed formula, abbreviated WFF or wff, often simply formula, is a finite sequence of symbols from a given alphabet that is part of a formal language. A formal language can ...
s in the case of a
formal language In logic, mathematics, computer science, and linguistics, a formal language consists of words whose letters are taken from an alphabet and are well-formed according to a specific set of rules. The alphabet of a formal language consists of sym ...
), each of which is an axiom, an assumption, or follows from the preceding sentences in the sequence by a rule of inference. It differs from a natural language argument in that it is rigorous, unambiguous and mechanically verifiable. If the set of assumptions is empty, then the last sentence in a formal proof is called a theorem of the
formal system A formal system is an abstract structure used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system. A fo ...
. 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 concepts of Fitch-style proof, sequent calculus and natural deduction are
generalization A generalization is a form of abstraction whereby common properties of specific instances are formulated as general concepts or claims. Generalizations posit the existence of a domain or set of elements, as well as one or more common character ...
s of the concept of proof. The theorem is a syntactic consequence of all the well-formed formulas preceding it in the proof. For a well-formed formula 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 well-formed formulas in the proof sequence. Formal proofs often are constructed with the help of computers in
interactive theorem proving In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof edito ...
(e.g., through the use of proof checker and automated theorem prover). Significantly, these proofs can be checked automatically, also by computer. Checking formal proofs is usually simple, while the problem of ''finding'' proofs (automated theorem proving) is usually
computationally intractable In theoretical computer science and mathematics, computational complexity theory focuses on classifying computational problems according to their resource usage, and relating these classes to each other. A computational problem is a task solved b ...
and/or only semi-decidable, depending upon the formal system in use.


Background


Formal language

A ''formal language'' is a
set Set, The Set, SET or SETS may refer to: Science, technology, and mathematics Mathematics *Set (mathematics), a collection of elements *Category of sets, the category whose objects and morphisms are sets and total functions, respectively Electro ...
of finite sequences of symbols. Such a language can be defined without
reference Reference is a relationship between objects in which one object designates, or acts as a means by which to connect to or link to, another object. The first object in this relation is said to ''refer to'' the second object. It is called a '' name'' ...
to any meanings of any of its expressions; it can exist before any
interpretation Interpretation may refer to: Culture * Aesthetic interpretation, an explanation of the meaning of a work of art * Allegorical interpretation, an approach that assumes a text should not be interpreted literally * Dramatic Interpretation, an event ...
is assigned to it – that is, before it has any meaning. Formal proofs are expressed in some formal languages.


Formal grammar

A ''formal grammar'' (also called ''formation rules'') is a precise description of the
well-formed formula In mathematical logic, propositional logic and predicate logic, a well-formed formula, abbreviated WFF or wff, often simply formula, is a finite sequence of symbols from a given alphabet that is part of a formal language. A formal language can ...
s of a formal language. It is synonymous with the set of strings over the
alphabet An alphabet is a standardized set of basic written graphemes (called letters) that represent the phonemes of certain spoken languages. Not all writing systems represent language in this way; in a syllabary, each character represents a syllab ...
of the formal language which constitute well formed formulas. However, it does not describe their
semantics Semantics (from grc, σημαντικός ''sēmantikós'', "significant") is the study of reference, meaning, or truth. The term can be used to refer to subfields of several distinct disciplines, including philosophy, linguistics and comput ...
(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 rule In the philosophy of logic, a rule of inference, inference rule or transformation rule is a logical form consisting of a function which takes premises, analyzes their syntax, and returns a conclusion (or conclusions). For example, the rule of in ...
s (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.


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 interpretations is called formal semantics. ''Giving an interpretation'' is synonymous with ''constructing a model.


See also

* Axiomatic system * Formal verification *
Mathematical proof A mathematical proof is an inferential argument for a mathematical statement, showing that the stated assumptions logically guarantee the conclusion. The argument may use other previously established statements, such as theorems; but every pr ...
*
Proof assistant In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof edi ...
* Proof calculus * Proof theory * Proof (truth) *
De Bruijn factor The de Bruijn Factor is a measure of how much harder it is to write a formal mathematical proof instead of an informal one. It was created by the Dutch computer-proof pioneer Nicolaas Govert de Bruijn Nicolaas Govert (Dick) de Bruijn (; 9 July ...


References


External links

*
2πix.com: Logic
Part of a series of articles covering mathematics and logic.
Archive of Formal Proofs

Mizar Home Page
{{Authority control Formal languages Proof theory Formal systems Syntax (logic) Logical truth de:Axiomatischer Beweis