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.


  • 4
    $\begingroup$ Actually calculus means stone. See Oxford English Dictionary. $\endgroup$ – Rene Schipperus Jul 21 '14 at 1:25
  • $\begingroup$ It's also that stuff on your teeth. $\endgroup$ – Emily Jul 21 '14 at 1:34
  • $\begingroup$ 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. $\endgroup$ – Rene Schipperus Jul 21 '14 at 1:34
  • 1
    $\begingroup$ No, I mean this: en.wikipedia.org/wiki/Calculus_(dental) $\endgroup$ – Emily Jul 21 '14 at 1:36
  • 1
    $\begingroup$ 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. $\endgroup$ – Emily Jul 21 '14 at 1:38

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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.