Rule ALLI Glossary
Definition
| X ⊢ A | ALLI | m not in any formula in X |
| X ⊢ ALLv Avm |
The one input (source) line holds a formula in which a name m occurs, depending on assumptions in which m does not occur. The conclusion is a formula with a universally quantified variable substituted for m, depending on the same assumptions. No assumptions are discharged by this rule.
Comments
The quantifier rules ALLI and ALLE allow reasoning with generalisations: the universal claim ALLv A behaves like a big (possibly infinite) conjunction asserting A of every thing in the universe of discourse. On that reading, ALLI is the generalised version of ANDI, corresponding to the thought that if A is true no matter what the arbitrary name m refers to, then it must hold universally. The side condition, requiring m not to be mentioned in any assumptions needed for the conclusion, is there to ensure that the name is genuinely arbitrary. As annotation, we cite the one source line number and "ALLI".
Example
SP {ALLxALLy Rxy ⊢ ALLxALLy Ryx} PL {1} {1} {ALLxALLy Rxy} {A} PL {1} {2} {ALLy Ray} {1 ALLE} PL { 1 } {4} { Rab } {3 ALLI} PL { 1 } {5} { ALLy Ryb } {4 ALLI} PL {1} {5} {ALLxALLy Ryx} {4 ALLI} EP|
|
|
Hover the mouse over elements in the proof or in the rule template above, to see how the inference at line 4 matches the abstract form of the rule.