LP, the Larch Prover -- The fix command
The fix command provides a method of forward inference, which can be used
to eliminate an existential quantifier from a fact in LP's
logical system.
<fix-command> ::= fix <variable> as <term> in <names>
Examples
fix x as s(0) in *Hyp
Usage
The fix command eliminates the unique accessible
prenex-existential quantifier over the variable
from the named facts and substitutes the term for all occurrences of the
variable bound by that quantifier. For example, given the formulas
user.1: \E x \A y (f(y) = x)
user.2: \E z (x < z)
the commands fix x as c in user and fix z as bigger(x) in user
produce the results
user.1.1: f(y) = c
user.2.1: x < bigger(x)
LP will reject a fix command unless the following conditions are
satisfied.
-
The named facts must contain exactly one
accessible prenex-existential quantifier over
the variable (because it is not sound to instantiate two different existential
quantifiers by the same term).
-
The term must have the form sk(x1, ..., xn), where sk is a function
identifier that does not appear in any fact or in the current conjecture, and
where x1, ..., xn include all variables that are bound by outer
(explicit or implicit) prenex-universal quantifiers in the formula containing
the eliminated quantifier. See Skolem function.
LP automatically changes bound variables in the named facts, as needed, to
avoid having them bind (or capture) variables that
occur free in the term. This action, together with the above two conditions,
guarantee that the results constitute a conservative extension to LP's logical
system, i.e., that any consequence of the extended system is either a
consequence of the original system or contains an occurrence of sk. The
last condition prevents unsound derivations such as c ~= c from
\E x (x ~= c) or \A y (c = y) from \A y \E x (x = y).