Formal Axiomatic Theory for Propositional Calculus

 

Normally, we can effectively decide whether a given well-formed formula is an axiom of formal theory T. If this happens, formal theory, T, is called an axiomatic theory, L. In other words, formal theory, T, is axiomatic, L, if there is an effective procedure for checking any given well-formed formula to see whether a given well-formed formula is an axiom.

To specify a formal axiomatic theory, L, we require (just like formal theory T ):

1.  An alphabet of symbols.
2. A set of finite strings of these symbols, called well-formed formulas. These formulas acts as the words and sentences in formal languages.
3. A set of well-formed formulas, called axioms.
4. A finite set of "deduction rules," i.e., rules which enable us to deduce a well-formed formula A (say) as a "direct consequence" of a finite set of well-formed formulas A1, A2, ..., Ak

 

Given these four conditions are satisfied, we can start with axioms and follow through deductive procedures by successive application of the rules of deductions. Formally, we define a formal system as follows:

The formal axiomatic theory, L, is defined by the following:

1. A countable set of symbols. The symbol of formal theory, , are ~, →, (, ), A1, A2, .... That is, the letter Ai with positive integer i as subscript. The symbols ~ and → are called primitive connectives, and the letter Ai are called statement letters. A finite sequence of symbols is called expression of the formal axiomatic theory, L.
2. There is a subset of the expressions called the set of well-formed formulas (wffs) of T. Instead of specifying the set explicitly we will give an inductive rule in three parts.
2a.  Ai is a well-formed formula for each i ≥ 1. In other words, all statement letters are wffs.
2b.  If A and B are wffs, then (~A) and (A → B) are wffs. Thus, well-formed formula of formal axiomatic theory, L, is just a statement form built up from the statement letters Ai by means of primitive connectives ~ and →.
2c.  The set of all well-formed formulas is generated by 2a and 2b.
3. A set of well-formed formulas called the set axioms of L. There are infinitely may axioms, so we cannot list them all. However, we can specify all of them by means of three axiom schemes. For any well-formed formula A, B and C of the formal axiomatic theory L, the following well-formed formulas are axioms of L.

Axiom A1:        (A → (B → A)).

Axiom A2:        ((A → (B → C)) → ((A → B) → (A → C))).

Axiom A3:        ((~A → ~B) → (~B → A) → B)).

Note that each axiom scheme has infinitely many "instances" as any well-formed formula of L can be substituted for statement letters A, B and C.

4. In formal axiomatic theory L there is only one rule of inference namely, law of detachment (modus ponens.) It says that B is a direct consequence of A and A → B.

 

Deduction (or Proof) in Formal Axiomatic Theory

A proof in the formal axiomatic theory, L, is a sequence of well-formed formulas

A1, A2, ..., An

such that for each i (1 ≤ i ≤ n) either Ai is an axiom of or Ai follows from two previous members of the sequence, say Aj and Ak (j < i, k < i) as a direct consequence using the rule of inference (law of detachment). Such a proof will be referred to as a proof of An in L , and An is said to be a theorem of L. 

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

Let Γ be a set of well-formed formulas in L . A sequence of well-formed formulas 

A1, A2, ..., An

is a deduction from the set Γ if for each i (where 1 ≤ i ≤ n), one of the following holds:

a.  Ai is an axiom of L.
b. Ai is a member of Γ. That is, Ai is in the set Γ.
c. Ai is a direct consequence of some preceding by some rule well-formed formulas (i.e. previous members) in the sequence by some rule of inference.

Such a sequence is called a proof (or deduction) of A from Γ and

Γ A

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

In other words, a deduction from Γ is just a "proof" in which members of Γ are considered as temporary axioms. The last member, An, of a sequence is said to be deducible from Γ, or to be a consequence of Γ in formal axiomatic theory L . If a well-formed formula A is the last member of some deduction from Γ, we say Γ yields A and write Γ A.

 

Lets conclude this section by saying that every proposition implies itself, and whatever is not a proposition implies nothing. Hence, to say 

"p is a proposition" 

is equivalent to saying

"p → p"

[Note that the above equivalence my be used to define proposition.]

 

As an example of proof construction, instead of proposition, let us use above implication for well-formed formula (or suppose the whole well-formed formula is a proposition [it works in any event]  as follows:

 

Lemma 1. For any well-formed formula A, A → A.

Proof. We shall construct a proof in L of A → A.

1. (A → ((A → A) → A)) → ((A → (A → A)) → (A → A)) Get the instance of Axiom A2 by substituting (A → A) for B and A for C.
2. A → ((A → A) → A) Get the instance of Axiom A1 by substituting (A → A) for B.
3. (A → (A → A)) → (A → A) From 1 and 2 by modus ponens.
5. A → (A → A) Get the instance of Axiom A1 by substituting A or B.
5. A → A From 3 and 4 by modus ponens.

 

As an example, suppose my mathematical system [or suppose L is some mathematical system and call it My Mathematical System] contains just the following axioms:

                                        MyAxiom 1: (x + y = z) → ((x < y ∧ (2 = 3))

                                        MyAxiom 2: (x + y = z)

 

MyLemma 0:  For any x and y, x < y.   [What are x and y - who gives the damn at this point.]

Formal Proof: We shall construct a proof in My_Mathematical_System of x < y.

1. (x + y = z) → ((x < y ∧ (2 = 3)) By MyAxiom 1.
2. (x + y = z) By MyAxiom 2.
3. (x < y ∧ (2 = 3) From 1 and 2 by modus ponens.
5. x < y By the tautology (p ∧ q) → p

This completes the formal proof.

 

Informal Proof:

From MyAxioms 1 and 2 it follows that

x < y ∧ (2 = 3).

Therefore, x < y.

This completes the informal proof.