@F.Zer I'm well, how about you? Though it seems there is at least one troll who is feeling unwell, because they did the only bad thing they could do to my activity page. =P
@F.Zer 4 downvotes, because it's needed to cover up all the upvotes in the activity page. Kind of funny also that they targeted the same post as before even after CMs reversed some votes earlier this year.
@user21820 Hahaha. No, don't start linking to it yet :-)
@user21820 I mean, only the person who has the link will find it. If you want to be extra secure, I could make it private for the time being and only you will have access.
@user21820 Here is my revised version of the new PA1. What do you think ?
@F.Zer Well line 9 doesn't make sense in that proof. The point was that you're supposed to squeeze line 8 to get "≥" inequalities, which should be there instead of line 9, because they are used in lines 10 and 11.
Also, you should have expanded 4·k ≥ ... ≥ 3·k+1 just to be clear.
Line 12 also doesn't make sense. Looks like you forgot about it.
And the lemmas are missing. I also noticed that there is a kind of mess in the Lemmas sibling folder...
@F.Zer Hmm, technically it's wrong, because the ∃elim rule requires the variable to be fresh (does not appear in any previous statement). Intuitively, it's not wrong, because the "Let a" in the preceding case cannot interfere once you exit that case. We talked about this before, but a more lenient rule is much harder to formulate.
@F.Zer Well in the system I gave, I actually defined "fresh variable" to mean "variable that does not appear in any previous statement", not just in surrounding contexts. In practice, this only poses a problem if in your proof you do many ∃elim steps, which is not typical unless you are writing a gigantic proof without lemmas. I think we can relax that a bit to "variable that does not appear in any statement in the surrounding contexts or in subcontexts of the current context".
If you do prefer the more lenient version, I'll check again to see whether it works.
@user21820 Yes, I do remember about that discussion, now. Fixed it. However, I'll appreciate if you could take a look at a more lenient version, since my programming background makes a bit difficult to forget that habit.
@user21820 I already filled the "..." here "4·k ≥ ... ≥ 3·k+1". Are you saying I missed a step ?
Given a∈ℕ
If ∀i∈ℕ(i<a ⇒ Q(i))
If a>1
If ¬∃q∈ℕ ( 1 < q < a ∧ q | a )
a | a
a > 1
a > 1 ∧ a | a ∧ ¬∃q∈ℕ ( 1 < q < a ∧ q | a )
∃p∈ℕ ( p > 1 ∧ p | a ∧ ¬∃q∈ℕ ( 1 < q < p ∧ q | p )
If ∃q∈ℕ ( 1 < q < a ∧ q | a )
Let c ∈ ℕ such that 1 < c < a ∧ c | a
Let d ∈ ℕ such that a = cd
∀i∈ℕ(i<a ⇒ Q(i))
c<a ⇒ Q(c)
c<a
Q(c)
c > 1 ⇒ ∃p∈ℕ ( p > 1 ∧ p | c ∧ ¬∃q∈ℕ ( 1 < q < p ∧ q | p ) )
c > 1
∃p∈ℕ ( p > 1 ∧ p | c ∧ ¬∃q∈ℕ ( 1 < q < p ∧ q | p ) )
e > 1 ∧ e | c ∧ ¬∃q∈ℕ ( 1 < q < e ∧ q | e )
@user21820 attempt at proving PA3 using Strong induction.
Given a ∈ ℕ
\\Define P(n) : n>1 ∧ n | a
If a>1
a | a
a > 1 ∧ a | a
∃p ∈ ℕ (p > 1 ∧ p | a)
∃p ∈ ℕ (P(p))
∃p ∈ ℕ ( P(p) ) ⇒ ∃p∈ℕ ( P(p) ∧ ∀q∈ℕ ( P(q) ⇒ q≥p )) [well-ordering]
∃p∈ℕ ( P(p) ∧ ∀q∈ℕ ( P(k) ⇒ q≥p ))
P(h) ∧ ∀k∈ℕ ( P(q) ⇒ q≥h ))
If ¬∃q ∈ ℕ (1<q<h ∧ q|h)
¬∃q ∈ ℕ (1<q<h ∧ q|h)
If ∃q ∈ ℕ (1<q<h ∧ q|h)
Let s ∈ ℕ such that 1<s<h ∧ s|h
s | h ∧ h | a
s | a
s < a
a ≤ s
s < s
⊥
¬∃q ∈ ℕ (1<q<h ∧ q|h)
¬∃q ∈ ℕ (1<q<h ∧ q|h)
P(h) ∧ ¬∃q ∈ ℕ (1<q<h ∧ q|h)
@user21820 attempt at proving PA3 using well ordering.
@user21820 Sorry for that. I forgot to at "let" to that. I guess it was a mental jump .
@Prithubiswas Just a comment while I'm halfway through. Immediately after "∃p ∈ ℕ (P(p))" you can write "Let h∈ℕ such that ∃h∈ℕ ( P(h) ∧ ∀q∈ℕ ( P(q) ⇒ q≥h )). [well-ordering]" and we all know what it means.
Given a,b,c ∈ ℕ
If a | b and b | c
Let d ∈ ℕ such that b=ad
Let e ∈ ℕ such that c=be
c = be = ade
a | ade
a | c
a | b ∧ b | c ⇒ a | c
∀x,y,z( x | y ∧ y | z ⇒ x | z )
@Prithubiswas The second half is funny. You didn't need the whole "If ¬∃q ∈ ℕ (1<q<h ∧ q|h)" case at all! Once you get contradiction in the second case, you just need ¬intro to finish.
@user21820 Yes, but the modification "variable that does not appear in any statement in the surrounding contexts or in subcontexts of the current context" requires more careful checking but it's still correct, right ? You are pointing out that the downside of relaxing the strict rule is that we would have to do more careful checking. Tell me if this is incorrect. Also, you said that the new rule prevented you from doing a wrong proof in your last example.
@F.Zer What you write here seems correct. But your initial comment is wrong. I believe it's because you misunderstand the meaning of the word "instead". Your statement means "Not only do we need to check every preceding line, we also need to check every sub-context of surrounding contexts.".
Also there is a second misunderstanding: When I wrote "I do believe what I quoted from myself is correct, but it needs some checking.", the "it" refers to "what I quoted from myself", not "the process of following the rule". I meant that I haven't checked well enough to be sure that the lenient rule is correct.
It does prevent the wrong proof in the last example, but I've to check to be sure it prevents all wrong proofs.
@user21820 Oh, I didn't mean that. I had an incorrect understanding, then. For me, if we "check every preceding line" implies that "we checked every sub-context of surrounding contexts". Could you tell me how that can fail ?
@user21820 "Check every preceding line" is stronger than "check every sub-context of surrounding contexts". In "check every preceding line", I mean, we are checking everything, right ?
@F.Zer Well in the system I gave, I actually defined "fresh variable" to mean "variable that does not appear in any previous statement", not just in surrounding contexts. In practice, this only poses a problem if in your proof you do many ∃elim steps, which is not typical unless you are writing a gigantic proof without lemmas. I think we can relax that a bit to "variable that does not appear in any statement in the surrounding contexts or in subcontexts of the current context".
Read the linked conversation for some examples besides the one I gave here.
"I actually defined "fresh variable" to mean "variable that does not appear in any previous statement", not just in surrounding contexts". Well, I assumed the words "not just" implied that you were checking more things in the strict rule. That's why I said what I said.
As I said, I understand what you're thinking, but you have to remember that unlike programming you can deduce statements based on statements inside subcontexts, so things can 'escape' local scope as you can see from the last example I gave. In the meantime, you should use the strict rule. If you come across any proof where it seems unnatural or painful to have the strict rule, tell me. If there are sufficiently many of them, then it would justify getting the lenient rule right.
In contrast, the stricter rule is obviously correct because the variable literally has never been seen before so it doesn't matter what variables can escape from preceding subcontexts.
Incidentally, in an informal mathematics proof, which would be in paragraph form, we would actually typically use fresh variables following the strict rule, so that readers do not get confused.
It's only when it's in Fitch-style that it becomes like programming where it would be nice to have local scoping.
Anyway, probably best to stick to strict now. Converting strict-to-lenient is easy (all proofs remain valid), but lenient-to-strict would require checking every single proof again, in the absence of a proof assistant program.
