- The transitivity of
leftOfis: - ∀x,y,z: (x leftOf y ∧ (y leftOf z)) ⇒ (x leftOf z))
- Cardinality restriction:
- ∀x: ((x ∈ X) ∧ (X ⊂ dom(prop))) ⇒ (∃!y: x prop y)
- Union, intersection, etc., can be trivially formalized, too
- etc.
- But, again: this is a restricted form of FOL only!