formalised "definitions" vs "mathematical statements"

Stream: new members

[rzeta0]

Chapter 8 of Type Theory and Formal Proof introduced formalised definitions:

$$\text{context} \triangleright \text{name} := \text{proof} : \text{type}$$

The exercise I'm doing asked us to identify which of the lines (1)-(8) in the attached flag-notation text are "formalised definitions" and which are "formalised mathematical statements".

81.png

Question: I think this is a trick question! I think they are the same. Am I mistaken?

---

Chapter 8.9 says:

if we realise that every statement in the judgement-format of λC,

Γ ⊢M : N,

can also be represented in definition format:

Γ ▷ a(...) := M : N

This small transformation enables us to treat statements and definitions in a similar manner, by taking the definition format as the reigning format

I read this as saying statements and definitions are actually the same.

---

Update - Here is my writeup of the full exercise, for broader context (link).

[Robert Maxton]

What do ∗ₛ and ∗ₚ mean?

[rzeta0]

Robert Maxton said:

What do ∗ₛ and ∗ₚ mean?

The author uses ∗ₛ and ∗ₚ to make clear which types are to be interpreted as "sets" and which as "propositions", but he also explains that this is for convenience as there is no real difference.

Screenshot 2025-11-08 at 02.01.37.png

[rzeta0]

Update - Here is my writeup of the full exercise, for broader context (link).

[Etienne Marion]

I don’t know how it is defined in the book, but for me a statement is a term whose type has type Prop (which seems to be called *p here), while a definition is a term whose type is Sort u for some u (looks like it is either *p or *s in the book?). In the end they are all definitions formally, but informally a definition and a statement are not the same, just as in lean we have def and theorem.

[rzeta0]

@Etienne Marion thanks, I would agree with the practical difference as you have stated. The textbook however says that, yes it is useful to think propositions and sets as different, they are the same. And this is why I was wondering if the exercise was a trick question.
I've attached the section from the book where he says they're the same.
Screenshot 2025-11-08 at 13.37.11.png