Sequent calculus: $0<1$

Question

Considering the axioms of real closed ordered fields, I'm having trouble proving $0<1$ using Gentzen sequent calculus enriched with the cut rule, i.e, $$\text{Ax}_{\text{RCOF}}\vdash 0<1.$$ Using the trichotomy axiom I was able to obtain the following sequents $$0<1,..., R\rightarrow 0<1$$ $$1<0,..., R\rightarrow 0<1$$ $$0\cong 1,..., R\rightarrow 0<1,$$ where $R$ is some subset of the set of axioms of RCOF and "$...$" are consequences of applying the rules $L\forall$ and $L\vee$. Now, the first sequent is an axiom and. Knowing that $\neg\, 0\cong 1$ belongs to $R$, I apply the rule $L\neg$ to it and I derive the third sequent.

My question: I've tried a couple different approaches but wasn't able to derive the second. Any suggestions? Many thanks in advance.

Answer 1

Wou have Trichotomy: exactly one of $1 < 0$ or $1=0$ or $0 < 1$ holds.

If we use the Law of Order: if $1 < 0$ and $z > 0$, then $1z <0z$, we have $z < 0$, contradicting Trichotomy.

Thus, we have $\lnot (1 < 0)$.

And we have the Non-triviality axiom: $\lnot (1=0)$.

In terms of sequents, we have:

$\text {Ax} \to \lnot (1=0)$, and

$\text {Ax} \to \lnot (1 < 0)$.

Here is the derivation:

1. $(1 < 0) \to (1 < 0)$

2. $[(1=0) \lor (0 < 1)] \to [(1=0) \lor (0 < 1)]$

3. $(1 < 0) \lor [(1=0) \lor (0 < 1)] \to (1 < 0), [(1=0) \lor (0 < 1)]$ --- from 1) and 2) by $(\lor \text L)$, that is:

3. $\text {Ax}\to (1 < 0), [(1=0) \lor (0 < 1)]$

4. $\text {Ax} \to \lnot (1 < 0)$ --- see above

5. $\text {Ax}, (1 < 0) \to$

The next step is to apply Cut to 3) and 5):

6. $\text {Ax} \to (1=0) \lor (0 < 1)$.

Now repeat:

7. $(1=0) \to (1=0)$

8. $(0<1) \to (0<1)$

9. $(1=0) \lor (0<1) \to (1=0),(0<1)$

Cut on 6) and 9):

10. $\text {Ax},\to (1=0),(0<1)$.

11. $\text {Ax}, \lnot (1=0) \to (0<1)$

12. $\text {Ax} \to \lnot (1=0)$ --- see above

13. $\text {Ax} \to (0<1)$ --- from 11) and 12) by Cut.