# Zulip Chat Archive

## Stream: new members

### Topic: are truth tables an option?

#### James B Clifford (Dec 02 2022 at 00:08):

I was taught that (a \/ b) is only false when both a and b are false. My prof drew a truth table on the board, crossed out the row where they were both false. Then concluded that the only truthful row where a was false b was true; therefore, not a implies b. I know this is a super simple example, but does lean have a form of truth table syntax? would I use a series of axioms, or define a function that returned false if they were both false and treat the function as the table?

#### Yaël Dillies (Dec 02 2022 at 00:39):

Typically, you would use tactic#by_cases in tactic mode in a proof.

#### Yaël Dillies (Dec 02 2022 at 00:39):

But maybe docs#bor is what you're after? This is precisely defined in a truth table kind of a way.

#### Arien Malec (Dec 02 2022 at 01:19):

It can be confusing at first, but `Prop`

isn't a boolean, and `∨`

in Lean is defined as an `inductive`

where you construct one precisely by giving a proof of either the left or right sides. Boolean or, as @Yaël Dillies notes, is easily defined via a match statement that's the normal truth table.

#### Arien Malec (Dec 02 2022 at 01:25):

I carried around the implicit belief that a `Prop`

is analogous to boolean, and that let me astray at first.

#### Eric Rodriguez (Dec 02 2022 at 01:29):

`Prop`

is like a boolean that you don't know the answer to; that is, `p : Prop`

is either equal to `true`

or to `false`

(docs#classical.prop_complete) but you can have a `Prop`

representing, i.e. the Riemann hypothesis. A `bool`

is always either _literally_ `true`

or `false`

, if that makes sense

#### Arien Malec (Dec 02 2022 at 01:34):

I think that's misleading (or at least it mislead me). If I have a proof of something (or take it as a premise), I have `hp: p`

where `p: Prop`

. I can also have a proof that `p → False`

(which is called `¬p`

in Lean). It turns out you need to know `p ∨ ¬p`

only rarely.

#### Arien Malec (Dec 02 2022 at 01:35):

The earlier you just accept the Curry-Howard correspondence the better.

#### Adam Topaz (Dec 02 2022 at 01:43):

The tactic `tauto!`

should also be mentioned (IIRC it essentially uses truth tables under the hood)

#### Adam Topaz (Dec 02 2022 at 01:43):

Not to be confused with tactic#tauto

#### Eric Wieser (Dec 02 2022 at 01:56):

To the documentation, `tauto`

and `tauto!`

are the same tactic... (docs#tactic.interactive.tauto)

#### Eric Wieser (Dec 02 2022 at 01:57):

... and I broke the rendering somehow, image.png (https://github.com/leanprover-community/lean/issues/789)

#### Eric Rodriguez (Dec 02 2022 at 10:08):

Arien Malec said:

I think that's misleading (or at least it mislead me). If I have a proof of something (or take it as a premise), I have

`hp: p`

where`p: Prop`

. I can also have a proof that`p → False`

(which is called`¬p`

in Lean). It turns out you need to know`p ∨ ¬p`

only rarely.

This is just a proof by contradiction, however. One of those terms cannot exist if Lean is sound; that is, it would have no constructors (but it's obviously hard to decide which one it is!)

#### Arien Malec (Dec 02 2022 at 16:59):

All I'm saying is that I carried around a mistaken belief that `Prop`

was like a boolean and it helped (me at least) to drop that and just follow the types

#### Mario Carneiro (Dec 02 2022 at 17:34):

I'm not sure I would characterize that belief as mistaken

#### Mario Carneiro (Dec 02 2022 at 17:35):

it's more natural to reason about propositions in natural deduction style, but there really are only two of them: docs4#Classical.prop_complete

#### Arien Malec (Dec 02 2022 at 20:19):

The kinds of issues that got me into trouble initially was thinking that in a function of type`p -> q`

I could pass a hypothesis of `¬p`

on the analogy of type `Bool -> Bool`

#### Arien Malec (Dec 02 2022 at 20:20):

Which is what I was used to in a non-dependent-type world.

#### Mario Carneiro (Dec 02 2022 at 20:21):

You can, that's the `absurd`

function

#### Mario Carneiro (Dec 02 2022 at 20:22):

or Not.elim I suppose

```
import Std.Logic
example {p q : Prop} (h1 : ¬p) : p → q := h1.elim
```

#### Arien Malec (Dec 02 2022 at 20:32):

my brain hurts.

```
variable {p q: Prop}
def imp : p → q → p := fun hp: p => fun _ => hp
def err: ¬p → q → ¬p := fun hnp: ¬p => imp hnp
```

#### Mario Carneiro (Dec 02 2022 at 20:34):

FYI `p → q → p`

means `p → (q → p)`

. It says that if p and q are true then p is true

#### Arien Malec (Dec 02 2022 at 20:36):

where my brain hurt was when I expected `imp hnp`

to fail with a type error

#### Jireh Loreaux (Dec 02 2022 at 21:06):

why would you think it would do that? (honest question)

#### Arien Malec (Dec 02 2022 at 21:39):

I've got a function of `p → False`

and I'm feeding it into a function of `p → q → p`

? So maybe I can reason that `imp`

takes `p`

and turns it into `p`

which then leads to a return of a function `p → False`

?

#### Kevin Buzzard (Dec 02 2022 at 21:40):

You're feeding it into a function of type `p' -> q -> p'`

so it just lets p' be not p.

#### Yaël Dillies (Dec 02 2022 at 21:40):

What's confusing is that both `p`

don't mean the same thing.

#### Jireh Loreaux (Dec 02 2022 at 22:00):

Yeah, the key point is that when you do `variable {p q : Prop}`

then these are (universally quantified, and implicit!) variables in the forthcoming declarations. So `imp`

says, *for any* propositions `p`

and `q`

, `p → q → p`

. Now, if `p`

is a proposition, so is `¬p`

and hence we can plug it in instead, to get `¬p → q → ¬p`

(i.e., `err := @imp ¬p q`

).

Perhaps Arien what you were trying to say is that you can't do this *in reverse*? That is, you can't go from `err`

to `imp`

in the same trivial way? (of course, you can after rewriting `¬¬p`

to `p`

, but that requires classical axioms)

#### Arien Malec (Dec 02 2022 at 22:05):

"Now, if p is a proposition, so is ¬p" is where I get confused. I **thought** `¬p`

was a function, not a `Prop`

#### Jireh Loreaux (Dec 02 2022 at 22:06):

Remember, Lean has impredicative `Prop`

, so a Pi type (i.e., edit: *type of* functions) from `Prop`

ends up in `Prop`

.

#### Yaël Dillies (Dec 02 2022 at 22:06):

Those are non contradictory statements. `¬ p`

is a function, but functions have a type too! And the type of `¬ p`

is `Prop`

.

#### Jireh Loreaux (Dec 02 2022 at 22:06):

`p : Prop`

, but also `p → False : Prop`

.

#### Mario Carneiro (Dec 02 2022 at 22:27):

Functions don't have the type `Prop`

, but `¬p`

is not a function, it is a type of functions, that is `p -> False`

, the type of all functions from `p`

to `False`

. `p -> False`

is not itself a function, it is a type, and the type of a type is a universe, in this case `Prop`

.

#### Arien Malec (Dec 02 2022 at 22:50):

and `hnp`

*is* a function, of type `Prop`

?

#### Mario Carneiro (Dec 02 2022 at 22:51):

`hnp`

*is* a function, of type `¬p`

/ `p -> False`

#### Mario Carneiro (Dec 02 2022 at 22:52):

`hnp`

is not of type `Prop`

#### Arien Malec (Dec 02 2022 at 22:57):

hmm. So then I get confused again by `imp hnp`

-- is my reasoning, that `imp hnp`

works by resolving `imp p`

to `p`

to produce `p -> False`

on the right track?

#### Mario Carneiro (Dec 02 2022 at 23:19):

The implicit arguments are doing you a disservice here. Here is your example again without them:

```
def imp : ∀ (p q: Prop), p → q → p := fun p => fun q => fun hp: p => fun _hq: q => hp
def err: ∀ (p q: Prop), ¬p → q → ¬p := fun p => fun q => fun hnp: ¬p => imp (¬p) q hnp
```

#### Mario Carneiro (Dec 02 2022 at 23:22):

`imp`

is actually a function that takes *four* arguments: two propositions `p`

and `q`

, and then a proof of that `p`

and `q`

. Depending on what propositions you pass for the first two arguments, the rest of the theorem can say different things. If you pass `(¬p)`

and `q`

to `imp`

, that's two arguments down and the remaining two arguments should be proofs of `(¬p)`

and `q`

respectively

Last updated: Dec 20 2023 at 11:08 UTC