« first day (1050 days earlier)      last day (1433 days later) » 

00:41
My last skeleton is wrong. I will continue thinking.
@user21820, I have one question. You said earlier that ∃ Intro rule had a restriction: variable "x" must be unused. However, your original proof (in line 5) applied that rule with an already used variable — "a", at line 2 (Let declaration). Could you explain, please ?
 
4 hours later…
05:09
@F.Zer The ∃elim rule is:
E∈S.
...
P(E).
...
---------------
∃x∈S ( P(x) ).
The rule requires that x is unused and does not appear in S or P. It never required anything about variables appearing in P.
05:49
@user21820 can you give some hints for the one I posted yesterday ?
@Rover Hint: f(t)+f(1−t).
 
2 hours later…
08:24
It's known that $\limsup$ distributes over maximum i.e $\limsup \max (a_b,b_n) = \max (\limsup a_n,\limsup b_n)$. Dually, distribution between $\liminf$ and minimum works, as well. What about $\limsup$ and minimum, though?

We can't just weasel our way through with $\min = -\max -$. The inequality $\limsup a_n\wedge b_n \leqslant \limsup a_n \wedge \limsup b_n$ does work, but the converse doesn't seem to work, but I can't think of a counter-example.
08:47
@user21820 yes thanks answer came 19
 
1 hour later…
10:00
@user21820 Thank you. Did you mean intro, there ?
10:31
@F.Zer Yes, sorry I typed wrongly.
@AlvinLepik Clearly you need sequences that do not converge. Try that.
a_n = 1,1/2,1,1/3 etc
b_n = -1,1-1,1 etc

seems to do the trick
1,0,1,...
0,1,0,...
Also does the trick.
11:33
(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(y):
		If ¬∀ y ∈ S(P (y) )
			Given y ∈ S:
			P(y)
			∀ y ∈ S(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, just did Q3.
12:18
@F.Zer Nope, "P(y)" is not a valid expression because "y" is undefined.
And there's something wrong with the inner contexts as well.
12:42
(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):
		If ¬∀ y ∈ S(P (y) )
			Given y ∈ S:
				...
				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 I see. Now, I fixed it.
Is this skeleton heading in the right direction ?
@F.Zer Well, you can use your intuition to guide you as to whether you believe you can find a proof with that outline. After all, if such a proof is possible then each statement you write must be true in its context, and you can try to use your intuition to guide you to a proof if one exists. For example, with your outline here you have the following statement:
If ∃x∈S (x∈S):
	Let a∈S such that a∈S.
	If P(a):
		...
		∀y∈S (P(y)).
This means that you believe that no matter what witness a∈S you are given, if P(a) then ∀y∈S (P(y)).
@user21820 I am not sure that's sure. If I know P is true for a specific "a", how can I be sure P is going to be true, for every y ∈ S ?
@F.Zer So that suggests that your desired proof outline is too ambitious.
@user21820 Good. Thank you.
13:28
(Q3): ∃ x ∈ S (x ∈ S) ⇒ ∃ x ∈ S( P(x) ⇒ ∀ y ∈ S( P(y))
If ∃ x ∈ S (x ∈ S):
	If ¬ ∃ x ∈ S( P(x) ⇒ ∀ y ∈ S( P(y)):
		Let a ∈ S such that a ∈ S
		If P(a):
			Given b ∈ S
				If ¬P(b):
					If P(b):
						⊥
						∀ y ∈ S (P(y))
					P(b) ⇒ ∀ y ∈ S (P(y))
					b ∈ S
					∃ x ∈ S( P(x) ⇒ ∀ y ∈ S( P(y))
					⊥
				P(b)
			∀ b ∈ S(P(b))
			∀ y ∈ S(P(y))
		P(a) ⇒ ∀ y ∈ S(P(y))
		∃ x ∈ S( P(x) ⇒ ∀ 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, fixed again.
@F.Zer Good that works now.
Thank you.
∀ b ∈ S(P(b))
∀ y ∈ S(P(y))

Can I omit this step and generalize with y directly, @user21820 ?
@F.Zer Eventually, you can do whatever you want as long as it is valid. But as far as the system I gave you goes, you have to write the first line. I always tell people that ironically, once you can follow the deductive system perfectly, you don't really need it anymore.
Understood !
(Q4): ∀ x, y, z ∈ S ( x = y ∧ y = z ⇒ y = z)
Given x ∈ S:
	Given y ∈ S:
		Given z ∈ S:
			If x = y ∧ y = z:
				x = y ∧ y = z
				x = y
				y = z
				x = z
			x = y ∧ y = z ⇒ y = z
		∀ z ∈ S ( x = y ∧ y = z ⇒ y = z)
	∀ y, z ∈ S ( x = y ∧ y = z ⇒ y = z)
∀ x, y, z ∈ S ( x = y ∧ y = z ⇒ y = z)
@user21820, Q4 is ready.
By the way, if you find your proof of (Q3) weird, you can take a look at how you can get a more intuitive proof using LEM (which you can of course prove separately if the deductive system doesn't natively support it):
1
A: Truth of a sentence in predicate logic

user21820 [...] It seems entirely trivial by comparison to the long chain of formal manipulations given as the solution, so I assumed it had to be faulty. [...] The problem with your assumption is that formal proofs from scratch need to prove every single bit of the reasoning involved. In particular, how...

@F.Zer Lol that typo got into my exercise again?
Nov 5 '20 at 18:00, by user21820
> (Q4) forall x,y,z in S ( x=z and y=z implies x=y ).
13:44
@user21820 Sorry, made a mistake
It's my mistake, not yours, because I keep forgetting that I made a typo and hence when I link to the original list the typo is always there.
That's the unfortunate result of using chat messages instead of something I can edit.
@user21820 No, I read (x = y and y = z ⇒ x = z) but I incorrectly wrote: ( x = y ∧ y = z ⇒ y = z). Yours is correct. In the link you shared with me last week, I think.
Oh, yes the link I gave you last week was indeed correct, though not the one I intended, which I just quoted.
My typos proliferate like mad...
@user21820 This is the link you gave me: chat.stackexchange.com/transcript/77161?m=56231776#56231776
By the way, my proof of Q4 is incorrect. Will fix it.
Yes. You should prove the one I just quoted though, as it is 'better'.
13:52
Ok, I will attempt that one.
(Q4): ∀ x, y, z ∈ S ( x = z ∧ y = z ⇒ x = y)
Given x ∈ S:
	Given y ∈ S:
		Given z ∈ S:
			If x = z ∧ y = z:
				y = z
				y = y
				z = y
				x = z
				x = y
			 x = z ∧ y = z ⇒ x = y
		∀ z ∈ S  (x = z ∧ y = z ⇒ x = y)
	∀ y, z ∈ S ( x = z ∧ y = z ⇒ x = y)
∀ x, y, z ∈ S ( x = z ∧ y = z ⇒ x = y)
@user21820, Q4 is ready.
@F.Zer Yup correct.
Good.
 
4 hours later…
17:36
(Q5):
(=>) ∀ x ∈ S ( ∀ y ∈ S ( Q (x, y) ⇒ P(x)) ⇒ ∀ x is ∈ S ( ∃ y ∈ S (Q(x, y)) ⇒ P(x))
If ∀ x ∈ S ( ∀ y ∈ S ( Q (x, y) ⇒ P(x))):
	Given a ∈ S:
		If ∃ y ∈ S (Q(a, y)):
			Let b ∈ S such that Q(a, b)
			∀ y ∈ S ( Q (a, y) ⇒ P(a) )
			Q(a, b) ⇒ P(a)
			Q(a, b)
			P(a)
		∃ y ∈ S (Q(a, y)) ⇒ P(a))
	∀ a ∈ S ( ∃ y ∈ S (Q(a, y)) ⇒ P(a)))
	∀ x ∈ S ( ∃ y ∈ S (Q(x, y)) ⇒ P(x)))
∀ x ∈ S ( ∀ y ∈ S ( Q (x, y) ⇒ P(x))) ⇒ ∀ x ∈ S ( ∃ y ∈ S (Q(x, y)) ⇒ P(x)))
@user21820, just did one side of Q5.
@F.Zer How did that "is" sneak in? =P
Looks good except you have an extra bracket in each of the last 4 lines.
@user21820 Well spotted :-) I have a Typinator snippet named “isin” as an abbreviation for “belongs” symbol.
@user21820 Yes, I didn’t notice that,
18:15
(Q5):
(<=)
∀ x is ∈ S ( ∃ y ∈ S (Q(x, y)) ⇒ P(x)) ⇒ ∀ x ∈ S ( ∀ y ∈ S ( Q (x, y) ⇒ P(x))
If ∀ x is ∈ S ( ∃ y ∈ S (Q(x, y)) ⇒ P(x)):
	Given a ∈ S:
		Given b ∈ S:
			If Q(a, b):
				∃ y ∈ S (Q(a,y))
				∃ y ∈ S (Q(a,y)) ⇒ P(a)
				P(a)
			Q(a, b) ⇒ P(a)
		∀ b ∈ S ( Q (x, b) ⇒ P(x))
		∀ y ∈ S ( Q (x, y) ⇒ P(x))
	∀ a ∈ S ( ∀ y ∈ S ( Q (a, y) ⇒ P(a)))
	∀ x ∈ S ( ∀ y ∈ S ( Q (x, y) ⇒ P(x)))
∀ x is ∈ S ( ∃ y ∈ S (Q(x, y)) ⇒ P(x)) ⇒ ∀ x ∈ S ( ∃ y ∈ S (Q(x, y)) ⇒ P(x))
@user21820, I leave here the other side of Q5.

« first day (1050 days earlier)      last day (1433 days later) »