Monthly Archives: December 2011

There is a class of all cardinalities , and it has elements , and operations , , and so forth defined on it. Furthermore, there is a map which takes sets to cardinalities such that (and so on). Ordinary generating … Continue reading →

In 1931, Alfred Tarski proved that the real ordered field allows quantifier elimination: i.e., every first-order formula is equivalent to one with no quantifiers.  This is implemented in Mathematica’s “Resolve” function. The Resolve function is called like Resolve[formula,domain] where domain … Continue reading →