Implementing mathematical theory of arithmetic in Haskell via Curry-Howard correspondence

Question

I have to ask for forgiveness in advance if the whole question doesn't make a lot of sense, but unfortunately, I have no better intuition as of right now and this seems like the best starting point I could come up with.

I'm reading Tarski's book "Introduction to Logic: and to the Methodology of Deductive Sciences", I'm on Part VII Chapter 43 "Primitive terms of the theory under construction; axioms concerning fundamental relations among numbers". It begins by laying out an elementary mathematical theory of arithmetic of real numbers.

The primitive terms are:

• real number (denoted as variables like x, y)
• is less than (<)
• is greater than (>)
• sum (+)
• N meaning "the set of all numbers". Thus, an expression "x is a number" would be written as x ∈ N
• is not less than (≮)
• is not greater than (≯)

Among the axioms of the theory under consideration, two groups may be distinguished. The axioms of the first group express fundamental properties of the relations less than and greater than, whereas those of the second are primarily concerned with addition. For the time being, we shall consider the first group only; it consists, altogether, of five statements:

• AXIOM 1. For any numbers x and y (e.g., for arbitrary elements of the set N) we have: x = y or x < y or x > y
• AXIOM 2. If x < y, then y ≮ x
• AXIOM 3. If x > y, then y ≯ x
• AXIOM 4. If x < y and y < z, then x < z
• AXIOM 5. If x > y and y > z, then x > z

Our next task consists in the derivation of a number of theorems from the axioms adopted by us:

• THEOREM 1. No number is smaller than itself x ≮ x
• THEOREM 2. No number is greater than itself: x ≯ x

Now I have to stop and finally explain my intentions. I've heard many times about a so-called "Curry–Howard–Lambek correspondence", and it made sense whenever I've read examples of it. I am also not comfortable with manually writing out the reasoning to prove the theorems, I'd like the machinery of going through reasoning steps to be checked by a computer for me.

So, I tried to encode the terms, axioms and potentially theorems (got stuck earlier) in Haskell, but I failed in many ways. I won't show you all the examples of what I did, but here's the most naive approach of encoding propositions as types and their proofs as programs:

data Nats
  = NatX
  | NatY
  | NatZ

x :: Nats
x = NatX

data OpGt =
  OpGt Nats
       Nats

data OpLt =
  OpLt Nats
       Nats

data OpEq =
  OpEq Nats
       Nats

data OpNotLt =
  OpNotLt Nats
          Nats

data OpNotGt =
  OpNotGt Nats
          Nats

data Ax1Res
  = Ax1ResLt OpLt
  | Ax1ResGt OpGt
  | Ax1ResEq OpEq

-- how to implement best?
ax1 :: Nats -> Nats -> Ax1Res
ax1 = undefined

-- this doesn't describe the x and y in the type
ax2 :: OpLt -> OpNotGt
ax2 = undefined

This piece of code brings more questions than it gives answers:

• should axioms be implemented or kept as unimplemented functions which we just assume to exist?
• how do I limit the implementation of my functions to only rely on available theorems and axioms if I can construct basically any term? Should I hide the constructors?
• types should obviously contain variables like x and y, I tried that in other approaches but that gets even hairier

My questions are:

• what would be a proper implementation of such proofs in Haskell?
• what materials should I read in order to make a proper implementation myself and understand the topic better?

I hope the vagueness and my level of ignorance in the question will not put you off from answering it. Thank you!