Proving some properties of real numbers using predicate logic

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?

• You are basically attempting to prove that $a = b \vdash f(a) = f(b)$. You shouldn't need to appeal to the axioms to prove this, it should be a basic theorem in your predicate logic. That's effectively what it means to be a function. – DanielV Sep 10 '16 at 5:00
• @DanielV Perhaps you are right and I should be focusing on learning more about predicate logic theorems so that stuff like this is easier to prove. My understanding is that functions are built from more primitive predicate logic constructs. I guess I just wanted to see if I could prove this using only atomic predicates, logical connectives and quantifiers, rather than using other derived theorems of predicate logic. – esotechnica Sep 10 '16 at 5:46

Long comment

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

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$.

• Posting this question has illuminated how much I don't know about first order logic. I didn't realise that there were other axioms that were required to prove this, so thanks for the insight! – esotechnica Sep 10 '16 at 10:10
• As per previous comment, the result is "obvious", thus we can prove it. But to do so "formally", we need some practice with proof systems. The more "natural" one is Natural Deduction. – Mauro ALLEGRANZA Sep 10 '16 at 10:17

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?

• Yes, this is the proof that I originally had until I realised I couldn't justify the step $x = y \rightarrow x \geq y$. How can you assume this? Btw, I know this is true for obvious reasons, but could not derive it from the axioms. – esotechnica Sep 10 '16 at 5:35
• I thought this was part of the real number axioms. – астон вілла олоф мэллбэрг Sep 10 '16 at 5:38
• Not to my knowledge, I got my base axioms from the Wikipedia article on real numbers, which say that all you need are the field axioms for $\times$ and + and the five axioms listed above. Oh, and completeness, but I don't really care about that in this context. – esotechnica Sep 10 '16 at 5:49
• See, the problem is that I don't know how to say that $x=y$ implies something. It must imply something, by definition of $=$, but then I don't know how this "=" is defined, or if it even is, in first order logic. My apologies on this . However, I was invited to assume that $=$ implies $\geq$, just because I couldn't think of anything else it implies. – астон вілла олоф мэллбэрг Sep 10 '16 at 5:53
• No problem. I don't have enough knowledge on this subject to answer these questions. It seems I need to develop a deeper understanding of first order logic perhaps? – esotechnica Sep 10 '16 at 6:10