First order proof system

Some axioms for the first order case are shown in Table 8.
Let $v$ refer to both static and state variables.
We denote by $f ev$ that in formula $f$ expression $e$ is substituted for variable $v$ .

Table 8: Some First Order Axioms and Rules for ITL.

|--------------------------------------------------------------------| | ForallSub ⊢ ∀v o f ⊃ fve, | | where the expression e has the same data and | | temporal type as the variable v and is free for | | v in f. | | ForallImplies ⊢ ∀v o (f1 ⊃ f2) ⊃ (f1 ⊃ ∀v o f2), | | where v doesn’t occur freely in f . | | SubstAxiom ⊢ ! (A = B ) ⊃ f ≡ fB . 1 | | StaticWeakNext ⊢ w ⊃ w, A | | c | | whereow only containsostatic variables. | | ExistsChopRight ⊢ ∃v (f1;f2) ⊃ (∃v f1);f2, | | whereov doesn’t occur freeoly in f2. | | ExistsChopLeft ⊢ ∃v (f1;f2) ⊃ f1;(∃v f2), | | where v doesn’t occur freely in f1. | | ForallGen ⊢ f ⇒ ⊢ ∀v o f , | | for any variable v. | ---------------------------------------------------------------------| ---------------------------------------------------------------------

5 First order proof system