Getting rid of universal quantifiers is easy: if you know ∀x :(φ) (where φ is a formula presumably involving x), well then you can replace x with
anything you want, and the resulting formula will be true. We say
![\forall x:(\phi )\vdash \phi [x \mapsto t]](/system/files/resource/9/9508/9615/media/eqn-img_1.gif)
where t is any term. Any variables
in t are arbitrary, unless it is an already-existing non-arbitrary variable.
For example, suppose we know that 
We can replace n with some term like m+4 to conclude 
. The variable m is arbitrary, unless it already occurred in non-arbitrary in a previous
line of the proof (perhaps introduced via ∃Elim). A more usual step is to use a term which is just a single variable, and (by coincidence) happens to have the same name as the quantified
variable we are eliminating. Thus we often conclude 
(note the absence of the initial ∀); n is arbitrary (unless it had already been confusingly in use as a non-arbitrary
variable earlier). This is helpful when we'll be later re-introducing the ∀ in a later step; see the example below.
- 1066 reads
