What does "calculus" mean? 
*

*"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?

*"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"?

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


Thanks.
 A: 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.)

