Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
Concept
Formal system
Summary
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 formal system is essentially an "axiomatic system".
In 1921, David Hilbert proposed to use such a system as the foundation for the knowledge in mathematics. A formal system may represent a well-defined system of abstract thought.
The term formalism is sometimes a rough synonym for formal system, but it also refers to a given style of notation, for example, Paul Dirac's bra–ket notation.
Logical form
Each formal system is described by primitive symbols (which collectively form an alphabet) to finitely construct a formal language from a set of axioms through inferential rules of formation.
The system thus consists of valid formulas built up through finite combinations of the primitive symbols—combinations that are formed from the axioms in accordance with the stated rules.
More formally, this can be expressed as the following:
A finite set of symbols, known as the alphabet, which are concatenated into finite strings called formulas.
A grammar consisting of rules to form formulas from simpler formulas. A formula is said to be well-formed if it can be formed using the rules of the formal grammar. It is often required that there be a decision procedure for deciding whether a formula is well-formed.
A set of axioms, or axiom schemata, consisting of well-formed formulas.
A set of inference rules. A well-formed formula that can be inferred from the axioms is known as a theorem of the formal system.
A formal system is said to be recursive (i.e. effective) or recursively enumerable if the set of axioms and the set of inference rules are decidable sets or semidecidable sets, respectively.
The entailment of the system by its logical foundation is what distinguishes a formal system from others which may have some basis in an abstract model.
Official source
About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.