What does "calculus" mean?

1. "calculus" and "formal system"

   From http://en.wikipedia.org/wiki/Propositional_calculus#Terminology

   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.

   From http://en.wikipedia.org/wiki/Formal_system

   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.

Solution 1:

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.)