© 1996-2018

1.2 First-Order Axioms and Inference Rules

Below are axioms and inference rules for reasoning about first-order concepts. They are to be used together with the ones already introduced. See Manna and Kröger for proof systems for chop-free first-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 first-order logic with arithmetic
v f f[ev], 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[v2v1]. 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.

Contact | Home | ITL home | Course | Proofs | Algebra | FL