Proving some properties of real numbers using predicate logic

Question

I am trying to understand how some basic properties of the real numbers can be proved from axioms expressed in predicate logic.

I start by accepting the field axioms of real numbers, in addition to the following axioms

1. $(\forall x,y \in \mathbb R)((x \geq y \wedge y \geq x) \rightarrow x = y)$
2. $(\forall x,y \in \mathbb R)((x \geq y \wedge y \geq z) \rightarrow x \geq z)$
3. $(\forall x,y \in \mathbb R)(x \geq y \vee y \geq x)$
4. $(\forall x,y \in \mathbb R)(x \geq y \rightarrow x + z \geq y + z)$
5. $(\forall x,y \in \mathbb R)((x \geq 0 \wedge y \geq 0) \rightarrow xy \geq 0)$

As a first step, I want to prove that $(x = y) \rightarrow (x + z = y + z)$ using only appropriate manipulations of the axioms above using the laws of predicate logic. It is obviously intuitive to me that this is true, but not entirely obvious how to prove this statement formally.

I start by redefining these statements (leaving out quantifiers for simplicity) in terms of predicates P and Q, as follows:

Let $P(x,y) \equiv x \geq y $ and $Q(x,y) \equiv x = y$

Then, I reformulate these axioms as:

1. $P(x,y) \wedge P(y,x) \rightarrow Q(x,y)$
2. $P(x,y) \wedge P(y,z) \rightarrow P(x,z)$
3. $P(x,y) \vee P(y,x)$
4. $P(x,y) \rightarrow P(x + z,y + z)$
5. $P(x,0) \wedge P(y, 0) \rightarrow P(xy,0)$

I need to prove that $Q(x,y) \rightarrow Q(x+z,y+z)$. I know that I can do this if I can prove that $P(x,y) \wedge P(y,x) \leftrightarrow Q(x,y)$. It is obvious to me that this is true.

I started by trying to prove that $Q(x,y) \rightarrow P(x,y) \wedge P(y,x)$. Once I have this I can prove the equivalence by combining this with 1. I think I need to show somehow that $P(x,y) \vee P(y,x)$ is not sufficient for $Q(x,y)$, because it is my understanding that 1. states that for them both to be true is sufficient for $Q(x,y)$ to be true, but there maybe other cases that make $Q(x,y)$ true. Can anyone help me out here?

Answer 1

Long comment

For First-Order Logic with equality I'll use the Hilbert-style proof system of :

• Herbert Enderton, A Mathematical Introduction to Logic (2nd ed, 2001), page 110-on.

Note. I'll abbreviate with $T$ the set of non-logical axioms for the real numbers.

Thus, $\vdash \alpha$ means that the formula $\alpha$ is derivable in FOL with equality alone, while $T \vdash \alpha$ means that $\alpha$ is a theorem of the theory of real numbers.

Proof

1) $\vdash (∀x,y)(x≥y ∨ y≥x) \to (x≥x ∨ x≥x)$ --- FOL Ax.2

2) $T \vdash (∀x,y)(x≥y ∨ y≥x)$ --- axiom T.3 above

3) $T \vdash (x≥x ∨ x≥x)$ --- from 1) and 2) by modus ponens

4) $\vdash (x≥x ∨ x≥x) \to x≥x$ --- tautology : FOL Ax.1

5) $T \vdash x≥x$ --- from 3) and 4) by mp

6) $\vdash x=y \to (x≥x \to x≥y)$ --- from FOL Ax.6 : $x=y → (α → α')$, where $α$ is atomic and $α'$ is obtained from $α$ by replacing $x$ in zero or more (but not necessarily all) places by $y$. In $T$ the atomic formulae are $t_1 = t_2$ and $t_1 \ge t_2$, because the only two predicate letters are $=$ and $\ge$.

7) $x = y, T \vdash x = y$ --- by definition of deduction : A deduction of $\varphi$ from $\Gamma$ is a finite sequence $α_0,\ldots, α_n$ of formulas such that $α_n$ is $\varphi$ and for each $k ≤ n$, either: (a) $α_k$ is in $\Gamma$ or is a logical axiom, or (b) ...

8) $x=y, T \vdash (x≥x \to x≥y)$ --- from 6) and 7) by mp

9) $x=y, T \vdash x \ge y$ --- from 5) and 8) by mp

10) $T \vdash x=y \to x \ge y$ --- from 9) by Deduction Th

11) $T \vdash (∀x,y)(x=y \to x \ge y)$ --- from 10) by Generalization Th twice: $x$ and $y$ are not free in any axiom in $T$.

Answer 2

I shall just write it down:

$$ x = y \implies x \geq y \implies x+z \geq y+z $$ $$ x=y \implies y=x \implies y \geq x \implies y+z\geq x+z $$ $$ (y+z\geq x+z) \wedge (x+z\geq y+z) \implies x+z=y+z $$

Now we will use your reformulations, with $P(x,y) \equiv x\geq y , Q(x,y) \equiv x=y$, and just translate:

$$ Q(x,y) \implies P(x,y) \implies P(x+z,y+z) $$ $$ Q(x,y) \implies Q(y,x) \implies P(y,x) \implies P(y+z,x+z) $$ $$ P(x+z,y+z)\wedge P(y+z,x+z)\implies Q(x+z,y+z) $$

Is that fine?