Apeirology Wiki

User:Alemagno12/Translation maps for SSS: Difference between revisions

User page Discussion

User:Alemagno12/Translation maps for SSS (edit)

Revision as of 05:41, 13 November 2023

564 bytes added ,  7 months ago
no edit summary
VisualWikitext
m (Formatting)
No edit summary
 
Line 1:
Here are some (conjectured) translation maps between SSS and BM2.3, alongside their proofs.
 
Term(PrSS),For Term(PSS)a BM2.3 or SSS expression X, Termo<sub>BM2.3</sub>(TSSX), Term(or o<sub>SSS</sub>(X) areis the setsorder type of all PrSS,possible PSSstandard expressions below it under expansion; for BM2.3, TSSthis andis SSSguaranteed expressionsto respectivelybe an ordinal by [https://arxiv.org/abs/2307.04606 <nowiki>[Yto2023]</nowiki>]. 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 lexicographicordering by comaparisonexpansion.
 
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').
Define a function Prune : Term(SSS) -> Term(SSS) inductively as follows:
 
* Prune(ES) = ES
<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').
* Prune((A,0)) = (Prune(A),0)
 
* Prune((A,0,B,1)) = (Prune(A),0,B), where B >= 1
* 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))).
* Otherwise, Prune(A) doesn't exist.
 
* 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;
Define a function Shift : Term(PrSS) -> Term(PrSS) inductively as follows:
* Shift(ES) = ES
* Shift((A,k)) = (Shift(A),k+1)
i.e. Shift(A) is the result of adding 1 to all the elements in A.
 
WIP
Define a function Map : Term(SSS) -> Term(PrSS) inductively as follows:
* Map(ES) = ES
* Map((A,0)) = (Map(A),0)
* Map((0,A)) = I'll finish this later, also maybe a more algorithmic approach would be better? E.g first turn all (0,1^k)s into (k)s, then add inbetween elements
Retrieved from "https://apeirology.com/wiki/Special:MobileDiff/608"