<p>Perhaps I can try giving a less metaphysical answer.</p>

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

<p>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".</p>

<p>Note that all the propositions of the base language have the status of <i>data</i> 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.</p>

CC BY-SA 3.0
2012-02-24T01:59:55.647Z
2012-02-24T01:59:55.647Z
Uday Reddy
<p>In <a href="https://en.wikipedia.org/wiki/Per_Martin-L%C3%B6f">Martin-Löf</a>'s type theories, judgments are a part of <a href="http://en.wikipedia.org/wiki/Speech_act">speech-acts</a>. There are four (or five according to Wikipedia) judgments:</p>

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

<p>To understand what this means we have to go back to Frege. <a href="http://plato.stanford.edu/entries/assertion/">Frege's turnstile symbol</a> $\vdash$ is a speech-act. It <em>asserts</em> the <em>content</em> (which follows it and is a judgment). In <a href="http://en.wikipedia.org/w/index.php?title=Martin-L%C3%B6f%27s_type_theory">Martin-Löf's type theories</a> we have the four (five?) judgments listed above. In these theories, propositions are just types.</p>

<p>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$.</p>

<p>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 <a href="https://intuitionistic.wordpress.com/works-on-martin-lofs-type-theory/">this website</a>).</p>

CC BY-SA 3.0
2012-01-23T10:01:30.080Z
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?
day
CC BY-SA 3.0
2012-01-23T10:40:24.863Z
I would have said that $\Gamma\vdash t:A$ is the judgement.
Dave Clarke
CC BY-SA 3.0
2012-01-23T19:47:45.283Z
@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).
Kaveh
CC BY-SA 3.0
2012-01-23T19:58:34.270Z
@plmday, AFAIU not all judgments can be turned into propositions. Remember that this is a foundation, it is not easy to think of these by interpreting them in some other foundations (say set theory) in a faithful way. From the perspective of Martin-Löf's type theories these are conceptually different things, and the language doesn't allow you to have Type itself a Type (Girard's paradox?). On the other hand some judgments can be turned into propositions.
Kaveh
CC BY-SA 3.0
2012-01-23T20:32:35.530Z
@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.)
Kaveh
CC BY-SA 3.0
2012-02-11T21:53:02.880Z
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.
Anthony
CC BY-SA 3.0
2012-02-13T00:40:16.560Z
@Anthony, the distinction is made by Per Martin-Löf as far as I know, if other people are using it in other senses that is not what I am talking about. I am also not saying there are no other kinds of judgments, what I have listed is the list of judgments in his theory. In short, I am answering the question based on what is Per's view and his theory (as I understand it).
Kaveh
CC BY-SA 3.0
2012-01-23T04:04:05.787Z
2012-01-23T04:04:05.787Z
Kaveh
<p>I'll try to be short where other answers were more exhaustive. There is a difference between a piece of text saying <em>"The butler did it."</em>, and Mrs. Marple proclaiming <em>"The butler did it."</em> In the second case, the butler might lose his freedom.</p>

CC BY-SA 3.0
2012-02-11T21:56:53.937Z
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?
Anthony
CC BY-SA 3.0
2012-02-12T14:44:06.973Z
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.
Andrej Bauer
CC BY-SA 3.0
2012-11-03T11:55:15.743Z
@Andrej Bauer: I must apologize for down voting you before, now I see the point.  Thanks a lot.
day
CC BY-SA 3.0
2012-01-23T08:35:59.590Z
2012-04-20T05:39:44.240Z
2012-04-20T05:39:44.240Z
Andrej Bauer
<p>Judgements are the composition of two things:</p>

<ol>
<li>A proposition $P$; and</li>
<li>A propositional attitude $\cal A$ – this is what philosophers call it, cf. <a href="http://plato.stanford.edu/entries/prop-attitude-reports/" rel="nofollow">propositional attitude reports</a> which tie propositional attitudes to the speech acts Kaveh talks of; </li>
</ol>

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

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

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

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

CC BY-SA 3.0
2012-04-18T09:20:57.743Z
2012-04-18T09:20:57.743Z
Charles Stewart
<p>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...</p>

CC BY-SA 3.0
2012-01-28T09:57:55.570Z
You are wrong about saying that a judgment has been verified. A verified (proved) judgment is called a theorem.
Andrej Bauer
CC BY-SA 3.0
2012-01-27T18:43:17.013Z
2012-01-27T18:51:27.173Z
2012-01-27T18:51:27.173Z
Samuel Duclos
<p>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:</p>

<blockquote>
  <p>A judgment is something we may know, that is, an object of knowledge. A judgment is evident if we in fact know it.</p>
</blockquote>

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

<blockquote>
  <p>A proposition is interpreted as a set whose elements represent the proofs of the proposition</p>
</blockquote>

<p>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".</p>

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

<p>I suggest "Constructive Logic" by <a href="http://www.cs.cmu.edu/~fp/publications.html">Frank Pfenning</a>, <a href="http://www.paultaylor.eu/stable/Proofs+Types.html">"Proofs and Types"</a> by Jean-Yves Girard and <a href="http://www.cse.chalmers.se/research/group/logic/book/book.pdf">"Programming in Martin-Löf's Type Theory"</a> 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.</p>

CC BY-SA 3.0
2012-02-07T00:31:38.457Z
That first quote is Frank Pfenning, not Girard.
Noam Zeilberger
CC BY-SA 3.0
2015-03-03T21:13:56.300Z
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?
Giorgio Mossa
CC BY-SA 3.0
2016-02-04T04:41:17.887Z
How do we know that we know something? (With regards to "A judgement is evident if we in fact know it"?)
CMCDragonkai
CC BY-SA 3.0
2012-01-20T17:48:17.910Z
2012-04-20T02:47:43.753Z
2012-04-20T02:47:43.753Z
Anthony
<p>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.</p>

CC BY-SA 3.0
2012-03-11T07:49:57.777Z
You may be interested to read http://en.wikipedia.org/wiki/Logical_implication#Proof_procedures.2C_and_relationship_between_entailment_and_deduction
Anthony
<lo.logic><pl.programming-languages><type-theory>
What is the difference between propositions and judgments?
day
# What is the difference between propositions and judgments?

(Asked by: username_0 on 2012-01-20)

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.

**Tags:** lo.logic, pl.programming-languages, type-theory
> **Comments:**
> **username_1**: You may be interested to read http://en.wikipedia.org/wiki/Logical_implication#Proof_procedures.2C_and_relationship_between_entailment_and_deduction  

---

## 6 answers

### Answer by username_1 on 2012-01-20. Score: 21 | Accepted answer

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](http://www.cs.cmu.edu/~fp/publications.html), ["Proofs and Types"](http://www.paultaylor.eu/stable/Proofs+Types.html) by Jean-Yves Girard and ["Programming in Martin-Löf's Type Theory"](http://www.cse.chalmers.se/research/group/logic/book/book.pdf) 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.

> **Comments:**
> **username_8**: That first quote is Frank Pfenning, not Girard.  
> **username_9**: 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?  
> **username_10**: How do we know that we know something? (With regards to "A judgement is evident if we in fact know it"?)  

---

### Answer by username_2 on 2012-02-24. Score: 19

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.


---

### Answer by username_3 on 2012-01-23. Score: 14

In [Martin-Löf](https://en.wikipedia.org/wiki/Per_Martin-L%C3%B6f)'s type theories, judgments are a part of [speech-acts](http://en.wikipedia.org/wiki/Speech_act). 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](http://plato.stanford.edu/entries/assertion/) $\vdash$ is a speech-act. It *asserts* the *content* (which follows it and is a judgment). In [Martin-Löf's type theories](http://en.wikipedia.org/w/index.php?title=Martin-L%C3%B6f%27s_type_theory) 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](https://intuitionistic.wordpress.com/works-on-martin-lofs-type-theory/)).

> **Comments:**
> **username_0**: 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?  
> **username_4**: I would have said that $\Gamma\vdash t:A$ is the judgement.  
> **username_3**: @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).  
> **username_3**: @plmday, AFAIU not all judgments can be turned into propositions. Remember that this is a foundation, it is not easy to think of these by interpreting them in some other foundations (say set theory) in a faithful way. From the perspective of Martin-Löf's type theories these are conceptually different things, and the language doesn't allow you to have Type itself a Type (Girard's paradox?). On the other hand some judgments can be turned into propositions.  
> **username_3**: @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.)  
> **username_1**: 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.  
> **username_3**: @Anthony, the distinction is made by Per Martin-Löf as far as I know, if other people are using it in other senses that is not what I am talking about. I am also not saying there are no other kinds of judgments, what I have listed is the list of judgments in his theory. In short, I am answering the question based on what is Per's view and his theory (as I understand it).  

---

### Answer by username_5 on 2012-01-23. Score: 13

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.

> **Comments:**
> **username_1**: 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?  
> **username_5**: 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.  
> **username_0**: @Andrej Bauer: I must apologize for down voting you before, now I see the point.  Thanks a lot.  

---

### Answer by username_6 on 2012-04-18. Score: 4

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](http://plato.stanford.edu/entries/prop-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.


---

### Answer by username_7 on 2012-01-27. Score: -3

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

> **Comments:**
> **username_5**: You are wrong about saying that a judgment has been verified. A verified (proved) judgment is called a theorem.  

---

