A formal theory, T, is defined when the following conditions are satisfied:

1.  A countable set of symbols. A finite string of symbols is called an expression of T.
2. There is a subset of the expressions called the set of well-formed formulas (wffs) of T.
3. A set of well-formed formulas is set aside and called the set of axioms of T.
4. There is a finite set of relations among well-formed formulas, called rules of inference.

 

Deduction or Proof in formal theory T

A deduction (or proof) in formal theory is a sequence of well-formed formulas such that for each well-formed formula in the sequence either it is an axiom of or it is a direct consequence of some of the preceding well-formed formulas using the rules of inference. 

More formally, a deduction in T  is a sequence of well-formed formulas 

A1, A2, ..., An

such that, for each i,

either     1. Ai is an axiom of T.

or          2. Ai is a direct consequence of the preceding well-formed formulas using the rules of inference.

 

Theorem of formal theory T

A theorem of is a well-formed formula A (say) such that there is a deduction the last well-formed formula of which is A. In other words, there is a sequence of well-formed formulas, as defined in the definition of proof, of which the last last well-formed formula is A. Such a deduction (or proof) is called deduction of A (or proof of A.)

More formally, we say A is a theorem of the formal theory if, and only if, there is a deduction (i.e. proof) 

A1, A2, ..., An

such that An is A. The notation 

A

means that A is a theorem of T.

From the above formalization, we see that a proof in the formal theory is a deduction starting from the axioms. In other words, it starts from the set whose members are axioms of . And this means we shall need also the more general notion of deduction from some given set of well-formed formulas.

Consequence in formal theory T

Let Γ be a set of well-formed formulas in T. A well-formed formula A is said to be a consequence of a set Γ if, and only if, there is a sequence of well-formed formulas

A1, A2, ..., An

such that An = A and , for each i, 1 ≤ i ≤ n, one of the following holds:

a. Ai is an axiom or
b. Ai is in Γ or
c. Ai is a direct consequence by some rule of inference of some of the preceding well-formed formulas in the sequence.

Such a sequence is called a proof (or deduction) of A from the set of well-formed formulas Γ. The member of Γ are called the hypothesis or premisses of the proof. In other words, well-formed formulas in the set Γ are called the hypothesis or premisses of the proof. And

Γ A

is an abbreviation for "A is a consequences of Γ" or "A is deducible from Γ."

If Γ is a finite set [of well-formed formulas] {B1, B2, ..., Bn}, we write

{B1, B2, ..., Bn} A

or simply

B1, B2, ..., Bn A

On the other hand, a theorem of Γ is deducible from the empty set of well-formed formulas. In other words, a theorem A is a consequence of an empty set [of well-formed formulas]. 

Formally,

If a set of well-formed formulas Γ in is the empty set {} or 0, then 0 A if, and only if, A is a theorem. 

 

Note that it is customary to omit the sign '0' and simply write

A

See the definition of theorem above.

 

 

 

Properties of the Consequence

The following are properties of the notion of consequence.

Proposition 1. If Γ ⊆ Δ and Γ A, then Δ A.

This proposition asserts that if A is provable from a set Γ of hypotheses, then, if we add still more hypothesis, A is still provable.

Proposition 2. Γ A if, and only if, there is a finite subset Δ of Γ such that Δ A.

Note that "one direction" is follows from Assertion 1. The other direction is obvious when we notice that any proof of A from Γ uses only a finite number of hypotheses from Γ.

Proposition 3. If Δ A, and, for each B in Δ, Γ B, then Γ A.

This proposition asserts that if A is provable from hypotheses in Δ, and each hypothesis in Δ is provable from the hypotheses in Γ, then A is provable from hypotheses in Γ.