En lógica matemática , un juicio (o juicio ) o aseveración es un enunciado o enunciación en un metalenguaje . Por ejemplo, los juicios típicos en lógica de primer orden serían que una cadena es una fórmula bien formada o que una proposición es verdadera . De manera similar, un juicio puede afirmar la aparición de una variable libre en una expresión del lenguaje objeto, o la demostrabilidad de una proposición . En general, un juicio puede ser cualquier afirmación definible inductivamente en la metateoría .
Los juicios se utilizan para formalizar sistemas de deducción : un axioma lógico expresa un juicio, las premisas de una regla de inferencia se forman como una secuencia de juicios y su conclusión también es un juicio (así, las hipótesis y las conclusiones de las pruebas son juicios). Un rasgo característico de las variantes de los sistemas de deducción del estilo de Hilbert es que el contexto no cambia en ninguna de sus reglas de inferencia, mientras que tanto la deducción natural como el cálculo secuencial contienen algunas reglas que cambian el contexto. Así, si estamos interesados sólo en la derivabilidad de tautologías , no en juicios hipotéticos, entonces podemos formalizar el sistema de deducción al estilo de Hilbert de tal manera que sus reglas de inferencia contengan sólo juicios de una forma bastante simple. No se puede hacer lo mismo con los otros dos sistemas de deducciones: a medida que se cambia el contexto en algunas de sus reglas de inferencia, no se pueden formalizar de modo que se puedan evitar juicios hipotéticos, ni siquiera si queremos usarlos sólo para demostrar la derivabilidad de tautologías. .
Esta diversidad básica entre los distintos cálculos permite tal diferencia que el mismo pensamiento básico (por ejemplo, el teorema de deducción ) debe demostrarse como un metateorema en el sistema de deducción al estilo de Hilbert, mientras que puede declararse explícitamente como una regla de inferencia en la deducción natural .
En la teoría de tipos , se utilizan algunas nociones análogas a las de la lógica matemática (dando lugar a conexiones entre los dos campos, por ejemplo, la correspondencia Curry-Howard ). La abstracción de la noción de juicio en lógica matemática también puede explotarse como fundamento de la teoría de tipos.