How "Principia Mathematica" builds foundations

I understand that "Principia Mathematica" tries to build foundations of mathematics. For comparison ZFC achieves same task. From what I understand ZFC are axioms formalized in First Order Logic. Question is what is Principia based on and why it took so many pages to prove 2=1+1. I suspect that this is less tedious task in ZFC.

If you're really interested in this, it would be worth your while to take a look at the actual Principia and see what it does and how it does it. There are a few reasons why it takes so long to prove $1+1=2$.

One reason is that the Principia starts with considerably less than the ZF axioms; it starts with only five logical axioms along the lines of $p\lor p \implies p$. It does not start with any axioms about sets or relations or numbers.

Another reason is that the foundational machinery was not fully developed in 1911. In 2013, we would define an ordered pair as a certain sort of set (typically, $\langle x, y\rangle {\buildrel \text{def}\over \equiv } \{\{x\}, \{x,y\}\} $) and then define a relation as a set of ordered pairs. This approach hadn't been invented yet at the time Whitehead and Russell were writing. So there are several chapters of Principia Mathematica that develop properties of sets, and then several more chapters that develop properties of relations which, from a 21st-century point of view, are completely redundant. Similarly there is a chapter on propositional functions of one variable, and then a very similar chapter about functions of two variables.

But the biggest reason for the length is that the Principia proves everything in extremely small steps. For example, an important precursor to the $1+1=2$ theorem is $$∗54\cdot 43.⊢((α,β∈1)⊃((α∩β=Λ)≡(α∪β∈2)))$$ which says that if $\alpha$ and $\beta$ are sets that each have one element, then they are disjoint if and only if their union has exactly two elements. The steps in the proof are tiny. They start with the previously-proved $\ast 54\cdot 26$, which states that $\{x\}\cup\{y\}$ has two elements if and only if $x\ne y$. To get from there to $\ast 54\cdot 43$ takes about twelve steps.

The hypotheses at one point of the proof include that $\alpha$ and $\beta$ are sets with one element each. They invoke a theorem to conclude that $\alpha = \{x\}$ and $\beta=\{y\}$ for some $x$ and $y$. Most treatments would gloss over this point. Then they prove, via a previous theorem $\ast51\cdot231$, that $\{x\}\cap\{y\}$ is empty. Most treatments at this point would take as proved that $\alpha\cap \beta$ is empty, but in Principia Mathematica this is a separate, explicit deduction, justified by theorem $\ast13\cdot12$, which states that if $x=y$, then a predicate $\psi$ is true of $x$ if and only if it is true of $y$.

All these tiny steps quickly add up to a lot of paper.

Finally, Principia Mathematica does not take 300 pages to only prove $1+1=2$. There is a great deal of explanation and discussion, and a great deal more is proved besides.

I wrote a blog article about this a few years back that provides more details.

Perhaps the first point to grasp is that Principia is a type theory rather than a set theory -- indeed the authors officially do not believe in sets, thinking that talk purportedly of such things needs to translated away.

Now, the obvious places one might first look at for an account of Russell and Whitehead's type theory and the overall project of Principia are unfortunately both rather unhelpful (I mean Wikipedia and the Stanford Encyclopedia of Philosophy, whose respective entries -- here and here -- are not up to the best standards). But they may help a bit, though here are two more serious suggestions:

For a philosophical discussion of the project, see Ch.5 of Michael Potter's fine book Reason's Nearest Kin (OUP, 2000)

For an excellent paper on the early history of type theories by Fairouz Kamareddine, Twan Laan, and Rob Nederpelt which puts things in perspective, see here.

But neither of those is exactly easy. I too would be interested to know if, somewhere out there on the web, someone has posted a decently reliable ten-page exposition of what's going on in Principia that you can point students to.

You are referring to the Russell--Whitehead "Principia" (rather than Newton's); see here. Russell's was a logicist program aimed at placing symbolic logic at the foundation of mathematics. ZFC is a competing program that placed set theory at the foundation, instead. The logicist approach was initiated by Frege and was much more popular at the beginning of the 20th century than it is today. Perhaps one of the reasons is the number of pages it took to prove 2=1+1 :-)