math.stackexchange.com/a/4192594/688539 @user21820 does my answer sound logically sound? There are ofc some parts needed to be made rigorous but I am bit nervous since the solution seemed 'too easy'

nevermind

@F.Zer If you simply write down the definition of x−1 in terms of the language of PA, which is (0,1,+,·,<), you will see that it is given by one of the axioms of PA−.

@user21820 Thank you for the advice ! I'll do it.

Seems like an interesting puzzle. How to write the definition without using the symbol "-".

@user21820 Could you tell me if this is a hard problem ? I'll give my best to figure it out.

Perhaps, best to ask first: what do you mean by "write down the definition of x-1" ? Could you give me another (unrelated) definition to write so I can practice ?

Not wise to spend time working without clarifying what I am being asked to do, I think.

@F.Zer I don't understand your question. Surely you know what subtraction means. Explain that, using only the language of PA.

In ∀xP(x) → ∀yP(y) is it possible to have different domains in the LHS and RHS?

@avistein No, because "∀" would be meaningless if we didn't give it a sensible interpretation.

@user21820 Now that you say it, I am not sure I know what subtraction means (from a formal point of view). I do know how to do arithmetic operations with it, though.

@F.Zer Uhh... that's... impossible. When you do subtraction in real life, you have a certain question in mind, for which the answer is found by subtraction.

I can't tell you more because the answer is just one single step (as I said, just one axiom of PA−).

@user21820 Sure. I understand.

@avistein If you want to have quantifiers over different ranges, then what you want are restricted quantifiers, such as "∀x∈S ( ... )".

@F.Zer So the point is. Why perform subtraction if it is meaningless? If it means something, what is that meaning?

@user21820 If I have x - 3 = 1, I know for sure x is 4.

@user21820 That's a great point ! I will think what is that meaning.

@F.Zer That's not relevant.

Look, just go and find real-life use of subtraction, and ask yourself why on earth you want to do subtraction.

Ok. I see that isn't the subtraction in real life you had in mind ?

@user21820 so, I can have ∀x∈N P(x) → ∀y∈R P(y) ?

@user21820 I'll do it.

@avistein Yes, if you wish. And if you mean ℕ (naturals) and ℝ (reals) then such an implication will be non-trivial (maybe true for some non-trivial reason, but false for general P).

@user21820 Yes, I was not asking about the validity of the FOL formula. I was wondering if I am allowed to have different domains for the same predicate. Anyways, I got my answer. Thanks!

@user21820 Suppose I have 600 USD, and now I have to pay 200 USD in taxes. I am left with 400 USD. What's the role of subtraction, there ? Calculating the final amount after paying taxes. Is that it ?

@F.Zer That is an example, but fails to explain why you are motivated to do the subtraction. In particular, what does "left with" and "final amount" mean?

@user21820 Interesting. Why am I motivated to do the subtraction ? For the sake of removing a quantity from another one.

Not sure "removing a quantity" makes sense.

@avistein Note that whether you can use restricted quantification in your foundational system or not is a matter of design. In my preferred formal system, I have restricted quantifiers. In formal systems more common in textbooks, they do not. As a result, in the more common systems you cannot use restricted quantifiers unless you have at least a predicate-symbol for each of the desired quantifier ranges. For example, "∀x∈S ( Q(x) )" in my system would translate to "∀x ( S'(x) ⇒ Q(x) )".

Here S' is a predicate-symbol that represents the domain S.

It is bad in my opinion because "∃x∈S ( Q(x) )" would translate to "∃x ( S'(x) ∧ Q(x) )", which confounds the symmetry in my system in the identity ¬∀x∈S ( Q(x) ) ≡ ∃x∈S ( ¬Q(x) ).

From a strength point of view, both variants of FOL are equivalent, because we can translate from one to the other (as I have just shown). But from a practical point of view, I prefer having restricted quantifiers.

@F.Zer What does "remove" mean??

@user21820 Mmm...take something away.

@user21820 By the way, that explanation clarifies a question I had a while ago while reading a book. Thank you.

@F.Zer You're going in circles now. What is 3−1, and WHY?

Do not use "take" or "remove" or "left" or any word of that sort.

@user21820 3 - 1 equals 2 because 2 + 1 = 3.

@F.Zer So why couldn't you answer the exact same question about x−1?

That's what stumps me. You clearly know the basics, but you are unaware of it.

You defined 3−1 in the language of PA, but failed to do so for x−1.

Do you get what I mean?

@user21820 I told you before. I've been trained to repeat mechanically instead of thinking. Every classmate I know has this exact problem.

@user21820 Perfectly. Thank you.

@F.Zer So which axiom of PA− is it?

@user21820 The third one (starting from the bottom).

@F.Zer That's right. So remember, whenever you can subtract and stay within ℕ, you can do it within PA−, because if x = x then of course x = x+0, and if x > y then using that axiom we can obtain the result of subtraction.

It would be convenient for you to first prove ∀x,y∈ℕ ( x≤y ⇒ ∃z∈ℕ ( x+z = y ) ), just so that you can use it next time for subtraction.

@F.Zer And so for the original problem, you just need to prove x ≥ 1 so that you can construct x−1 and finish what you want to get.

@user21820 1 < x ⇒ ∃ z ∈ ℕ ( 1 + z = x )

That's the specific instance of that axiom, right ?

x can't be zero.

@F.Zer That's an instance, but it's not enough; read my other comments first.

@user21820 What do you mean by "if x = x then of course x = x+0". I am not sure get what you are after.

@F.Zer If x = x then x−x stays within ℕ but cannot be obtained from that axiom.

@user21820 Perfect.

Sorry I should have written "If x = y then x−y ...".

Not sure why I wrote a dumb "If x = x" ...

@user21820 Of, so ∀x,y∈ℕ ( x≤y ⇒ ∃z∈ℕ ( x+z = y ) ) covers both cases.

Yes.

Got it. I will prove it.

∀x,y∈ℕ ( x≤y ⇒ ∃z∈ℕ ( x+z = y ) ) [Lemma]
  Given x, y ∈ ℕ:
    If x ≤ y:
      If x < y:
        ∀x,y∈ℕ ( x < y ⇒ ∃z∈ℕ ( x+z = y ) )
        ∃z∈ℕ ( x+z = y )
      If x = y:
        ∀ x ∈ ℕ ( x + 0 = x )
        x + 0 = x
        x + 0 = y
        ∃z∈ℕ ( x+z = y )
      ∃z∈ℕ ( x+z = y )
  ∀x,y∈ℕ ( x≤y ⇒ ∃z∈ℕ ( x+z = y ) )

@user21820 Here is the proof.

Yeap.

Good. I'll continue working on (PA5).

@user21820 Yes, I got your point. I have actually seen the last one you mentioned in my textbook. On the same note, can I safely assume that in ∃y∀xP(y, x) → ∀y∃xP(x, y), the first variable in P(a, b) is going to take values from the same domain in both LHS and RHS, and similarly for the second variable?

@avistein Why do you distinguish the variables? All unrestricted quantifiers range over the entire world.

If your book says it ranges over a specific domain, than your book is wrong. You can interpret an FOL sentence in a given structure, and in that interpretation the quantifier ranges over the domain of that structure. However, that's part of the interpretation. Neither the unrestricted quantifier itself nor the quantified variables come with a domain.

If r ≥ k:
  If ¬ (x ≥ 1):
    x = 0
    k·0 ≥ m
    ∀ x ∈ ℕ ( x·0 = 0 ) [Lemma]
    0 ≥ m
    m > 1
    0 > 1
    ⊥
  x ≥ 1
  ∀x,y∈ℕ ( x≤y ⇒ ∃z∈ℕ ( x+z = y ) ) [Lemma]
  1≤x ⇒ ∃z∈ℕ ( 1+z = x )
  ∃z∈ℕ ( 1+z = x )
  Let x' such that 1 + x' = x
  x' < x
  k·(1 + x') ≥ m
  k + k · x' ≥ m
  ...

@user21820, I continued with the proof.