Operations and Predicates
Luis Elpidio Sanchis · 2022
This chapter discusses a first order system involving set operations, set predicates, and the usual first order constructions: propositional connectives and quantifiers. It introduces meaningful constructions that can be applied to arbitrary sets in D to generate new sets that are also elements of D. All axioms in the system are written as local expressions with free variables ranging over the universe. The system is organized as a system of rules, and each rule introduces set operations or set predicates. Besides basic operations and predicates, we have general set operations and general set predicates, which are derived from basic set operations and predicates by substitution with arbitrary sets. There are two substitution rules, one for set operations and the other for set predicates.