¿Equivale a mayor orden Mecanografíe la teoría lógica de orden superior?

Question

El lenguaje interno de un topos es mayor orden tipo intuicionista teoría (o lógica). Aquí la orden más alta se refiere simplemente a permitir que los tipos de función.

En lógica matemática tenemos lógicas de orden superior donde se permite la cuantificación no sólo juegos, sino poderes de conjuntos.

¿Son la misma noción de orden superior aquí?

Answer 1

Realmente hay dos diferentes significados de "orden superior":

En referencia a la sintaxis

Los sistemas que incluyen variables para uno o más tipos de "individuos", y también variabels de "conjuntos" de los individuos, las "relaciones" en el conjunto de los individuos, o "funciones" de los individuos a los individuos que son llamados "de orden superior".

Un sistema común de un orden más elevado de la lógica (con un tipo de individuos) es el siguiente definición inductiva de una gran colección de "tipos":

• El conjunto de los individuos es un tipo de
• Si $\sigma_1, \ldots, \sigma_k$ son tipos, entonces hay un tipo de $\sigma_1 \times \cdots \times \sigma_k$ cuyos elementos son secuencias de $(a_1, \ldots, a_k)$ donde $a_i$ es de tipo $\sigma_1$ por cada $i \leq k$. También hay proyección funciones para extraer cada uno de los componentes de dicha secuencia.
• Si $\sigma$ $\delta$ son tipos, hay un tipo de $\sigma \to \delta$ cuyos elementos son funciones con dominio $\sigma$ y codominio $\delta$ (es decir, las funciones que toman una entrada de tipo $\sigma$ a una salida de tipo $\delta$)
• Si $\sigma$ es un tipo, no es un tipo de $P(\sigma)$ cada elemento de que es un subconjunto de a $\sigma$

La lógica contiene, para cada tipo, el cuantificador universal sobre los objetos de ese tipo y el cuantificador existencial sobre los objetos de ese tipo. Como se puede ver, esto sólo se ve como una especie de tipo de teoría. Una diferencia es que el orden superior de la lógica se parece más a la lógica clásica que intuitionistic tipo de teoría. En particular, no existen tipos de dependientes y no "juicios", sólo las fórmulas y las pruebas que son análogos a los de la lógica de primer orden.

De hecho, toda la sintaxis de este "orden superior" que la lógica puede ser interpretado como un multi-ordenan la lógica de primer orden.

En referencia a la semántica

"De orden superior de la semántica", también llamada "semántica" y "estándar de la semántica", son de una semántica particular de orden superior de la lógica en la que el "orden superior tipo" se tienen que incluir todos los elementos que posible. Por ejemplo, en la semántica completa, una vez que el conjunto de individuos $i$ está determinado por un modelo de la colección de objetos de tipo $P(i)$ en que el modelo debe contener todos los subconjuntos de a $i$, y la colección de objetos de tipo $i\to i$ debe contener todas las funciones de$i$$i$, etc. De esta manera, todos los mayores tipos de un modelo determinado únicamente por el conjunto de individuos en el modelo.

En "la semántica de Henkin" por orden superior de la lógica, de la colección de objetos de tipo $P(i)$ en el modelo podría ser un subconjunto del powerset de $i$ en ese modelo, y la colección de objetos de tipo $i \to i$ podría ser sólo un subconjunto de todas las funciones de$i$$i$, etc.

Estos semántica tienen propiedades muy diferentes. Semántica completa, más o menos arbitrariamente la reducción del número de modelos, permite categórica teorías de los números naturales y los números reales. La semántica de Henkin tienen el mismo completitud y compacidad propiedades como la lógica de primer orden.

Answer 2

Básicamente sí. Vea Introducción a la lógica categórica orden superior por Lambek y Scott 1988 para los detalles.