@F.Zer You're welcome. Anyway to get back to the proof attempt, you need to try proving small cases, and see whether you can generalize it.

@LeadDeveloper: Hello. Do you have a mathematical inquiry?

how are you.

yes, it's really simple one, but I can't get an answer myself.

@LeadDeveloper Well that's actually not mathematics. It's a puzzle, and you should ask on Puzzling SE. It is not much different from find-the-pattern questions, which are also puzzles. The only way of making such questions mathematically meaningful is to stipulate the kind of solutions desired (e.g. polynomial with minimal degree, ...) or to ask for a solution with minimal Kolmogorov complexity. For the latter, you may be interested in this:

@user21820 thanks

@LeadDeveloper Sure. By the way, why did you pick this room instead of any other chat-room on SE?

@user21820 I thought that's simple math.

@LeadDeveloper Ah okay. I hope you understand what I just told you explains why it is actually just a puzzle.

We frequently get this kind of questions on Math SE, so it's normal.

@user21820 can you give me the proper chat room for this ?

@LeadDeveloper Well for real puzzles you should ask on Puzzling SE as I said, and they have their own chat-room. However, for this particular question you posed, I am convinced that there is no reasonable answer, because as I showed you the shortest Python-3 function is so very short that nothing can beat it in simplicity, and yet it doesn't use one of the inputs!

I assume you can read Python since you're from SO.

@user21820 thanks

:59448281 I'm not sure how to use small cases when both the antecedent and consequent have an existential quantifier, like this: "∃k∈ℕ ( P(k) ) ⇒ ∃m∈ℕ ( P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) )". This is my attempt:

I pick a specific P(x) ≡ x > 3

P(4) holds.
P(4) holds, and ∀k ∈ ℕ ( P(k) ⇒ k ≥ 4 )

@F.Zer You're not supposed to pick a specific P.

You are unable to prove contradiction in some subcontext. So you should try to figure out what is wrong in that subcontext. Try small cases there.

If ∃k∈ℕ ( P(k) ):
  Let m ∈ ℕ such that P(m)
  If ¬∃m∈ℕ ( P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) ):
    [try here]

Thank you.

@user21820 Are you allowed to write "If ¬∃m∈ℕ ( P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) ):" ? Isn't "m" used in the previous line ?

Perhaps, I am mistaken.

@F.Zer Sorry, you're not allowed, as per my previous remarks. I copied what you wrote just to display the context structure and forgot to fix the error.

If ∃k∈ℕ ( P(k) ):
  Let a∈ℕ such that P(a).
  If ¬∃m∈ℕ ( P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) ):
    [try here]

Good. Got it.

@user21820 I understood why it isn't allowed. I am still not sure about the intuition behind it. If "m" is already used to refer to something, I think it make sense to say, for example, "If ∀x ∈ ℕ ( x > m ):". I am making a claim involving that specific "m". Does it make sense ?

@F.Zer That makes sense, and is allowed by the syntax rules!

That's a relief :-) And what's the subtle difference between my last (correct) statement, and the wrong one ?

I don't understand.

@user21820 Why is "If ∀x ∈ ℕ ( x > m ):" allowed, but "¬∃m∈ℕ ( P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) )" isn't ?

Oh, m is bound in the second one.

Intuitively, that's exactly the point. But if you really want to see the hard rules act, then you really have to use them and see how they block the invalid things:

You won't have a problem deducing "∀x ∈ ℕ ( x > m ) : bool" in that context you want.

Good. I will try to use them.

@user21820 This is my first attempt at a proof using syntax rules. I am not sure about x > m : bool. Could you give me your opinion ?

...
Let m ∈ ℕ such that m ∈ ℕ
Given x ∈ ℕ:
	[v is a used variable] ⊢ v : term
	[m is a used variable] ⊢ m : term
	m : term
	x > m : bool
∀x ∈ ℕ ( x > m ) : bool

The rule is not something you can copy-paste into the proof itself, just as you don't copy-paste the conditions given in the other deductive rules into your proof.

So your copy-pasted lines (with renaming) are incorrect as they are not part of the proof. The "m : term" is correct because m is a used variable at that point.

Your next line is incorrect because you didn't satisfy the requirements of the last syntax rule:

> t[1],...,t[k] : term ; [Q is a k-input predicate-symbol] ⊢ Q(t[1],...,t[k]) : bool

The last line would be correct once you fix the gap.

@user21820 Second attempt:

...
Let m ∈ ℕ such that m ∈ ℕ
Given x ∈ ℕ:
	x : term
	m : term
	> is a 2-input predicate symbol
	x > m : bool
∀x ∈ ℕ ( x > m ) : bool

@user21820 I have one question: how do you write deduction rules on one line ? Is it like this "A; B ⊢ A ∧ B (∧ Intro)." Each new line is translated as a semicolon.

@F.Zer Again, "> is a 2-input predicate symbol" is an observation about the state of the system at that point, and cannot be written into the proof itself.

Deleting that line, yes, that's precisely how to deduce "∀x ∈ ℕ ( x > m ) : bool".

...
Let m ∈ ℕ such that m ∈ ℕ
Given x ∈ ℕ:
	x : term
	m : term
	x > m : bool
∀x ∈ ℕ ( x > m ) : bool

@F.Zer Yes I used semi-colon to separate lines, so that's indeed how I would express ∧intro. It's not important though, because of course what's important is that you get what the rule means, and there's no need for 100% precision in expressing the rule. There can't be anyway; it would be circular. =)

At the most you can write a program that only accepts correct proofs. That would push the circularity all into the programming language and the compiler and the computer.

@user21820 Hahaha. Ok. The important bit is: I should have A and B deduced in separate lines in the current context. If they are in different contexts, I should use restate (taking into account its restrictions). Then, I can use ∧ intro.

@F.Zer Yup.

Good. I'll try to derive "∃m∈ℕ ( P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) )", and see why it is forbidden.

@user21820 If we suppress the "Let m ∈ ℕ such that m ∈ ℕ", is the rest of the derivation correct ?

...
Let m ∈ ℕ such that m ∈ ℕ
Given m ∈ ℕ: [forbidden]
	m : term
	P(m) : bool
	Given k ∈ ℕ:
		k : term
		P(k) : bool
		k ≥ m : term
		P(k) ⇒ k ≥ m : bool
	∀k∈ℕ ( P(k) ⇒ k≥m ) : bool
	P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) : bool
∃m∈ℕ ( P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) ) : bool

I fixed two errors.

@F.Zer Yes, but there is still one more error: "k ≥ m : term" shouldn't have "term".

Other than that, precisely that is how you can arrive at the judgement (this terminology is common in the literature) that "∃m∈ℕ ( P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) )" is a boolean statement in that context (if "m" was not used).

@user21820 Thank you. I found the rule. Fixing now.

...
Let m ∈ ℕ such that m ∈ ℕ
Given m ∈ ℕ: [forbidden]
	m : term
	P(m) : bool
	Given k ∈ ℕ:
		k : term
		P(k) : bool
		k ≥ m : bool
		P(k) ⇒ k ≥ m : bool
	∀k∈ℕ ( P(k) ⇒ k≥m ) : bool
	P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) : bool
∃m∈ℕ ( P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) ) : bool

Yes!

Good ! I understand how can I arrive at this judgement, if "m" wasn't used. In this case, I can't create the ∀subcontext since "m" is used.

Exactly.

@user21820 So, I will continue with the proof sketch you proposed. Trying small cases there means assigning "m" different values ?

@F.Zer I gave you the context to try in.

I'm not sure what you mean by "assigning m", since there is no used variable "m" in that context.

@user21820 Yes, that's exactly the outline I am working with.

@user21820 Sorry, I meant "a".

@F.Zer If you do that, then you're trying small cases (of the desired theorem) outside that context.

What I meant is that you are given a already. You still can try proving small cases in the context I pointed you to. Earlier on, you tried proving some things, but they were not small cases, and you got nowhere.

This is just a matter of searching wisely for things you can prove. You tried more complicated things first. You should have tried simpler things first.

Your complicated thing you got was "∃k∈ℕ ( P(k) ∧ k<m )". But that is not the simplest thing you can prove in that context. That is what "small cases" means there.

@user21820 I should clarify something. When you say "small cases", do you mean replacing a specific variable with (small) numbers ?

You just clarified.

Yes I was going to say I just did.

"Small cases" is rarely a precise notion.

But you need to try simple things first. "Simple" is not precise either.

@user21820 I should've asked earlier. I thought "small cases" meant using small numbers. That's why I always get nowhere :-)

Simple is good.

@F.Zer No, it's not why you get nowhere. You really didn't use small numbers either.

@user21820 How can I use small numbers ?

Do you want me to tell you?

@user21820 No, I will show you one of my attempts :-)

Ok. =)

@user21820 First attempt at using numbers:

If ∃k∈ℕ ( P(k) ):
	Let a ∈ ℕ such that P(a)
	If ¬∃m∈ℕ ( P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) ):
		If P(4) ∧ ∀k∈ℕ ( P(k) ⇒ k≥4 ) ):
			...
	∃m∈ℕ ( P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) )

If ∃k∈ℕ ( P(k) ):
	Let a ∈ ℕ such that P(a)
	If ¬∃m∈ℕ ( P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) ):
		∀m∈ℕ ( P(m) ⇒ ∃k∈ℕ ( P(k) ∧ k<m ) )
		P(0) ⇒ ∃k∈ℕ ( P(k) ∧ k<0 )
		P(1) ⇒ ∃k∈ℕ ( P(k) ∧ k<1 )
		...
	∃m∈ℕ ( P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) )

Then?

Let me see.

If ∃k∈ℕ ( P(k) ):
	Let a ∈ ℕ such that P(a)
	If ¬∃m∈ℕ ( P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) ):
		∀m∈ℕ ( P(m) ⇒ ∃k∈ℕ ( P(k) ∧ k<m ) )
		P(0) ⇒ ∃k∈ℕ ( P(k) ∧ k<0 )
		P(1) ⇒ ∃k∈ℕ ( P(k) ∧ k<1 )
		If a = 0:
			P(0)
			∃k∈ℕ ( P(k) ∧ k<0 )
			Let b ∈ ℕ  such that P(b) ∧ b < 0
			...
		...
	∃m∈ℕ ( P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) )

@user21820 I continued a bit more.

No no no. You're not aiming for the simplest thing you can prove.

Ok.

If ∃k∈ℕ ( P(k) ):
	Let a ∈ ℕ such that P(a)
	If ¬∃m∈ℕ ( P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) ):
		∀m∈ℕ ( P(m) ⇒ ∃k∈ℕ ( P(k) ∧ k<m ) )
		P(0) ⇒ ∃k∈ℕ ( P(k) ∧ k<0 )
		P(1) ⇒ ∃k∈ℕ ( P(k) ∧ k<1 )
		P(a) ⇒ ∃k∈ℕ ( P(k) ∧ k<a )
		∃k∈ℕ ( P(k) ∧ k<a )
		Let b ∈ ℕ such that P(b) ∧ b < a
		...
	∃m∈ℕ ( P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) )

@user21820 Another attempt.

No. Same reason.

Ok. I will fix my attempt.

@user21820 I have three statements to work with: ∃k ∈ P(k), P(a) and ∀m∈ℕ ( P(m) ⇒ ∃k∈ℕ ( P(k) ∧ k<m ) ). I don't seem to find simpler statements to prove. Since ∀m∈ℕ ( P(m) ⇒ ∃k∈ℕ ( P(k) ∧ k<m ) ) is false, I can't prove anything inside that context.

You had this. But you didn't think through what each of the lines you deduced means. Otherwise you would easily see what simpler things you can prove.

@user21820 Each of those lines mean: whenever I find P holds for a fixed k, there exists some i for which P(i) holds. Does that make sense ?

No!

Read exactly what you wrote. Don't read what you didn't write.

@user21820 If P(0) holds, then there exists some k ∈ ℕ for which P(k) holds and k < 0.

Tell yourself that.

Then?

@user21820 "If P(0) holds, ..." (to myself :-)

@user21820 If P(1) holds, then there exists some k ∈ ℕ for which P(k) holds and k < 1.

I am starting to notice this pattern: ∀i∈ℕ[≥0] ( P(i) ⇒ ∃k∈ℕ ( P(k) ∧ k<i ) ).

You're not thinking about what you're saying...

Anyway, I need to go.

@user21820 I will keep trying. Thank you for your help and have a nice day !

@user21820 This obviously can't be true since k ∈ ℕ ∧ k ≥ 0.

Well, I would first have to prove P(0).

If ∃k∈ℕ ( P(k) ):
	Let a ∈ ℕ such that P(a)
	If ¬∃m∈ℕ ( P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) ):
		∀m∈ℕ ( P(m) ⇒ ∃k∈ℕ ( P(k) ∧ k<m ) )
		P(0) ⇒ ∃k∈ℕ ( P(k) ∧ k<0 )
		P(1) ⇒ ∃k∈ℕ ( P(k) ∧ k<1 )
		If P(0):
			∃k∈ℕ ( P(k) ∧ k<0 )
			Let b ∈ ℕ such that P(b) ∧ b < 0
			b < 0
			⊥
		¬P(0)
		If P(1):
			∃k∈ℕ ( P(k) ∧ k<1 )
			Let c ∈ ℕ such that P(c) ∧ c < 1
			c = 0
			P(0)
			⊥
		¬P(1)
		...

@user21820 Does my latest attempt using small cases make any sense ?