Bool vs Prop

Stream: Lean for teaching

[Martin Dvořák]

How would you explain the difference between Bool and Prop to (smart) highschoolers?

[Kevin Buzzard]

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]

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]

Actually, I first taught them about computation, during which Bool appeared. Now I teach them about proving.

[Martin Dvořák]

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]

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]

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]

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]

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)]

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]

That looks like a lousy pedagogical example, because it leaves the reader baffled over whether age > 40 is decidable or not

[Flo (Florent Schaffhauser)]

Yes, that's the whole point.

[Eric Wieser]

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

[Eric Wieser]

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)]

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:

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