The formalism presented in this post turned out to be erroneous (as opposed to the formalism in the previous post). The problem is that the step in the proof of the main proposition in which the soundness schema is applied cannot be generalized to the ordinal setting since we don't know whether ακ is a successor ordinal so we can't replace it by ακ'=ακ-1. I'm not deleting this post primarily to preserve the useful discussion in the comments.
Followup to: Parametric polymorphism in updateless intelligence metric
In the previous post, I formulated a variant of Benja's parametric polymorphism suitable for constructing updateless intelligence metrics. More generally, this variants admits agents which are utility maximizers (in the informal sense of trying their best to maximize a utility function, not in the formal sense of finding the absolutely optimal solution; for example they might be "meliorizers" to use the terminology of Yudkowsky and Herreshoff) rather than satisficers. The agents using this formalism labor under a certain "delusion", namely, since they believe that κ ("the number of ineffable mystery") is an actual finite number (whereas it is secretly infinite, in a sense), they think that the chain of tiling agents is effectively finite as well (since at some point agent #n in the chain will discover that κ > n is false and will fail to construct a subsequent agent of the same "epistemic strength"). The same problem exists in Weaver's intuitionistic assertability predicate formalism.
To overcome this limitation, I suggest to extend κ's semantics from natural numbers to elements of a certain recursive ordinal (at least morally; technically it is done a bit differently, see below). In Benja's original formulation this doesn't appear a valid option, since κ is interpreted as a time interval. However, in my variant κ is just an abstract parameter queries about which can be directed to a special "oracle", so there is no such limitation.
Formalism
Fix α a recursive ordinal and αi a system of notations for ordinals smaller than α such that α0=0, the function f defined by αf(i)=αi+1 is recursive and the bit-valued function g(i,j) which equals 1 iff αi < αj is also recursive. We also assume that
(0) T |- For all i: g(i,f(i))=1
where T is our starting theory. We define Tκ(α) to be T extended by the symbol κ (which stands for the index of the ordinal, not the ordinal itself) and the following self-referential soundness schema:
(1) For all formulae φ: For all n, i: ((@_Tκ(α) "φ(n)" and g(i,κ)=1) -> φ(n)[κ\i])
Tκ(α) is proven to be sound analogously to Yudkowsky and Herreshoff, with transfinite induction over ordinals below α replacing the ordinary induction.
The licensing condition for agent A0 to perform action b0 is
(2) Exists n: Tκ(α) |- (g(n,κ)=1 -> (A0()=b0 -> G))
The property which is sufficient for agent B1 to be creatable by agent A0 is
(3) Tκ(α) |- For all b1: (B1()=b1 -> (b1=0 or Exists n: (g(n,κ)=1 and @_Tκ(α) "(g(n,f(κ))=1 and B1()[κ\f(κ)]=b1) -> G[κ\f(κ)]")))
The proof that (3) indeed enables tiling is analogous to the previous post (but requires using (0)).
Discussion
In order for A0 to know that the tiling chain is infinite, it is enough for her to verify ακ >= ω. In order for her to know that A1 is going to know the tiling chain is infinite, she needs to verify ακ >= ω+1. In order for her to know that all agents are going to know the tiling chain is infinite, she needs to verify ακ >= 2ω. In order for her to know that all agents are going to know that, she needs to verify ακ >= 3ω et cetera.
It remains to decide which ordinal should we actually use. My intuition is that the correct ordinal is the least α with the property that α is the proof-theoretic ordinal of Tκ(α) extended by the axiom schema {g(i,κ)=1}. This seems right since the agent shouldn't get much from ακ > β for β above the proof theoretic ordinal. However, a more formal justification is probably in order.
Thx a dozen for writing that latex and recommending writelatex!
Indeed, in the formalism from the previous post (which you very kindly latexed) the agent thinks the tiling is going to effectively end after kappa steps (i.e. that the following agents won't operate by looking for arbitrary proofs of theorems in a theory of the same power). This is exactly the problem the current post sets out to solve. By working with ordinals instead of natural numbers, the agent can prove the tiling is infinite by verifying that alpha_kappa >= omega.
Moreover, even the formalism in the previous post does not reduce to vanilla PP. This is because, as opposed to what you wrote in the document, the goal G doesn't say something like "the world is safe for kappa steps". Indeed, the proof of tiling doesn't assume anything about G! For example, assuming that the motor action a_m is a natural number, G can be "at step m, the motor action must equal m^2". There is no kappa-time-limit in sight: kappa only enters G through the oracle's role in the agents' computations. This is important when passing from goals to expected utilities since I want the agent to be able to prove non-trivial bounds on the expected utility which would be impossible if the utility only depended on time interval [0, kappa] without anything known about kappa.
Ah, sorry, I assumed we were using the original PP assumptions. In that case, I'm guessing that such an agent is vulnerable to the procrastination paradox. Unfortunately, I don't have any more time to toy with this today.
I'd love to see a walkthrough (first in the previous system, then in the ordinal system) of how the proof goes through with a goal of the form "there exists a time at which the button becomes pressed" where the parent agent is attempting to construct a perfect copy o... (read more)