Formal system

Encyclopedia

In formal logic

, a

and a set of inference rules, used to derive (to conclude

) an expression from one or more other premise

s that are antecedently supposed (axiom

s) or derived (theorem

s). The axioms and rules may be called a deductive apparatus. A formal system may be formulated and studied for its intrinsic properties, or it may be intended as a description (i.e. a model) of external phenomena

.

, which is composed by primitive symbols

. These symbols act on certain rules of formation and are developed by inference from a set of axiom

s. The system thus consists of any number of formulas built up through finite combinations of the primitive symbols—combinations that are formed from the axioms in accordance with the stated rules.

Formal systems in mathematics consist of the following elements:

A formal system is said to be recursive

(i.e. effective) if the set of axioms and the set of inference rules are decidable sets or semidecidable sets

, according to context.

Some theorists use the term

's bra-ket notation

.

, usually in the form of model-theoretic

interpretation

, which assigns truth values to sentence

s of the formal language, that is, formulae that contain no free variables. A logic is sound

if all sentences that can be derived are true in the interpretation, and complete if, conversely, all true sentences can be derived.

or be the product of applying an inference rule on previous wffs in the proof sequence. The last wff in the sequence is recognized as a theorem.

The point of view that generating formal proofs is all there is to mathematics is often called

founded metamathematics

as a discipline for discussing formal systems. Any language that one uses to talk about a formal system is called a

Once a formal system is given, one can define the set of theorems which can be proved inside the formal system. This set consists of all wffs for which there is a proof. Thus all axioms are considered theorems. Unlike the grammar for wffs, there is no guarantee that there will be a decision procedure

for deciding whether a given wff is a theorem or not. The notion of

s.

is a language that is defined by precise mathematical or machine processable formulas. Like languages in linguistics

, formal languages generally have two aspects:

A special branch of mathematics and computer science exists that is devoted exclusively to the theory of language syntax: formal language theory. In formal language theory, a language is nothing more than its syntax; questions of semantics are not included in this specialty.

and linguistics

a formal grammar is a precise description of a formal languageA formal language is a set of words—that is, finite strings of letters, symbols, or tokens that are defined in the language. The set from which these letters are taken is the alphabet over which the language is defined. A formal language is often defined by means of a formal grammar...

: a set of strings

. The two main categories of formal grammar are that of generative grammar

s, which are sets of rules for how strings in a language can be generated, and that of analytic grammars, which are sets of rules for how a string can be analyzed to determine whether it is a member of the language. In short, an analytic grammar describes how to

Other related topics

Logic

In philosophy, Logic is the formal systematic study of the principles of valid inference and correct reasoning. Logic is used in most intellectual activities, but is studied primarily in the disciplines of philosophy, mathematics, semantics, and computer science...

, a

**formal system**(also called a**logical calculus**) consists of a formal languageFormal language

A formal language is a set of words—that is, finite strings of letters, symbols, or tokens that are defined in the language. The set from which these letters are taken is the alphabet over which the language is defined. A formal language is often defined by means of a formal grammar...

and a set of inference rules, used to derive (to conclude

Conclusion

-Logic:*Logical consequence*Affirmative conclusion from a negative premise, a logical fallacy-Music:*Conclusion , the end of a musical composition*The Conclusion, an album by Bombshell Rocks*Conclusion of an Age, an album by the band Sylosis...

) an expression from one or more other premise

Premise

Premise can refer to:* Premise, a claim that is a reason for, or an objection against, some other claim as part of an argument...

s that are antecedently supposed (axiom

Axiom

In traditional logic, an axiom or postulate is a proposition that is not proven or demonstrated but considered either to be self-evident or to define and delimit the realm of analysis. In other words, an axiom is a logical statement that is assumed to be true...

s) or derived (theorem

Theorem

In mathematics, a theorem is a statement that has been proven on the basis of previously established statements, such as other theorems, and previously accepted statements, such as axioms...

s). The axioms and rules may be called a deductive apparatus. A formal system may be formulated and studied for its intrinsic properties, or it may be intended as a description (i.e. a model) of external phenomena

Phenomenon

A phenomenon , plural phenomena, is any observable occurrence. Phenomena are often, but not always, understood as 'appearances' or 'experiences'...

.

## Overview

Each formal system has a formal languageFormal language

A formal language is a set of words—that is, finite strings of letters, symbols, or tokens that are defined in the language. The set from which these letters are taken is the alphabet over which the language is defined. A formal language is often defined by means of a formal grammar...

, which is composed by primitive symbols

Symbol (formal)

For other uses see Symbol In logic, symbols build literal utility to illustrate ideas. A symbol is an abstraction, tokens of which may be marks or a configuration of marks which form a particular pattern...

. These symbols act on certain rules of formation and are developed by inference from a set of axiom

Axiom

In traditional logic, an axiom or postulate is a proposition that is not proven or demonstrated but considered either to be self-evident or to define and delimit the realm of analysis. In other words, an axiom is a logical statement that is assumed to be true...

s. The system thus consists of any number of formulas built up through finite combinations of the primitive symbols—combinations that are formed from the axioms in accordance with the stated rules.

Formal systems in mathematics consist of the following elements:

- A finite set of symbols (i.e. the alphabet), that can be used for constructing formulas (i.e. finite strings of symbols).
- A grammarGrammarIn linguistics, grammar is the set of structural rules that govern the composition of clauses, phrases, and words in any given natural language. The term refers also to the study of such rules, and this field includes morphology, syntax, and phonology, often complemented by phonetics, semantics,...

, which tells how well-formed formulaWell-formed formulaIn mathematical logic, a well-formed formula, shortly wff, often simply formula, is a word which is part of a formal language...

s (abbreviated*wff*) are constructed out of the symbols in the alphabet. It is usually required that there be a decision procedure for deciding whether a formula is well formed or not. - A set of axioms or axiom schemaAxiom schemaIn mathematical logic, an axiom schema generalizes the notion of axiom.An axiom schema is a formula in the language of an axiomatic system, in which one or more schematic variables appear. These variables, which are metalinguistic constructs, stand for any term or subformula of the system, which...

ta: each axiom must be a wff. - A set of inference rulesRule of inferenceIn logic, a rule of inference, inference rule, or transformation rule is the act of drawing a conclusion based on the form of premises interpreted as a function which takes premises, analyses their syntax, and returns a conclusion...

.

A formal system is said to be recursive

Recursive set

In computability theory, a set of natural numbers is called recursive, computable or decidable if there is an algorithm which terminates after a finite amount of time and correctly decides whether or not a given number belongs to the set....

(i.e. effective) if the set of axioms and the set of inference rules are decidable sets or semidecidable sets

Recursively enumerable set

In computability theory, traditionally called recursion theory, a set S of natural numbers is called recursively enumerable, computably enumerable, semidecidable, provable or Turing-recognizable if:...

, according to context.

Some theorists use the term

*formalism*as a rough synonym for*formal system*, but the term is also used to refer to a particular style of*notation*, for example, Paul DiracPaul Dirac

Paul Adrien Maurice Dirac, OM, FRS was an English theoretical physicist who made fundamental contributions to the early development of both quantum mechanics and quantum electrodynamics...

's bra-ket notation

Bra-ket notation

Bra-ket notation is a standard notation for describing quantum states in the theory of quantum mechanics composed of angle brackets and vertical bars. It can also be used to denote abstract vectors and linear functionals in mathematics...

.

### Logical system

A*logical system*or, for short,*logic*, is a formal system together with a form of semanticsSemantics of logic

In logic, formal semantics is the study of the semantics, or interpretations, of formal and natural languages usually trying to capture the pre-theoretic notion of entailment...

, usually in the form of model-theoretic

Model theory

In mathematics, model theory is the study of mathematical structures using tools from mathematical logic....

interpretation

Interpretation (logic)

An interpretation is an assignment of meaning to the symbols of a formal language. Many formal languages used in mathematics, logic, and theoretical computer science are defined in solely syntactic terms, and as such do not have any meaning until they are given some interpretation...

, which assigns truth values to sentence

Sentence (mathematical logic)

In mathematical logic, a sentence of a predicate logic is a boolean-valued well formed formula with no free variables. A sentence can be viewed as expressing a proposition, something that may be true or false...

s of the formal language, that is, formulae that contain no free variables. A logic is sound

Soundness

In mathematical logic, a logical system has the soundness property if and only if its inference rules prove only formulas that are valid with respect to its semantics. In most cases, this comes down to its rules having the property of preserving truth, but this is not the case in general. The word...

if all sentences that can be derived are true in the interpretation, and complete if, conversely, all true sentences can be derived.

### Formal proofs

Formal proofs are sequences of wffs. For a wff to qualify as part of a proof, it might either be an axiomAxiom

In traditional logic, an axiom or postulate is a proposition that is not proven or demonstrated but considered either to be self-evident or to define and delimit the realm of analysis. In other words, an axiom is a logical statement that is assumed to be true...

or be the product of applying an inference rule on previous wffs in the proof sequence. The last wff in the sequence is recognized as a theorem.

The point of view that generating formal proofs is all there is to mathematics is often called

*formalism*. David HilbertDavid Hilbert

David Hilbert was a German mathematician. He is recognized as one of the most influential and universal mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many areas, including invariant theory and the axiomatization of...

founded metamathematics

Metamathematics

Metamathematics is the study of mathematics itself using mathematical methods. This study produces metatheories, which are mathematical theories about other mathematical theories...

as a discipline for discussing formal systems. Any language that one uses to talk about a formal system is called a

*metalanguage*

. The metalanguage may be nothing more than ordinary natural language, or it may be partially formalized itself, but it is generally less completely formalized than the formal language component of the formal system under examination, which is then called theMetalanguage

Broadly, any metalanguage is language or symbols used when language itself is being discussed or examined. In logic and linguistics, a metalanguage is a language used to make statements about statements in another language...

*object language*

, that is, the object of the discussion in question.Object language

An object language is a language which is the "object" of study in various fields including logic, linguistics, mathematics and theoretical computer science. The language being used to talk about an object language is called a metalanguage...

Once a formal system is given, one can define the set of theorems which can be proved inside the formal system. This set consists of all wffs for which there is a proof. Thus all axioms are considered theorems. Unlike the grammar for wffs, there is no guarantee that there will be a decision procedure

Decidability (logic)

In logic, the term decidable refers to the decision problem, the question of the existence of an effective method for determining membership in a set of formulas. Logical systems such as propositional logic are decidable if membership in their set of logically valid formulas can be effectively...

for deciding whether a given wff is a theorem or not. The notion of

*theorem*just defined should not be confused with*theorems about the formal system*, which, in order to avoid confusion, are usually called metatheoremMetatheorem

In logic, a metatheorem is a statement about a formal system proven in a metalanguage. Unlike theorems proved within a given formal system, a metatheorem is proved within a metatheory, and may reference concepts that are present in the metatheory but not the object theory.- Discussion :A formal...

s.

### Formal language

In mathematics, logic, and computer science, a formal languageFormal language

A formal language is a set of words—that is, finite strings of letters, symbols, or tokens that are defined in the language. The set from which these letters are taken is the alphabet over which the language is defined. A formal language is often defined by means of a formal grammar...

is a language that is defined by precise mathematical or machine processable formulas. Like languages in linguistics

Linguistics

Linguistics is the scientific study of human language. Linguistics can be broadly broken into three categories or subfields of study: language form, language meaning, and language in context....

, formal languages generally have two aspects:

- the syntaxSyntaxIn linguistics, syntax is the study of the principles and rules for constructing phrases and sentences in natural languages....

of a language is what the language looks like (more formally: the set of possible expressions that are valid utterances in the language) - the semanticsSemanticsSemantics is the study of meaning. It focuses on the relation between signifiers, such as words, phrases, signs and symbols, and what they stand for, their denotata....

of a language are what the utterances of the language mean (which is formalized in various ways, depending on the type of language in question)

A special branch of mathematics and computer science exists that is devoted exclusively to the theory of language syntax: formal language theory. In formal language theory, a language is nothing more than its syntax; questions of semantics are not included in this specialty.

### Formal grammar

In computer scienceComputer science

Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...

and linguistics

Linguistics

Linguistics is the scientific study of human language. Linguistics can be broadly broken into three categories or subfields of study: language form, language meaning, and language in context....

a formal grammar is a precise description of a formal language

Formal language

: a set of strings

String (computer science)

In formal languages, which are used in mathematical logic and theoretical computer science, a string is a finite sequence of symbols that are chosen from a set or alphabet....

. The two main categories of formal grammar are that of generative grammar

Generative grammar

In theoretical linguistics, generative grammar refers to a particular approach to the study of syntax. A generative grammar of a language attempts to give a set of rules that will correctly predict which combinations of words will form grammatical sentences...

s, which are sets of rules for how strings in a language can be generated, and that of analytic grammars, which are sets of rules for how a string can be analyzed to determine whether it is a member of the language. In short, an analytic grammar describes how to

*recognize*when strings are members in the set, whereas a generative grammar describes how to*write*only those strings in the set.## See also

Examples of formal systems- Axiomatic systemAxiomatic systemIn mathematics, an axiomatic system is any set of axioms from which some or all axioms can be used in conjunction to logically derive theorems. A mathematical theory consists of an axiomatic system and all its derived theorems...
- Formal ethicsFormal ethicsFormal ethics is a formal logical system for describing and evaluating the form as opposed to the content of ethical principles. Formal ethics was introduced by Harry J...
- Lambda calculusLambda calculusIn mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped lambda calculus...
- Proof calculusProof calculusIn mathematical logic, a proof calculus corresponds to a family of formal systems that use a common style of formal inference for its inference rules...
- List of formal systems

Other related topics

- AxiomAxiom
- Formal grammarFormal grammarA formal grammar is a set of formation rules for strings in a formal language. The rules describe how to form strings from the language's alphabet that are valid according to the language's syntax...
- Formal languageFormal language
- Formal method
- Formal scienceFormal scienceThe formal sciences are the branches of knowledge that are concerned with formal systems, such as logic, mathematics, theoretical computer science, information theory, systems theory, decision theory, statistics, and some aspects of linguistics....
- Gödel's incompleteness theoremsGödel's incompleteness theoremsGödel's incompleteness theorems are two theorems of mathematical logic that establish inherent limitations of all but the most trivial axiomatic systems capable of doing arithmetic. The theorems, proven by Kurt Gödel in 1931, are important both in mathematical logic and in the philosophy of...
- QED manifesto
- substitution instance

## Further reading

- Raymond M. Smullyan, 1961.
*Theory of Formal Systems: Annals of Mathematics Studies*, Princeton University Press (April 1, 1961) 156 pages ISBN 069108047X - S. C. Kleene, 1967.
*Mathematical Logic*Reprinted by Dover, 2002. ISBN 0486425339 - Douglas HofstadterDouglas HofstadterDouglas Richard Hofstadter is an American academic whose research focuses on consciousness, analogy-making, artistic creation, literary translation, and discovery in mathematics and physics...

, 1979,.*Gödel, Escher, Bach: An Eternal Golden Braid*ISBN 978-0465026562. 777 pages.

## External links

- Encyclopædia Britannica, Formal system definition, 2007.
- Christer Blomqvist, an introduction to formal systems, webpage 1997.
- What is a Formal System?: Some quotes from John Haugeland's `Artificial Intelligence: The Very Idea' (1985), pp. 48–64.
- Heinrich Herre Formal Language and systems, 1997.
- Peter Suber, Formal Systems and Machines: An Isomorphism, 1997.