@Rover: Upon looking again at what we discussed yesterday, I realized why my intuition was telling me something was wrong. Although what you wrote in your last explanation was correct, it is not in general true that x ≤ y implies 1/x ≥ 1/y. Were you aware of that? In particular, if you only had 25/(7−a) ≤ 5 (and no lower bound), you cannot get (7−a)/25 ≥ 1/5 (and it actually is wrong).
It just so happens that the lower bound forces what you wrote to be correct, but I need to ask you to confirm whether you actually know what you were doing or not. So please explain how exactly you got from the first to the second line.
∃ x ∈ S(∀ y ∈ T(P(x,y)))
Given b ∈ T:
Let a ∈ S such that ∀ y ∈ T ( P(a, y))
∀ y ∈ T ( P(a, y))
b ∈ T
P(a, b)
a ∈ S
∃ x ∈ S( P(x, b))
∀ b ∈ T( ∃ x ∈ S(P(x, b)))
∀ y ∈ T( ∃ x ∈ S(P(x, y)))
∃ x ∈ S(∀ y ∈ T(P(x,y))) ⇒ ∀ y ∈ T( ∃ x ∈ S(P(x, y)))
@user21820, I just did an alternative proof of the example you posted in your original post. Could you tell me if this is correct?
Also, could yo explain why you did (on step 6) ∀ rename ?
If ∃ x ∈ S(∀ y ∈ T(P(x,y))):
Given b ∈ T:
Let a ∈ S such that ∀ y ∈ T ( P(a, y))
∀ y ∈ T ( P(a, y))
b ∈ T
P(a, b)
a ∈ S
∃ x ∈ S( P(x, b))
∀ b ∈ T( ∃ x ∈ S(P(x, b)))
∀ y ∈ T( ∃ x ∈ S(P(x, y)))
∃ x ∈ S(∀ y ∈ T(P(x,y))) ⇒ ∀ y ∈ T( ∃ x ∈ S(P(x, y)))
What you did is fine. You just did the ∃elim further inside, whereas I did it outside. And you did the ∀rename at the end rather than at the start. I had to do the ∀rename so that I could pull it inside the inner subcontext. You didn't because you used "Given b∈T:" instead of my "Given y∈T:".
@user21820 Perfect. Thank you. " I had to do the ∀rename so that I could pull it inside the inner subcontext. " Could you please further clarify that ? What's the restriction about ?
...
∀ y ∈ T(P(a, y)) (*)
Given y ∈ T:
y ∈ T
∀ y ∈ T(P(a, y))
P(a, y)
...
@user21820, focusing on the problem, this is forbidden since "y" appears in (*) ? Is this related to variable capturing ? I forgot about these subtle details.
I read the restriction under the ∀restate rule, but cannot make sense of it.
(Q1): ¬ ∀ x ∈ S(P(x)) ⇒ ∃ x ∈ S(¬P(x))
If ¬ ∀ x ∈ S(P(x)):
If ¬ ∃ x ∈ S(¬P(x)):
Given x ∈ S:
If ¬P(x):
∃ x ∈ S(¬P(x))
⊥
P(x)
∀ x ∈ S(P(x))
∃ x ∈ S(¬P(x))
¬ ∀ x ∈ S(P(x)) ⇒ ∃ x ∈ S(¬P(x))
(Q2): ¬∃ x ∈ S(P(x)) ⇒ ∀ x ∈ S(¬P(x))
If ¬∃ x ∈ S(P(x)):
Given x ∈ S:
If P(x):
∃ x ∈ S(P(x))
⊥
¬P(x)
∀ x ∈ S (¬P(x))
¬∃ x ∈ S(P(x)) ⇒ ∀ x ∈ S(¬P(x))
By the way, we were not actually done after that reasoning.
So far we have:
Given any a∈T, you have ∃x∈D ( f'(x) = 0 ), so let c∈D such that f'(c) = 0, and (by your earlier reasoning) you get (4a−3)+(a−7)·cos(c) = 0, and so −1 ≤ (3−4a)/(a−7) < 1 since cos(c) ∈ [−1,1), and hence 3 ≤ 25/(7−a) < 5, which implies −4/3 ≤ a < 2.
We still need to check that −4/3 ≤ a < 2 implies ∃x∈D ( f'(x) = 0 ).
But once you've done that, then you're really done.
@Rover Well if you wanted to do the way I said earlier, you show that if −4/3 ≤ a < 2 then (3−4a)/(a−7) ∈ [−1,1) and so you can find a suitable x∈D such that (3−4a)/(a−7) = cos(x).
In the second method that I just showed you via equivalences, this part occurs exactly in the step Ran(cos↾D) = [−1,1).
The forward reasoning needed Ran(cos↾D) ⊆ [−1,1). The backward check needs [−1,1) ⊆ Ran(cos↾D).
:57412610 You didn't have to delete your question of why it doesn't always work. It's a good question. I don't have a simple answer for you, except that it's always possible to express the solution via equivalences but it is sometimes ridiculously troublesome to do so.
There is no easy way to do it via equivalences, but it is easy if you do it in the two directions. First observe that 1 ∈ U. Next show that d(x^7+2x−3)/dx > 0 for every x∈ℝ, and so U has at most one member.
@user21820 Thanks for taking a look at my attempts. Did you add that ∃ Intro restriction in the original post ? I cannot find where it says that the (witness variable ?) must be unused.
(Q1): ¬ ∀ x ∈ S(P(x)) ⇒ ∃ x ∈ S(¬P(x))
If ¬ ∀ x ∈ S(P(x)):
If ¬ ∃ x ∈ S(¬P(x)):
Given x ∈ S:
If ¬P(x):
∃ y ∈ S(¬P(y))
∃ x ∈ S(¬P(x))
⊥
P(x)
∀ x ∈ S(P(x))
∃ x ∈ S(¬P(x))
¬ ∀ x ∈ S(P(x)) ⇒ ∃ x ∈ S(¬P(x))
(Q2): ¬∃ x ∈ S(P(x)) ⇒ ∀ x ∈ S(¬P(x))
If ¬∃ x ∈ S(P(x)):
Given x ∈ S:
If P(x):
∃ y ∈ S(P(y))
∃ x ∈ S(P(x))
⊥
¬P(x)
∀ x ∈ S (¬P(x))
¬∃ x ∈ S(P(x)) ⇒ ∀ x ∈ S(¬P(x))
(Q1): ¬ ∀ x ∈ S(P(x)) ⇒ ∃ x ∈ S(¬P(x))
If ¬ ∀ x ∈ S(P(x)):
If ¬ ∃ x ∈ S(¬P(x)):
Given x ∈ S:
If ¬P(x):
∃ z ∈ S(¬P(z))
∃ x ∈ S(¬P(x))
⊥
P(x)
∀ x ∈ S(P(x))
∃ x ∈ S(¬P(x))
¬ ∀ x ∈ S(P(x)) ⇒ ∃ x ∈ S(¬P(x))
(Q1): ¬ ∀ x ∈ S(P(x)) ⇒ ∃ x ∈ S(¬P(x))
If ¬ ∀ x ∈ S(P(x)):
If ¬ ∃ x ∈ S(¬P(x)):
Given y ∈ S:
If ¬P(y):
∃ z ∈ S(¬P(z))
∃ x ∈ S(¬P(x))
⊥
P(y)
∀ y ∈ S(P(y))
∀ x ∈ S(P(x))
∃ x ∈ S(¬P(x))
¬ ∀ x ∈ S(P(x)) ⇒ ∃ x ∈ S(¬P(x))
@F.Zer Yes that works. Alternatively, you could rename before pulling in.
If ¬ ∀ x∈S (P(x)):
If ¬ ∃ x∈S (¬P(x)):
¬ ∃ y∈S (¬P(y)).
Given x∈S:
If ¬P(x):
∃ y∈S (¬P(y)).
⊥
Note that "y" is unused inside, but not fresh. Which is fine; the ∃intro rule doesn't require a fresh variable. Only the ∃elim rule needs a fresh variable.
@user21820 Thank you. "y" is unused inside because it does not appear in any previous headers. But it does appear in other statements (that's why it is not fresh). Is that correct ?
(Q2): ¬∃ x ∈ S(P(x)) ⇒ ∀ x ∈ S(¬P(x))
If ¬∃ x ∈ S(P(x)):
Given x ∈ S:
If P(x):
¬∃ y ∈ S(P(y))
∃ y ∈ S(P(y))
⊥
¬P(x)
∀ x ∈ S (¬P(x))
¬∃ x ∈ S(P(x)) ⇒ ∀ x ∈ S(¬P(x))
(Q3):
∃ x ∈ S (x ∈ S) ⇒ ∃ x ∈ S( P(x) ⇒ ∀ y ∈ S( P(y))
If ∃ x ∈ S (x ∈ S):
Let a ∈ S such that a ∈ S
If P(a):
Given y ∈ S:
If ¬P(y):
...
⊥
P(y)
∀ y ∈ S( P(y))
P(a) ⇒ ∀ y ∈ S( P(y))
∃ x ∈ S( P(x) ⇒ ∀ y ∈ S( P(y))
∃ x ∈ S (x ∈ S) ⇒ ∃ x ∈ S( P(x) ⇒ ∀ y ∈ S( P(y))