• Emlightened

    A Largest Number

    April 22, 2018 by Emlightened

    This is an essay on largest numbers. Go figure. There's a remark at the end you should check out if the rest isn't all that interesting.

    First, a new largest number (a yet larger one is defined at the bottom of the page). Work in ZFC+WA0, the theory of ZFC with an elementary embedding symbol \(j:V \to V\) without replacement for formulae involving \(j\) and only bounded seperation for formulae involving \(j\). The critical point is denoted \(\kappa_0\), and let \(\kappa_{n+1} = j(\kappa_n)\). The language used is \(\langle \in, j, V_{\kappa_0} \rangle\).

    • k-Wholeness Number: The largest integer uniquely defined by a \(\Delta_0\) formula with quantifier depth \(\leq k\) and \(\leq 2^k\) occurances of the symbols \(j\), \(V_{\kappa_0}\).
    • k-Large…
    Read more >
  • Emlightened

    Ordinals in Type Theory

    January 28, 2018 by Emlightened

    Here a simple type system which can represent powerful fast-growing recursive functions is presented.

    It is based on the simply typed lambda calculus, and contains expressions for countible ordinals. The system could be extended in a way which permits multiple cardinaities and collapsing functions.

    This system is presented without contexts, and with \(\beta\) but not \(\eta\) equivalence.

    The lambda calculus has two sorts of thing: terms (which are represented by lowercase letters) and types (which are represented by uppercase letters). There are also three statements (judgements) that can be formed. These are:

    • \(A\text{ Type}\) which expresses that \(A\) is a type.
    • \(a : A\) which expresses that the term \(a\) has (unique) type \(A\). This sym…

    Read more >
  • Emlightened

    System Tau Notes

    November 3, 2017 by Emlightened

    I'm really really sorry, but this is incomplete. I have been making a text document (up to 42kb rn) trying to formalise and explain a Googological System, but it was never finished. I've not edited it in two months, and thought it was a better idea to let it die here than on my hard drive.

    Still, I'm pretty sure there are some interesting and salvageable ideas here. Since writing it, I've learned a lot of type theory (in particular, I think I have a decent understanding of inductive-recursive types), so if I come back here at some point, I should be able to clean up the presentation and present what I have in an inductive, not recursive, manner. (I'd probably also switch from math notation to computing notation, too. Easier to work with in …

    Read more >
  • Emlightened

    Terms are identified up to equivalence ≡. A model is consistent iff KSK is false.

    • Sabc ≡ ac(bc)
    • Kab ≡ a
    • If ac ≡ bc, c is a free variable and c does not occur in a or b, a ≡ b

    The extensions additionally include some of the following terms. It is not guaranteed that all extensions or combinations of extensions are consistent.

    • Qab ≡ K if a≡b and Qab ≡ SK otherwise
    • Eab ≡ K if there is some c such that ac ≡ b, and Eab ≡ SK otherwise
    • Cab ≡ Kc for some c such that ac ≡ b (if it exists), and Cab ≡ SKK otherwise
    • Mabc ≡ K if there is some d such that bd ≡ c and ad ≡ K, and Mabc ≡ SK otherwise
    • Nabc ≡ Kd for some d such that bd ≡ c and ad ≡ K, and Nabc ≡ SKK otherwise

    First off, K and SK represent the truth values true and false, respectively. Given this, it is somewhat clear what each of…

    Read more >
  • Emlightened

    Literally. As of writing, there are 10,787 pages on this wikia, and 11,084 articles in the numbers category.

    I'm mainly using this as an excuse to pick up the discussion which was dropped about a month ago from the comments here. Please have a quick read of them if you haven't yet.

    I believe the two popular ideas were to:

    • A) Consolidate similar-sized numbers from the same notation into one article each, possibly with a section on each number
    • B) Create a splinter site or forum, probably non-wikia based.

    I want to get this discussion going again. Both ideas appeal to me and honestly, I want to see us getting together and doing something towards these possible goals. It's better than deciding stuff should happen but not following through, so hopef…

    Read more >