You might not get new sets -- you might get fewer bijections between the sets you already have! Sometimes getting more cardinals means having fewer sets.

@Joel's answer is concise and correct, and I am glad that @Henry mentioned the connection to modal logic. I'd like to add one more perspective: they seem similar because -- when you look at the right ...

The intuitive explanation is that $\kappa$-categories are to first-order functions what cartesian closed categories are to higher-order functions. This all started with Lambek's work on polynomial ...

You write: "set theory permeates the formulation of first order logic. In first order logic, structures are sets together with constants" No; first order logic does not assume any set theory. The ...

Yes, this still occurs in modern type theory; in particular, you'll find it in the calculus of constructions employed by the Coq language. Consider the type called Prop, whose inhabitants are logical ...

"Every finitely-branching tree with infinitely many nodes has an infinite branch" is constructively false, as witnessed by the following counterexample: http://math.andrej.com/wp-content/uploads/2006/...

Short answer: category theorists often elide the extra annotations when employing typical ambiguity or universe polymorphism. Proof theorists demand that these annotations be provided, and study how ...

What are the consequences of technically proving anything in Coq? This is a question in the Coq faq.

It leads to a well-typed term, having no normal form, which is assigned the type False. You can find the term given explicitly in A simplification of Girard's paradox

You're supposed to think of sets. Definitely. Here's an analogy you might find helpful: let's use the name "ZFC-" for the axioms of ZFC but without the axiom of infinity. Now, if I suddenly decreed ...

If you're willing to accept register machines (rather than just tape machines), you can get what you want via the Grzegorczyk hierarchy, which generates the class of primitive recursive functions in ...

Any programming languages based on lambda calculus (Haskell, (OCa)ML, Clean, Coq, Agda) forms a category -- in many different ways, in fact. One way is to have an object for each type of the language ...

I had similar questions, and after stumbling around for a long time figured out that Kaye's book Models of Peano Arithmetic is pretty much the first book to read if you want to start building ...

See question #5 in the Coq FAQ: http://coq.inria.fr/faq "You have to trust that the implementation of the Coq kernel mirrors the theory behind Coq. The kernel is intentionally small to limit the ...

Grammars involving the usual context-free operations plus intersection are called conjunctive grammars. Adding negation (in addition to intersection) gives boolean grammars. Alexander Okhotin has ...

A ZF-algebra (as in Algebraic Set Theory) is a collection of sets closed under singleton and union. A Grothendieck Universe (aka strongly inaccessible cardinal, aka model of set theory) is a ...

Well, if you want to know how computers work, the authoritative reference on computer architecture happens to have been written by a set theorist! John von Neumann. First Draft of a Report on the ...

In order to talk about provability, we need to say what provability is. There are basically two options: Define an explicit provability predicate: encode some proof calculus in the natural numbers, ...

Just as a bit of a "big picture" comment... most grammatical formalisms are chosen for parsing use because they admit efficient implementations as some sort of automaton. An automaton implementation ...

I think most people here would agree that Category Theory is part of mathematics. The study of strongly-typed functional programming languages is really just the study of cartesian closed categories, ...

Off-hand, I can think of at least two reasons why a collection whose elements are all sets might fail to be a set: The collection is too big (which you've mentioned) The collection is too complicated....

"Term category of a hyperdoctrine." The hyperdoctrine approach to categorical logic segregates the individuals (terms inhabiting types) in a category completely apart from the categories containing ...

I think the more fundamental question to ask is why set theorists insist that the axioms of set theory be strictly first-order in nature (*). I claim that you can't really explain the motivations of ...

Regarding Question 2, rather than having finitely many function symbols $S_n(x)$, the easiest solution is to have a single relation symbol $S(n,x,m)$ asserting that the "$n$-labeled" successor of $x$ ...

The statement "for any type-indexed family of propositions exists a proposition isomorphic to their coproduct" is inconsistent with impredicative type theory (CC); this leads to Girard's Paradox. The ...

I would posit that proof theory is exactly the syntactical part of logic, and the other three branches (set theory, model theory, and recursion theory) are what's left when you get rid of the syntax. ...