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