Lógica de muchos ordenamientos
Muchos lógica-ordenada puede reflejar formalmente nuestra intención de no manejar el universo como una homogénea colección de objetos, sino para crear particiones de una manera que es similar a los tipos de programación con tipo . Tanto las " partes del discurso " funcionales y asertivas en el lenguaje de la lógica reflejan esta partición tipográfica del universo, incluso en el nivel de sintaxis: la sustitución y el paso de argumentos sólo se pueden hacer en consecuencia, respetando los "géneros".
Hay varias formas de formalizar la intención mencionada anteriormente; una lógica de muchos ordenamientos es cualquier paquete de información que la cumple. En la mayoría de los casos, se proporciona lo siguiente:
El dominio del discurso de cualquier estructura de esa firma se fragmenta en subconjuntos disjuntos, uno para cada tipo.
Al razonar sobre organismos biológicos, es útil distinguir dos tipos: y . Si bien una función tiene sentido, una función similar generalmente no lo tiene. La lógica de muchos ordenamientos permite tener términos como , pero descartar términos como como sintácticamente mal formados.
La algebraización de la lógica de muchos ordenamientos se explica en un artículo de Caleiro y Gonçalves, [1] que generaliza la lógica algebraica abstracta al caso de muchos ordenadas, pero también se puede utilizar como material introductorio.
Mientras que la lógica de muchos ordenamientos requiere que dos tipos distintos tengan conjuntos de universos disjuntos, la lógica ordenada por orden permite que un tipo se declare como un subgrupo de otro tipo , generalmente mediante escritura o sintaxis similar. En el ejemplo de biología anterior , es deseable declarar
