Formal Systems - Definitions

(from Ruth E. Davis, Truth, Deduction, and Computation. New York: Computer Science press, 1989.)

Listed below are the technical definitions of many of the terms that are used in the investigation of deductive reasoning.

Denumerable - A set is denumerable if it can be put into a one-to-one correspondence with the positive integers.

Countable - A set is countable if it is either finite or denumerable.

A formal theory T consists of:

(1) A countable set of symbols. (A finite sequence of symbols of T is called an expression of T.)

(2) A subset of the expressions, called the well-formed formulas (abbreviated wffs) of T. The wffs are the legal sentences of the theory.

(3) A subset of the wffs called the axioms of T.

(4) A finite set of relations R1, ..., Rn on wffs, called rules of inference. For each Ri there is a unique positive integer j such that for every j wffs and each wff A one can effectively decide whether the given j wffs are in the relation Ri to A; if so, A is called a direct consequence of the given wffs by virtue of Ri. For example, the rule modus ponens is a relation on three wffs, A, A -> B, and B, by which B is a direct consequence of A and A -> B.

Since the set of axioms is often infinite, this set is often specified by providing a finite set of axiom schemata. A schema is a statement form; it provides a template showing the form of a wff while leaving some pieces unspecified through the use of metavariables. In the above example A and B are metavariables which stand for wffs of the theory. An instance of a schema is a wff obtained from the statement form by substitution.

Deducible from S in T - Let S be a set of wffs, and let P be a wff in the formal theory T. We say that P is deducible from S in T (denoted by S |-T P) if there exists a finite sequence of wffs P1, ..., Pn such that Pn = P and for 1 < i < n Pi is either an axiom, a formula in S (called a hypothesis), or a direct consequence of previous Pi's by virtue of one of the rules of inference.

Proof or Derivation - The sequence of Pi's is called a derivation of P from S, or a proof of P from S.

Theorem - If P is deducible from the empty set, we write |-T P , and say that P is a theorem or P is provable in T.

The following properties of deducibility are consequences of the definition of deducible from:

Let S1 and S2 be sets of wffs, and A a wff, then

1. If S1 is a subset of S2 and S1 |- A, then S2 |- A. This property is called monotonicity.

2. S1 |- A if and only if there is a finite subset S2 of S1 such that S2 |- A. This property is called compactness. (Since a derivation must be finite, it must require only a finite number of hypotheses)

3. If S2 |- A, and for each wff B in S2, S1 |- B, then S1 |- A. (If every wff in S2 can be derived from the set of wffs S1, then anything that can be derived from S2 can also be derived from S1.)

Interpretation - An interpretation supplies a meaning for each of the symbols of a formal theory such that any wff can be understood as a statement that is either true or false in the interpretation.

Model - An interpretation is a model for a set of wffs S if every wff in S is true in the interpretation.

Completeness - A theory is complete if every sentence that is true in all interpretations is provable in the theory.

Soundness - A theory is sound if every provable sentence is true in all interpretations.

If a theory is sound and complete then truth and deduction are equivalent.

A computation method is complete if for every sentence S, the algorithm will terminate on input S in a finite amount of time, indicating whether or not S is true in all interpretations.

Decidable - A formal theory is decidable if there exists an effective procedure that will determine, for any sentence of the theory, whether or not that sentence is provable in the theory.

(Any property is said to be decidable if there exists an effective procedure (i.e., terminating algorithm) that will determine whether or not the property holds.)

Consistent - A theory is consistent if it contains no wff such that both the wff and its negation are provable.

First Order Predicate Calculus (Logic) is sound, complete, and consistent, but not decidable.


© Charles F. Schmidt