Changes

In general terms, a calculus is a [[formal system]] that consists of a set of syntactic expressions (''well-formed formulas'' or ''wffs''), a distinguished subset of these expressions, plus a set of transformation rules that define a [[binary relation]] on the space of expressions.   

In general terms, a calculus is a [[formal system]] that consists of a set of syntactic expressions (''well-formed formulas'' or ''wffs''), a distinguished subset of these expressions, plus a set of transformation rules that define a [[binary relation]] on the space of expressions.   

When the expressions are interpreted for mathematical purposes, the transformation rules are typically intended to preserve some type of [[semantic equivalence relation]] among the expressions.  In particular, when the expressions are intepreted as a [[logical system]], the [[semantic equivalence]] is typically intended to be [[logical equivalence]].  In this setting, the transformation rules can be used to derive logically equivalent expressions from any given expression.  These derivations include as special cases (1) the problem of ''simplifying'' expressions and (2) the problem of deciding whether a given expression is equivalent to an expression in the distinguished subset, typically interpreted as the subset of logical ''[[axiom]]s''.

When the expressions are interpreted for mathematical purposes, the transformation rules are typically intended to preserve some type of [[semantic equivalence relation]] among the expressions.  In particular, when the expressions are interpreted as a [[logical system]], the [[semantic equivalence]] is typically intended to be [[logical equivalence]].  In this setting, the transformation rules can be used to derive logically equivalent expressions from any given expression.  These derivations include as special cases (1) the problem of ''simplifying'' expressions and (2) the problem of deciding whether a given expression is equivalent to an expression in the distinguished subset, typically interpreted as the subset of logical ''[[axiom]]s''.

The set of axioms may be empty, a nonempty finite set, a countably infinite set, or given by axiom schemata.  A [[formal grammar]] recursively defines the expressions and well-formed formulas (wffs) of the [[formal language|language]].  In addition a [[semantics]] is given which defines truth and valuations (or interpretations).  It allows us to determine which wffs are valid, that is, are [[theorem]]s.

The set of axioms may be empty, a nonempty finite set, a countably infinite set, or given by axiom schemata.  A [[formal grammar]] recursively defines the expressions and well-formed formulas (wffs) of the [[formal language|language]].  In addition a [[semantics]] is given which defines truth and valuations (or interpretations).  It allows us to determine which wffs are valid, that is, are [[theorem]]s.