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>


fix x as s(0) in *Hyp


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.

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).