(∃ x : A, true) → (∃ x:A, PP x) → ∀ x : A, PP x :=

Stream: new members

[Jia Xuan Ng]

Hi everyone,

I'm not understanding:

(∃ x : A, true)

from:

(∃ x : A, true) → (∃ x:A, PP x) → ∀ x : A, PP x :=

Is it saying "there exists an x in A"? If so isn't it redundant? Personally, I don't think it's provable because from my interpretation, it's saying "there exists x : A such that if PP x, then for all A, PP", which isn't a tautology.

[Kyle Miller]

Yes, the first hypothesis is redundant given the second one.

Without knowing what PP is, this statement is not provable.

[Kyle Miller]

For example, if PP x were "for all (y : A), x = y" then it would be provable.

[Kyle Miller]

and if A = nat and PP x means x = 0, then the statement is false.

[Ruben Van de Velde]

Is this an exercise from somewhere? Now if it had said (∃ x : A, true) → (∀ x : A, PP x) → ∃ x:A, PP x, that would make sense

[Reid Barton]

I think it is supposed to be

(∃ x : A, true) → ∃ x:A, (PP x → ∀ x : A, PP x) :=

[Kevin Buzzard]

oh it's "there's someone in the bar who is drinking iff everyone in the bar is drinking"

[Ruben Van de Velde]

It's too late here for that kind of logic puzzle, but at least I convinced lean of it :)

[Kevin Buzzard]

Is your proof constructive?

[Jia Xuan Ng]

Ruben Van de Velde said:

Is this an exercise from somewhere? Now if it had said (∃ x : A, true) → (∀ x : A, PP x) → ∃ x:A, PP x, that would make sense

Erm, we got given this as lab work, we either have to say if it can be proven constructively, classically or not provable at all.

[Jia Xuan Ng]

Reid Barton said:

I think it is supposed to be

(∃ x : A, true) → ∃ x:A, (PP x → ∀ x : A, PP x) :=

Not too sure, but it was given to me as I posted it in the original.

[Ruben Van de Velde]

I only have a vague idea what's constructive, but I guess by_cases isn't it

[Jia Xuan Ng]

Ruben Van de Velde said:

I only have a vague idea what's constructive, but I guess by_cases isn't it

Ye, by_cases is classical if I remember correctly. We call constructive "intuitionistic" here I believe. I'm not too sure if they mean the same.

[Mario Carneiro]

they are mostly synonymous, certainly in this context they are talking about the same thing

[Eric Wieser]

by_cases tries to be constructive if it can, but won't make any noise if it decides to use choice instead

[Mario Carneiro]

in these examples though, it's pretty much always going to be classical because the things to case on are all uninterpreted predicates

[Jia Xuan Ng]

Eric Wieser said:

by_cases tries to be constructive if it can, but won't make any noise if it decides to use choice instead

Oh, I see. The lean document was going on about it being "decidable".

[Jia Xuan Ng]

Kevin Buzzard said:

Is your proof constructive?

Classical is allowed if required.