Propositional proof system

Table 7: Propositional Axioms and Rules for 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; f1 ≡ f1 | |ChopEmpty ⊢ f ;empty ≡ f | | 1 1 | |BiBoxChopImpChop ⊢ I(f0 ⊃ f1) ∧ ! (f2 ⊃ f3) ⊃ (f0;f2) ⊃ (f1;f3) | |StateImpBi ⊢ p ⊃ I p | |NextImpNotNextNot ⊢ Cf0 ⊃ ¬ C ¬f0 | |KeepnowImpNotKeepnowNot ⊢ keepnow (f0) ⊃ ¬ keepnow(¬f0 ) | |BoxInduct ⊢ f0 ∧ !(f0 ⊃ c f0) ⊃ ! f0 | |InfChop ⊢ (f0 ∧ inf);f1 ≡ (f0 ∧ inf) | |ChopStarEqv ⊢ f *≡ (empty ∨ ((f0 ∧ more) ;f*)) | |ChopstarInduct ⊢ (0inf ∧ f ∧ ! (f ⊃ (f ∧ fmore 0);f )) ⊃ f * | | 0 0 1 0 1 | |MP ⊢ f0 ⊃ f1, ⊢ f0 ⇒ ⊢ f1 | |BoxGen ⊢ f0 ⇒ ⊢ ! f0 | |BiGen ⊢ f0 ⇒ ⊢ I f0 | | | ----------------------------------------------------------------------------