Below are axioms and inference rules for reasoning about ﬁrst-order concepts. They are to be used together
with the ones already introduced. See Manna and Kröger for proof systems for chop-free ﬁrst-order
temporal logic. We let v and v_{1} refer to both static and state variables.

⊢

All substitution instances of valid nonmodal formulas