Rule ALLE Glossary
Definition
| X ⊢ ALLv A | ALLE |
| X ⊢ Atv |
The one input (source) line holds a universally quantified formula ALLv A. The output of the rule is a line holding an instance of A, got by substituting a term for the variable v. The assumptions on which the conclusion depends are the same as those of the premise. No assumptions are discharged by this rule.
Comments
The quantifier rules ALLI and ALLE allow reasoning with generalisations: the universal claim ALLvA behaves like a big (possibly infinite) conjunction asserting A of every thing in the universe of discourse. On that reading, ALLE is the generalised version of ANDE, corresponding to the thought that whatever is universally true is thereby true in particular of the individual picked out by t. As annotation, we cite the one source line number and "ALLE".
Example
SP {ALLx(Fx IMP ALLy Rxy) ⊢ Fa IMP Rab} PL {1} {1} {ALLx(Fx IMP ALLy Rxy)} {A} PL {2} {2} {Fa} {A} PL {1} {3} {Fa IMP ALLy Ray} {1 ALLE} PL { 1,2 } {4} { ALLy Ray } {2, 3 IMPE} PL { 1,2 } {5} { Rab } {4 ALLE} PL {1} {6} {Fa IMP Rab} {5 [2] IMPI} EP|
|
|
Hover the mouse over elements in the proof or in the rule template above, to see how the inference at line 5 matches the abstract form of the rule.
Note that we cannot apply ALLE directly to substitute b for y until after lines 2, 3 and 4, because "ALLy" must be the main operator of the input formula in order for the rule to apply to it, and this is not achieved until line 4.