# What does “calculus” mean?

1. "calculus" and "formal system"

a calculus is a formal system that consists of

• a set of syntactic expressions (well-formed formulæ or wffs),
• a distinguished subset of these expressions (axioms), plus
• a set of formal rules that define a specific binary relation on the space of expressions.

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 grammar, which tells how well-formed formulas (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 schemata: each axiom must be a wff.
• A set of inference rules.

what is the difference between a formal system, and a calculus, then? I think they are the same?

2. "calculus" and "logic system"

"Calculus" appears in "propositional calculus" and "first-order predicate calculus", which are also called "propositional logic" and "first-order logic" respectively. So I thought "calculus" and "logic" mean the same, and "a logic" is, according to http://en.wikipedia.org/wiki/Formal_system#Logical_system,

A logical system or, for short, logic, is a formal system together with a form of semantics, usually in the form of model-theoretic interpretation, which assigns truth values to sentences of the formal language, that is, formulae that contain no free variables.

But then I saw "calculus" also appears in "lambda calculus", which is also a formal system. I think a lambda calculus isn't a logic system, right? What does "calculus" mean in "lambda calculus"?

3. Furthermore "calculus" can also mean computational real analysis for first-year college students.

Thanks.

• Actually calculus means stone. See Oxford English Dictionary. – Rene Schipperus Jul 21 '14 at 1:25
• It's also that stuff on your teeth. – Emily Jul 21 '14 at 1:34
• Stones, in the sense of abacus were used in calculation, it also refers to a medical condition of having a calcified solid in the organs or ducts, I think its quite painful. – Rene Schipperus Jul 21 '14 at 1:34
• No, I mean this: en.wikipedia.org/wiki/Calculus_(dental) – Emily Jul 21 '14 at 1:36
• It's original meaning comes from the notion of "stone counting", the idea of using small stones to tally some quantity. In a sense, with small stones (e.g. pebbles), the notion of calculus can be extrapolated to the idea of examining behavior as one adds or removes stones. – Emily Jul 21 '14 at 1:38

## 1 Answer

Following my answer to your previous post, we can say that a formal system is made by an alphabet (the set of symbols), a gramamr (the formation rules, defining the "correct" expressions, i.e. the set of well-formed formulas) and a proof system or deductive calculus.

See Herbert Enderton, A Mathematical Introduction to Logic (2nd ed - 2001), page 110 :

We will introduce formal proofs but we will call them deductions, to avoid confusion with our English-language proofs.

We will [...] select an infinite set $\Lambda$ of formulas to be called logical axioms. And we will have a rule of inference [i.e. modus ponens], which will enable us to obtain a new formula from certain others. Then for a set $\Gamma$ of formulas, the theorems of $\Gamma$ will be the formulas which can be obtained from $\Gamma \cup \Lambda$ by use of the rule of inference (some finite number of times).

If $\varphi$ is a theorem of $\Gamma$ (written $\vdash \varphi$), then a sequence of formulas that records (as explained below) how $\varphi$ was obtained from $\Gamma \cup \Lambda$ with the rule of inference will be called a deduction of $\varphi$ from $\Gamma$.

The choice of $\Lambda$ and the choice of the rule (or rules) of inference are far from unique. In this [book] we are presenting one deductive calculus for first-order logic, chosen from the array of possible calculi. (For example, one can have $\Gamma = \emptyset$ by using many rules of inference [i.e. Natural Deduction]. We will take the opposite extreme; our set $\Lambda$ will be infinite but we will have only one rule of inference.)