4
$\begingroup$

Just had a look at a transcript of Gödel's 1931, On formally undecidable propositions of Principia Mathematica here. The original is found for example here. There is a particular axiom schema V on page numbered 178.

I noticed that his system, which he formalizes, uses very few axioms schemas and inference rules. Its basically a higher-order calculus with typed variables. One of the axiom schemas, not showing the typing of the variables, is as follows:

Axiom Schema V: $$\forall z(x(z) \leftrightarrow y(z)) \rightarrow x = y$$

I wonder why Gödel didn't put a bi-implication in the above and only an implication. So my question is can we somehow derive strictly in his explicitly mentioned axiom schemas and inference rules the converse:

$$x = y \rightarrow \forall z(x(z) \leftrightarrow y(z)) \quad ?$$

Or alternatively how in Gödels system could be shown the simpler form a substitution property, which would also imply the converse:

$$x = y \wedge x(z) \rightarrow y(z) \quad ?$$

Anybody knowledgeable in this matter? Note that this answer here is not a duplicate, since the answer assumes the substitution property, but we would need to first show that Gödels system admits the substitution property.

$\endgroup$
1

1 Answer 1

Reset to default
4
$\begingroup$

Does this work? Use footnote 21 of Gödel's paper (which defines $x = y$ as $\forall W(Wx \equiv Wy)$.

And then use the type raising and lowering powers of Gödel's Axiom IV (to trade between x(z) and an equivalent Z(x)).

$\endgroup$
2
  • $\begingroup$ Very good find! You could indeed write u=λv.a as a memo for Gödels IV comprehension axiom ∃u∀v(u(v) <-> a). If we then use u=λv.v(z), we get u(x) <-> x(z) and u(y) <-> y(z). The rest follows from x=y implies u(x) -> u(y) with the foot note definition. $\endgroup$
    – user4414
    Feb 3, 2018 at 0:01
  • $\begingroup$ See also math.stackexchange.com/a/1503973/4414 $\endgroup$
    – user4414
    Feb 3, 2018 at 1:36

You must log in to answer this question.