Mapeo de problemas simples de primer orden a la teoría de tipos

Question

Dado que los axiomas de Peano expresados en teoría de tipos no parecen estar avanzando, aquí hay una pregunta más sencilla:

¿Cómo podría mapear sistemas simples de primer orden a una notación equivalente en teoría de tipos?

Concretamente:

para todo x, si eshombre(x) entonces esmortal(x)

eshombre(Sócrates)

demuestra:

esmortal(Sócrates)

¿y cómo se vería una prueba en teoría de tipos?

Answer 1

No estoy seguro de qué tipo de pruebas estás buscando (hay muy poco contexto en tu publicación). A continuación se muestra un enfoque, pero como realmente no trabajo en teoría de tipos, tómalo con precaución, es posible que ni siquiera sea representativo de las pruebas estándar en esa área.

---

Sea $\mathtt{IsMan}(x)$ y $\mathtt{IsMortal}(x)$ estructuras que dependen del tipo $x$. Entonces $$\forall x.\ \mathtt{IsMan}(x) \to \mathtt{IsMortal}(x) \tag{1}$$ es un tipo válido, es decir, el tipo de funciones que convierten estructuras de $\mathtt{IsMan}(x)$ a estructuras $\mathtt{IsMortal}(x)$ para cualquier tipo $x$. Si sabemos que $(1)$ es verdadero, entonces sabemos que está habitado, es decir, existe $f$ de tipo $(1)$. Luego, dado un elemento $a$ de tipo $\mathtt{IsMan(Socrates)}$ podemos construir un elemento $f(a)$ de tipo $\mathtt{IsMortal(Socrates)}$ y hemos terminado.

¡Espero que esto ayude! ;-)

Answer 2

La teoría de tipos, sistemas de significado en libros de texto y demostradores de teoremas como la familia HOL basada en la teoría de tipos de Church, son superconjuntos de la lógica de primer orden. Modus ponens es generalmente una regla de inferencia derivada, pero es perfectamente válida, al igual que otros teoremas de primer orden y reglas de inferencia.

La teoría de tipos, sin embargo, adopta un enfoque diferente al de la teoría de conjuntos, especialmente en comparación con ZFC. ZFC tiene solo conjuntos, y todas las variables abarcan conjuntos, mientras que en la teoría de tipos las variables, constantes y términos generalmente tienen tipos. Las expresiones no son válidas sintácticamente a menos que las tipos de función y argumento se correspondan correctamente.

Entonces, una prueba en teoría de tipos no necesita verse diferente a una prueba en lógica de primer orden, aunque técnicamente debería haber anotaciones de tipos al menos en suficientes variables para determinar los tipos de los términos en ella.