27
$\begingroup$

I get confused by the subtle difference between propositions and judgments when exposed to intuitionistic type theory. Can any one explain to me what is the point to distinguish them and what distinguishes them? Especially in view of the Curry-Howard Isomorphsim.

$\endgroup$
17
$\begingroup$

First, you should know that, in general, there is not consensus about these terms and their definitions depend on the system in which one is working.Since you asked about intuitionist type theory, I'll quote Pfenning:

A judgment is something we may know, that is, an object of knowledge. A judgment is evident if we in fact know it.

Propositions on the other hand, according to Martin-Löf are sets of proofs. In this interpretation, if the set of proofs for a proposition is empty then it is false and otherwise true.

A proposition is interpreted as a set whose elements represent the proofs of the proposition

says Nordström et al. On the other hand, in classical logic and in general, propositions are objects expressed in a language which can be either "true" or "false".

To give you some extra intuition; from my point of view, judgments are metalogical and propositions logical.

I suggest "Constructive Logic" by Frank Pfenning, "Proofs and Types" by Jean-Yves Girard and "Programming in Martin-Löf's Type Theory" by Bengt Nordström et al. All three are freely available on the Internet. The last one is probably the closest to what you want as it is oriented to programming and goes into great detail, at length, about the meanings of these terms and many more.

$\endgroup$
  • 2
    $\begingroup$ That first quote is Frank Pfenning, not Girard. $\endgroup$ – Noam Zeilberger Feb 7 '12 at 0:31
  • $\begingroup$ One question: is it correct to state that (under proposition as type paradigm) propositions are types while judgments are sequents/expression of the (logical framework) type theory? $\endgroup$ – Giorgio Mossa Mar 3 '15 at 21:13
  • 1
    $\begingroup$ How do we know that we know something? (With regards to "A judgement is evident if we in fact know it"?) $\endgroup$ – CMCDragonkai Feb 4 '16 at 4:41
16
$\begingroup$

Perhaps I can try giving a less metaphysical answer.

There is a language, a logical language, that we are studying. In this language, there are things called "propositions" which are supposed to be things that are true or false.

There is a meta-language, which is also a logical language, in which we are trying to explain which things in the base language are true or false. The statements we make in this meta-language are called "judgements".

Note that all the propositions of the base language have the status of data in the meta-language. They are as good as strings. You can't ask a string whether it is true or false. A judgement is the interpreter that interprets the string as a proposition and decides whether it is true or false.

$\endgroup$
14
$\begingroup$

I'll try to be short where other answers were more exhaustive. There is a difference between a piece of text saying "The butler did it.", and Mrs. Marple proclaiming "The butler did it." In the second case, the butler might lose his freedom.

$\endgroup$
  • 1
    $\begingroup$ I usually like your answers Andrej, but in this case I don't follow. Why would the medium of a statement matter? Or is it the difference in the verbs "saying" and "proclaiming." In that case, how do we know the text is not proclaiming and Mrs. Marple not saying? The only other difference I see is that the text is passive, while Mrs. Marple is active; but, someone wrote the text, right? $\endgroup$ – Anthony Feb 11 '12 at 21:56
  • 6
    $\begingroup$ The fact that we can formulate the sentence "The butler did it" means nothing. The fact that it exists on a piece of paper means nothing. But when Mrs. Marple makes the judgment "The butler did it" in front of everyone gathered in a nice Victorian reading room, that's an entirely different thing. Perhaps I was too cryptic. $\endgroup$ – Andrej Bauer Feb 12 '12 at 14:44
  • $\begingroup$ @Andrej Bauer: I must apologize for down voting you before, now I see the point. Thanks a lot. $\endgroup$ – day Nov 3 '12 at 11:55
12
$\begingroup$

In Martin-Löf's type theories, judgments are a part of speech-acts. There are four (or five according to Wikipedia) judgments:

  • $A \ \mathsf{Type}$ ($A$ is a type/set/proposition),
  • $s : A$ ($s$ is a member/proof of $A$),
  • $s=t : A$ ($s$ and $t$ are equal members/proofs of $A$),
  • $A=B$ ($A$ and $B$ are equal types/sets/propositions),
  • $\Gamma \ \mathsf{Context}$ ($\Gamma$ is well-formed context).

To understand what this means we have to go back to Frege. Frege's turnstile symbol $\vdash$ is a speech-act. It asserts the content (which follows it and is a judgment). In Martin-Löf's type theories we have the four (five?) judgments listed above. In these theories, propositions are just types.

Let's assume that $A$ is a proposition. Then $A$ is a type. Let's assume that $t$ is a term of type $A$. Then $t : A$ is a judgment (you can think of it as $t$ is a proof of $A$). Now we can assert that is the case, in which case we use $\vdash t:A$.

I would add Michael Beeson's "Foundations of Constructive Mathematics" to the suggestions in Anthony's answer. Martin-Löf has given several talks which explain his theory very nicely but unfortunately most of them haven't turned into published form by him (but check this website).

$\endgroup$
  • $\begingroup$ Thanks for the enumeration. But my question now is aren't these judgments be trivially turned into propositions? e.g., "A is a type" is a just predicate, when A is instantiated by, say Nat, it becomes a proposition, doesn't it? $\endgroup$ – day Jan 23 '12 at 10:01
  • $\begingroup$ I would have said that $\Gamma\vdash t:A$ is the judgement. $\endgroup$ – Dave Clarke Jan 23 '12 at 10:40
  • 1
    $\begingroup$ @Dave, I followed Beeson's account from 1980 here but you are right to some extent (although Per seems to prefer $t:A (\Gamma)$ for conditional judgments, historically the notation you have written is a common abuse, there shouldn't be anything to the left of turnstile). $\endgroup$ – Kaveh Jan 23 '12 at 19:47
  • 2
    $\begingroup$ @plmday, the following might be helpful about why that cannot happen from mathematical point of view: "you can't have a universe, treat "p proves A" as a proposition, and have a decidable proof-predicate." [Beeson 1980, p. 409]. (But for Martin-Löf, the main issue is that these are conceptually different and confusing them will lead to unjustified foundations which might lead to paradoxical results.) $\endgroup$ – Kaveh Jan 23 '12 at 20:32
  • 2
    $\begingroup$ I'd like to add that this is seems overly specific to me since there are many other versions of ITT with other judgements (e.g. CoC's Prop). I think the more important concept here is in Kaveh's second comment: trying to turn some judgements into propositions can introduce subtle and dangerous problems into the theory. That's not to say that a type theory couldn't be described in a type theory but only that there are clear lines drawn between the metatheory, the theory and the expressions in that theory. $\endgroup$ – Anthony Feb 11 '12 at 21:53
4
$\begingroup$

Judgements are the composition of two things:

  1. A proposition $P$; and
  2. A propositional attitude $\cal A$ – this is what philosophers call it, cf. propositional attitude reports which tie propositional attitudes to the speech acts Kaveh talks of;

giving the basic form ${\cal A} [P]$. More complex syntaxes are possible if we allow multi-arity propositional judgements.

Usual formulations of first-order logic need only one propositional attitude, which is usually either "$[P]$ is a theorem" or the binary judgement "$[P]$ is a consequence of $[T]$". In the two-sided sequent calculus, we have a more complex theory of judgements, most commonly $H_1, \dots, H_n \vdash A_1, \dots, A_n$, where some logics have such judgements that are not trivially equivalent to any proposition of the logic's language. So different kinds of propositional are seen in fairly elementary classical logic.

Martin-Löf's type theory resorts to a more complex family of judgements for three reasons: First, it is dependently typed, meaning that the propositions occur as syntactic entities inside terms. Second, he dispensed using a grammar to define which strings of symbols are valid terms and propositions, but used the inferential system to do so – a reasonable thing to do since propositions in such typed theories are generally not context free. Third, he devised a novel theory of equality, often called propositional equality, which leverages the beta-eta theory (or in some variants, just the beta theory), and the judgements that two terms share the same normal form are expressed using judgements expressing the beta/eta equivalence of two terms – again reasonable, given that beta/eta equivalence is computationally expensive and non-obvious in the proof theory.

The judgements expressing beta/eta equivalence can be eliminated with not too much difficulty - have as the grounds for the introduction rule for propositional equality being that the two terms are beta equivalent (beta-eta equivalence is slightly more problematic) – but eliminating the judgement that terms inhabit types is much trickier; the least bad way I can think of for doing this is to reconstruct type inference in the term grammar, which leads to a more complex and less intuitive theory overall.

$\endgroup$
-3
$\begingroup$

Claims, propositions and statements are all the same; but a jugement is a proposition that has been verified (whether right or wrong), endorsed, or used as a conclusion. No need for fancy formulas like the answers above seem to abuse...

$\endgroup$
  • 1
    $\begingroup$ You are wrong about saying that a judgment has been verified. A verified (proved) judgment is called a theorem. $\endgroup$ – Andrej Bauer Jan 28 '12 at 9:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.