# Zulip Chat Archive

## Stream: new members

### Topic: prop false and type false

#### Huỳnh Trần Khanh (Mar 01 2021 at 00:02):

it seems that the two are different right? this is making me really confused can anyone explain this stuff

#### Huỳnh Trần Khanh (Mar 01 2021 at 00:06):

from what i understand type false is a type that has no inhabitants and there is a function that maps an instance of an uninhabited type to any type on earth called `false.elim`

#### Huỳnh Trần Khanh (Mar 01 2021 at 00:06):

and the false prop is like a boolean value and that's it

#### Huỳnh Trần Khanh (Mar 01 2021 at 00:06):

but under that mental model there are things that feel incongruent

#### Huỳnh Trần Khanh (Mar 01 2021 at 00:06):

so I'm pretty sure my understanding is wrong somehow

#### Kevin Buzzard (Mar 01 2021 at 00:22):

Can you link to the terms you're talking about e.g. docs#false ? I only know of `false : Prop`

, which is the false proposition. Sure you can call it a type, if you're happy to call Propositions types. If you're confused about the whole "propositions as types" thing then maybe you want to look at #tpil chapter 3 or my blog post about it.

#### Adam Topaz (Mar 01 2021 at 00:53):

By type false do you mean docs#pempty ?

#### Huỳnh Trần Khanh (Mar 01 2021 at 05:52):

I think now I know where my confusion stems from. The `false`

type that I talk about is actually the proof of false type. There is the proof type and there is the prop type. And the two types are conflated to simplify the syntax. When I write `def something : Prop := false`

, I'm telling Lean that there is `something`

that is false. It doesn't constitute a proof of false, the word `false`

here is only a truth value. However when I use exfalso for example and the goal turns into `false`

, the word `false`

here indicates that I have to show a term that has type `Proof false`

, and the word `Proof`

is elided because proof and prop are conflated.

From #tpil chapter 3:

This approach would provide us with a reasonable way of building assertions and proofs. Determining that an expression

`t`

is a correct proof of assertion`p`

would then simply be a matter of checking that`t`

has type`Proof p`

.Some simplifications are possible, however. To start with, we can avoid writing the term

`Proof`

repeatedly by conflating`Proof p`

with`p`

itself. In other words, whenever we have`p : Prop`

, we can interpret`p`

as a type, namely, the type of its proofs. We can then read`t : p`

as the assertion that`t`

is a proof of`p`

.

#### Eric Wieser (Mar 01 2021 at 06:41):

I think your "there is the proof for and there is the prop type" model is not a good one. Try replacing `false`

with `nat`

in your above code snippets; the nat in `37 : nat`

and `nat : Type`

are the same.

#### Eric Wieser (Mar 01 2021 at 06:42):

Just as the false in `(sorry : false)`

and `(false : Prop)`

are the same

#### Mario Carneiro (Mar 01 2021 at 08:35):

There are type theories that would require some transformation or coercion in order to treat a term as a type, so that the latter example would be `sorry : T(false)`

and `false : Prop`

where `T`

is a constructor that makes types from terms representing types. This `T`

, renamed to `Proof`

, is what TPIL is talking about, but in lean there is no such coercion, the set of types is a literal subset of the set of terms so `T`

is an identity

Last updated: May 10 2021 at 00:31 UTC