Calculus

This article deals with calculus in formal sciences. For the calculus in the database, see Calculus (database) .

In the formal sciences such as logic and mathematics, the calculus ( French calcul "invoice"; from Latin calculus " calculus ", " game stone ") is a formal system of rules with which further statements can be made from given statements ( axioms ) derive. Calculi applied to a logic itself are also called logic calculi .

The word calculus in the logical and mathematical sense is a masculine ( the calculus). Calculus in the colloquial sense is also used as a neuter ( the calculus, therefore also "draw into the calculus") in the meaning of "calculation" or "consideration".

Components

A calculus consists of the following components:

• Building blocks, i.e. basic elements (basic characters) from which more complex expressions are put together. The totality of the building blocks of the calculus is also called its alphabet . For a calculus of propositional logic e.g. B. one selects sentence letters (sentence variables), some connective (e.g. →, ∧, ∨ and ¬) and, if necessary, structural symbols (brackets) as building blocks . In analogy to natural languages, the list of building blocks can be called a “dictionary” (in the sense of a list of words) of the calculus.
• Formation rules that determine how the building blocks can be put together to form complex objects, which are also known as well-formed formulas . The totality of the well-formed expressions formed by the formation rules is also called the set of sentences of the calculus and is a formal language about the building blocks. For example, a calculus for propositional logic could stipulate that two existing sentences can be formed into a new sentence by connecting the two with a two-digit connective. In analogy to natural language, the formation rules are the “grammar” of the calculus.
• Transformation rules ( rules of derivation , rules of inference ) which specify how existing well-formed objects (expressions, sentences) of the calculus may be transformed in order to generate new objects from them. In a logical calculus, the transformation rules are inference rules that indicate how one can infer new sentences from existing sentences. An example of a final rule would be the modus ponendo ponens , which allows one to infer from two sentences of the form "A → B" and "A" to the sentence of the form "B".
• Axioms are objects (expressions), which are formed according to the formation rules of the calculus and which without further justification, i.e. H. may be used without applying a transformation rule to already existing expressions.

Of these components, only the last one (the axioms ) is optional. A calculus that contains axioms - no matter how many or how few - is called an axiomatic calculus (also "axiomatic rule calculus"). Calculi that get by without axioms, but usually contain more transformation rules, are often referred to as rule calculi (also final rule calculi ).

A calculus assigns a meaning neither to its building blocks nor to the objects composed from them. If one gives an interpretation for the character series generated by a calculus , i. H. if one defines a meaning for it, one speaks of an interpreted calculus, otherwise of an uninterpreted calculus.

A calculation forms, so to speak, a firmly closed scope for action. The chess game with the pieces (axioms) and rules of move (final rules), like games in general, offers a vivid example. A given goal (e.g. winning the game, solving a - political - conflict, finding a way out of the labyrinth ) is not part of the calculation.

Calculi in logic

In logic , calculi are precisely defined: there axioms are formulas (statements), transformation rules are substitution schemes above the formulas. The notion of closing plays in logic a central role, and so you try to semantically defined inference operator (see tautology ) by the syntactically defined derivative operator replicate, the application of rules of inference symbolizes. ${\displaystyle \models }$ ${\displaystyle \vdash }$

A calculus is called

correct ,

if only semantically valid (generally valid) formulas can be derived from it. (However, it can easily be the case that there are semantically valid formulas that cannot be derived in the calculus.)

Expressed formally: If the following applies for all formulas and for all formula sets : ${\displaystyle G}$ ${\displaystyle \Gamma }$ ${\displaystyle (\Gamma \vdash G)\Rightarrow (\Gamma \models G)}$

completely ,

if all semantically valid formulas can be derived from it. (However, it is quite possible that formulas that are not semantically valid can also be derived from the calculus.)

Expressed formally: If the following applies for all formulas and for all formula sets : ${\displaystyle G}$ ${\displaystyle \Gamma }$ ${\displaystyle (\Gamma \models G)\Rightarrow (\Gamma \vdash G)}$

adequate ,

if it is both complete and correct, d. H. if “the terms of provability and deducibility in the calculus coincide with the respective terms of general validity and logical conclusion”.

free of contradictions ,

if no contradiction can be derived from it (if it is impossible to derive a formula and its negation from non-contradicting premises). ${\displaystyle \varphi }$ ${\displaystyle \neg \varphi }$

consistent ,

if at least one formula cannot be derived from it.

Comment: Consistency and consistency are the same in classical logic and intuitionistic logic .

Reason: If a calculus is free of contradictions, it is z. B. impossible to prove both and . This means that there is at least one formula (namely or ) that cannot be derived. On the other hand, if the calculus is not free of contradictions and can be derived both as well as , then any formula can be derived ex falso quodlibet (this final form applies to both classical and intuitionist logic). ${\displaystyle \vdash P}$ ${\displaystyle \vdash \neg P}$ ${\displaystyle P}$ ${\displaystyle \neg P}$ ${\displaystyle \varphi }$ ${\displaystyle \neg \varphi }$

There are logical systems or general formal systems for which adequate calculations can be made, for example classical logic. Other formal systems are of such a nature that it is not possible to produce a calculus that is complete and correct (e.g., higher level predicate logic ).

For propositional logic, there is a semantic decision-making process in the form of truth tables (see decision problem ) with which the conclusive validity or invalidity of all formulas and arguments can be clearly determined without deriving the respective formula or the respective argument in a calculus would have to. In this respect, the use of a logic calculus is not required for propositional questions.

In contrast, there are neither semantic nor syntactic decision-making processes for general predicate logic ; in order to prove the validity of an argument , it is therefore necessary here to derive it in a suitable calculus. If the derivation succeeds, then the argument is proven valid; if the derivation is unsuccessful, then that says nothing about the validity of the argument: It could be invalid, but the search for a suitable proof could not have been thorough enough.

Logical calculations find practical application in computer science in the field of machine-aided proof .

Examples

• Propositional calculus
• Conceptual writing
• Beth tableaux
• Existential graphs
• Fitch calculus
• Gentzen calculus or sequence calculus
• Hilbert calculus
• Hoare calculus
• Lambda calculus
• Predicate calculus
• Relational calculus
• Resolution calculus
• Situation calculation
• Syllogistics

Calculi in Mathematics

In mathematics, all systems of rules that, when applied correctly, lead to correct results, can be referred to as calculus.

Examples

• arithmetic
• Integral calculus
• calculus
• Calculus of differential forms
• O calculus
• Pi calculus
• Residual calculus
• Stochastic calculus
• Calculations in the balance sheet valuation
• Wp calculation

History of the theory of calculus

The philosophical roots of the calculus can be traced back to the syllogistics of Aristotle , which is a formal system in the modern sense. The history of the theory of calculus is traced back differently. Leibniz is usually named as the actual founder . The aim of his theory of a characteristica universalis was to gain new knowledge with the help of language through the pure application of previously determined rules . For others, Leibniz took up the first approaches of a logic calculus in the combinatorics of Raimundus Lullus .

Importance of calculating

The calculating of logic in its area of ​​application makes logical thinking a type of calculation. It is a hallmark of modern logic and makes it formal, mathematical or symbolic logic. According to Hilbert / Ackermann, the calculation serves the logical conclusion of their decomposition into final elements, so that the logical conclusion “appears as a formal transformation of the initial formulas according to certain rules that are analogous to the rules of calculation; logical thinking is reflected in a logic calculus. "

The mathematization that goes along with the calculation gives logic the advantages of the accuracy and verifiability of mathematics. It is a phenomenon of convergence to the logicistic program ( logicism ), i. H. for the return of mathematics to logic.

The calculation makes the logic suitable for programming languages .

According to Paul Lorenzen , the importance of calculating consists first of all in that it dissolves the circle of axiomatic theories that they themselves presuppose logic by stating that calculi should not presuppose any logic. "The calculation does not provide an answer to the problem of justification, ie to the question of what right to recognize certain conclusions as logical conclusions."

It is stated as philosophically relevant that an (uninterpreted) calculus is "nothing real", "but only contains rules for our own actions, for operating with figures."

The refusal of an interpretation means a methodical relief from semantic questions and controversies. If the formal is set absolutely, the formalization harbors the danger of a reductionist formalism , i. H. to the assumption that the semantic reinterpretation and the relation to reality of logical statements in a calculus are ultimately arbitrary or not given.

literature

• Heinz Bachmann: The way of basic mathematical research. Peter Lang, Bern 1983, ISBN 3-261-05089-6 .

swell

1. ↑ Homberger, specialist dictionary for linguistics (2000) / calculus.
2. ↑ So Regenbogen / Meyer, Dictionary of Philosophical Terms (2005) / Calculus.
3. ↑ Hoyningen-Huene , Logic (1998), p. 270
4. ↑ Hoyningen-Huene, Logic (1998), p. 258.
5. ↑ So z. B. Lorenzen, Logic, 4th ed. (1970), p. 62.
6. ↑ Schülerduden, Philosophie, 2nd ed. (2002) / Lullus.
7. ↑ Hilbert / Ackermann, Grundzüge, 6th edition (1972), p. 1.
8. ↑ Lorenzen, Logic, 4th ed. (1970), p. 62.
9. ↑ Lorenzen, Logic, 4th ed. (1970), p. 74.

Web links

Wiktionary: calculus  - explanations of meanings, word origins, synonyms, translations