Formal system

A formal system is a system of symbol chains and rules. The rules are regulations for converting one chain of symbols into another, i.e. productions of a formal grammar . The rules can be applied without knowing the meaning of the symbols, i.e. purely syntactically . Formal systems are used in various scientific disciplines such as logic , mathematics , computer science and linguistics , in particular to derive new statements from already known knowledge.

Calculus is often used with the same meaning as formal system; sometimes, however, a calculus is understood to be a formal system with certain restrictions.

Definition of a formal system

A formal system can be understood as a quadruple , that is, it is constituted by the following determinants: ${\ displaystyle F = \ langle A, B, AU, R \ rangle \ quad}$

${\ displaystyle A \ quad}$ is an alphabet , that is, a set of arbitrary characters. These are the basic signs from which the symbol chains of the formal system are composed.
${\ displaystyle B \ quad}$ is a subset of all words that can be formed above the alphabet . These are the " well-formed " or "well-formed formulas" (English well-formed formulas , wff ), i.e. those among the symbol chains that make "sense". “Make sense” here means nothing else than that these character series correspond to the grammar of the formal system and should therefore be allowed for further investigation. is thus a formal language above the alphabet . In practice, the (mostly infinite) set of sentences is in turn determined by formation rules or defined inductively. ${\ displaystyle A}$ ${\ displaystyle B}$ ${\ displaystyle A}$

${\ displaystyle AU \ quad}$ is a set of axioms . Axioms must be wff s. In other words, it must be a subset of . Incidentally, this term is also to be understood quite formally: axioms are the - basically arbitrarily chosen - initial formulas for the derivative relation of the formal system. ${\ displaystyle AU}$ ${\ displaystyle B}$

${\ displaystyle R \ quad}$ is a set of at least two-digit relations over words that define a derivative relation . contains the rules for deriving. Are two (or more) wff s in any of these relations to each other, then the last of the preceding or the derivable . Based on the axioms - which are previously defined as "derivable" - there is a set of - according to the relation - derivable wff s. ${\ displaystyle B}$ ${\ displaystyle R}$ ${\ displaystyle R}$

With regard to the efficiency of formal systems, the axioms and the last-mentioned relation must be considered. This defines the derivation relation. It is often symbolized with . The notation for two words a and b from the set B means that b can be formally derived from a . So there is a sequence of relations in R that put a and b (possibly using other derivable formulas) into a formal derivative relationship. ${\ displaystyle \ vdash}$ ${\ displaystyle a \ vdash b}$

The term “formal system” is very general. There can be no or an infinite number of axioms. At least one relation must exist, but this can also be infinitely many. However, the following always applies: A wff a belongs to the (formally) derivable formulas if and only if an “inverted tree-shaped” structure of derivation rules can be specified, which starts from axioms and whose “stem” ends at a. If the formal system has no axioms, there are empty rows of symbols at the "leaf tips" of the tree.

Such a derivation term is called syntactic . In principle, there is no reflection on what the derivable formula a stands for; in principle it is not related to any conceivable world, has no meaning, no semantics .

Of course, those formal systems are of interest whose derivation relation comes as close as possible to a semantic inference relation (possibly especially the human one). In other words, you want to be able to derive formally everything that can be semantically deduced. However, this already exceeds the framework of formal systems. More information on this can be found in the article Knowledge Representation with Logic .

Calculus

Occasionally one finds the restriction for calculi that the set of relations in must be finite. In addition, further requirements are often placed on the derivation relation of calculi, such as the fulfillment of the envelope axioms and the finiteness axiom . Otherwise the term calculus is mostly used synonymously with the term formal system. ${\ displaystyle R}$

Formal system in mathematics

The mathematics uses always formal systems. The elementary algebra , how they learn at school, is one such system. It uses numbers, arithmetic symbols for addition , subtraction , multiplication and division as well as letters for unknowns. The rules of calculation are the rules of transformation that can be applied mechanically once you have seen them. For example, you can use the

1. Algebra rule:

{\ displaystyle a + 0 = a}

interpret as

Any expression a can be increased by zero without changing the result.

A mechanical rule could then be:

If you have an expression "a", you can add or remove the symbol chain "+0" (observing the rules in brackets ) without changing the result.

Application example

The basic arithmetic of arithmetic are the first formal system that is learned in elementary school. There you take symbols for the digits 1, 2, 3, 4, 5, 6, 7, 8, 9 and a symbol for the zero, namely 0. The addition contains the symbol “+”. You can now line up the symbols and get symbol chains, such as:

The first three correspond to the rules for well-formed symbol chains (not formulated here in detail). The last two do not and cannot be subject to the following rule.

Addition rule: Take the two digits furthest to the right of each digit sequence and replace them with the following rule: 0 + 1 = 1, 1 + 1 = 2, 1 + 2 = 3, ..., 5 + 5 = 0 + carry,. .. 9 + 9 = 8 + carry. Write the resulting digits in the right place of the new string of digits and note the carryover. Now take the second digit from the right from each chain and replace it with the same rule. If there was a carryover in the previous step, apply the replacement to the new digit and 1. In the result, replace the second digit from the right with the new symbol and remember the carryover again. Continue the process from right to left until there are no digits left. If one string is shorter than the other, replace missing digits with '0'. If there is a carry at the end, write a '1' in the result on the far left.

The chain "987 + 789" is replaced by the chain 1776 by applying this addition rule. To transfer this procedure into the formalization described above, we can say: "1776" was derived from "987 + 789". In doing so, however, we have to be aware that the derivation was only made at the drawing level. It would also be possible to use another derivation rule to derive the character string "198" from "987 + 789" (this is the difference in this case) or the character string "87 + 78" according to the rule: "Leave the first and the last character path". Sum and difference in the sense of our everyday language use belong to semantics and are therefore beyond the reach of the mathematical systems that have been calculated up to now.

literature

Douglas R. Hofstadter : Gödel, Escher, Bach , an endlessly plaited ribbon . DTV 1991, ISBN 3-423-30017-5 .
David Hilbert , W. Ackermann: Fundamentals of theoretical logic . 6th edition, Springer 1972, ISBN 3-540-05843-5 .
Logical language rules. An introduction to logic. (Together with H. Wessel) - Berlin, 1975, Munich / Salzburg, 1975, 592 pages, ISBN 978-3-7705-1264-5 .