# Zulip Chat Archive

## Stream: Lean for teaching

### Topic: Bool vs Prop

#### Martin Dvořák (Dec 17 2023 at 08:49):

How would you explain the difference between `Bool`

and `Prop`

to (smart) highschoolers?

#### Kevin Buzzard (Dec 17 2023 at 11:08):

They're the same thing, but at different levels in the hierarchy: one is a type and one is a universe. I usually explain universes, types and terms on day 1

#### Alex J. Best (Dec 17 2023 at 14:06):

That said, why do you want to explain that to highschoolers? If you are just teaching them a bit about formalizing maths and not about computation it seems an unnecessary confusion to even introduce Bool at all

#### Martin Dvořák (Dec 17 2023 at 14:18):

Actually, I first taught them about computation, during which `Bool`

appeared. Now I teach them about proving.

#### Martin Dvořák (Dec 17 2023 at 14:19):

Kevin Buzzard said:

They're the same thing, but at different levels in the hierarchy: one is a type and one is a universe. I usually explain universes, types and terms on day 1

D-D-D-Day 1? I hoped I could avoid talking about universes altogether!

#### Mario Carneiro (Dec 17 2023 at 14:24):

well, once you say "everything has a type" it's a pretty natural question to ask what the type of `Type`

is, even at a high school level. For extra fun you can climb the universe hierarchy using lean's nested hovers

#### Kevin Buzzard (Dec 17 2023 at 14:37):

I say x : Real : Type and proof : statement : Prop and that's about it as far as type theory is concerned, so Prop is explained on day 1 yes. I never talk about bool because I'm talking to mathematicians

#### Yury G. Kudryashov (Dec 17 2023 at 14:53):

There are quite a few open questions that can be explained to high schoolers. E.g., "every triangle admits a periodic billiard trajectory". That's a `Prop`

that you don't know how to convert to `Bool`

.

#### Kyle Miller (Dec 17 2023 at 15:41):

A `Bool`

is either true or false, and if you let Lean run for long enough it will tell you which it is. A `Prop`

is either True or False, but you can't depend on Lean to tell you -- but you can try to write a proof.

You need some passing familiarity with incompleteness to appreciate that there really is a distinction. Otherwise, I guess you could say something like what Yury is suggesting, that `Prop`

is like `Bool`

but it doesn't come with any algorithms to evaluate the statements. (How would you evaluate a universal quantifier over Nat? That's like an infinite `for`

loop.)

#### Flo (Florent Schaffhauser) (Dec 17 2023 at 17:28):

Martin Dvořák said:

Actually, I first taught them about computation, during which

`Bool`

appeared. Now I teach them about proving.

How about giving them some intuition of what a decidable proposition is, and then say that a decidable proposition can be converted into a boolean value?

```
def testAge (age : Nat) := age > 40
#check testAge 21 -- testAge 21 : Prop
#eval testAge 21 -- failed to synthesize Decidable (testAge 21)
def testAgeBool (age : Nat) : Bool := age > 40
#check testAgeBool 21 -- testAgeBool 21 : Bool
#eval testAgeBool 21 -- false
```

Conversely, a term `b : Bool`

can be converted into the proposition `P := Eq b true `

and we see that `P`

has a proof if `b = true `

and that `¬P`

has a proof if `b = false`

.

Surely, somebody will ask if every proposition is decidable :sweat_smile:

#### Eric Wieser (Dec 18 2023 at 10:50):

That looks like a lousy pedagogical example, because it leaves the reader baffled over whether `age > 40`

is decidable or not

#### Flo (Florent Schaffhauser) (Dec 18 2023 at 11:09):

Yes, that's the whole point.

#### Eric Wieser (Dec 18 2023 at 12:00):

So is the point in that example to teach the reader about reducibility?

#### Eric Wieser (Dec 18 2023 at 12:01):

Because certainly that seems to be what this extended example shows:

```
def testAge (age : Nat) : Prop := age > 40
#check testAge 21 -- testAge 21 : Prop
#eval testAge 21 -- failed to synthesize Decidable (testAge 21)
abbrev testAgeAbbrev (age : Nat) : Prop := age > 40
#check testAgeAbbrev 21 -- testAgeAbbrev 21 : Prop
#eval testAgeAbbrev 21 -- false
def testAgeBool (age : Nat) : Bool := age > 40
#check testAgeBool 21 -- testAgeBool 21 : Bool
#eval testAgeBool 21 -- false
```

#### Flo (Florent Schaffhauser) (Dec 18 2023 at 12:54):

Oh, I see.

But no, I was hoping it would trigger questions surrounding decidability instead, in relation with #decPropToBool.

```
instance decPropToBool (p : Prop) [Decidable p] : CoeDep Prop p Bool where
coe := decide p
```

So, to sum up, two (hoped for) points:

- Show that a decidable proposition can be converted into a boolean value.
- Discuss non-decidable propositions (informally).

Last updated: Dec 20 2023 at 11:08 UTC