An uncomputable number

Let L denote the formal language of ZFC set theory consisting of variable term symbols x₀, x₁,... indexed by natural numbers, a 2-ary relation symbol ∈, logical connectives ¬ and →, a universal quantifier ∀, and parenthesis ( and ).

Let S be the set of all L-formulae.

A sequence T is valid iff:

1. Every element of T is an element of S.
2. Call k the index of the last member of T. For all i<=k.i∈ω there isn't some j<i.j∈ω such that T_i contains T_j or T_j contradicts T_j.
3. T_i has at most i+100 symbols.

I define ZFC-LVS as the length of the longest valid sequence.

LVS stands for longest valid sequence.

While there is a significantly stronger computable version of this (create by removing ' or T_j contradicts T_j'). The purpose of this is not (entirely) to create a large number. We can rank formal languages by how large their LVS is if we change L to the formal language.