A formal proof in symbolic logic for my S&P puzzle solution

In my last post with my solution to the classic "The two perfect logicians S & P: A solution to a classic logical puzzle puzzle", I included a brief, informal proof in one step, noting that I was taking "shortcuts."  I want to present now a complete formal proof of that same step.

The two perfect logicians S & P: A solution to a classic logical puzzle

P: "I cannot determine the two numbers."  — S: "I knew that."  — P: "Now I can determine them." — S: "So can I."  — This dialogue is from a classic logical puzzle with many interesting implications.  I'm going to try to illustrate one solution using a combination of set theory, number theory, and formal logic.

Why 1+1=2: A proof with axioms of first-order mathematical logic

Everyone knows that 1 + 1 =  2.  But why?  Is there some sort of universal law that makes this always true?  It was only in relatively recent history that the fundamentals of mathematical logic began to be outlined explicitely.  Some of the most important work here was done in the 19th century, when Guiseppe Peano discovered a set of axioms that explain the very logic behind number theory (arithematic) itself.  Referred to as "Peano's Arithematic" or first-order mathematical logic, the principles can be summarized into a few simple axioms, plus one more axiom that is a little more complex, known as the "rule of mathematical induction", which I will not get into here.

"Cur nunc Latinam studeo": but why now?

So, my new spontaneous interest is to learn Latin.  But why?  What could I possibly gain from that?  Not much, I guess, but then again, what do I really gain from creating algorithms for generating mazes on n-sided polygon tessellations?  The answer is simple.  I have long enjoyed, and have been very good at, studying and learning languages, but... I don't enjoy talking to people.  Latin is a dead language.  Thus it is the obvious choice.

An overview of Russell's paradox

This will be the first in a set of two articles about Russell's paradox.  Russell's paradox, discovered in 1901 by mathematitian Bertrand Russell,  is an antinomy that illustrates that certain attempted formalizations of naive set theory lead to contradiction.  Most simply, it is defined as: