@MatheinBoulomenos It means for every ordinal stage, whether successor or not. Have you read my post on ordinals? The explanation and proof of transfinite recursive construction is there, and you need to go through it to grasp how and why recursive definitions work. Treat the stages as a function on an ordered set, which function is to be recursively defined, each point depending only on values on smaller inputs. As explained, it works if the ordered set is well-ordered, and sometimes fails otherwise.

In this comment I described building S algorithmically by modifying S in ordinal stages, but to translate it to be compatible with transfinite recursion, you are essentially building a fixed function S where S(i) is defined in terms of S(j) for j<i, for each stage i. This corresponds to the extender.

Such an algorithmic process can be translated only because the process is monotonic; we only add to S and never take away, so S(i) = Union { S(j) : j<i } possibly adding {v(i)} depending on the condition.

@MatheinBoulomenos: Hi! Do you want me to make it more precise?

Well I just spotted a slightly ambiguous part so I edited the post.

@LeakyNun This wasn't in your original list, right? It's correct, but it's not so short to prove that it implies left-neighbour for successors, right? If S(x) = y and z < y then S(z) ≤ y = S(x), and then now you have to use the addition axioms to get z ≤ x.

@LeakyNun Yes. If x<y and ¬∃z ( x<z<y ), then S(x) ≤ y by your new axiom and S(x) ≥ y because S(x) > x and ¬∃z ( x<z<y ), and hence S(x) = y.

@LeakyNun Ah I see okay.

@user21820 do we have different notion of "left neighbour for successor"? The one I wrote down is what I have in mind

@LeakyNun You are right; my notion is the same as yours, and my comment was silly.

I would have written it as ∀x ( ¬∃y ( x < y < S(x) ) ), which is no doubt equivalent to yours. I don't know why I didn't realize that, and had a detouring proof.

@user21820 how can we know that the metasystem is consistent?

I think you mentioned in mathworks that we can't, and that it is the ideal case

class ordinal (α : Type u) extends
  linear_order α, has_zero α, has_add α, has_mul α :=
(omega : α)
(succ : α → α)
(zero_le : ∀ x : α, 0 ≤ x)
(zero_lt_omega : 0 < omega)
(zero_or_succ_of_lt_omega : ∀ x : α, x < omega → (x = 0 ∨ ∃ y, x = succ y))
(succ_ne_zero : ∀ x : α, succ x ≠ 0)
(succ_ne_omega : ∀ x : α, succ x ≠ omega)
(succ_inj : ∀ x y : α, succ x = succ y → x = y)
(lt_succ : ∀ x : α, x < succ x)
(le_of_lt_succ : ∀ {x y : α}, x < succ y → x ≤ y)
(add_zero : ∀ x : α, x + 0 = x)
(add_limit_le : ∀ {x y z : α}, y ≠ 0 → (∀ w : α, w < y → x + w < z) → x + y ≤ z)

@user21820 must Godel's sentence be true?