El artículo de nlab parece un poco fuera de lugar. Sospecho que se debe más a que intenta explicar demasiado en muy poco espacio, de modo que las cosas se mezclan. Estoy completamente de acuerdo contigo y yo llamaría a toda la expresión " $\vdash J$ " una sentencia y no sólo $J$ . Elaboro sobre lo que está pasando en un diferente responder et le entrada en mi blog a la que se hace referencia. El secuente que enumeras también sería una sentencia. De hecho, la afirmación de que un fragmento de sintaxis es una fórmula bien formada sería otra sentencia.
Normalmente (aunque no siempre) los juicios son relaciones definidas inductivamente y, adoptando un punto de vista de la teoría de conjuntos, una derivación es entonces un elemento del juicio. Esto significa algo así como $\vdash P \to P$ es en realidad un predicado y cuando decimos que el juicio se mantiene queremos decir en la semántica de la meta-lógica que $\exists d. d \in (\vdash P \to P)$ . Desde otra perspectiva, una derivación es una testigo o una prueba constructiva de que se cumple la sentencia. Estas relaciones se definen sobre la sintaxis, es decir, los términos (en bruto), del lenguaje objeto que se describe (por ejemplo, la lógica proposicional) y quizás otros conjuntos, por ejemplo, los naturales.
La respuesta y la entrada de blog a las que se hace referencia lo explican todo con ejemplos en un lenguaje formal comprobado por máquinas.
Edito: Uff, después de leer la página en detalle, en realidad no son incoherentes con la frase de la pregunta (aunque cambian drástica pero explícitamente el significado de " $\vdash$ "cuando hablan de juicios hipotéticos/genéricos). Dicho esto, la forma en que está redactada la página hace que sea extraordinariamente fácil dejarse engañar. Si se quiere decir " $M:A$ " es una sentencia que significa $M$ tiene tipo $A$ Bien. Si quieres decir " $\vdash M : A$ " afirma la derivabilidad de esta sentencia, de acuerdo. Sin embargo, si realmente se necesitan juicios genéricos, entonces el " $\vdash$ " en la sentencia genérica, por ejemplo " $x : A \vdash x : A$ ", es algo totalmente distinto, y las apariciones de " $x:A$ " a la izquierda o a la derecha en el juicio genérico no son en sí mismos juicios ni tienen significado por sí mismos. Los " $\vdash$ " en la sentencia genérica no es ningún tipo de operador. La página no afirma lo contrario (en realidad lo hace un poco...), pero incita mucho a este tipo de malentendidos. Hay comentarios en las páginas a las que hace referencia que afirman la mayor parte de lo que he dicho, por ejemplo aquí y aquí . (Obsérvese que el primero de ellos utiliza " $\vdash$ " en el segundo sentido, y el segundo en el primero). En ambas observaciones señalan que a veces podemos hacer que este juego de palabras funcione. LF depende en gran medida de este juego de palabras en la práctica, pero su fracaso es parte de la razón por la que existen sistemas como NLF, LLF y CLF.
El resultado es " $\vdash$ " se utiliza de (al menos) dos formas muy distintas, ambas presentes en esa página. En algunos casos estos dos significados pueden coincidir aproximadamente, pero eso no está en absoluto garantizado ni lo recomiendo como forma de entender cualquiera de los dos usos de la notación en general (aunque puede ser una técnica poderosa cuando se aplica).
