« first day (1049 days earlier)      last day (1434 days later) » 

12:05
@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.
12:30
∃ 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 ?
This is the post I am referring to: math.stackexchange.com/questions/1681857/…
My proof is incorrect, will post in a moment.
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)))
Wait what's the difference between the two you posted?
@user21820 An If is missing in the first step.
Oh lol I didn't see that.
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 ?
@F.Zer See the condition under the ∀restate rule: "x must not appear in A".
12:50
...
∀ 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.
13:37
I leave here one FOL exercise, @user21820.
(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))
 
2 hours later…
15:16
@F.Zer Yes that's exactly what it means; "y" appears in "∀ y ∈ T(P(a, y))" so you cannot restate "∀ y ∈ T(P(a, y))" under "Given y ...".
@F.Zer Your ∃intro step is wrong because "x" is not unused under "Given x∈S:". If you fix that then it would be ok.
Same mistake for (Q2).
15:51
@user21820 for what I wrote the signs of both sides of inequality should be same..
@Rover That's right!
Good that you know, so I didn't have to worry.
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.
@user21820 okay
The other way is to attempt to manipulate the desired set directly using equivalences.
@user21820 I don't know about it ..
If you are saying about equivalence relation I know what it is .
@user21820 it does, at a=-4\3 for cos(c)=-1
16:10
T = { a : a∈ℝ and ∃x∈D ( f'(x) = 0 ) }
= { a : a∈ℝ and ∃x∈D ( (4a−3)+(a−7)·cos(x) = 0 ) }
= { a : a∈ℝ and ∃x∈D ( cos(x) = (3−4a)/(a−7) ) }
= { a : a∈ℝ and (3−4a)/(a−7) ∈ Ran(cos↾D) }
= { a : a∈ℝ and (3−4a)/(a−7) ∈ [−1,1) }
= { a : a∈ℝ and −25/(a−7) ∈ [3,5) }
= { a : a∈ℝ and (a−7)/25 ∈ −1/[3,5) }
= { a : a∈ℝ and (a−7)/25 ∈ [−1/3,1/5) }
= { a : a∈ℝ and (a−7) ∈ [−25/3,5) }
= { a : a∈ℝ and a ∈ [−4/3,2) }
= [−4/3,2).
How can we checking interval , by taking any random a ?
@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).
Okay
Note that equivalences don't always work well, so you still need to learn to solve such problems using the full logical reasoning.
But I hope you now know what I meant earlier on when I said:
yesterday, by user21820
So, replace the "f'(x) = 0" with what you found, and continue from there.
Yes now I know it
@user21820 so, it's what called equivalence method, it's better, but as you said it won't work always .
@user21820 ok
16:17
@Rover That's right, it is neat and tidy when you can get it to work.
16:33
: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.
Okok
For example, suppose you want to find U = { x : x∈ℝ and x^7+2x = 3 }.
Ok
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 Hmm yes
16:48
@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.
@F.Zer It says before all the quantifier rules haha..
> Now take any type S and a property P and an unused variable x that does not appear in S or P.
It's just to prevent potential nonsense later. It's not that your intuition is actually wrong.
@user21820 Good. Thank you. I see, now. Variable "x" is being used in the header "Given x ∈ S:"
:57412962 So,
If ¬ P(x)
	∃ y ∈ S (¬P(y))

But, how can I find a contradiction ? Do I have to use variable renaming ?
@F.Zer Yes the easiest way is just to use renaming to get the stuff you want.
Anything that can be done using renaming can be done without renaming, but it's kind of silly to.
(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))
@user21820, are they correct, now?
Nope; the rename rules also require unused variables.
17:02
Ok.
(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))
No, still wrong for the same reason.
You're trying to rename "∃ z ∈ S(¬P(z))" to "∃ x ∈ S(¬P(x))" but "x" is already used!
(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))
@user21820 Fixed.
17:35
@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 ?
@F.Zer Right.
17:51
(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))
@user21820, just fixed Q2.
@F.Zer Yea that's it.
Thank you.
18:18
(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))
@user21820, is my proof skeleton of Q3 correct ?

« first day (1049 days earlier)      last day (1434 days later) »