#### 8.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

Proof:

 1 g ⊃g 2 (g ⊃g) 1,BoxGen 3 (f ⊃f1) ∧(g ⊃g) ⊃(f ⌢ g) ⊃(f1 ⌢ g) BfAndBoxImpChopImpChop 4 (f ⊃f1) ⊃(f ⌢ g) ⊃(f1 ⌢ g) 2, 3,Prop

qed

 ⊢ (g ⊃g1) ⊃(f ⌢ g) ⊃(f ⌢ g1) BoxChopImpChop

Proof:

 1 ﬁnite ⊃(f ⊃f) 2 (f ⊃f) 1,BfFGen 3 (f ⊃f) ∧(g ⊃g1) ⊃(f ⌢ g) ⊃(f ⌢ g1) BfAndBoxImpChopImpChop 4 (g ⊃g1) ⊃(f ⌢ g) ⊃(f ⌢ g1) 2, 3,Prop

qed

 ⊢ (g ≡ g1) ⊃(f ⌢ g) ≡ (f ⌢ g1) BoxChopEqvChop

Proof:

 1 (g ≡ g1) ≡(g ⊃g1) ∧(g1 ⊃g) 2 (g ⊃g1) ⊃(f ⌢ g) ⊃(f ⌢ g1) BoxChopImpChop 3 (g1 ⊃g) ⊃(f ⌢ g1) ⊃(f ⌢ g) BoxChopImpChop 4 (g ≡ g1) ⊃(f ⌢ g) ≡ (f ⌢ g1) 2, 3,Prop

qed

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

 ⊢ f ⇒ ⊢ f BfGen

Proof:

 1 f Assump 2 ﬁnite ⊃f 1,Prop 3 f 2,BfFGen

qed

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

Proof:

 1 f ⊃f1 Assump 2 (f ⊃f1) 1,BfGen 3 (f ⊃f1) ⊃(f ⌢ g) ⊃(f1 ⌢ g) BfChopImpChop 4 f ⌢ g ⊃f1 ⌢ g 2, 3,MP

qed

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

Proof:

 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

qed

 ⊢ f ⊃g ⇒ ⊢ f ⊃g DfImpDf

Proof:

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

qed

 ⊢ f ≡ g ⇒ ⊢ f ≡g DfEqvDf

Proof:

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

qed

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

Proof:

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

qed

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

Proof:

 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

qed

 ⊢ f ≡ g ⇒ ⊢ f ≡g DiamondEqvDiamond

Proof:

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

qed

 ⊢ f ≡ g ⇒ ⊢ f ≡g BoxEqvBox

Proof:

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

qed

 ⊢ f ⊃g ⇒ ⊢ f ⊃g BoxImpInferBoxImpBox

Proof:

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

qed

 ⊢ (f ∧ f1) ⌢ g ⊃f ⌢ g AndChopA

Proof:

 1 f ∧ f1 ⊃f 2 (f ∧ f1) ⌢ g ⊃f ⌢ g

qed

 ⊢ (f ∧ f1) ⌢ g ⊃f1 ⌢ g AndChopB

Proof:

 1 f ∧ f1 ⊃f1 2 (f ∧ f1) ⌢ g ⊃f1 ⌢ g

qed

 ⊢ (f ∧ f1) ⌢ g ⊃(f ⌢ g) ∧ (f1 ⌢ g) AndChopImpChopAndChop

Proof:

 1 (f ∧ f1) ⌢ g ⊃f ⌢ g AndChopA 2 (f ∧ f1) ⌢ g ⊃f1 ⌢ g AndChopB 3 (f ∧ f1) ⌢ g ⊃(f ⌢ g) ∧ (f1 ⌢ g) 1, 2,Prop

qed

 ⊢ (f ∧ f1) ⌢ g ≡ (f1 ∧ f) ⌢ g AndChopCommute

Proof:

 1 f ∧ f1 ≡ f1 ∧ f 2 (f ∧ f1) ⌢ g ≡ (f1 ∧ f) ⌢ g

qed

 ⊢ (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

qed

 ⊢ f ⌢ g ⊃f ChopImpDf

Proof:

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

qed

 ⊢ empty DfEmpty

Proof:

 1 empty ⌢ true ≡ true EmptyChop 2 empty ⌢ true ⊃ empty ChopImpDf 3 empty 1, 2,Prop

qed

 ⊢ f ⌢ g ⊃g ChopImpDiamond

Proof:

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

qed

 2018-10-21 Contact | Home | ITL home | Course | Proofs | Algebra | FL