In Table 7 we list the propositional axioms and rules for finite ITL.
ChopAssoc |
⊢ (f0 ; f1) ; f2 ≡ f0 ; (f1 ; f2) |
OrChopImp |
⊢ (f0 ∨ f1) ; f2 ⊃ (f0 ; f2) ∨ (f1 ; f2) |
ChopOrImp |
⊢ f0 ; (f1 ∨ f2) ⊃ (f0 ; f1) ∨ (f0 ; f2) |
EmptyChop |
⊢ empty ; f ≡ f |
ChopEmpty |
⊢ f ; empty ≡ f |
BiBoxChopImpChop |
⊢ (f0 ⊃ f1) ∧ (f2 ⊃ f3) ⊃ (f0 ; f2) ⊃ (f1 ; f3) |
StateImpBi | ⊢ w ⊃ w |
NextImpNotNextNot |
⊢ f ⊃ ¬¬f |
BoxInduct |
⊢ f ∧ (f ⊃ f) ⊃ f |
ChopStarEqv |
⊢ f∗≡ (empty ∨ ((f ∧ more) ; f∗)) |
MP |
⊢ f0 ⊃ f1, ⊢ f0 ⇒ ⊢ f1 |
BoxGen |
⊢ f0 ⇒ ⊢ f0 |
BiGen |
⊢ f0 ⇒ ⊢ f0 |