## Stream: general

### Topic: What is this Real-like number system

#### Locria Cyber (Aug 16 2022 at 12:06):

axiom R : Type

class Inv (α : Type u) where
inv : α → α

prefix:100 "/"    => Inv.inv

namespace R

axiom R0 : R
axiom R1 : R

noncomputable
instance : OfNat R 0 where
ofNat := R0

noncomputable
instance : OfNat R 1 where
ofNat := R1

axiom opp : R -> R
axiom plus : R -> R -> R

noncomputable
instance : Neg R where
neg := opp

noncomputable

axiom inv : R -> R
axiom mult : R -> R -> R

noncomputable
instance : Inv R where
inv := inv

noncomputable
instance : Mul R where
mul := mult

axiom plus_opp_r (r: R) : r + -r = 0
axiom mult_inv_r (r: R) : r * /r = 1

axiom plus_comm (a: R) (b: R) : a + b = b + a
axiom mult_comm (a: R) (b: R) : a * b = b * a

axiom lt : R -> R -> Prop

noncomputable
instance : LT R where
lt := lt

axiom lt_is_not_eq (a: R) (b: R) : ¬ (lt a b ∧ a = b)
axiom lt_trans (a: R) (b: R) (c: R) : a < b ∧ b < c -> a < c
axiom r0_lt_1 : lt 0 1

end R


#### Locria Cyber (Aug 16 2022 at 12:08):

This is not quite Real numbers, since 0 has properly defined inverse

#### Locria Cyber (Aug 16 2022 at 12:09):

Someone must have given this number system a name before.

#### Yaël Dillies (Aug 16 2022 at 12:10):

Actually it's more like field + linear_order + 0 < 1, because you're not requiring any monotonicity on + and *.

#### Jason Rute (Aug 16 2022 at 12:29):

If you add associativity of addition and multiplication and distributivity (edit: and that 0 and 1 are identities), then you would have a field where 0 has an inverse but 0 != 1. That would be a contradiction. But since you have no rules on how plus and times play together, I guess you could just have two groups on the same set that have little to do with each other. For example your + could be the usual addition on the reals. Then x * y could be shifted plus, namely (x - 1) + (y -1) + 1 or something like that.

#### Jason Rute (Aug 16 2022 at 12:35):

If you haven’t already, I think you would enjoy learning abstract algebra.

#### Jason Rute (Aug 16 2022 at 12:51):

Another trivial solution: x + y is always 0 (and -x could be anything including just x) and x * y is always 1. This works because you don’t even assume 0 and 1 are identities.

Last updated: Aug 03 2023 at 10:10 UTC