Logic - 2024-04-22

« first day (2805 days earlier) ← previous day next day → last day (6 days later) »

2:13 PM

@user21820 I came up with a neat axiomatization for ordinal machines which has a relatively simple framework. I haven't finished proving that it's as strong as it's supposed to be (should interpret PA2), but I think it works. Take a look, if you're interested :)

Consider a two typed theory: one type for the ordinals, and the other is a class of partial functions between ordinals. We also include "null" as a constant object, which is not an ordinal. Our language includes a function application operator, which is suppressed in favor of the typical "F(x)" notation. For simplicity, we restrict…

Jade Vanadium

2:27 PM

If you include the assumption that there's a cofinal class of cardinals, then it should also interpret ZFC. For that purpose, cardinals may be defined as those ordinals not admitting a surjection from a lesser ordinal:
IsCardinal(α) ⇔ ∀(β<α), ∀F, ∃(y<α), ∀(x<β), F(x)≠y
Where F ranges over our class of partial functions, and α,β,x,y range over the ordinals.

Axiom 5 is really doing all the work of giving us the functions, along with the formation rules for our terms. Since axiom 5 is coded as a schema, we don't need to assume anything about string manipulation, except in the metatheory.

You should be able to use these axioms to build up to ordinal exponentiation, at which point you can encode arbitrary finite sequences of ordinals using something like CNF. That lets you bypass the 3-input restriction imposed on functions. I imposed that restriction after having worked up that far, just because it's kinda cute.

Jade Vanadium

2:48 PM

Axiom 3 basically gives the ? trinary operator, sometimes named 'If', and axiom 4 encodes < as a function (where 0=false and 1=true). You know how to use those to get the other logical connectives, and we can also encode = in terms of <. We can also superficially extend our formation rules by defining the behavior of some bounded quantifiers, which work similarly to 'min'. For example, given any term φ, we can define
All{x<y : φ} := ¬(y = min{x : (x=y) ?∨ φ})
We can similarly encode bounded existentials. This also lets us define an operator to calculate supremum. Where S is not free in the …

We can define some simple operations with these things:
Succ(x) := min{y : x<y}
Pred(x) := min{y : x≤Succ(y)}
IsLimit(x) := (x=Pred(x))
Axiom 5 doesn't have any implicit restrictions, other than the ones laid out, so it permits built-in recursions. For example, since "If(IsLimit(x), x, F(Prec(x)))" is a term, then axiom 5 guarantees the existence of F such that F(x) equals this term. This is allowed even though the term mentions F itself, i.e. axiom 5 gives us recursion.
∃F, ∀x, F(x) = If(IsLimit(x), x, F(Pred(x)))

Add(x,y) = if(y=0, x, sup{Succ(Add(x,z)) : z<y})
Mult(x,y) = sup{Add(Mult(x,z), x) : z<y}
Pow(x,y) = if(y=0, 1, sup{Mult(Pow(x,z), x) : z<y})

Jade Vanadium

3:24 PM

Typo: The definition of the 'All' quantifier should have been this:
All{x<y : φ} := (y = min{x : (x=y) ?∨ ¬φ})
Previously I had accidentally put the definition for the existential quantifier, which is structured similarly:
Exists{x<y : φ} := ¬(y = min{x : (x=y) ?∨ φ})

Jade Vanadium

3:47 PM

I should also clarify that our Ord-Replacement needs to be a schema ranging over every formula-defined function. If we only assert Replacement for object functions, then we only get something like Σ1 replacement. This is in contrast to my definition of the "IsCardinal" proposition: with full Ord-Replacement, we can prove that any bounded-domain formula-defined function is encodable as an object, hence if there's no object encoding a surjection β→α, then there's no definable surjection at all.

Jade Vanadium

4:08 PM

As a proof for why the first-order Replacement is not enough, consider the model where our ordinals are all those below ℵ[ω] (using the ℵ[ω] of L), and our object functions are all those defined by ordinal machines with parameters below ℵ[ω].

Given any object function F in our model, there's some ordinal machine M such that generally F(x)=M(x) for all x<ℵ[ω]. Moreover M has all its parameters being less than ℵ[ω]. Since M has only finitely many parameters, then there's some finite n such that all the parameters of M are below ℵ[n]. Since ℵ[n] is a cardinal, then it's a stable ordinal, so i…

« first day (2805 days earlier) ← previous day next day → last day (6 days later) »

all rooms