ITL
© 1996-2018







17.1 Some Basic Properties of Chop

We now consider deducing various simple properties of chop and the associated operators , , and which have a wide range of uses.


(f f1) (f g) (f1 g) BfChopImpChop


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


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


(g g1) (f g) (f g1) BoxChopEqvChop


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

The following derived variant of Inference Rule BfFGen omits the subformula finite:


f ⇒ ⊢ f BfGen


1
f
Assump
2
finite f
1,Prop
3
f

The derived inference rule BfGen can also be referred to as Gen (analogous to the inference rule BoxGen).


f f1 ⇒ ⊢ (f g) (f1 g) LeftChopImpChop


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


f f1 ⇒ ⊢ (f g) (f1 g) LeftChopEqvChop


1
f f1
Assump
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


f g ⇒ ⊢ f g DfImpDf


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


f g ⇒ ⊢ f g DfEqvDf


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


g g1 ⇒ ⊢ (f g) (f g1) RightChopImpChop


1
g g1
Assump
2
(g g1)
3
(g g1) (f g) (f g1)
4
f g f g1
2, 3,MP


g g1 ⇒ ⊢ (f g) (f g1) RightChopEqvChop


1
g g1
Assump
2
g g1
1,Prop
3
f g f g1
4
g1 g
1,Prop
5
f g1 f g
6
f g f g1
3, 5,Prop


f g ⇒ ⊢ f g DiamondEqvDiamond


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


f g ⇒ ⊢ f g BoxEqvBox


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


f g ⇒ ⊢ f g BoxImpInferBoxImpBox


1
f g
Assump
2
( f g)
3
( f g) ( f g)
4
f g
2, 3,MP


(f f1) g f g AndChopA


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


(f f1) g f1 g AndChopB


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


(f f1) g (f g) (f1 g) AndChopImpChopAndChop


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


(f f1) g (f1 f) g AndChopCommute


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


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


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

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 g f ChopImpDf


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


empty DfEmpty


1
empty true true
2
empty true empty
3
empty
1, 2,Prop


f g g ChopImpDiamond


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







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