Help
Index

Maarten Maartensz:    Philosophical Dictionary | Filosofisch Woordenboek

L  - Logic - Basic - semantics - Note MT2

This note contains the proof of the following proposition:

MT2. The PL-part of BL entails standard classical propositional logic.

The strategy for proving MT2 is to prove that the PL-part of BL entails the axioms of Hilbert-Bernays for CPL. These are well-known, and specified by Wang, 'Logic, Computers and Sets' p. 308, as follows:

HB1a.  P --> (Q --> P)
HB1b. (P --> (P --> Q)) --> (P --> Q)
HB1c. (P --> Q) --> ((Q --> R) --> (P --> R))
HB2a. (P&Q) --> P
HB2b. (P&Q) --> Q
HB2c. (P --> Q) --> ( (P --> R) --> (P --> (Q&R)) )
HB3a.  P --> (PVQ)
HB3b.  Q --> (PVQ)
HB3c. (P --> Q) --> ( (Q --> R) --> ((PVQ) --> R)) )
HB4a. (P IFF  Q) --> (P -->Q)
HB4b. (P IFF  Q) --> (Q -->P)
HB4c. (P --> Q) --> ( (Q --> P) --> (P IFF Q) ) )
HB5a. (P --> Q) --> (~Q --> ~P)
HB5b.  P --> ~~P
HB5c.  ~~P --> P

For convenience of reference, here is the PL-part of BL:

Argument rules

Rep |- (Si |= Si)
IFe  |- (Sk |= Sn  |= ~Sk V Sn)
IFi   |- (~Sk V Sn |=  Sk |= Sn)

Assumption rules

Ai   |- (Si*)
Ae  |- (Si* .. Sn) |= (Si |= Sn)) - if Si is the last assumption in (S Si* .. Sn)

Conjunction rules

Ci    |- (Si .. Sk) |= Si&Sk)
Ce1 |- (Si&Sk)   |= (Si)
Ce2 |- (Si&Sk)   |= (Sk)

Disjunction rules

Di1  |- (Si)                  |= (SiVSj)
Di2  |- (Sj)                  |= (SiVSj)
De   |- (SiVSj .. ~SiVSj) |= (Sj)

Definitions of logical constants

|- 'Si --> Sj' for '~SiVSj'
|- 'Si IFF Sj' for 'Si --> Sj & Sj --> Si'

Substitution rules

Var  |- If |-(A) and (A') is a variant of (A), then |-(A')
Sub |- If |-(A), then |-B|C.A

In the substitution-rules, the term 'variant' is explained as follows. The term 'expression' stands for 'a sequence of terms', regardless of whether we can attribute a meaning to an expression. Now, if A and B are two expression, then B is said to be a variant of A if and only if whenever the i-th and the j-th terms of A are the same so are the i-th and the j-th terms of B and whenever the i-th term of A is a constant the i-th term of B is the same constant.

Intuitively speaking, a variant of A is just the same as A except for variables, and the variables of a variant of A preserve the pattern of the variables in A.

The Sub rule enables us to expand a valid proposition to a longer one, by substituting longer formulas for propositional variables.

Now to prove the HB-axioms in BL, it is necessary first to prove some other theorems.

Theorems:

 T1: |- ~Si V Si Proof: (1) Si |= Si Rep (2) ~Si V Si 1, IFe
 T2: |- Si V Si |= Si Proof: (1)   Si V Si Ai (2) ~Si V Si T1 (3)   Si 1,2,De (4)   Si V Si |= Si 1,3, Ae

In the proofs that follow last steps like the last step in the above proof will be left out as obvious.

 T3: |- ((Si|= Sj) & Si )|= Sj (Rule MP) Proof: (1) (Si |= Sj) & Si Ai (2) Si |= Sj 1, Ce1 (3) Si 1, Ce2 (4) ~SiVSj 2, IFe (5) SiVSj 3, Di (6) Sj 4,5, De
 T4: |- Si |= Sj&~Sj |= ~Si (Rule Noti ) Proof: (1)  Si |= Sj&~Sj Ai (2)  Si Ai (3)  Sj&~Sj 1,2,MP (4)  ~Sj 3, Ce2 (5)  ~SjV~Si 4, Di1 (6)  Sj 3, Ce1 (7)  SjV~Si 6, Di1 (8)  ~Si 5,7, De (9)  ~SiV~Si 2,8, Ae (10) ~Si 9,T2
 T5: |- ~~Si |= Si Proof: (1)  ~~Si AI (2)  ~~Si V Si 1,Di1 (3)  ~Si V Si T1 (4)  Si 2,3,De
 T6: |- Si |= ~~Si Proof: (1)  Si AI (2)  ~~~Si AI (3)  ~Si 2, T5 (4)  Si&~Si 1,3, Ci (5)  ~~~Si |= Si&~Si 2,4, Ae (6)  ~~~~Si 5, DNi (7)  ~~Si 6, T5
 T7: |- ~(SiVSj) |= ~Si&~Sj Proof: (1)    ~(SiVSj) AI (2)    Si AI (3)    SiVSj 2, Di1 (4)    SiVSj & ~(SiVSj) 1,3, Ci (5)    Si |= SiVSj & ~(SiVSj) 2,4, Ae (6)    ~Si 5, Sub, Noti (7)    Sj AI (8)    SiVSj 7,  Di2 (9)    SiVSj & ~(SiVSj) 1,8, Ci (10)   Sj |= SiVSj & ~(SiVSj) 7,9, Ae (11)  ~Sj 10, Sub, DNi (12) ~Si&~Sj 6,11, Ci
 T8: |- Si V Sj |= Sj V Si Proof: (1)   Si V Sj Ai (2)   ~(Sj V Si) Ai (3)   ~Sj & ~Si 2, T7 (4)   ~Si 3, Ce2 (5)   ~Si V Sj 4, Di1 (6)   Sj 1,5, De (7)   ~Sj 3, Ce1 (8)   Sj & ~Sj 6,7, Ci (9)   ~(Sj V Si) |= Sj & ~Sj 2,8, Ae (10)  ~~(Sj V Si) 9, DNi (11) Sj V Si 10, T5
 T9: |- ~(Si & ~Si) Proof: (1) (Si & ~Si) |= (Si & ~Si) Sub, Rep (2) ~(Si & ~Si) 1, Noti
 T10: |- (Si |= Sj) |= (~Sj |= ~Si) (1) Si |= Sj Ai (2) ~Sj Ai (3) ~Si V Sj 1, IFe (4) Sj V ~Si 3, T8 (5) ~Sj V ~Si 2, Ci1 (6) ~Si 4,5, De (7) ~Sj |= ~Si 2,6, Ae

Now to prove the axioms of Hilbert-Bernays for CPL I will presuppose
that P|=Q and P --> Q are equivalent, as is also easily provable.

 T11: |- Si |= (Sj |= Si) (HB1a) Proof: (1) Si AI (2) ~Sj V Si 1, Ci2 (3) Sj |= Si 2, IFi
 T12: |- (Si |= (Si |= Sj)) |= (Si |= Sj) (HB1b) Proof: (1) (Si |= (Si |= Sj)) Ai (2) Si Ai (3) Si |= Sj 1,2, MP (4) Sj 2,3, MP (5) Si |= Sj 2,4, Ae
 T13: |- Si|=Sj  |= (Sj|=Sk |= Si|=Sk) (HB1c) Proof: (1) Si|=Sj Ai (2) Sj|=Sk Ai (3) Si Ai (4) Sj 1,3, MP (5) Sk 2,4, MP (6) Si|=Sk 3,5, Ae (7) Sj|=Sk |= Si|=Sk 2,6, Ae
 T14: |- Si|=Sj |= ((Si|=Sk) |= Si|=(Sj&Sk)) Proof: (1) Si|=Sj Ai (2) Si|=Sk Ai (3) Si Ai (4) Sj 1,3, MP (5) Sk 2,4, MP (6) Sj&Sk 4,5, Ci (7) Si |= Sj&Sk 3,6, Ae (8) Si|=R |= Si |= Sj&Sk 2,7, Ae
 T15: |- Si|=Sj |= Sj|=R |= SiVSj|=Sk (1)  Si|=Sj Ai (2)  Sj|=Sk Ai (3)  SiVSj Ai (4)  ~Sk Ai (5)  ~Sj 2,4, T10 (6)  ~Si 1,5, T10 (7)  ~PVSj 6, Di1 (8)  Sj 3,7, De (9) Sj&~Sj 5,8, Ci (10) ~Sk |= Q&~Q 4,9, Ae (11) ~~Sk 10, Noti (12) Sk 11, T5 (13) SiVSj |= Sk 3, 12, Ae (14) Sj|=Sk |= SiVSj|=Sk 2, 13, Ae

The other axioms of HB have been proved or assumed already:

HB2a and HB2b are the Ce-rules.
HB3a and HB3b are the Di-rules.
HB4a and HB4b and HB4c are consequences of the definition of IFF.
HB5a is T10.
HB5b is T6.
HB5c is T5.

Thus all axioms for PL of Hilbert-Bernays are derivable in BL. Qed.

Literature:

Original: May 7, 2005                                                Last edited: 12 September 2005.