Como saulspatz dicho, esto es una forma más bien vaga pregunta si no precisar de un sistema a prueba. Una vez que lo haces hacia abajo el pasador (formal) prueba del sistema, entonces todavía hay preguntas acerca de lo que "de hecho, el mismo" significa, y hay varias respuestas a esa pregunta. En ese punto, sin embargo, el problema cae en el campo de prueba de la teoría.
Para muchos sistemas, especialmente constructivo/intuitionistic sistemas, podemos tener una buena noción de "forma normal" para las pruebas de lo que significa una manera de definir "lo mismo" es cuando dos pruebas puede ser reducido a la misma forma normal. Hablamos de "normal " pruebas" en la deducción natural y sistemas de corte "libre de pruebas" en el secuente cálculos.
Una forma particular de la de Curry-Howard correspondencia enlaces términos en escrito lambda cálculos para las pruebas en diversas lógicas. El arquetipo por ejemplo, los de tipo simple cálculo lambda y intuitionistic lógica proposicional. Desde esta perspectiva, la pregunta es equivalente a (usando la misma noción de "lo mismo" como el párrafo anterior) para preguntar si hay tipos que tienen una sola forma normal habitante. La respuesta a esto es definitivamente "sí" a pesar de que puede depender de que la lógica que usted está utilizando y algunos otros detalles. Ampliamente utilizado ejemplo es el tipo de $\forall A.A\to A$ en el polimórficos cálculo lambda tiene sólo una (forma normal) habitante, es decir, la polimórficos función identidad (formalmente: $\Lambda\tau.\lambda x\!:\!\tau.x$). El polimórficos cálculo lambda corresponde a intuitionistic de segundo orden proposicional (no predicado) de la lógica. Por el contrario, $\forall A.A\to(A\to A)$ tiene dos distinta forma normal las pruebas correspondientes a los términos de $\Lambda\tau.\lambda x\!:\!\tau.\lambda y\!:\!\tau.x$ e $\Lambda\tau.\lambda x\!:\!\tau.\lambda y\!:\!\tau.y$.
Esta noción de "lo mismo" es algo razonable, pero probablemente no sea perfecto. Por un lado, no es tan gruesa como para hacer todo demostrable proposiciones equivalentes, y la prueba de reducción es basado generalmente se ven "burocrático". Por otro lado, puede haber un aumento exponencial en el tamaño de una prueba cuando se reduce a su forma normal, y relativamente pequeños detalles pueden hacer pruebas distintas, incluso si utilizan el mismo "ideas". Es poco probable que haya un (claro) formal análogo a lo intuitivo, la noción informal de dos pruebas de ser "lo mismo". Esta probabilidad depende de los aspectos de la psicología humana. Diferentes intuitiva perspectivas puede conducir fácilmente a las mismas pruebas. A ser muy reduccionista acerca de él, la intuición es generalmente una guía para la prueba de búsqueda (especialmente cuando se trabaja en un sistema formal).
