# Zulip Chat Archive

## Stream: new members

### Topic: proving trivial facts about types

#### Joseph Corneli (Jan 24 2019 at 13:57):

I can `#check ff`

but can I *prove* ff : bool or similar facts?

Let's see:

-- works example (ff : bool) := tt example (ff : bool) := ff -- breaks example (1 : ℕ) := (1 : ℕ) -- breaks theorem ff_is_a_bool : (ff : bool) := (↥ff : Prop)

Oh dear, I am confused again.

#### Reid Barton (Jan 24 2019 at 14:06):

The typing relation is not something you can prove or really talk about at all internal to the system.

#### Reid Barton (Jan 24 2019 at 14:06):

In logic terminology it's a judgment, not a proposition.

#### Joseph Corneli (Jan 24 2019 at 14:08):

I guess I can say tautological things like "every bool is a bool"...

theorem t (x : bool) : bool := x

#### Joseph Corneli (Jan 24 2019 at 14:10):

but it's interesting, these type judgments don't live in the hierarchy of types?

#### Joseph Corneli (Jan 24 2019 at 14:13):

In general, a judgment may be any inductively definable assertion in the metatheory.

So is Lean's metatheory accessible somewhere?

#### Reid Barton (Jan 24 2019 at 14:17):

Metatheory here means whatever logical framework you are using to define and reason about the formal system (Lean in this case).

#### Reid Barton (Jan 24 2019 at 14:17):

For example, it can just be ordinary informal mathematics.

#### Reid Barton (Jan 24 2019 at 14:21):

For example, you could prove a "unique typing" theorem like "if `e : t1`

and `e : t2`

[are derivable judgments], then `t1 = t2`

[is a derivable judgment]".

#### Reid Barton (Jan 24 2019 at 14:22):

that's a theorem you would prove in an ordinary math paper, probably using induction on the ordinary natural numbers and so on

#### Reid Barton (Jan 24 2019 at 14:44):

I should add that encoding "`ff`

is a `bool`

" as a judgment `ff : bool`

is part of what it means to use type theory as a foundation. In a system based on set theory, for example, `ff`

would be represented by some set and `bool`

would be represented by some other set and `ff ∈ bool`

would be a proposition that you could prove.

#### Reid Barton (Jan 24 2019 at 14:48):

https://github.com/digama0/lean-type-theory/releases is Mario's paper on the theory of Lean in particular, though it doesn't have much in the way of background material

#### Kevin Buzzard (Jan 24 2019 at 15:20):

I guess I can say tautological things like "every bool is a bool"...

theorem t (x : bool) : bool := x

That's not a theorem. That's a definition of a function t from `bool`

to `bool`

; you can check the type of `t`

to see this. Theorems are terms whose type is `Prop`

.

#### Kevin Buzzard (Jan 24 2019 at 15:21):

PS if you write ` ```lean `

rather than just ` ``` `

then you get cool syntax highlighting :-)

Last updated: May 11 2021 at 00:31 UTC