First order proof system

Some axioms for the ﬁrst order case are shown in Table 8.
Let V denote a state variable.
We denote by f [e ∕ V ] that in formula f expression e is substituted for variable V .

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

ForallSub	⊢ ∀V f ⊃ f [e ∕ V ],
	where the expression e has the same data
	and temporal type as the variable V and
	is free for V in f.
ForallImplies	⊢ ∀V (f₁ ⊃ f₂) ⊃ (f₁ ⊃ ∀V f₂),
	where V doesn’t occur freely in f₁.
SubstAxiom	⊢ (V ₁ = V ₂) ⊃ f ≡ f [V ₂ ∕ V ₁].
ExistsChopRight	⊢ ∃V (f₁ ; f₂) ⊃ (∃V f₁) ; f₂,
	where V doesn’t occur freely in f₂.
ExistsChopLeft	⊢ ∃V (f₁ ; f₂) ⊃ f₁ ; (∃V f₂),
	where V doesn’t occur freely in f₁.
ForallGen	⊢ f ⇒ ⊢ ∀V f,
	for any variable V .

2.5 First order proof system