| |
Existential
Instantiation
restriction: flag "a" |
| (∃x)Fx |
| Fa |
| |
Universal
Instantiation
|
| (x)Fx |
| Fa |
| |
Existential
Generalization |
| Fa |
| (∃x)Fx |
| flag a |
SP, UG |
Universal
Generalization restriction: requires
flagged subproof |
| Fa |
|
| (x)Fx |
|
Summary of flagging restrictions:
- Flagged constants must be new to the proof.
- Flagged constants may not appear in the premises or
the conclusion of a proof.
- When a constant is flagged in a subproof, it may
not appear outside the subproof.
|