| Index: > A B C D E F G H I J K L M N O P Q R S T U V W X Y Z |
|
|||||
| First Prev [ 1 2 3 4 5 ] Next Last |
A calculus, or proof theory is that part of a logical system which determines how to construct arguments: to derive conclusions from premises. It is a set of axioms (which may be an empty set), and a set of inference rules for deriving new well-formed formulas (wffs) from a given set of wffs. It must thus include or be defined in terms of a formal grammar, which will state all of the allowable expressions, the wffs, in the language. Any grammar will in general also be given a semantics, which explains those features (truth, implication) that are, presumably, of interest. Ideally the axioms and inference rules of a calculus are chosen such that if the formulas in a set are semantically true then any formulas derivable from them are also true. (Hence a calculus is formulated independently of a semantics, but with the aim of agreeing with it.)
In a propositional calculus the vocabulary consists of atomic sentences and sentential operators or connectives. The wffs are all sentences; they include the atomic sentences and any sentences built up from those and the sentential operators.
In what follows we will outline a standard propositional calculus. Many different such formulations exist which are all more or less equivalent but differ in (1) which sentential operators they allow, (hence, which language or grammar they are designed for); (2) which (if any) axioms, and which inference rules are used; and (3) in what form derivations are presented. There is no limit to the number of such systems that can be devised.
The vocabulary is composed of:
The set of wffs is recursiveSee: Recursion Recursive function Recursive set Recursively enumerable set Recursively enumerable language Primitive recursive function.ly defined by the following rules:
Repeated applications of these three rules permit the generation of complex wffs. For example:
For simplicity, we will use a natural deductionIn mathematical logic, natural deduction is the name given to a class of foundational approaches for two key concepts in logic, propositions and proofs. There is no universal agreement on the proper foundation of these concepts; natural deduction takes th system, which has no axioms; or, equivalently, which has an empty axiom set.
Derivations using our calculus will be laid out in the form of a list of numbered lines, with a single wff and a justification on each line. Any premisses will be at the top, with a "p" for their justification. The conclusion will be on the last line. A derivation will be considered complete if every line follows from previous ones by correct application of a rule. (For a contrasting approach, see proof-trees ).