# Zulip Chat Archive

## Stream: new members

### Topic: quantifier exercises

#### Olli (Sep 08 2018 at 09:10):

could I get a hint how to make progress here:

https://gist.github.com/luxbock/853bdcdde0f333502055c6913fc91e9c

#### Reid Barton (Sep 08 2018 at 09:11):

You can't make progress without some classical axiom.

#### Kenny Lau (Sep 08 2018 at 09:12):

please provide a minimum *working* example (MWE).

#### Reid Barton (Sep 08 2018 at 09:13):

Most directly, `classical.by_contradiction`

#### Reid Barton (Sep 08 2018 at 09:14):

Or, wait. Also what Kenny said. Where did `a`

come from?

#### Olli (Sep 08 2018 at 09:15):

sorry, I'll edit to include the full context and also my attempt with `by_contradiction`

where I got stuck

#### Kenny Lau (Sep 08 2018 at 09:16):

please provide a *minimum* working example (MWE).

#### Olli (Sep 08 2018 at 09:18):

https://gist.github.com/luxbock/853bdcdde0f333502055c6913fc91e9c updated

#### Kenny Lau (Sep 08 2018 at 09:20):

I don't think that's what you want to prove.

#### Reid Barton (Sep 08 2018 at 09:22):

This `variable a : α`

isn't doing what you want--now you have to prove `p a`

for *every* `a`

#### Olli (Sep 08 2018 at 09:22):

this is one of the exercises from here:

https://leanprover.github.io/theorem_proving_in_lean/quantifiers_and_equality.html

#### Olli (Sep 08 2018 at 09:23):

so my attempt is clearly wrong (it does not work after all), but I don't know how to make progress beyond `by_contradiction (λ ha, _)`

#### Olli (Sep 08 2018 at 09:24):

I don't know how to go about getting a `p a`

from what I have:

nanpx : (∀ (x : α), p x → false) → false, hnpa : ¬p a ⊢ false

#### Kenny Lau (Sep 08 2018 at 09:24):

Notice that the declaration

`variable a : α`

amounts to the assumption that there is at least one element of type`α`

. This assumption is needed in thesecondexample, as well as in thelast two.

#### Kenny Lau (Sep 08 2018 at 09:25):

your example is neither the second nor the last two

#### Reid Barton (Sep 08 2018 at 09:25):

You can never get `p a`

, because `a`

is an arbitrary member of `α`

, and it might not be one for which `p`

holds.

#### Reid Barton (Sep 08 2018 at 09:26):

So line 11 `suffices hpa : p a, from ...`

is already the wrong way to go.

#### Reid Barton (Sep 08 2018 at 09:28):

The way to do this is to use `by_contradiction`

at the top level--suppose `¬ (∃ x, p x)`

, then what?

#### Olli (Sep 08 2018 at 09:29):

thanks, I'll try to see where backtracking to beginning gets me. although now that @Kenny Lau commented about the `variable`

declaration, I'm a little bit confused about if I need to change anything outside this example

#### Olli (Sep 08 2018 at 09:30):

oh I think I understand what you mean, I don't need the `variable`

declaration for this particular example

#### Olli (Sep 08 2018 at 09:30):

I just copy/pasted the exercises from the page and I'm filling in the `sorry`

's

#### Olli (Sep 08 2018 at 09:33):

actually that can't be the case, so yeah I am confused about what you meant @Kenny Lau

#### Kenny Lau (Sep 08 2018 at 09:34):

You don't need `variable a : α`

#### Olli (Sep 08 2018 at 09:35):

I think I need it, because `p`

uses it

#### Olli (Sep 08 2018 at 09:36):

oh sorry, I now realize what you meant

#### Olli (Sep 08 2018 at 09:42):

got it, thanks for the help

#### Wojciech Nawrocki (Sep 09 2018 at 00:27):

I'm doing the same exercise atm!

I found some disparities in mathlib's intuitionist and classical namespaces, namely in intuitionist we have this:

theorem not_forall {p : α → Prop} [decidable (∃ x, ¬ p x)] [∀ x, decidable (p x)] : (¬ ∀ x, p x) ↔ ∃ x, ¬ p x := ⟨not.imp_symm $ λ nx x, nx.imp_symm $ λ h, ⟨x, h⟩, not_forall_of_exists_not⟩ @[simp] theorem not_forall_not [decidable (∃ x, p x)] : (¬ ∀ x, ¬ p x) ↔ ∃ x, p x := by haveI := decidable_of_iff (¬ ∃ x, p x) not_exists; exact not_iff_comm.1 not_exists

but in classical only this:

protected theorem not_forall : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) := not_forall

So from `classical.not_forall.mp h`

with `h: ¬ ∀ x, ¬ p x`

we get a double negation. Now, I know that `¬¬p ↔ p`

is easy to prove from classical axioms, but despite how common its usage seems to be, there is no theorem for it built into the library. Is there some reason why double-negation is redundant, or should I make a PR to add it?

#### Kevin Buzzard (Sep 09 2018 at 00:30):

lean and mathlib are pretty huge, it would surprise me if `¬¬p ↔ p`

were not there already.

#### Mario Carneiro (Sep 09 2018 at 00:30):

The idea is that you should use the "intuitionist" theorem and use `classical.dec`

to fulfill the decidability assumptions

#### Mario Carneiro (Sep 09 2018 at 00:31):

(aka `classical.prop_decidable`

)

#### Wojciech Nawrocki (Sep 09 2018 at 00:31):

@Kevin Buzzard `#find`

tells me that there are versions for `decidable p`

, but not for generic propositions in classical reasoning

#### Wojciech Nawrocki (Sep 09 2018 at 00:32):

@Mario Carneiro oh i see, so i should use all the `decidable`

stuff with classical reasoning and then that one axiom to make it work? Ok

#### Mario Carneiro (Sep 09 2018 at 00:33):

This is why you often see `local attribute [instance] classical.prop_decidable`

at the top of files that do classical reasoning

#### Kevin Buzzard (Sep 09 2018 at 00:34):

I've taken to using `local attribute [instance, priority 1] classical.prop_decidable`

#### Kevin Buzzard (Sep 09 2018 at 00:34):

because I ran into situations where this local attribute clobbered some decidability result which type class inference had given me and I ended up with typeclass problems.

#### Mario Carneiro (Sep 09 2018 at 00:35):

is `priority 0`

problematic?

#### Wojciech Nawrocki (Sep 09 2018 at 00:37):

I see, this attribute is indeed used in `classical.lean`

#### Kevin Buzzard (Sep 09 2018 at 00:49):

is

`priority 0`

problematic?

my bad, I just went back to the file where some undergrads were having trouble and indeed I fixed it with `priority 0`

#### Olli (Sep 11 2018 at 02:13):

is it possible to solve the barber paradox exercise without using `classical`

?https://leanprover.github.io/theorem_proving_in_lean/quantifiers_and_equality.html

#### Mario Carneiro (Sep 11 2018 at 02:19):

yes

#### Olli (Sep 11 2018 at 02:20):

can I have a hint? this is what I have so far:

example (h : ∀ x : α, S x x ↔ ¬ S x x) : false := have saa : S a a → ¬S a a, from (h a).mp, have nsaa : ¬ S a a → S a a, from (h a).mpr, sorry

#### Mario Carneiro (Sep 11 2018 at 02:21):

hint: solve exercise 3.7.2

#### Mario Carneiro (Sep 11 2018 at 02:21):

also your problem statement isn't quite right for the barber paradox

#### Olli (Sep 11 2018 at 02:23):

thanks, looks like I actually overlooked 3.7.2, so I'll go back to that and try to figure it out from there (and also fix what you mentioned)

#### Mario Carneiro (Sep 11 2018 at 02:23):

example {α} (b : α) (r : α → α → Prop) (H : ∀ x : α, r b x ↔ ¬ r x x) : false := sorry

#### Eduardo Cavazos (Nov 08 2019 at 00:29):

hint: solve exercise 3.7.2

@Mario Carneiro, Your hint here helped me. Thanks again!

#### Eduardo Cavazos (Nov 08 2019 at 00:34):

For any folks who come back to this thread by searching for "barber"...

In 4.6.3 (the barber paradox) we're given the following to start:

h : ∀ x : men, shaves barber x ↔ ¬ shaves x x

But I kept thinking, what can I apply this to??? We'll, `barber`

is a `men`

so... this is valid:

h barber

It gives us a value of type:

shaves barber barber ↔ ¬shaves barber barber

And for the rest, as @Mario Carneiro mentions, consider 3.7.2.

Last updated: May 15 2021 at 00:39 UTC