Sólo tuvimos un vistazo a una transcripción de Gödel de 1931, Sobre formalmente indecidible proposiciones de Principia Mathematica aquí. El original se encuentra, por ejemplo, aquí. Hay una en particular axioma esquema de V en la página numerada 178.
Me di cuenta de que su sistema, que se formaliza, utiliza muy pocos esquemas de axiomas y reglas de inferencia. Es básicamente un orden superior de cálculo con variables con tipo. Uno de los esquemas de axioma, no se muestra la tipificación de las variables, es la siguiente:
Axioma Esquema De V: $$\forall z(x(z) \leftrightarrow y(z)) \rightarrow x = y$$
Me pregunto por qué Gödel no poner un bi-implicación en el anterior y sólo una insinuación. Así que mi pregunta es ¿podemos de alguna manera derivan estrictamente en su explícitamente mencionado axioma de esquemas y reglas de inferencia a la inversa:
$$x = y \rightarrow \forall z(x(z) \leftrightarrow y(z)) \quad ?$$
O, alternativamente, cómo en Gödels sistema podría ser muestra de la forma más simple de una sustitución de la propiedad, lo que implicaría también a la inversa:
$$x = y \wedge x(z) \rightarrow y(z) \quad ?$$
Alguien con experiencia en esta materia? Tenga en cuenta que esta respuesta aquí no es un duplicado, ya que la respuesta supone la sustitución de la propiedad, pero tendríamos que muestran que la primera Gödels sistema admite la sustitución de la propiedad.