User:Alemagno12/Translation maps for SSS: Difference between revisions
Alemagno12 (talk | contribs) m (Formatting) |
Alemagno12 (talk | contribs) No edit summary |
||
Line 1:
Here are some
TODO: Prove that lexicographic ordering is equivalent to expansion for SSS. This is already proven for BM2.3 in <nowiki>[Yto2023]</nowiki>
== Up to \(\varepsilon_0\) ==
<b>Lemma 1.</b> Assume that o<sub>SSS</sub>(X) = o<sub>BM2.3</sub>(X') and o<sub>SSS</sub>(Y) = o<sub>BM2.3</sub>(Y') for some standard X,X',Y,Y'. Then, o<sub>SSS</sub>(X+(0)+Y) = o<sub>BM2.3</sub>(X'+Y').
<i>Proof.</i> By induction on Y. Zero and successor cases are trivial. For the limit case, let Z < Y and o<sub>SSS</sub>(Z) = o<sub>BM2.3</sub>(Z').
* BM2.3 does not have any "stop at the leftmost element if you can't find the bad root" condition, so the bad root of X'+Z' is the bad root of Z', and o<sub>BM2.3</sub>(X'+Z') = sup<sub>n<ω</sub>(o<sub>BM2.3</sub>(X'+exp(Z',n))).
* For SSS, if the second bad root check finds a bad root in Z, the bad root of X+(0)+Z is the bad root of Z. If it does not find a bad root, then since the first bad root must be at least (0,1) and every standard expression starts with 0, (0)+Z = (0,0)+W for some W < (0,1) <= bad root;
WIP
|
Latest revision as of 05:41, 13 November 2023
Here are some translation maps between SSS and BM2.3, alongside their proofs.
For a BM2.3 or SSS expression X, oBM2.3(X) or oSSS(X) is the order type of all possible standard expressions below it under expansion; for BM2.3, this is guaranteed to be an ordinal by [Yto2023]. ES is the empty string/matrix, + is string/matrix concatenation, X*k = X+X+X+...+X k times for some natural number k, and > is ordering by expansion.
TODO: Prove that lexicographic ordering is equivalent to expansion for SSS. This is already proven for BM2.3 in [Yto2023]
Up to \(\varepsilon_0\)[edit | edit source]
Lemma 1. Assume that oSSS(X) = oBM2.3(X') and oSSS(Y) = oBM2.3(Y') for some standard X,X',Y,Y'. Then, oSSS(X+(0)+Y) = oBM2.3(X'+Y').
Proof. By induction on Y. Zero and successor cases are trivial. For the limit case, let Z < Y and oSSS(Z) = oBM2.3(Z').
- BM2.3 does not have any "stop at the leftmost element if you can't find the bad root" condition, so the bad root of X'+Z' is the bad root of Z', and oBM2.3(X'+Z') = supn<ω(oBM2.3(X'+exp(Z',n))).
- For SSS, if the second bad root check finds a bad root in Z, the bad root of X+(0)+Z is the bad root of Z. If it does not find a bad root, then since the first bad root must be at least (0,1) and every standard expression starts with 0, (0)+Z = (0,0)+W for some W < (0,1) <= bad root;
WIP