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

27

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.

día
fuente
Te puede interesar leer en.wikipedia.org/wiki/…
Anthony

Respuestas:

17

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.

Antonio
fuente
2
Esa primera cita es Frank Pfenning, no Girard.
Noam Zeilberger
Una pregunta: ¿es correcto afirmar que (bajo la proposición como paradigma de tipo) las proposiciones son tipos mientras que los juicios son secuencias / expresión de la teoría de tipos (marco lógico)?
Giorgio Mossa
1
¿Cómo sabemos que sabemos algo? (Con respecto a "Un juicio es evidente si de hecho lo sabemos")
CMCDragonkai
16

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.

Uday Reddy
fuente
14

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.

Andrej Bauer
fuente
1
Usualmente me gustan tus respuestas Andrej, pero en este caso no te sigo. ¿Por qué importaría el medio de una declaración? ¿O es la diferencia en los verbos "decir" y "proclamar". En ese caso, ¿cómo sabemos que el texto no proclama y que la Sra. Marple no dice? La única otra diferencia que veo es que el texto es pasivo, mientras que la Sra. Marple está activa; pero, alguien escribió el texto, ¿verdad?
Anthony
66
El hecho de que podamos formular la oración "El mayordomo lo hizo" no significa nada. El hecho de que exista en una hoja de papel no significa nada. Pero cuando la Sra. Marple hace el juicio "El mayordomo lo hizo" frente a todos reunidos en una bonita sala de lectura victoriana, eso es algo completamente diferente. Quizás era demasiado críptico.
Andrej Bauer
@Andrej Bauer: Debo disculparme por no haberle votado antes, ahora veo el punto. Muchas gracias.
día
12

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 TypeA
  • s:AsA
  • s=t:AstA
  • A=BAB
  • Γ ContextΓ

AAtAt:AtAt: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 ).

Kaveh
fuente
Gracias por la enumeración. Pero mi pregunta ahora es si estos juicios no se convierten trivialmente en proposiciones. por ejemplo, "A es un tipo" es un predicado justo, cuando A es instanciado por, digamos Nat, se convierte en una proposición, ¿no?
día
Γt:A
1
t:A(Γ)
2
@plmday, lo siguiente podría ser útil sobre por qué eso no puede suceder desde el punto de vista matemático: "no se puede tener un universo, tratar" p prueba A "como una proposición y tener un predicado de prueba decidible". [Beeson 1980, p. 409]. (Pero para Martin-Löf, el problema principal es que estos son conceptualmente diferentes y confundirlos conducirá a fundamentos injustificados que podrían conducir a resultados paradójicos).
Kaveh
2
Me gustaría agregar que esto me parece demasiado específico ya que hay muchas otras versiones de ITT con otros juicios (por ejemplo, la Proposición de CoC). Creo que el concepto más importante aquí está en el segundo comentario de Kaveh: tratar de convertir algunos juicios en proposiciones puede introducir problemas sutiles y peligrosos en la teoría. Eso no quiere decir que una teoría de tipos no pueda describirse en una teoría de tipos, sino solo que hay líneas claras dibujadas entre la metateoría, la teoría y las expresiones en esa teoría.
Anthony
4

Los juicios son la composición de dos cosas:

  1. P
  2. A

A[P]

[P][P][T]H1,,HnA1,,An, 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.

Charles Stewart
fuente
-3

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 ...

Samuel Duclos
fuente
1
Se equivoca al decir que se ha verificado un fallo. Un juicio verificado (probado) se llama teorema.
Andrej Bauer