Proving Russell's Paradox in Predicate Calculus

[solakis1]

Can we prove in the predicate calculus,that there does not exist someone who can shave all those that do not shave themselfs?? (Russell's Paradox)

 

[Evgeny.Makarov]

Let $S(x,y)$ mean that $x$ shaves $y$. Then the statement that no barber with the desired property exists is
\[
\neg\exists b\,\forall x.\,S(b,x)\leftrightarrow\neg S(x,x).
\]
I believe this is a tautology, so it is provable.

 

[solakis1]

Let $S(x,y)$ mean that $x$ shaves $y$. Then the statement that no barber with the desired property exists is
\[
\neg\exists b\,\forall x.\,S(b,x)\leftrightarrow\neg S(x,x).
\]
I believe this is a tautology, so it is provable.

1)Is the above formula an exact translation of the RASSELL'S papadoxe.

2) Is it provable??,since predicate calculus is not a decidable theory

 

[Evgeny.Makarov]

1)Is the above formula an exact translation of the RASSELL'S papadoxe.

First, Russell's paradox is usually stated about sets. Second, it's difficult to say whether a formula is an exact translation of a claim in the natural language. Sometimes we change the claim into an equivalent one during translation into a formula, but there are infinitely many formulas equivalent to any given formula, so there are many translation variants to choose from. Also, I started the formula with negation, so it is a tautology. If the negation is omitted, it becomes a contradiction, which is more like a paradox. Wikipedia has the following version.
\[
(\exists x)({\text{man}}(x)\wedge (\forall y)({\text{man}}(y)\rightarrow ({\text{shaves}}(x,y)\leftrightarrow \neg {\text{shaves}}(y,y))))
\]

2) Is it provable??,since predicate calculus is not a decidable theory

Decidability is not important here. In fact, the word "decidable" has two meanings with respect to logical theories. The modern meaning is that there exists an algorithm that says whether a given formula is in the theory (or is a corollary of the theory) or not. The older meaning, which Gödel used in the title of his article "On Formally Undecidable Propositions"), says that the theory is complete, i.e., derives $A$ or $\neg A$ for every formula $A$. But every first-order theory is complete with respect to the set of all of its models (this is Gödel's completeness theorem). This means that if $T$ is a theory, $A$ is a formula and $I\models A$ for all interpretations $I$ such that $I\models T$, then $T\vdash A$. The problem with arithmetic is that we consider not all models, but the natural model $\mathbb{N}$, and arithmetic is incomplete w.r.t. this model: there exists a formula $A$ such that $\mathbb{N}\models A$, but $\text{PA}\not\vdash A$ where PA stands for Peano Arithmetic.

Anyway, all tautologies are provable in first-order logic, so the formula from post #2 is provable.

 

[solakis1]

Also, I started the formula with negation, so it is a tautology.

.

So whenever we start a formula in predicate calculus with a negation ,automatically we have created a tautology??

By a tautology ,you mean a valid argument and thus provable, I suppose

 

[Evgeny.Makarov]

So whenever we start a formula in predicate calculus with a negation ,automatically we have created a tautology?

Of course not. I am saying that my formula asserts that no barber exists (which is true), while the Wikipedia formula asserts that he exists (which is false).

By a tautology ,you mean a valid argument and thus provable, I suppose

A tautology (rather, a valid formula in the context of first-order logic) is a formula that is true in every interpretation. By completeness theorem, every valid formula is derivable.

 

[solakis1]

Of course not. I am saying that my formula asserts that no barber exists (which is true), while the Wikipedia formula asserts that he exists (which is false)..

How do we formally prove that in set theory

 

[Evgeny.Makarov]

How do we formally prove that in set theory

In set theory we can prove $\neg\exists y\,\forall x\,(x\in y\leftrightarrow \neg x\in x)$. We don't even need to use any axioms of set theory, just first-order logic.