¿Cuál es la diferencia entre proposiciones y juicios?

Me confunde la sutil diferencia entre proposiciones y juicios cuando se expone a la teoría del tipo intuicionista. ¿Alguien puede explicarme cuál es el punto para distinguirlos y qué los distingue? Especialmente en vista del Curry-Howard Isomorphsim.

En primer lugar, debe saber que, en general, no hay consenso sobre estos términos y sus definiciones dependen del sistema en el que se está trabajando. Dado que usted preguntó sobre la teoría del tipo intuicionista, citaré a Pfenning:

Un juicio es algo que podemos saber, es decir, un objeto de conocimiento. Un juicio es evidente si de hecho lo sabemos.

Las propuestas, por otro lado, según Martin-Löf, son conjuntos de pruebas. En esta interpretación, si el conjunto de pruebas para una proposición está vacío, entonces es falso y por lo demás verdadero.

Una proposición se interpreta como un conjunto cuyos elementos representan las pruebas de la proposición.

dice Nordström et al. Por otro lado, en la lógica clásica y en general, las proposiciones son objetos expresados ​​en un lenguaje que puede ser "verdadero" o "falso".

Para darle una intuición extra; desde mi punto de vista, los juicios son metalogicos y las proposiciones logicas.

Sugiero "Lógica constructiva" de Frank Pfenning , "Pruebas y tipos" de Jean-Yves Girard y "Programación en la teoría de tipos de Martin-Löf" de Bengt Nordström et al. Los tres están disponibles gratuitamente en Internet. El último es probablemente el más cercano a lo que desea, ya que está orientado a la programación y entra en gran detalle, en detalle, sobre los significados de estos términos y muchos más.

Quizás pueda intentar dar una respuesta menos metafísica.

Hay un lenguaje, un lenguaje lógico, que estamos estudiando. En este lenguaje, hay cosas llamadas "proposiciones" que se supone que son cosas que son verdaderas o falsas.

Hay un metalenguaje, que también es un lenguaje lógico, en el que estamos tratando de explicar qué cosas en el lenguaje base son verdaderas o falsas. Las declaraciones que hacemos en este metalenguaje se llaman "juicios".

Tenga en cuenta que todas las proposiciones del lenguaje base tienen el estado de los datos en el metalenguaje. Son tan buenas como las cuerdas. No se puede preguntar a una cadena si es verdadera o falsa. Un juicio es el intérprete que interpreta la cadena como una proposición y decide si es verdadera o falsa.

Trataré de ser breve donde otras respuestas fueron más exhaustivas. Hay una diferencia entre un texto que dice "El mayordomo lo hizo". y la Sra. Marple proclamando "El mayordomo lo hizo". En el segundo caso, el mayordomo podría perder su libertad.

En las teorías de tipo de Martin-Löf , los juicios son parte de los actos de habla . Hay cuatro juicios (o cinco según Wikipedia):

• $A \ \mathsf{Type}$$A$
• $s : A$$s$$A$
• $s=t : A$$s$$t$$A$
• $A=B$$A$$B$
• $\Gamma \ \mathsf{Context}$$\Gamma$

$\vdash$

$A$$A$$t$$A$$t : A$$t$$A$$\vdash t:A$

Añadiría "Fundamentos de las matemáticas constructivas" de Michael Beeson a las sugerencias en la respuesta de Anthony. Martin-Löf ha dado varias charlas que explican muy bien su teoría, pero desafortunadamente la mayoría de ellas no han sido publicadas por él (pero consulte este sitio web ).

Los juicios son la composición de dos cosas:

1. $P$
2. $\cal A$

${\cal A} [P]$

$[P]$$[P]$$[T]$$H_1, \dots, H_n \vdash A_1, \dots, A_n$, donde algunas lógicas tienen tales juicios que no son trivialmente equivalentes a ninguna proposición del lenguaje de la lógica. Por lo tanto, se ven diferentes tipos de proposicional en la lógica clásica bastante elemental.

La teoría de tipos de Martin-Löf recurre a una familia de juicios más compleja por tres razones: Primero, se tipea de manera dependiente, lo que significa que las proposiciones ocurren como entidades sintácticas dentro de los términos. En segundo lugar, prescindió del uso de una gramática para definir qué cadenas de símbolos son términos y proposiciones válidos, pero utilizó el sistema inferencial para hacerlo, algo razonable de hacer ya que las proposiciones en tales teorías mecanografiadas generalmente no están libres de contexto. Tercero, ideó una nueva teoría de la igualdad, a menudo llamada igualdad proposicional, que aprovecha la teoría beta-eta (o en algunas variantes, solo la teoría beta), y los juicios de que dos términos comparten la misma forma normal se expresan usando juicios que expresan la equivalencia beta / eta de dos términos - nuevamente razonable,

Los juicios que expresan la equivalencia beta / eta pueden eliminarse sin demasiada dificultad; los fundamentos de la regla de introducción para la igualdad proposicional son que los dos términos son equivalentes beta (la equivalencia beta-eta es un poco más problemática), pero eliminando el juicio que los términos habitan tipos es mucho más complicado; La forma menos mala en la que puedo pensar para hacer esto es reconstruir la inferencia de tipos en el término gramática, lo que conduce a una teoría general más compleja y menos intuitiva.

Reclamaciones, proposiciones y declaraciones son todas iguales; pero un jugement es una proposición que ha sido verificada (sea correcta o incorrecta), aprobada o utilizada como conclusión. No hay necesidad de fórmulas elegantes como las respuestas anteriores parecen abusar ...