cruegge
Joined 10 years ago
Joined 10 years ago
Yeah, sorry, wasn't really necessary to repeat that point. I was too focused on the "limiting the height of the tree to 32" formulation.
I have to admit that I don't quite understand what invariants along the lookup you mean. All lookups that reach a particular node on level 32 have the same hash, so regardless of how you compute the branch from the hash below level 32, they will always follow the same path starting from there (except for terminating at different levels, obviously). So nodes only ever have one child at most, and there's no loss in simply picking child 0 in all cases.
Sorry if what I'm describing is again obvious, maybe I just don't understand your point correctly.
type Cantor = Natural -> Bit
search :: (Cantor -> Bool) -> Maybe Cantor
that returns in finite time if its argument does.Source: https://math.andrej.com/2007/09/28/seemingly-impossible-func...
Edit: however, consistent second order theories don't always have a model. In first order, if S is an undecideable statement in theory T, then both T+S and T+!S have models, both of which are models for T, so undecideable statements always come from multiple models. But that does not need to be the case in second order, so your claim "it is independent from the axioms, i.e. there exist multiple models" is not neccessarily true, i.e. there may be cases when decideability of some statement fails in a theory with a unique model. Or is there another argument for your claim?
Forgive me for spamming questions, I just try to understand how these things fit together. But maybe we should just stick to first order, since everything else is too weird anyway.
Concerning multiple models of ZFC: I'm always confused by such statements about the foundations of set theory itself, they seem weirdly self-referential. ZFC certainly can't prove that it has multiple (or even any) models. Does such a statement need additional axioms, or is there a general theorem like "If a first order theory has any model, then it has multiple ones."?