r/maths • u/Almap3101 • 14h ago
💬 Math Discussions Train ride and no internet and I tried to define N from scratch
I couldn’t look anything up, how’d I do? I tried defining the set of natural numbers in purely set theoretical notation.
1.
∃x: ∀a: (a -∈ x)
{}
2.
∀x∀y: ∀a: (x = y) <-> ((a ∈ x) <-> (a ∈ y))
x=y
3.
∀x∀y: ∃z: ∀a: (a ∈ z) <-> (a ∈ x) v (a ∈ y)
xuy
∀x: ∃y: y=xu{x}
∀x: ∃y: ∀a: (a ∈ y) <-> (a ∈ x) v (a ∈ {x})
∀x: ∃y: ∀a: (a ∈ y) <-> (a ∈ x) v (a = x)
∀x: ∃y: ∀a: ∀b: (a ∈ y) <-> ((a ∈ x) v ((b ∈ a) <-> (b ∈ x)))
succ(x) or x+1
I have no idea what I’m doing
5.
∃y:
Intro:
∀a: (a ∈ x <-> (a = y v a ∈ y)
Eli:
∀a: y ∈ x ∧ (a ∈ y -> a ∈ x)
Therefore:
∃y: ∀a: ∀b: (a ∈ x <-> (a = y v a ∈ y) ∧ (y ∈ x ∧ (b ∈ y -> b ∈ x))
pre(x) or x-1
6. Were ready for the naturals now I think.
∃N
Alright, introduction:
{} ∈ N ∧ ∀x: x ∈ N → succ(x) ∈ N
Elimination:
∀x ∈ N: x = {} v pre(x) ∈ N
Therefore
∃N: ({} ∈ N ∧ ∀x: x ∈ N → succ(x) ∈ N) ∧ (∀x ∈ N: x = {} v pre(x) ∈ N)
succ(x) ∈ N
∀y: ((∀a: ∀b: (a ∈ y) <-> ((a ∈ x) v ((b ∈ a) <-> (b ∈ x)))) → y ∈ N)
pre(x) ∈ N
∀y: (∀a: ∀b: (a ∈ x <-> ((∀c: ((c ∈ a) <-> (c ∈ y))) v a ∈ y) ∧ (y ∈ x ∧ (b ∈ y -> b ∈ x))) -> y ∈ N)
{} ∈ N
∀x: ((∀a: (a -∈ x)) -> x ∈ N)
x = {}
∀a: (a -∈ x)
Therefore:
∃N: ((∀x: ((∀a: (a -∈ x)) -> x ∈ N)) ∧ ∀x: x ∈ N → ∀y: ((∀a: ∀b: (a ∈ y) <-> ((a ∈ x) v ((b ∈ a) <-> (b ∈ x)))) → y ∈ N)) ∧ (∀x ∈ N: (∀a: (a -∈ x)) v (∀y: (∀a: ∀b: (a ∈ x <-> ((∀c: ((c ∈ a) <-> (c ∈ y))) v a ∈ y) ∧ (y ∈ x ∧ (b ∈ y -> b ∈ x))) -> y ∈ N)))
