#### 1.2 First-Order Axioms and Inference Rules

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 v1 refer to both static and state variables.

 ⊢ All substitution instances of valid nonmodal formulas BasicFOL of conventional ﬁrst-order logic with arithmetic ⊢ ∀v f ⊃ f[e∕v], ForallElim where the expression e has the same data and temporal type as the variable v and is free for v in f. ⊢ ∀v (f ⊃g) ⊃ (f ⊃∀v g), ForallImpExportLeft where v doesn’t occur freely in f. ⊢ (v1 = v2) ⊃ f ≡ f[v2∕v1]. SubstAxiom ⊢ w ⊃w, StaticWeakNext where w only contains static variables. ⊢ ∃v (f ; g) ⊃ (∃v f) ; g, OuterExistsChopImpLeftExistsChop where v doesn’t occur freely in g. ⊢ ∃v (f ; g) ⊃ f ; (∃v g), OuterExistsChopImpRightExistsChop where v doesn’t occur freely in f. ⊢ f ⇒ ⊢ ∀v f, ForallGen for any variable v.

 2018-02-26 Contact | Home | ITL home | Course | Proofs | Algebra | FL