Quantified Terms
Set-Forming Term - (setofall <term> <sentence>)
E.g, (setofall ?block (Above ?block A))
- SIV((setofall term sent)) = {SIV’(term) | TIV’(sent) = true}
for all versions V’ of V wrt the variables in term
Designator - (the <term> <sentence>)
E.g., (the ?block (Above ?block A))
- SIV((the term sent)) =
- SIV’(term) when
V’ is a version of V wrt the variables in term, and
TIV’(sent) = true, and
SIV’’(term) = SIV’(term)
for all versions V’’ of V such that TIV’’(sent) = true
- ^ otherwise