Tengo una comprensión muy fuerte de la lógica de primer orden y estoy tratando de inclinar la teoría de tipos como una alternativa. ¿Podría alguien expresar los axiomas de Peano con la teoría de tipos? Estoy especialmente interesado en ver cómo se representa la inducción.
Respuestas
¿Demasiados anuncios?
Deje $\bot$ ser la deshabitada tipo de especie $*$, y dejar que los tipos de
- $\mathtt{Zero}$ ser de tipo $*$,
- $\mathtt{Nat}$ $\mathtt{S}$ ser de tipo $* \to *$,
- $\mathtt{Eq}$ ser de tipo $* \to * \to *$.
A continuación, los axiomas de Peano puede ser formalizado en el tipo de teoría diciendo que los siguientes tipos están habitadas (en el formato"$\mathtt{inhabitant} : \mathtt{type}$, libre variables cuantificadas universalmente):
\begin{align} \newcommand{\Zero}{\mathtt{Zero}} \newcommand{\zero}{\mathtt{zero}} \newcommand{\pa}[1]{\mathtt{pa}_{\mathrm{#1}}} \newcommand{\Nat}[1]{(\mathtt{Nat}\ #1)} \newcommand{\Eq}[2]{(\mathtt{Eq}\ #1\ #2)} \newcommand{\S}[1]{(\mathtt{S}\ #1)} \newcommand{\T}[1]{(\mathtt{T}\ #1)} \newcommand{\Plus}[2]{(\mathtt{Plus}\ #1\ #2)} \newcommand{\plus}[1]{\mathtt{plus}_{\mathrm{#1}}} \newcommand{\Comm}[1]{(\mathtt{Comm}\ #1)} \zero &: \Zero \\ \pa1 &: \Nat{\Zero} \\ \pa2 &:\Nat{x} \to \Eq{x}{x} \\ \pa3 &: \Nat{x} \to \Nat{y} \to \Eq{x}{y} \to \Eq{y}{x} \\ \pa4 &: \Nat{x} \to \Nat{y} \to \Nat{z} \to \Eq{x}{y} \to \Eq{y}{z} \to \Eq{x}{z} \\ \pa5 &: \Nat{x} \to \Eq{x}{y} \to \Nat{y} \\ \pa6 &: \Nat{x} \to \Nat{\S{x}} \\ \pa7 &: \Nat{x} \to \Eq{\S{x}}{\Zero} \to \bot \\ \pa8 &: \Nat{x} \to \Nat{y} \to \Eq{\S{x}}{\S{y}} \to \Eq{x}{y} \\ \end{align}
y también, para cualquier tipo de $\mathtt{T}$ tipo $\mathtt{T} : * \to *$ el siguiente tipo también está habitado: $$ \pa{T} : \T{\Cero} \(\Nat{x} \\T{x} \\T{\S{x}}) \a \Nat{y} \\T{y}. $$
Esos son los axiomas de Peano, como en Wikipedia, pero creo que también debe ser algo de lo que implica que $\mathtt{S}$ es una función (con respecto a $\mathtt{Eq}$) en lugar de cualquier relación, que es:
$$f : \Nat{x} \to \Nat{y} \to \Eq{x}{y} \to \Eq{\S{x}}{\S{y}}.$$
Espero que esta ayuda ;-)
user68585
Puntos
21
El libro del profesor Peter B. Andrews "Introducción a la lógica matemática y la teoría de tipos" (2002) abarca exactamente este tema. Expresa los postulados como éste. (Omito símbolos de tipo de variables y constantes.)
Unesdoc.unesco.org unesdoc.unesco.org
Unesdoc.unesco.org unesdoc.unesco.org
Unesdoc.unesco.org unesdoc.unesco.org
Unesdoc.unesco.org unesdoc.unesco.org
Unesdoc.unesco.org unesdoc.unesco.org
La teoría de tipos es una lógica de orden superior, y la inducción cuantifica sobre los predicados "p".
Feratile
Puntos
58
Solo quiero agregar
Http://people.inf.elte.hu/divip/AgdaTutorial/Index.html
Es un buen recurso que tiene una gran cantidad de problemas Arithmatic Peano.
