Natural Language proof of additive inverse

[Tomp]

I have been given a question by my tutor to try out for our next class

Using the axioms for addition of numbers give a natural language proof that the additive inverse of a number is unique, that is prove:
∀x∀y∀z (x + y = 0) ^ (x + z = 0) → (y = z)

I am new at writing proofs!

My attempt
1. x + y = 0 premis
2. x + (-x) +y = (-x)
3. 0 + y = -x
4. y = -x
5. x + z = 0 premis
6. z = -x
7. (y = -x) ^ (z = -x) --> x = z transivity axiom
therefore (x + y = 0) ^ (x + z = 0) → (y = z) by ded principle line 4, 6

I think this right, but as it's one of my first proofs I am unsure if this is enough...

 

[mfb]

2. x + (-x) +y = (-x)

What is "-x"? At this point, you do not know that -x is unique.
You see this problem in (7).

As indication that something has to be wrong: Your attempt could be used in systems where the inverse is not unique as well - where it has to fail.

 

[Tomp]

What is "-x"? At this point, you do not know that -x is unique.
You see this problem in (7).

As indication that something has to be wrong: Your attempt could be used in systems where the inverse is not unique as well - where it has to fail.

Would I have to indtroduce something like
(there exists) w such that x + w = 0

So,
1. x + y = 0 premis
2. ∃w x + w = 0
3. x + y + w = w commutative axiom
4. y + 0 = w
5. y = w
6. x + z = 0 premis
7. z = w
8. (y = w) ^ (z = w) --> x = z transivity axiom
therefore (x + y = 0) ^ (x + z = 0) → (y = z) by ded principle line 5, 7

 

[Stephen Tashi]

I have been given a question by my tutor to try out for our next class

Using the axioms for addition of numbers give a natural language proof that the additive inverse of a number is unique, that is prove:
∀x∀y∀z (x + y = 0) ^ (x + z = 0) → (y = z)

I am new at writing proofs!

My attempt
1. x + y = 0 premis

There are different way to state axioms for the "the numbers", so it's not possible to evaluate if you used them. (You didn't say how any axioms justified your steps. You didn't even say which numbers you are dealing with - the integers? the reals? )

I don't know how your tutor uses the phrase "natural language proof", but most people use it to mean a proof that is written in the style that one would write an essay in an English class. It wouldn't consist of steps using only symbolic expressions.

To write your proof (in natural language or otherwise), you must first understand a principle of logic that very subtle. You are trying to proof a statement that has the quantification "for each x and for each y...". You begin by writing a statement that involves symbols like "x", "y". However the statement that you wrote has no quantifier. So, symbolically, it isn't clear whether you mean your statement to be quantified by "for each x, for each y" or whether you mean "x" to be a particular number, quantified by "there exists".

The way proofs are written in natural language, if we wish to prove something "for each number x", we often begin by saying "Let x be a number" or "Let x be any number". Then we write the proof as if "x" represents one particular number. Although we treat "x" as a particular number in the proof, if do not assume it has any special properties not possessed by other numbers, we are allowed to conclude at the end that we have done a proof "for each number x". In symbolic logic, this principle of logic is often called "universal generalization". There may be other terms for it. In your symbolic proof, you appear to use this principle instinctively. Just be aware that this is what you are doing.

In speaking of math in natural language, people often leave out the quantifier "for each". For example if we hear someone declare "if x is greater than 1 then x squared is greater than 1", we tend to take this as a claim about "for each x, ..." rather than a claim about "there exists an x such that...".

 

[Tomp]

Thanks for your detailed response.

My tutor hasn't been incredibly clear about what he means by a "nutural language proof", but based on the examples provided by my lecturer, they indicate the idea of a very compressed proof (in steps) where he assumes the axioms.

For these reasons, I will have to clarify this with my tutor tomorrow as it seems "natural proof" is quite ambiguous.