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 ~S 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.

 


 See also: Basic Logic - semantics, Logic, Logic Notation


Literature:

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