Wait, but rational-delimited open intervals don't form a locale, because they aren't closed under infinite union. (For example, the union of all rational-delimited open intervals contained in (0,√2) is (0,√2) itself, which is not rational-delimited.) Of course you could talk about the locale generated by such intervals, but then it contains all open intervals and is uncountable, defeating your main point about going from countable to uncountable. Or am I missing something?
I'm actually not sure it's a regular grammar. Consider this program:
f(n) := n+f(n-1)
Which gives the tree
n+(n-1)+((n-1)-1)+...
The path from any 1 to the root contains a bunch of minuses, then at least as many pluses. That's not regular.
So it's probably some other kind of grammar, and I don't know if it has decidable equivalence.
Ok, if we disallow cycles of outermost function calls, then it seems the trees are indeed infinite only in one direction. Here's a half-baked idea then: 1) interpret every path from node to root as a finite word 2) interpret the tree as a grammar for recognizing these words 3) figure out if equivalence of two such grammars is decidable. For example, if each tree corresponds to a regular grammar, then you're in luck because equivalence of regular grammars is decidable. Does that make sense?
Then isn't it possible to also have infinite expansions "in the middle", not only "inside" and "outside"? Something like this:
f(n) := f(g(n))
g(n) := g(n+1)
Maybe there's even some way to have infinite towers of infinite expansions. I'm having trouble wrapping my head around this.
I don't understand why the second looks like that, can you explain?
Not sure I understand the question. Consider these two programs:
f(n) := f(n)
f(n) := f(n+1)
Which expression trees do they correspond to? Are these trees equivalent?
I just thought of a simple way to explain tensors. Imagine a linear function that accepts two numbers and returns a number, let's call it f(x,y). Except there are two ways to imagine it:
Linear in both arguments combined: f(1,2)+f(1,3)=f(2,5). Every such function has the form f(x,y)=ax+by for some a and b, so the space of such functions is 2-dimensional. We say that the Cartesian product of R^1 and R^1 is R^2, because 1+1=2.
Linear in each argument when the other is fixed: f(1,2)+f(1,3)=f(1,5). Every such function has the form f(x,y)=axy for some a, so the space of such functions is 1-dimensional. We say that the tensor product of R^1 and R^1 is R^1, because 1*1=1.
In this case the tensor product is lower dimensional than the Cartesian product. But if we take say R^3 and R^3, then the Cartesian product will be R^6 and the tensor product will be R^9, because it will have separate coefficients a_(ij)*x_i*y_j.
Your arbitration oracle seems equivalent to the consistent guessing problem described by Scott Aaronson here. Also see the comment from Andy D proving that it's indeed strictly simpler than the halting problem.
I think your argument will also work for PA and many other theories. It's known as game semantics:
The simplest application of game semantics is to propositional logic. Each formula of this language is interpreted as a game between two players, known as the "Verifier" and the "Falsifier". The Verifier is given "ownership" of all the disjunctions in the formula, and the Falsifier is likewise given ownership of all the conjunctions. Each move of the game consists of allowing the owner of the dominant connective to pick one of its branches; play will then continue in that subformula, with whichever player controls its dominant connective making the next move. Play ends when a primitive proposition has been so chosen by the two players; at this point the Verifier is deemed the winner if the resulting proposition is true, and the Falsifier is deemed the winner if it is false. The original formula will be considered true precisely when the Verifier has a winning strategy, while it will be false whenever the Falsifier has the winning strategy.
I see. In that case does the procedure for defining points stay the same, or do you need to use recursively enumerable sets of opens, giving you only countably many reals?