@F.Zer Did you justify "z = z'·x" mentally?

You could shorten the proof a bit like this:

...
  If d | a' ∧ d | m':
    If d = 0:
      ...
      ⊥.
    If d ≥ 1:
      ...
      z' > 0.
      ...
      z' ≥ m' = d·z'.
      1 ≥ d.
      d = 1.  [*]

Of course [*] is using ∀x,y∈ℕ ( x ≤ y ≤ x ⇒ x = y ), which certainly you know how to prove. It may be a bit cleaner than to repeat the contradiction argument inside [*].

This SE chat's italic feature has annoyed me sufficiently that I will use ✻ instead of asterisk from now on...

@user21820 Yes, that's right. I used this lemma "∀ x,y,c ∈ ℕ ( c·x = c·y ∧ c > 0 ⇒ x = y ) [lemma]", and since ℤ is an ordered ring containing ℕ, I replaced every occurrence of ℤ by ℕ, and translated the proof. In the proof, I didn't use the axioms "[ring] ∀x∈ℤ ( x+(−x) = 0 )" nor "[ring] ∀x,y∈ℤ ( (x−y)+y = x )", since they are exclusive to ℤ. I obtained "∀ x,y,c ∈ ℤ ( c·x = c·y ∧ c > 0 ⇒ x = y ) [lemma]".

I did a similar thing to obtain "∀ x,y,c ∈ ℚ ( c·x = c·y ∧ c > 0 ⇒ x = y ) [lemma]", since ℚ is an ordered field containing ℤ. Does this make sense ?

@user21820 I like your solution. I will prove that lemma.

∀ x,y,c ∈ ℕ ( c·x ≥ c·y ∧ c > 0 ⇒ x ≥ y ) [lemma]
  Given x,y,c ∈ ℕ:
    If c·x ≥ c·y ∧ c > 0:
      If x < y:
        c·x < c·y
        c·y ≤ c·x < c·y
        c·y < c·y
        ⊥
      x ≥ y
  ∀ x,y,c ∈ ℕ ( c·x ≥ c·y ∧ c > 0 ⇒ x ≥ y )

∀x,y∈ℕ ( x ≤ y ≤ x ⇒ x = y ) [lemma]
  If x ≤ y ≤ x:
    x ≤ y ∧ y ≤ x
    If x < y:
      x < x
      ⊥
      x = y
    If x > y:
      y < y
      ⊥
      x = y
    x = y
  ∀x,y∈ℕ ( x ≤ y ≤ x ⇒ x = y )

@F.Zer No need lol! You could have done it in almost one step!

Multiply by (1/d). It's true that you don't need division, as you noted you can do it entirely in ℕ or ℤ. And if you wonder why things are much simpler when using division than when avoiding it, it's roughly because foundationally it does take some work to construct ℚ to satisfy the given axioms including involving division.

@user21820 Only one step ? Could you show me how ?

Read on.

@user21820 You quoted "I did a similar thing to obtain "∀ x,y,c ∈ ℚ ( c·x = c·y ∧ c > 0 ⇒ x = y ) [lemma]", since ℚ is an ordered field containing ℤ.". My question is: what's the thing I can do in only one step ? The translation from ℤ to ℚ ?

Oh, you mean I don't need the cancellation theorem.

Yes..

Got it :-)

@user21820 I am learning absolute value from Spivak. Can I ask you a question about that function ?

Sure.

@user21820 Great. This is not an exercise from Spivak but one I am wondering about: "Find all numbers x for which |x – 3| < 3"

What's the author asking, from a logic standpoint ? Do I have to prove |x – 3| < 3 ⇒ x < ... ?

@F.Zer No. Equivalence.

And not "x < ...".

Just an equivalence that makes it easy to identify those x.

Same as if the question was "find all x∈ℝ such that x^2 = 4".

So, my proof would go:
  Given x ∈ ℝ:
    If |x–3| < 3:
      If x–3 ≥ 0:
        x ≥ 3
        |x–3| = x–3 [since x–3 ≥ 0]
        x–3 < 3
        x < 6
        x < 6 ∧ x ≥ 3
        ⊥
        [Can I derive any statement by explosion ?]
      ...

@user21820 Oh, just reading your comment. Thank you. How would you do an equivalence in this case where there are multiple cases ?

You have been using explosion so many times already. Why do you doubt it now?

Figure out what my other example wants you to prove first.

@user21820 Well, because then if I assume |x – 3| < 3 is true and reach a contradiction; I could derive for example, |x – 3| < 3 ⇒ x < 6000...

@user21820 Doing it.

"find all x∈ℝ such that x^2 = 4"
  x^2 = 2^2
  √(x^2) = √(2^2)
  |x| = 2
  x = 2 ∨ x = –2

@user21820 Does my solution look good ?

No.

I did not ask you to prove anything.

Mmm. I will try again.

@user21820 The exercise asks me to prove: " x^2 = 4 ⇔ x = 2 ∨ x = –2" ?

I do not know the sentence "x = 2 ∨ x = –2" in advance.

@user21820 That's very interesting. I've seen thousands of times the sentence "find all x..." but I never understood what's supposed to mean.

@F.Zer Yes, if you add quantifiers.

@F.Zer And yes, you do not know the sentence in advance.

That is why such questions are not always well-defined.

@user21820 Good. "∀ x ∈ ℝ ( x^2 = 4 ⇔ x = 2 ∨ x = –2 )"

Generally, people want equivalences that make it easy to identify the 'solutions'.

@user21820 Oh, so the question asks me to prove something I do not know ? So, first I should find the sentence, and then prove it.

@F.Zer Sometimes you can discover that sentence by just deducing from the starting equality or inequality until you reach some conclusion, and then trying to see which possible x that satisfies the conclusion also satisfies the original.

@F.Zer Also, your attempt to solve "x^2 = 4" was not good because you're should not use √ when it's not needed. Instead:

Given x∈ℝ:
  If x^2 = 4:
    (x+2)·(x−2) = 0.
    ...
    x = 2 ∨ x = −2.
  If x = 2 ∨ x = −2:
    ...

@user21820 That's good.

@user21820 I wonder about this sentence: (x+2)·(x−2) = 0. What tools am I allowed to use ?

I see 2 and –2 "fit" there. Although, that's clearly not a justification.

@F.Zer That's what the "..." is there for. It's your job to figure out how to finish the proof.

You only need the field axioms for ℝ.

@user21820 Perfect.

∀ x ∈ ℝ ( x^2 = 4 ⇔ x = 2 ∨ x = –2 )
  Given x ∈ ℝ:
    If x^2 = 4:
      (x+2)·(x−2) = 0
      If ¬(x = 2 ∨ x = –2):
        If x ≠ 2:
          (1/(x−2))·(x+2)·(x−2) = (1/(x−2))·0
          x+2 = 0
          x = –2
          x = 2 ∨ x = –2
          ⊥
        x = 2
        x = 2 ∨ x = –2
      x = 2 ∨ x = –2
    If x = 2 ∨ x = –2:
      If x = 2:
        2^2 = 4
        x^2 = 4
      If x = –2
        (–2)^2 = 4
        x^2 = 4
      x^2 = 4
  ∀ x ∈ ℝ ( x^2 = 4 ⇔ x = 2 ∨ x = –2 )

@user21820 What do you think ?

I should go out a moment and come back. See you !

@F.Zer That's one way to do it, yes.

See you!

@user21820 Thank you ! Is there a way of completing the proof without relying on "If ¬(x = 2 ∨ x = –2):" ?

@F.Zer Your proof is wrong; you need to at least include the original two solutions otherwise you can't even prove it.

@user21820 Oh, I see. Your comment is gold. "x = 2 ∨ x = –2 ∨ x = 6000"

@F.Zer I'm not talking about that.

@F.Zer Yes that can be obtained, but the reverse direction fails.

@user21820 I've understood more about solving equations with you in an hour than a 2 months course in my University. Thank you !

@user21820 Good. Could you teach me how can I solve: "Find all numbers x for which |x – 3| < 3" ?

Unfortunately, it turns out I cannot move a message that was edited from a "move" operation.

@F.Zer Well so you just try proving an implication but try not to add extra solutions along the way.

@user21820 Are you replying to any of my messages ?

@user21820 Ok. I will try.

@F.Zer The move failed on the "I'm not talking ..." message.

@user21820 Got it.

"Find all numbers x for which |x–3| < 3"
  Given x ∈ ℝ:
    If x–3 ≥ 0:
      x ≥ 3
      |x–3| = x–3
      x–3 < 3
      x < 6
      x < 6 ∧ x ≥ 3
      ⊥
      0 < x ≤ 3
    If x–3 ≤ 0:
      x ≤ 3
      –x+3 < 3
      0 < x
      0 < x ≤ 3
    0 < x ≤ 3
  ∀ x ∈ ℝ ( |x–3| < 3 ⇒ 0 < x ≤ 3 )

@user21820 Done.

@user21820 I would have to go out a moment again. Could you please take a look at this one, also ?

"Find all numbers x for which |x–3| < –3"
  Given x ∈ ℝ:
    If x–3 ≥ 0:
      x ≥ 3
      |x–3| = x–3
      x–3 < –3
      x < 0
      x < 0 ∧ x ≥ 3
      ⊥
    If x–3 ≤ 0:
      x ≤ 3
      –x+3 < –3
      6 < x
      x ≤ 3 ∧ x > 6
      ⊥
    ⊥
  ∀ x ∈ ℝ ( |x–3| < –3 ⇒ ⊥ )

See you !

@F.Zer Wrong.

@user21820 Ok. I will check again line by line.

@user21820 I've just checked it again. I missed the assumption. What do you think, now ?

"Find all numbers x for which |x–3| < 3"
  Given x ∈ ℝ:
    If |x–3| < 3:
      If x–3 ≥ 0:
        x ≥ 3
        |x–3| = x–3
        x–3 < 3
        x < 6
        x < 6 ∧ x ≥ 3
        ⊥
        0 < x ≤ 3
      If x–3 ≤ 0:
        x ≤ 3
        |x–3| = –x+3
        –x+3 < 3
        0 < x
        0 < x ≤ 3
      0 < x ≤ 3
  ∀ x ∈ ℝ ( |x–3| < 3 ⇒ 0 < x ≤ 3 )

Look, you're not checking...

@user21820 Why I derived a contradiction from "x < 6 ∧ x ≥ 3" ? I can't believe it. I checked line by line...

Doing it again.

"Find all numbers x for which |x–3| < 3"
  Given x ∈ ℝ:
    If |x–3| < 3:
      If x–3 ≥ 0:
        x ≥ 3
        |x–3| = x–3
        x–3 < 3
        x < 6
        x < 6 ∧ x ≥ 3
        0 < x ≤ 3 ∨ 3 ≤ x < 6
        0 < x < 6
      If x–3 ≤ 0:
        x ≤ 3
        |x–3| = –x+3
        –x+3 < 3
        0 < x
        0 < x ≤ 3
        0 < x ≤ 3 ∨ 3 ≤ x < 6
        0 < x < 6
      0 < x < 6
  ∀ x ∈ ℝ ( |x–3| < 3 ⇒ 0 < x < 6 )

@user21820 Now, it is correct, I think. Is 0 < x ≤ 3 ∨ 3 ≤ x < 6 equivalent to 0 < x < 6 ?

I don't think those are equivalent.

@F.Zer They are in fact equivalent, but you should get the conclusion directly rather than trying to pass through "0 < x ≤ 3 ∨ 3 ≤ x < 6".

@user21820 Could you explain intuitively why they are ?

I felt they were equivalent; however, I didn't know how to justify it.

@user21820 Oh, it's like an union of intervals.

0 < x ≤ 3 ∧ 3 ≤ x < 6 is the intersection. So, only 3 satisfies it.

@user21820 Therefore, I can get the conclusion directly because from 0 < x ≤ 3, I can directly derive 0 < x < 6. I am not "losing" anything.

Everything that is true of 0 < x ≤ 3, will be true of 0 < x < 6.

@F.Zer Yes.

0 < x ≤ 3 < 6.

@user21820 Great.

Similarly for the other case.

@user21820 I am getting the hang of it. I did other exercise.

"Find all numbers x for which x^2 < –3"
  ¬∃x ∈ ℝ ( x^2 < –3 )
    If ∃x ∈ ℝ ( x^2 < –3 ):
      Let a ∈ ℝ such that a^2 < –3
      a ∈ ℝ ⇒ a^2 ≥ 0
      a^2 ≥ 0
      a^2 ≥ 0 ∧ a^2 < –3
      ⊥
    ¬∃x ∈ ℝ ( x^2 < –3 )

@F.Zer Yes, you used the lemma I stated earlier. It's indeed a useful lemma.

@user21820 Where did you state it ? I missed it.

Search doesn't return results.

@F.Zer I found it via "simple facts".

Now that's precisely why I want your text file later.

This stupid SE chat doesn't search symbols.

And anyway a curated text file is better than a meandering conversation.

@user21820 Perfect, found it in my text file. ∀x∈ℝ[≠0] ( x·x > 0 )

@user21820 I found it using the exponentiation symbol. That's why I didn't obtain any results.

Oh yes note that for now "x^k" is only meaningful for fixed natural k.

@user21820 Noted.

It is not trivial to even define x^k for k∈ℕ.

@user21820 Wait. What's the difference between your two latest comments ?

For fixed natural k, you can just treat x^k as x·x·...·x with k terms.

@user21820 Excellent. I've been treating exponentiation symbol as a shorthand

I am not intending to use exponentiation function.

@user21820 Of course, I'll be glad to send it to you, when you prefer.

@F.Zer Indeed. Defining x^k for arbitrary k∈ℕ would require you to actually define the exponentiation function. Which we haven't come to yet. You should read (1) in the post I linked to before, because it's relevant:

@user21820 Yes, that's why I copy everything in my text file.

In particular, when you reach "Don't laugh!" you will realize why indeed many people who don't know proper logic will laugh.

Wrongly laugh.

@user21820 I read (1). Why do you think someone who don't know proper logic will laugh ?

You claimed an f : ℕ -> ℕ exists such that... Then, you can instantiate it. Seems clear enough, I think.

Correct me if I am mistaken, we didn't see how to prove a theorem like the one you mentioned in (1) so far, right ? Well, Intersection had something related, but I am not sure.

@F.Zer They will laugh because they think that theorem is trivial.

Of course, once you have that theorem, you can then use ∃elim, as you said.

@user21820 Ohh. I see.

It's non-trivial to prove such a theorem in ZFC-type foundational systems. The shortest proof is longer than you might expect.

@user21820 And the exponentiation function ? Is it even longer ?

@F.Zer No, what we would prove is something called the recursion theorem, which is a general theorem that says that given any recursive relation on ℕ there exists a function on ℕ that satisfies it.

@user21820 Good. So, the exponentiation function relies on the recursion theorem ?

And then to do any recursive definition, such as the one in (1) or exponentiation with natural exponent, we first construct the desired recursive relation and then apply the recursion theorem.

Got it.

If you want some "light reading", you can just skim through:

@user21820 I realise now that I didn't use your lemma. Yours has a restriction: "∀x∈ℝ[≠0] ( x·x > 0 )"

It's not time for you to attempt to prove the recursion theorem, but maybe you can get an idea of what it feels like.

@user21820 Still not the right time for me to attempt it but interesting to see something I've never seen. Upvoted.

Thanks for sharing.

@user21820 I will now prove the used lemma:

∀x∈ℝ ( x·x ≥ 0 )
  Given x ∈ ℝ:
    If x = 0:
      0·0 = 0
      x·x = 0
      x·x ≥ 0
    If x ≠ 0:
      x·x > 0 [lemma]
      x·x ≥ 0
  ∀x∈ℝ ( x·x ≥ 0 )

Also, do you think the proof below is correct ?

@F.Zer Instead of doing that, you should have proven ∀x∈ℝ ( abs(x) ≥ 0 ) first. And there is a strange "6" loitering around.

@user21820 Good. I will fix.

There is actually an alternative to the approach in the linked post, which you might prefer. I'll do it now for the desired pow : ℝ×ℕ→ℝ. Let pow = { t : t∈(ℝ×ℕ)×ℝ ∧ ∃x∈ℝ ∃k∈ℕ ∃c∈ℕ ∃f∈FN(ℕ[≤c],ℝ) ( f(0)=1 ∧ ∀i∈ℕ[<c] ( f(i+1) = f(i)·x ) ∧ ⟨⟨x,k⟩,f(k)⟩ = t ) }. I claim that pow∈FN(ℝ×ℕ,ℝ). This is the non-trivial part, but if you manage to read and understand what this set means, you will see that it is just the set of all mappings in some function that obeys the recursion up to a finite point.

Induction would be necessary to prove this non-trivial part.

Notation: ℕ[≤c] = { k : k∈ℕ ∧ k ≤ c }. ℕ[<c] = { k : k∈ℕ ∧ k < c }.

@user21820 Is it better, now ?

"Find all numbers x for which |x–3| < –3"
  ∀ x ∈ ℝ ( |x| ≥ 0 ) [lemma]
  Given x ∈ ℝ:
    If |x–3| < –3:
      |x–3| ≥ 0 [lemma]
      ⊥
  ∀ x ∈ ℝ ( |x–3| < –3 ⇒ ⊥ )

∀ x ∈ ℝ ( |x| ≥ 0 ) [lemma]
  Given x ∈ ℝ:
    If x ≥ 0:
      |x| = x ≥ 0
      |x| ≥ 0
    If x < 0:
      |x| = –x
      –x > 0
      |x| > 0
      |x| ≥ 0
  ∀ x ∈ ℝ ( |x| ≥ 0 )

@F.Zer: Fun fact. That very post on recursion was what prompted me to create the Logic chat-room, where we discussed that theorem. And then later of course I created this room for more basic mathematics. So you could say that I'm here largely because of that post!

@F.Zer Yea.

@user21820 So glad you are here. I am very glad that post was created :-)

@user21820 I will try to get a sense of that alternative approach.

@user21820 What's the purpose of this set: "{ k : k∈ℕ ∧ k ≤ c }" ?

@F.Zer It's just to make it easy to read the definition of pow.

Sorry, made a mistake. Let me fix it:

pow = { t : t∈(ℝ×ℕ)×ℝ ∧ ∃x∈ℝ ∃k∈ℕ ∃f∈FN(ℕ[≤k],ℝ) ( f(0)=1 ∧ ∀i∈ℕ[<k] ( f(i+1) = f(i)·x ) ∧ ⟨⟨x,k⟩,f(k)⟩ = t ) }.

@user21820 Good.

@user21820 Whenever I find (doing Spivak) things like "x + 3^x < 4"; do think it is better that I skip them until I can do them rigorously or perhaps I should make handwaving arguments considering it's still chapter 1 ? I am inclined to skip them but I would like your advice.

@F.Zer Where did he define exponentiation?

I thought he did that rigorously at some point. Did he give rules for them before the rigorous definition?

@user21820 I will look at Chapter 1 and reply.

I suppose he did, since you say it's just chapter 1.

Check if he has stated precise axioms for exponentiation. If he has, you can use them (and just label them so I know) if you want me to check your proofs.

@user21820 Nope. No definitions, rules nor axioms for exponentiation. I'm glad to have asked you.

I will continue checking. Perhaps, I missed it.

@user21820 Unfortunately, I can't find them.

Also, he briefly mentioned √x as the positive square root of x; he said this symbol is only defined when x ≥ 0.

@F.Zer: Ok I just grabbed a copy to take a look.

Well you're just at the beginning, haha, of course he hasn't started to do any serious mathematics. =)

That exercise you mention with the "3^x" is in the Prologue in the 4th edition.

I suppose I don't like jumping straight into real analysis without playing with ordered fields like the exercises you're doing right now, so you should just continue what you're doing, skipping things that cannot be done rigorously yet.

@user21820 Perfect. That seems an excellent advice.

@user21820 I wonder why he did define absolute value but didn't exponentiation. How is a student supposed to deal with that symbol ?

Maybe he is assuming some prior pre-calculus knowledge ?

@F.Zer Yes most textbooks assume some prior knowledge. However, he does eventually do it rigorously. All the way at chapter 18 "The Logarithm and Exponential Functions", he says "In algebra, 10^x is usually defined only for rational x, while the definition for irrational x is quietly ignored. A brief review of the definition for rational x will not only explain this omission, but also recall an important principle behind the definition of 10^x.".

He then proceeds via the log-based approach to define exponentiation. That is not my preferred approach, but well it's one way.

@user21820 Thank you. Yes, I am looking at the book and I found that quote.

@user21820 I have a question regarding logic. Do you have any explanation as to why in the proof of "∀ x ∈ ℝ ( |x–3| < –3 ⇒ ⊥ )", I can't derive for example, "∀ x ∈ ℝ ( |x–3| < –3 ⇒ x > 6000 )". As you said, I've previously used explosion many times. What would stop me to conclude x > 6000 ?

Just realised it. The antecedent is never true. So, it doesn't matter. Is that right ?

@F.Zer Why can't you derive what you stated?

@F.Zer Indeed.

@user21820 Validity is like a promise. If the antecedent is true, then the consequent is true. If the antecedent is false, it doesn't matter.

That statement is vacuously true.

And, I didn't do anything forbidden to derive it. In the end, I derived a true sentence using valid inference rules.

Right.

That alone (that the rules are sound) should convince you that it is true.

Good.

As long as you believe all the axioms we have so far, that is.

=)

@user21820 Please, remind me about rule soundness.

@user21820 Haha. Ok.

@F.Zer The deductive rules for FOL are sound, which just means that each rule only allows you to deduce a true sentence (in its context) from previous true sentences (in their contexts).

It's a bit cumbersome to actually state it properly for Fitch-style proofs, but you should get what I mean.

@user21820 Excellent. Got it.

@user21820 Why do you make a distinction between "in its context" and "in their contexts" ? Shouldn't "in its context" already include every governing context ?

@F.Zer The other true sentences may not be in the same context. Most rules work in the same context, but a few rules cross contexts, such as ⇒sub, ∀sub, ⇒intro, ∀intro, ∃elim. I include ∃elim because after that step you have one more variable in the subsequent part of the current context.

For example:

Given a,b,c,d ∈ ℕ:
  If 0 < a < b ∧ d > 0:
    If a·c ≥ b·d:
      a < b
      a < b ∧ 0 < d
      ∀ x,y,z ∈ ℕ ( x < y ⇒ x·z < y·z )
      a·d < b·d
      b·d ≤ a·c
      a·d < b·d ≤ a·c
      ∀x,y,z∈ℕ ( x<y≤z ⇒ x<z ) [lemma]
      a·d < a·c
      ∀k,x,y∈ℕ ( k·x > k·y ⇒ x > y ) [lemma]
      c > d

@user21820 For example, I derived the true sentence "a < b" in its context, and I assume it is "a·c ≥ b·d" but also "0 < a < b ∧ d > 0" and finally "Given a,b,c,d ∈ ℕ" are also in its context. Is that right ?

@F.Zer Yes.

For example look at ∀intro.

Given x∈S:
  ...
  Q(x).
∀x∈S ( Q(x) ).

In the context where you are given some x∈S, you manage to deduce Q(x).

The rule says that just outside that context, you can deduce ∀x∈S ( Q(x) ).

The rule is sound, but if you're not convinced you need to think through what you're allowed to do in the "...". Basically, you could not make any assumption about x except x∈S. So you could pick any x∈S at the "given" header and whatever you deduced in there is true for that x.

@user21820 Great example. It clicked, now. However, I am still not sure why you included ∃elim in that list.

@user21820 Perfect.

You said: "I include ∃elim because after that step you have one more variable in the subsequent part of the current context".

Not sure I get that.

Before that step, the fresh variable you used in that step is not used. After that step, that variable is now used. So the context has changed a bit.

That's why I said "It's a bit cumbersome ...".

@user21820 Got it.

@user21820 Thank you for all you help ! I should go, now. Have a nice day and see you !

See you!

alright, well this wasn't as easy as I first thought, but I think this proves there exists a surjective function between N and Z within the system using the function-type axiom

Prove there exists a surjective function from N to Z.

1 p ∈ F <-> (∃n ∈ N)(∃z ∈ Z): p = ⟨n,z⟩ ^ φ(n,z)
2 F := {⟨x,y⟩:x∈N ^ y ∈ Z ^ φ(x,y)} \\shorthand for 1
3 φ(x,y) := ∃z∈N [(x=2z ^ y=z) v (x=2z+1 ^ y=-z)]

\\Prove F is a function:
4 N x Z = {x: n ∈ N ^ z ∈ Z ^ x = ⟨n, z⟩}
5 ∴F ⊆ N x Z \\ since φ(n,z) is just a restriction on which n,z satisfy ⟨n,z⟩
6 ∴F ∈ P(N x Z)

7 If ⟨x',y_1⟩, ⟨x', y_2⟩ ∈ F:
8	φ(x', y_1) ^ φ(x', y_2)
9	z_1 := z_1 ∈ N ^ (x'=2z_1 ^ y_1=z_1) v (x'=2z_1 +1 ^ y_1=-z_1)	\\from φ's definition

it's slightly informal at times to make it easier to read

I forgot: (14) is from (PA1)

but even though I'm able to do the proof, it is baffling to me why even at infinity, I can still find a desired pair ⟨n,z⟩ ∈ F. I think it is ∀intro that is surprising, even if I see it in all proof systems. Somehow, we can be given any x in the universe of discourse we want

and somehow, the universe of discourse is infinite

maybe it is induction that is bothering me, i don't know, but hopefully the proof works

of course, how is this almost not surprising: I found a post of yours that discusses this hehe math.stackexchange.com/questions/2371760/…