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

Deduction or Proof in formal theory T

A deduction (or proof) in formal theory T  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 

A₁, A₂, ..., A_n

such that, for each i,

either     1. A_i is an axiom of T.

or          2. A_i 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 T  if, and only if, there is a deduction (i.e. proof) 

A₁, A₂, ..., A_n

such that A_n 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 T  is a deduction starting from the axioms. In other words, it starts from the set whose members are axioms of T . 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

A₁, A₂, ..., A_n

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

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] {B₁, B₂, ..., B_n}, we write

{B₁, B₂, ..., B_n} A

or simply

B₁, B₂, ..., B_n 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 Γ.