<p>From <a href="http://www.scholarpedia.org/article/Computational_type_theory#Judgements_and_Propositions" rel="nofollow">http://www.scholarpedia.org/article/Computational_type_theory#Judgements_and_Propositions</a>:</p>

<blockquote>
  <p>The other kind of logical claim made in CTT is the judgment that a belongs to A. This can be reduced to the equality claim by writing a=a in A.</p>
</blockquote>

<p>From <a href="http://www.nuprl.org/documents/Constable/naive.pdf" rel="nofollow">http://www.nuprl.org/documents/Constable/naive.pdf</a>:</p>

<blockquote>
  <p>It does not make sense to regard a in B as a proposition; for instance, it is not clear what the negation of a in B would mean.</p>
</blockquote>

<p>and again, from the same paper:</p>

<blockquote>
  <p>Also we can define an empty type, void. $$ void= \{ x:A \space |\space x \neq x \space in \space A \} $$</p>
</blockquote>

<p>If $a\space in\space B$ can be written $a=a\space in\space B$, then surely the negation of $a\space in\space B$ is $a\neq a\space in\space B$?</p>

CC BY-SA 3.0
2014-07-07T11:30:41.210Z
Before answering this, do you understand the difference between a judgment and a proposition in the sense of type theory? That may be the first stumbling block.
Andrej Bauer
CC BY-SA 3.0
2014-07-07T18:57:26.903Z
My current understanding is: a proposition is a claim that can turn out to be true or false - it can be considered as a set of proofs, where the set being empty means the proposition is false; a judgment is something that is true because we have decided that it is?
hdgarrood
CC BY-SA 3.0
2014-07-08T06:30:48.320Z
It is also very important to note that a judgment is "top level", it is a basic building block of the formal system, whereas a proposition is something that lives "inside" type theory. It is an object in the theory.
Andrej Bauer
CC BY-SA 3.0
2014-07-08T06:32:33.107Z
Judgments are not about being true or false. They are basic "constructors" from which we build derivations. For instance, you can have a judgment which tells you how to build an ordered pair. What's "true" about that?
Andrej Bauer
CC BY-SA 3.0
2014-07-08T08:55:54.793Z
@AndrejBauer thank you, this is making more sense now. So does that mean `a=a in A` is a judgment, too? What is meant by "logical claim"?
hdgarrood
CC BY-SA 3.0
2014-07-08T13:19:08.560Z
Logical claim is synonymous with Judgment. The issue here, I believe is that $a = a\mbox{ in }A$  is a judgment in the first textbook, but a *proposition* in the second! This means that the texts are in agreement, but they diverge in notation.
cody
<type-theory>
How are these statements about CTT reconcilable?
hdgarrood
# How are these statements about CTT reconcilable?

(Asked by: username_0 on 2014-07-07)

From <http://www.scholarpedia.org/article/Computational_type_theory#Judgements_and_Propositions>:

> The other kind of logical claim made in CTT is the judgment that a belongs to A. This can be reduced to the equality claim by writing a=a in A.

From <http://www.nuprl.org/documents/Constable/naive.pdf>:

> It does not make sense to regard a in B as a proposition; for instance, it is not clear what the negation of a in B would mean.

and again, from the same paper:

> Also we can define an empty type, void. $$ void= \{ x:A \space |\space x \neq x \space in \space A \} $$

If $a\space in\space B$ can be written $a=a\space in\space B$, then surely the negation of $a\space in\space B$ is $a\neq a\space in\space B$?

**Tags:** type-theory
> **Comments:**
> **username_1**: Before answering this, do you understand the difference between a judgment and a proposition in the sense of type theory? That may be the first stumbling block.  
> **username_0**: My current understanding is: a proposition is a claim that can turn out to be true or false - it can be considered as a set of proofs, where the set being empty means the proposition is false; a judgment is something that is true because we have decided that it is?  
> **username_1**: It is also very important to note that a judgment is "top level", it is a basic building block of the formal system, whereas a proposition is something that lives "inside" type theory. It is an object in the theory.  
> **username_1**: Judgments are not about being true or false. They are basic "constructors" from which we build derivations. For instance, you can have a judgment which tells you how to build an ordered pair. What's "true" about that?  
> **username_0**: @AndrejBauer thank you, this is making more sense now. So does that mean `a=a in A` is a judgment, too? What is meant by "logical claim"?  
> **username_2**: Logical claim is synonymous with Judgment. The issue here, I believe is that $a = a\mbox{ in }A$  is a judgment in the first textbook, but a *proposition* in the second! This means that the texts are in agreement, but they diverge in notation.  

---

## 0 answers

