2
votes
2answers
130 views

Second order logic and quantification over formulas

According to Wikipedia second order logic allows quantification over sets of individuals and thus goes beyond first-order logic, e.g. in expressive power. On the other hand some sort of ...
1
vote
1answer
121 views

What makes Tarski Grothendieck set theory non-empty?

I'm fighting with Grothendieck set theory for some time now. This is the framework for the automated proof checking system of Mizar and hence there is a formalized version of the axioms here too, and ...
2
votes
1answer
358 views

Existential Quantifier as Predicate?

I was reading this document on axiomatic set theory, and on page 4, it defines $\exists \{x:P\}$ as an alternative notation for $\exists y \forall x P$. Since the first notation looks very much like a ...