True and False From Scratch

This time we'll build True and False from almost nothing.

This is part two of my adventure into learning how Lean works. Here's a quick recap of the concepts I started with last time:

With those concepts behind us, I think we have enough substance to try and build True and False from scratch with as few ingredients as possible.

Inhabitation

Before I could build False on my own, I had to work out some more terminology.

Of course, it's the ideas behind the new words that matter. But these words are useful to know (and practice using) because they help us talk about what we're building more directly.

I think we covered terms and types well enough as an introduction in the last post. Now we'll talk about how they interact.

The first bit to nail down: terms inhabit types.

The number 3 inhabits Nat.

That word is important, because it lets us say the next bit, which is that uninhabited means unproven.

Uninhabited means unproven

A type with a term is inhabited. A type with no terms at all is uninhabited. That type is empty. Nothing exists that you can point to as a value of it.

In a world where Nat is uninhabited, there is no 3 and there are no other numbers. Thankfully we don't live in that world.

This emptiness is the first ingredient to building False.

Propositions as types

We met Prop in passing last time, and we saw that a proposition is a type, as we saw by running #check Prop.

Say the following sentence out loud a few times to get comfortable with it, using your fresh understanding of the terms proposition, term, and type.

A proof of a proposition is a term of that proposition's type.

A proof is any term that inhabits a proposition. To inhabit a proposition is to prove it.

"Prove P" and "construct a term of type P" are the same thing in Lean.

And here's a fun fact: this relationship between proofs, terms, and types is called propositions as types or the Curry-Howard correspondence and it shows that logic and type theory are basically the same machine wearing different clothing.

With that (extremely profound) relationship at our disposal, we now have a few fresh ideas to put together:

• build Lean types (inductives, last post)
• terms + types + Prop
• emptiness, inhabitation
• propositions as types

If we can frame False as "our name for that which is empty" and translate that into Lean as uninhabited or "that which cannot be proven" then our approach to building it becomes clear: we can express the concept of absolute emptiness by building something that can never be proven.

Building False

One more new thing to introduce: we need a namespace, otherwise we'll have a name clash with the built-in False type (assuming we're running this code in a Lean environment).

namespace TrueAndFalseFromScratch

inductive False : Prop

end TrueAndFalseFromScratch

That's it! Notice the inductive has no constructors, so there is no way to build a term of type False.

Therefore, False is uninhabited, and therefore unproven.

Furthermore, we've made it impossible to prove False because there is no way to construct a term of type False in our system.

To me, this constraint feels intuitively correct, because "proving False to be True" sounds like something our system should very much disallow from happening!

The winning feature of False is precisely this trait, that we can't construct a proof of it by definition.

Let's build True

Can we build True?

What does True mean exactly?

My first attempt at assigning meaning to it felt very circular. "True is... true... by definition" is an empty tautology that just hands True right back to itself.

Here is an idea that helped me a little bit: think of True as the mirror image of False. We just built False as a proposition that nothing can ever prove. True is the opposite extreme: the proposition you can always prove.

"Always" is an important word there, because "always" implies something like "in all circumstances" which in Lean parlance we can translate into something like "without any evidence required." It's unconditional.

That's the idea we will land on: proving True demands no evidence.

How can we capture this idea in Lean? We can give True a nullary constructor: a constructor that takes no arguments. Its arity, the number of arguments it demands, is zero. That means we can construct a term of type True without supplying anything.

The same sentence with the full idea:

Proving True demands no evidence because its one and only constructor requires no arguments to pass in.

In Lean, that shakes out as an inductive with a single constructor and nothing else. We'll name the constructor trivial, which feels right for a proof that asks for nothing.

namespace TrueAndFalseFromScratch

inductive True : Prop
  | trivial

end TrueAndFalseFromScratch

"How much evidence does a proposition demand?" is literally "what is the arity of its constructors?"

True has only one path to it, a single constructor, with no arguments.

Let's compare True and False so far.

False has zero doors to enter, so you can never get a term and it's never provable; True has one door that asks for nothing to pass through (no arguments), so you can always construct a term and it's therefore trivially provable.

Prove it

We have the two types. A proof of a proposition is a term of that proposition's type. To prove True, we construct a term of type True. We hand that term to an example, which is how we state a proposition and prove that proposition in a single line of Lean.

namespace TrueAndFalseFromScratch

example : True := True.trivial

end TrueAndFalseFromScratch

The : True part is the proposition we are claiming.

The := means "is defined to be" and because we're Lean beginners, let's line up all the colons and equals we've seen so far and review:

So True.trivial on the right is that proof term. Lean accepts it because trivial asks for nothing, so the term always exists.

Now picture trying the same thing for False:

example : False := -- What can we put here? Nothing!

There is no constructor to name on the right side, so there is no term to supply, so the proof cannot exist. That is precisely the property we built False to have.

What I find most interesting is that we never really had to define truth or falsity directly. We only asked how much evidence a proposition demands, and found the two extremes: demand the impossible and you get False, demand nothing at all and you get True. Everything in between, the propositions that ask for some particular evidence, is where all the interesting stuff is.