ITL
© 1996-2016







4 Propositional proof system

In table 7 we list the propositional axioms and rules for ITL.


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