ITL
© 1996-2018







3 Derived proof system for chop-free temporal logic


( f) ; g (f ; g) NextChop


Proof:

1
(skip ; f) ; g skip ; (f ; g)
2
( f) ; g (f ; g)
1, def. of 


(f f1) (f ; g) (f1 ; g) BiChopImpChop


Proof:

1
g g
2
(g g)
3
(f f1) (g g) (f ; g) (f1 ; g)
4
(f f1) (f ; g) (f1 ; g)
2, 3,Prop


(g g1) (f ; g) (f ; g1) BoxChopImpChop


Proof:

1
f f
2
(f f)
3
(f f) (g g1) (f ; g) (f ; g1)
4
(g g1) (f ; g) (f ; g1)
2, 3,Prop


f f1 ⇒ ⊢ f ; g f1 ; g LeftChopImpChop


Proof:

1
f f1
given
2
(f f1)
3
(f f1) f ; g f1 ; g
4
f ; g f1 ; g
2, 3,MP


g g1 ⇒ ⊢ f ; g f ; g1 RightChopImpChop


1
g g1
given
2
(g g1)
3
(g g1) (f ; g) (f ; g1)
4
f ; g f ; g1
2, 3,MP

Here is a derived rule that is a corollary of RightChopImpChop:


g g1 ⇒ ⊢ f ; g f ; g1 RightChopEqvChop


We omit the proof.


f ; (g g1) f ; g f ; g1 ChopOrEqv


The proof for is immediate from axiom ChopOrImp. Here is the proof for the converse:

1
g g g1
2
f ; g f ; (g g1)
3
g1 g g1
4
f ; g1 f ; (g g1)
5
f ; g f ; g1 f ; (g g1)
2, 4,Prop


f f1 f2 ⇒ ⊢ f ; g (f1 ; g) (f2 ; g) OrChopImpRule


Proof:

1
f f1 f2
given
2
f ; g (f1 f2) ; g
3
(f f1) ; g f1 ; g f2 ; g
4
f ; g (f1 ; g) (f2 ; g)
2, 3,Prop


f f f1 ⇒ ⊢ f ; g (f1 ; g) (f2 ; g) OrChopEqvRule


Proof:

1
f f1 f2
given
2
f ; g (f1 f2) ; g
3
(f f1) ; g f1 ; g f2 ; g
4
f ; g (f1 ; g) (f2 ; g)
2, 3,EqvChain


f g ⇒ ⊢f g NextImpNext


Proof:

1
f g
given
2
(f g)
3
(f g) (skip ; f) (skip ; g)
4
(skip ; f) (skip ; g)
2, 3,MP
5
f g
4, def. of 


(f g) f g NextImpDist


Proof:

1
⊢ ¬(f g) f ¬g
2
skip ; ¬(f g) skip ; (f ¬g)
3
f g (f ¬g)
4
skip ; f (skip ; g) (skip ; (f ¬g))
5
⊢ ¬(skip ; (f ¬g)) (skip ; f) (skip ; g)
4,Prop
6
⊢ ¬(skip ; ¬(f g)) (skip ; f) (skip ; g)
2, 5,Prop
7
⊢ ¬¬(f g) f g
6, def. of 
8
(f g) ¬¬(f g)
9
(f g) f g
7, 8,Prop


f ; g g ChopImpDiamond


Proof:

1
f true
2
f ; g true ; g
3
f ; g g
2, def. of 


f f NowImpDiamond


Proof:

1
empty ; f f
2
empty true
3
empty ; f true ; f
4
f true ; f
1, 3,Prop
5
f f
4, def. of 


f f NextDiamondImpDiamond


Proof:

1
(skip ; true) ; f skip ; (true ; f)
2
(skip ; true) ; f f
1, def. of ,
3
(skip ; true) ; f f
4
f f
2, 3,Prop


f f f BoxImpNowAndWeakNext


Proof:

1
⊢ ¬f ¬f
2
⊢ ¬¬f f
1,Prop
3
f f
2, def. of 
4
¬f ¬f
5
⊢ ¬¬¬f ¬f
6
¬¬¬f ¬f
7
¬¬¬f ¬f
4, 6,ImpChain
8
¬f ¬f
7, def. of 
9
⊢ ¬¬f ¬¬f
8,Prop
10
f f
9, def. of ,
11
f f f
3, 10,Prop


f g f g BoxImpBoxRule


Proof:

1
f g
given
2
⊢ ¬g ¬f
1,Prop
3
(¬g ¬f)
4
(¬g ¬f) (true ; ¬g) (true ; ¬f)
5
true ; ¬g true ; ¬f
3, 4,MP
6
¬g ¬f
5, def. of 
7
⊢ ¬¬f ¬¬g
6,Prop
8
f g
7, def. of 


(f g) f g BoxImpDist


Proof:

1
f g ¬g ¬f
2
(f g) (¬g ¬f)
3
(¬g ¬f) (true ; ¬g) (true ; ¬f)
4
(f g) (true ; ¬g) (true ; ¬f)
2, 3,Prop
5
(f g) ¬g ¬f
4, def. of 
6
(f g) ¬¬f ¬¬g
5,Prop
7
(f g) f g
6, def. of 


empty DiamondEmpty


Proof:

1
true
2
true ; empty true
3
true ; empty
1, 2,Prop
4
empty
3, def. of 

Here are some use derived rules for linear time temporal logic. We omit their proofs:


f g ⇒ ⊢f g NextEqvNext



f g h ⇒ ⊢f g h NextAndNextImpNextRule



f g h ⇒ ⊢f g h NextAndNextEqvNextRule



f g ⇒ ⊢f g WeakNextEqvWeakNext



f g ⇒ ⊢f g DiamondImpDiamond



f g ⇒ ⊢f g DiamondEqvDiamond



f g ⇒ ⊢f g BoxImpBox



f g ⇒ ⊢f g BoxEqvBox



f g h ⇒ ⊢f g h BoxAndBoxImpBoxRule



f g h ⇒ ⊢f g h BoxAndBoxEqvBoxRule



f g, more f f ⇒ ⊢ f g BoxIntro



(f ¬g) f ⇒ ⊢ f g DiamondIntro



f f ⇒ ⊢¬f NextLoop



f ¬g f ¬g ⇒ ⊢ f g NextContra



f f ⇒ ⊢ f WeakNextBoxInduct



empty f, f f ⇒ ⊢ f EmptyNextInducta



empty f g,(f g) f g ⇒ ⊢ f g EmptyNextInductb



f g ⇒ ⊢ fin f fin g FinImpFin



f g ⇒ ⊢ fin f fin g FinEqvFin



f g h ⇒ ⊢ fin f fin g fin h FinAndFinImpFinRule



f g h ⇒ ⊢ fin f fin g fin h FinAndFinEqvFinRule



f g ⇒ ⊢ halt f halt g HaltImpHalt



f g ⇒ ⊢ halt f halt g HaltEqvHalt


Note that ImpChain can be viewed as a special case of Prop. If desired, a deduction theorem can also be proved.

We now give proofs of some derived inference rules and theorems:


(f g) f g BiImpDiImpDi


Proof:

1
(f g) (f ; true) (g ; true)
2
(f g) f g
1, def. of 


f g ⇒ ⊢f g DiImpDi


Proof:

1
f g
given
2
f ; true g ; true
3
f g
2, def. of 

Another corollary is the following:


f g ⇒ ⊢f g BiImpBiRule


Proof:

1
f g
given
2
⊢ ¬g ¬f
1,Prop
3
¬g ¬f
4
⊢ ¬¬f ¬¬g
3,Prop
5
f g
4, def. of 


f f1 ⇒ ⊢ f ; g f1 ; g LeftChopEqvChop


Proof:

1
f f1
given
2
f f1
1,Prop
3
f ; g f1 ; g
4
f1 f
1,Prop
5
f1 ; g f ; g
6
f ; g f1 ; g
3, 5,Prop

Here is a corollary for the operator :


f g ⇒ ⊢f g DiEqvDi


Proof:

1
f f1
given
2
f ; true g ; true
3
f g
2, def. of 

Here is a corollary for the operator :


f g ⇒ ⊢f g BiEqvBi


Proof:

1
f g
given
2
⊢ ¬f ≡¬g
1,Prop
3
¬f ¬g
4
⊢ ¬¬f ≡¬¬g
3,Prop
5
f g
4, def. of 


f ; g g ⇒ ⊢ f ; g ; h g ; h LeftChopChopImpChopRule


Proof:

1
f ; g g
given
2
(f ; g) ; h g ; h
3
(f ; g) ; h f ; g ; h
4
f ; g ; h g ; h
2, 3,Prop


(f f1) ; g (f1 f) ; g AndChopCommute


Proof:

1
f f1 f1 f
2
(f f1) ; g (f1 f) ; g


w f f1 ⇒ ⊢ w (f ; g) (f1 ; g) StateAndChopImpChopRule


Proof:

1
w f f1
given
2
(w f) ; g f1 ; g
3
(w f) ; g w (f ; g)
4
w f ; g f1 ; g
2, 3,Prop


w (f f1) ⇒ ⊢ w ((f ; g) (f1 ; g)) StateImpChopEqvChop


Proof:

1
w f f1
given
2
w f f1
1,Prop
3
w (f ; g) (f1 ; g)
4
w f1 f
1,Prop
5
w (f1 ; g) (f ; g)
6
w (f ; g) (f1 ; g)
3, 5,Prop


f w f1 ⇒ ⊢ (f ; g) w (f1 ; g) ChopEqvStateAndChop


Proof:

1
f w f1
given
2
f ; g (w f1) ; g
3
(w f1) ; g w (f1 ; g)
4
(f ; g) w (f1 ; g)
2, 3,EqvChain


f f DiIntro


Proof:

1
f ; empty f
2
empty true
3
(empty true)
4
(empty true) (f ; empty f ; true)
5
f ; empty f ; true
3, 4,MP
6
f ; empty f
5, def. of 
7
f f
1, 6,Prop

The following is a corollary of DiIntro:


f f BiElim


Proof:

1
⊢ ¬f ¬f
2
(¬f ¬f) (¬¬f f)
3
⊢ ¬¬f f
1, 2,MP
4
f f
3, def. of 

The following is used in the proof of lemma BiImpDist:


(¬g ¬f) ( f) ( g) BiContraPosImpDist


Proof:

1
(¬g ¬f) ( ¬g) ( ¬f)
2
(¬g ¬f) (¬¬f) (¬¬g)
1,Prop
3
(¬g ¬f) ( f) ( g)
2, def. of 


(f g) ( f) ( g) BiImpDist


Proof:

1
(f g) (¬g ¬f)
2
⊢ ¬(¬g ¬f) ¬(f g)
1,Prop
3
(¬(¬g ¬f) ¬(f g))
4
(¬(¬g ¬f) ¬(f g))
(f g) (¬g ¬f)
5
(f g) (¬g ¬f)
3, 4,MP
6
(¬g ¬f) ( f) ( g)
7
(f g) ( f) ( g)
5, 6,ImpChain


(f f1) ; g f ; g f1 ; g OrChopEqv


The proof for is immediate from axiom OrChopImp. Here is the proof for the converse:

1
f f f1
2
f ; g (f f1) ; g
3
f1 f f1
4
f1 ; g (f f1) ; g
5
f ; g f ; g1 (f f1) ; g
2, 4,Prop


f if w then f1 else f2 ⇒ ⊢ f ; g if w then (f1 ; g) else (f2 ; g) IfChopEqvRule


Proof:

1
f if w then f1 else f2
given
2
f (w f1) (¬w f2)
1,Prop
3
f ; g (w f1) ; g (¬w f2) ; g
4
(w f1) ; g w (f1 ; g)
5
(¬w f2) ; g ≡¬w (f2 ; g)
6
f ; g (w f1 ; g) (¬w f2 ; g)
3, 4, 5,Prop
7
f ; g if w then f1 ; g else f2 ; g
6,Prop


g g1 g2 ⇒ ⊢ f ; g (f ; g1) (f ; g2) ChopOrImpRule


Proof:

1
g g1 g2
given
2
f ; g f ; (g1 g2)
3
f ; (g g) f ; g1 f ; g2
4
f ; g (f ; g1) (f ; g2)
2, 3,Prop


g g1 g2 ⇒ ⊢ f ; g (f ; g1) (f ; g2) ChopOrEqvRule


Proof:

1
g g1 g2
given
2
f ; g f ; (g1 g2)
3
(f f1) ; g f1 ; g f2 ; g
4
f ; g (f1 ; g) (f2 ; g)
2, 3,EqvChain


(empty f) ; g g (f ; g) EmptyOrChopEqv


Proof:

1
(empty f) ; g (empty ; g) (f ; g)
2
empty ; g g
3
(empty f) ; g g (f ; g)
1, 2,Prop


(empty f) ; g g (f ; g) EmptyOrNextChopEqv


Proof:

1
(empty f) ; g g (( f) ; g)
2
( f) ; g (f ; g)
3
(empty f) ; g g (f ; g)
1, 2,Prop


f empty f1 ⇒ ⊢ f ; g g (f1 ; g) EmptyOrChopImpRule


Proof:

1
f empty f1
given
2
f ; g (empty f1) ; g
3
(empty f1) ; g g (f1 ; g)
4
f ; g g (f1 ; g)
2, 3,Prop

Here is a related lemma:


f empty f1 ⇒ ⊢ f ; g g (f1 ; g) EmptyOrChopEqvRule


Proof:

1
f empty f1
given
2
f ; g (empty f) ; g
3
(empty f) ; g g (f ; g)
4
f ; g g (f ; g)
2, 3,Prop

The following is a useful special case of EmptyOrChopImpRule:


f empty f1 ⇒ ⊢ f ; g g (f1 ; g) EmptyOrNextChopImpRule


Proof:

1
f empty f1
given
2
f ; g (empty f1) ; g
3
(empty f1) ; g g (f1 ; g)
4
f ; g g (f1 ; g)
2, 3,Prop

The following an analogous special case of EmptyOrChopEqvRule:


f empty f1 ⇒ ⊢ f ; g g (f1 ; g) EmptyOrNextChopEqvRule


Proof:

1
f empty f1
given
2
f ; g (empty f1) ; g
3
(empty f1) ; g g (f1 ; g)
4
f ; g g (f1 ; g)
2, 3,Prop

Here is a corollary of ChopOrImpRule:


g empty g1 ⇒ ⊢ f ; g f (f ; g1) ChopEmptyOrImpRule


Proof:

1
g empty g1
given
2
f ; g (f ; empty) (f ; g1)
3
f ; empty f
4
f ; g f (f ; g1)
2, 3,Prop


w ; w w BoxStateChopBoxEqvBox


Proof for :

1
w w (empty w)
2
w ; w w ((empty w) ; w)
3
(empty w) ; w w ( w ; w)
4
w ; w w ( w ( w ; w))
2, 3,Prop
5
⊢ ¬w ¬w ¬w
6
( w ; w) ¬w ( w ; w) ¬
4, 5,Prop
7
w ; w w

Proof for :

1
w w w
2
empty ; w w
3
(w empty) ; w w (empty ; w)
4
w (w empty) ; w
1, 2, 3,Prop
5
w empty w
6
(w empty) ; w w ; w
7
w w ; w
4, 6,Prop


¬w ( w) ¬w NotBoxStateImpBoxYieldsNotBox


Proof:

1
w ; w w
2
w ≡¬¬w
3
w ; w w ; ¬¬w
4
⊢ ¬w ¬( w ; ¬¬w)
1, 3,Prop
5
⊢ ¬w ( w) ¬w
4, def. of 


w (f ; g) ( w f) ; ( w g) BoxStateAndChopEqvChop


Proof for :

1
w w
2
w (f ; g) ( w f) ; ( w g)

Proof for :

1
( w f) ; ( w g) ( w) ; ( w g)
2
( w) ; ( w g) ( w) ; ( w)
3
( w) ; ( w) w
4
( w f) ; ( w g) f ; ( w g)
5
f ; ( w g) f ; g
6
( w f) ; ( w g) w (f ; g)
1, 2, 3, 4, 5,Prop

See also the lemma BoxStateAndCSEqvCS for chop-star.


w w StateEqvBi


Proof:

1
w w
2
w w
3
w w
1, 2,Prop


¬f ≡¬f DiNotEqvNotBi


Proof:

1
f ≡¬¬f
def. of 
2
¬f ≡¬f


f ≡¬¬f DiEqvNotBiNot


Proof:

1
¬f ≡¬¬¬f
def. of 
2
¬¬f ≡¬¬f
1,Prop
3
f ≡¬¬f
4
f ¬¬f
5
f ≡¬¬f


h f ; g f ; (h g) BoxAndChopImport


Proof:

1
h g (h g)
2
h (g (h g))
3
(g (h g)) f ; g f ; (h g)
4
h f ; g f ; (h g)
2, 3,Prop


f ; g h f ; (g h) ChopAndBoxImport


Proof:

1
h f ; g f ; (h g)
2
f ; (h g) f ; (g h)
3
h f ; g f ; (g h)
1, 2,Prop

The following are easily proved:


f ; (g g1) f ; g ChopAndA



f ; (g g1) f ; g1 ChopAndB



f ; (g g1) f ; (g1 g) ChopAndCommute



(f g) ; (f1 g1) (g f) ; (g1 f1) AndChopAndCommute


Proof:

1
(f g) ; (f1 g1) (g f) ; (f1 g1)
2
(g f) ; (f1 g1) (g f) ; (g1 f1)
3
(f g) ; (f1 g1) (g f) ; (g1 f1)
1, 2,EqvChain


f f1, g g1 ⇒ ⊢ f ; g f1 ; g1 ChopImpChop


Proof:

1
f f1
given
2
f ; g f1 ; g
3
g g1
given
4
f1 ; g f1 ; g1
5
f ; g f1 ; g1
2, 4,ImpChain


f f1, g g1 ⇒ ⊢ f ; g f1 ; g1 ChopEqvChop


Proof:

1
f f1
given
2
f ; g f1 ; g
3
g g1
given
4
f1 ; g f1 ; g1
5
f ; g f1 ; g1
2, 4,EqvChain


f1 g1,,fn gn ⇒ ⊢ (f1 ; ; fn) (g1 ; gn) MultChopImpChop


Proof is by induction on n.
Proof for n = 1:

1
f1 g1
given

Proof for n > 1:

1
f1 g1
given
2
fi gi, for 2 i n
given
3
(f2 ; ; fn) (g2 ; gn)
2,induction
4
f1 ; f2 ; ; fn g1 ; g2 ; gn


h f ; g f ; ( h g) BoxChopImpChopBox


Proof:

1
h (g h g)
2
(g h g) f ; g f ; ( h g)
3
h f ; g f ; ( h g)
1, 2,Prop


¬(f ; g) f ¬g NotChopEqvYieldsNot


1
g ≡¬¬g
2
f ; g f ; ¬¬g
3
⊢ ¬(f ; g) ≡¬(f ; ¬¬g)
2,Prop
4
⊢ ¬(f ; g) ≡¬(f g)
def. of 

The following lemma TrueChopEqvDiamond is no longer needed since is now defined in terms of chop:


true ; f f TrueChopEqvDiamond


The proof of is immediate by the following former axiom:


true ; f f TrueChopImpDiamond



f true ; f DiamondImpTrueChop


Proof:

1
f f f
2
true empty true
3
true ; f (empty true) ; f
4
(empty true) ; f empty ; f ( true) ; f
5
empty ; f f
6
( true) ; f (true ; f)
7
true ; f f (true ; f)
3, 4, 5, 6,Prop
8
f ¬(true ; f) f ¬(true ; f)
1, 7,Prop
9
f true ; f


f (f1 ; g) (f f1) ; g BiAndChopImport


Proof:

1
f (f1 f f1)
2
f (f1 f f1)
3
(f1 f f1) f ; g (f f1) ; g
4
f ; g (f f1) ; g
1, 3,MP







2018-02-26
Contact | Home | ITL home | Course | Proofs | Algebra | FL