## 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).

#### 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 the second example, as well as in the last 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

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

#### 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