Formal proof

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, an assumption, 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 natural deduction is a generalization of the concept of proof.^[1]

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 formulae in the proof sequence.

Formal proofs often are constructed with the help of computers in interactive theorem proving. 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 and/or only semi-decidable, depending upon the formal system in use.

Background

Formal language

Main article: Formal language

A formal language is a set of finite sequences of symbols. Such a language can be defined without reference to any meanings of any of its expressions; it can exist before any interpretation is assigned to it – that is, before it has any meaning. Formal proofs are expressed in some formal language.

Formal grammar

Main articles: Formal grammar and Formation rule

A formal grammar (also called formation rules) is a precise description of 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

Main article: Formal system

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.

Interpretations

Main articles: Formal semantics (logic) and Interpretation (logic)

An interpretation of a formal system is the assignment of meanings to the symbols, and 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.

References

↑ The Cambridge Dictionary of Philosophy, deduction

External links

"A Special Issue on Formal Proof". Notices of the American Mathematical Society. December 2008.
2πix.com: Logic Part of a series of articles covering mathematics and logic.

‌Logical truth ⊤

Functional:	truth value truth function ⊨ tautology

Formal:	theory formal proof theorem

Negation	⊥ false contradiction inconsistency

Mathematical logic

General	Formal language Formation rule Formal system Deductive system Formal proof Formal semantics Well-formed formula Set Element Class Classical logic Axiom Natural deduction Rule of inference Relation Theorem Logical consequence Axiomatic system Type theory Symbol Syntax Theory

Traditional logic	Proposition Inference Argument Validity Cogency Syllogism Square of opposition Venn diagram

Propositional calculus Boolean logic	Boolean functions Propositional calculus Propositional formula Logical connectives Truth tables

Predicate logic	First-order Quantifiers Predicate Second-order Monadic predicate calculus

Naive set theory	Set Empty set Enumeration Extensionality Finite set Infinite set Subset Power set Countable set Uncountable set Recursive set Domain Range Map Function Relation Ordered pair

Set theory	Foundations of mathematics Zermelo–Fraenkel set theory Axiom of choice General set theory Kripke–Platek set theory Von Neumann–Bernays–Gödel set theory Morse–Kelley set theory Tarski–Grothendieck set theory

Model theory	Model Interpretation Non-standard model Finite model theory Truth value Validity

Proof theory	Formal proof Deductive system Formal system Theorem Logical consequence Rule of inference Syntax

Computability theory	Recursion Recursive set Recursively enumerable set Decision problem Church–Turing thesis Computable function Primitive recursive function

This article is issued from Wikipedia - version of the Thursday, March 31, 2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.