(note: some readers may find the LaTeX easier to read on LessWrong)

The purpose of this post isn’t to convince you that cut elimination is important. See, for example, the nLab article. Rather, the purpose of this post is to (semi-formally) prove cut elimination in a way that I at least find easy to understand. I have consulted existing sources (such as these lecture notes), but have found it hard to fill in all the details, given the sparsity of the usual presentations. I’ll build on the previous post (on Gödel’s Completeness Theorem) and show cut elimination in the first-order sequent calculus defined in that post. Recall that the cut rule states:

We can think of as the assumptions, as the conclusion, and P as a lemma. Intuitively, this states that, if it’s possible to prove the conclusion or the lemma from the assumptions, and it’s possible to prove the conclusion from the assumptions and the lemma, then it’s possible to prove the conclusions from the assumptions. Cut-elimination is, therefore, the automated elimination of lemmas in a sequent proof. (As stated in the previous post, this presentation of the cut rule is somewhat nonstandard, but it can be shown equivalent to the standard form using weakening and contraction.)

Throughout the post, I will use the notion of the depth of a sentence, and the cut rank of a proof. The depth of a sentence is the depth of nesting of compound sentences; in particular, the depth of an atomic sentence is 0, the depth of a negation is one plus the depth of its inner sentence, the depth of a conjunction is one plus the maximum depth of the inner sentences, and the depth of a universal is one plus the depth of the inner sentence. The cut rank of a proof is a mapping , where is the number of times a cut is performed on a sentence of depth i; note that this is zero almost everywhere. We compare cut ranks lexicographically, with later entries counting more than previous ones.

Constant substitution

As a preliminary, we will show that constants can be substituted with terms in proofs without changing the proof structure (in particular, cut rank stays the same). As notation, if P is a term, sentence, or set of sentences, let P[t/c] indicate replacing the constant c with the term t anywhere in P. Suppose we have a proof of the judgment . We wish to show that there is a proof of with the same cut rank as the original proof.

Call the height of a sequent proof the longest path from top to bottom, counting by number of rule applications. I will show by induction that, for all natural , constant substitution holds for a proof whose height is n.

In the base case, the only rule is the assumption rule. Then and both contain some sentence P. So and both contain . So the assumption rule also shows .

In the inductive case, we consider different cases for the bottom-most rule. Suppose the bottom-most rule in the proof is the weakening rule. Then the proof looks like:

By the inductive assumption, we have a proof of . Then we straightforwardly show using weakening.

Suppose the bottom-most rule in the proof is the cut rule. Then the proof looks like:

By the inductive assumption, we have proofs of and . Now we cut on to get the result.

Suppose the bottom-most rule in the proof is the left negation rule. Then the proof looks like:

By the inductive assumption, we have a proof of . We apply the left negation rule on to get a proof of .

Most of the remaining rules are similar, so I will skip them. I will consider the non-trivial case of the right universal rule. In this case, the proof looks like this:

where d is a constant not appearing in , , or . Let d’ be a constant not appearing in , , , or t, and not equal to c. First we apply the inductive assumption to get a proof of or equivalently . Now we apply the inductive assumption again to get a proof of . Since d’ does not appear in t and is unequal to c, we can swap the substitution order to get a proof of . At this point, since d’ does not appear in , or , we can apply the right universal rule to get a proof of .

Eliminating weakening

It will be easier to show cut elimination in a logic without weakening. So it is more convenient to eliminate weakening before eliminating cut. This has the added benefit of eliminating weakening in addition to cut. Recall the weakening rule:

I will show by induction that, for all natural , weakening can be eliminated for a proof whose height is n+1, and whose last step is weakening.

Let’s consider the base case. If the proof has height 2, and the bottom-most rule is weakening, then the top-most rule must be the assumption rule. In this case, the assumption rule could have been applied to the pre-weakened judgment.

Let’s consider the inductive case. Suppose weakening can be eliminated form any proof whose height is at most n and whose last step is weakening. We now consider showing weakening can be eliminated from a proof whose height is n+1 and whose last step is weakening.

We do this by cases on the second-to-last rule. We have no need to handle the assumption rule, as that would make the height 2 (the base case).

Suppose the second-to-last rule is weakening. Then the two weakenings can be combined into one weakening. This reduces the height of the proof by one, so weakening can be eliminated inductively.

Suppose the second-to-last rule is cut. Then the proof looks like this:

Call the proof of the top-left judgment X and the proof of the top-right judgment Y. Then X and Y have height at most n-1. Now we consider re-writing the proof to put weakening higher:

The left proof of has height at most n, and the right proof of has height at most n. So weakening can be eliminated from both sides (using the inductive assumption).

Suppose the second-to-last rule is left negation. Then the proof looks like this:

As before, we re-write to move weakening higher:

And observe that the size of the proof with weakening at the bottom is now at most n, so weakening can be eliminated from it inductively.

I will skip most of the rules, as they are similar. The only nontrivial case is the right universal rule. The proof would look like this:

where c does not appear in , , or . Now we find a constant d which does not appear in , , , , or . We move weakening up:

We can convert the original proof of to one of equal height and cut rank proving using constant substitution. Now weakening can be eliminated from this proof using the inductive assumption.

Note that throughout this process, the structure of cuts has not been changed; the same cuts are applied to the same sentences. As such, the cut rank is the same.

As a corollary of weakening elimination, we can transform proofs so that, if a rule application is of the form

then and . This is because the non-weakening rules, such as the negation rules, have “implicit contraction” where there is no requirement to eliminate any sentence, and weakening elimination means these extra sentences in judgments are not a problem (as they could be eliminated with weakening anyway, and then the weakenings could be eliminated). I will call this transformation “redundant contraction”. Note also that this does not change the cut rank of the proof.

Making the assumption rule only apply to atoms

Recall that an atomic sentence is a predicate applied to some terms. The assumption rule may apply to arbitrary sentences. We would like to transform sequent proofs to ones that only apply the assumption rule to atomic sentences.

To do this, we will consider proving judgments of the form without using the assumption rule except on atomic sentences. We will do this by induction on the structure of P.

Now we consider what form P could take. If P is atomic, we simply apply the assumption rule. Suppose P is . Then we prove the judgment as follows:

with the top judgment proven by the inductive assumption.

Suppose P is . Then we prove the judgment as follows:

with the top judgments proven by the inductive assumption.

Suppose P is . Then we prove the judgment as follows:

with the top judgment proven by the inductive assumption, and where c is a constant not appearing in , , or .

The inversion lemma

The rules for compound sentences are, for the most part, invertible, in that if the bottom judgment is provable with no cuts, so is the top judgment. I will show invertibility for these rules, assuming no weakening and that the assumption rule only applies to atoms.

In general, these proofs will work by applying redundant contraction to the proof of the bottom judgment and observing that the proof steps work for a modified version of the judgments, except for certain rule applications. Note that we intentionally omit the left universal rule, as it is not invertible like the others. It will instead be handled manually later.

A property that will be true throughout is that, if the original proof has no cuts, neither does the inverted proof.

Left negation

Consider the left negation rule:

Suppose the bottom judgment is provable. Apply redundant contraction to the proof. We will do induction over the proof to show that each sub-proof of a judgment can be converted to one of a converted form of the judgment, where is removed on the left and P is added to the right. Every step in the proof will convert automatically except for instances of the left negation rule applied to . Those cases originally look like

and in the conversion we are trying to show . We can prove this by inductively converting the proof of .

Overall, the converted proof proves . And if the original proof has no cuts, neither does the converted proof.

Right negation

Consider the right negation rule:

Suppose the bottom judgment is provable. Symmetric with the left negation case, we convert the proof to a proof of . And if the original proof has no cuts, neither does the converted proof.

Left conjunction

Consider the left conjunction rule:

Suppose the bottom judgment is provable. Apply redundant contraction to the proof. We will do induction over the proof to show that each sub-proof of a judgment can be converted to one of a converted form of the judgment, where is removed from and P and Q are added to the left. Every step in the proof will convert automatically except for when left conjunction is applied to . Those cases look like:

and in the conversion we are trying to show . We can prove this by inductively converting the proof of .

Overall, the converted proof proves , as desired. And if the original proof has no cuts, neither does the converted proof.

Right conjunction

Consider the right conjunction rule:

We will consider proofs of and separately.

First consider . Suppose the bottom judgment is provable. Apply redundant contraction to the proof. We will do induction over this proof to show that each sub-proof of a judgment can be converted to one of a converted form of the judgment, where is removed from and P is added to the right side. Each step of the proof will convert automatically except for applications of the right conjunction rule to . Those cases look like:

and in the conversion we are trying to show . We prove this by inductively converting the proof of .

Overall, the converted proof proves , as desired.

Now consider . This is symmetric with the previous case, yielding a converted proof.

In both cases, if the original proof has no cuts, neither does the converted proof.

Right universal

Consider the right universal rule:

where c does not appear in . Suppose the bottom judgment is provable. Apply redundant contraction to this proof. We will do induction over the proof to show that each sub-proof of a judgment can be converted to one of a converted form of the judgment, where is removed from and is added to the right, where c’ is a constant appearing nowhere in the proof. Every step will convert automatically except for applications of the right universal rule to . Those cases look like:

where d is a constant not appearing in , and in the conversion we are trying to show . We inductively convert the proof of to get a proof of . Then we apply constant substitution to this proof, replacing d with c’, to get a proof of .

Overall, the converted proof proves . Now we apply constant substitution again to get a proof of . And if the original proof has no cuts, neither does the converted proof.

Showing cut elimination

We are now ready to eliminate cut from an arbitrary proof. Assume the proof has no weakening and that the assumption rule is only used on atoms (we have already shown how to convert a proof to one of this form). An instance of the cut rule looks like this:

We consider different forms P could take in turn. Each time, we eliminate one instance of cut from the proof (a “cut reduction”), in a way that reduces the cut rank of the overall proof. We only eliminate cuts where the proofs of the premises do not themselves have any cuts; if the proof has at least one cut, a cut exists whose premise proofs don’t have any cuts, so this is not an obstacle to the algorithm.

Atomic sentences

Suppose P is atomic. Assume the proofs of and are cut-free. Apply redundant contraction to the first proof. Each leaf of this proof now uses the assumption rule to prove where and . Now we consider eliminating P from the right hand side of every judgment in this proof (so the converted “proof” now “proves” ); every non-assumption rule can still be applied, but some of the leaves will now fail to be proven with the assumption rule. In those cases, when the judgment of the leaf is , we know , as the elimination of P from the right caused a failure of the assumption rule. In those cases, it is sufficient to show , by weakening elimination (since and ). But we already have a cut-free proof of this, the original cut-free proof of . By repairing the leaves, we now have a cut-free proof of .

Negations

Suppose . Then the premises of the cut rule imply we have proofs of and . Assume these proofs are cut-free. Using invertibility, we can get cut-free proofs of and . Then apply cut on Q:

This reduces the cut rank because cut is applied to a simpler sentence.

Conjunctions

Suppose . Then the premises of the cut rule imply we have proofs of and . Assume these proofs are cut-free. Using invertibility we can get cut-free proofs of , , and . Then apply cut twice:

This reduces the cut rank because cut is applied to simpler sentences. Note that we can convert the proof of to one of using weakening elimination.

Universals

Suppose . Then the premises of the cut rule imply that we have proofs of and . Assume both these proofs are cut-free, and apply redundant contraction to the second. Using invertibility on the first proof, we can get a cut-free proof of where c is a constant not appearing in .

We will do induction over the proof of to show that each sub-proof of a judgment can be converted to one of a converted form of the judgment, where is removed from the left, and where we only introduce cuts on sentences of the form . Each step of the proof will convert automatically except for applications of the left universal rule, of the form

where and . In the converted proof, we are instead trying to show . We can prove this by inductively converting the proof of to one of , and then applying cut:

We can show by applying constant substitution to our cut-free proof of to get a cut-free proof of , and then applying weakening elimination.

While we introduce more cuts into the proof, these all apply to a sentences of the form , which have lower depth than the original universal , so this still decreases the cut rank.

Summary

To summarize, we first modify our proof to have no weakening and to only apply the assumption rule to atoms. Then we find an instance of cut where the proofs of the premises are cut-free. Depending on what sentence is cut, we find a way to remove this cut, only replacing it with cuts on sentences with lower depth. Overall, this succeeds in reducing the cut rank of the proof. Since the set of cut ranks (assumed to be zero almost everywhere) are well-ordered, this iterative process will eventually eliminate all cuts from the proof.

Conclusion

Cut elimination is a fundamental theorem of formal logic. I have shown cut elimination for the first-order sequent calculus described in the post on Gödel’s completeness theorem, which is a simplified form of system LK. Compared to explanations of cut elimination I have found in the literature, this is a relatively complete proof relative to its simplicity. It helps me at least understand how cut elimination can proceed in an algorithmic, syntactic manner on the proof tree. While applications of cut elimination are beyond the scope of this post, understanding the actual proof might help to understand how these applications work.

(note: some readers may find the LaTeX more readable on LessWrong.)

In this post I prove a variant of Gödel’s completeness theorem. My intention has been to really understand the theorem, so that I am not simply shuffling symbols around, but am actually understanding why it is true. I hope it is helpful for at least some other people.

For sources, I have myself relied mainly on Srivastava’s presentation. I have relied a lot on intuitions about sequent calculus; while I present a sequent calculus in this post, this is not a complete introduction to sequent calculus. I recommend Logitext as an online proof tool for gaining more intuition about sequent proofs. I am familiar with sequent calculus mainly through type theory.

First-order theories and models

A first-order theory consists of:

• A countable set of functions, which each have an arity, a non-negative integer.
• A countable set of predicates, which also have non-negative integer arities.
• A countable set of axioms, which are sentences in the theory.

Assume a countably infinite set of variables. A term consists of either a variable, or a function applied to a number of terms equal to its arity. An atomic sentence is a predicate applied to a number of terms equal to its arity. A sentence may be one of:

• an atomic sentence.
• a negated sentence, .
• a conjunction of sentences, .
• a universal, , where x is a variable.

Define disjunctions (), implications (), and existentials () from these other terms in the usual manner. A first-order theory has a countable set of axioms, each of which are sentences.

So far this is fairly standard; see Peano arithmetic for an example of a first-order theory. I am omitting equality from first-order theories, as in general equality can be replaced with an equality predicate and axioms.

A term or sentence is said to be closed if it has no free variables (that is, variables which are not quantified over). A closed term or sentence can be interpreted without reference to variable assignments, similar to a variable-free expression in a programming language.

Let a constant be a function of arity zero. I will make the non-standard assumption that first-order theories have a countably infinite set of constants which do not appear in any axiom. This will help in defining inference rules and proving completeness. Generally it is not a problem to add a countably infinite set of constants to a first-order theory; it does not strengthen the theory (except in that it aids in proving universals, as defined below).

Before defining inference rules, I will define models. A model of a theory consists of a set (the domain of discourse), interpretations of the functions (as mapping finite lists of values in the domain to other values), and interpretations of predicates (as mapping finite lists of values in the domain to Booleans), which satisfies the axioms. Closed terms have straightforward interpretations in a model, as evaluating the expression (as if in a programming language). Closed sentences have straightforward truth values, e.g. the formula is true in a model when P is false in the model.

Judgments and sequent rules

A judgment is of the form , where Γ and Δ are (possibly infinite) countable sets of closed sentences. The judgment is true in a model if at least one of Γ is false or at least one of Δ is true. As notation, if Γ is a set of sentences and P is a sentence, then denotes .

The inference rules are expressed as sequents. A sequent has one judgment on the bottom, and a finite set of judgments on top. Intuitively, it states that if all the judgments on top are provable, the rule yields a proof of the judgment on the bottom. Along the way, I will show that each rule is sound: if every judgment on the top is true in all models, then the judgment on the bottom is also true in all models. Note that the rules do not take into account axioms; we can add the axioms as assumptions on the left hand side later, to compensate.

In these rules, Γ, Δ, Σ, and Π represent countable sets of closed sentences, P and Q represent closed sentences, x represents a variable, c represents a constant, and t represents a closed term. represents a sentence with zero or one free variables; if it has no free variables, , and if it has one free variable, represents substituting the term t for the free variable of .

Assumption rule:

This states that if the same sentence appears on both sides, the judgment can be trivially proven. Clearly, in any model, P must be true or false, so either a sentence on the left is false or one on the right is true.

Cut rule:

Suppose the top two judgments are true in all models. Then in any model where all of Γ are true and all of Δ are false, P must be true, but it also must be false, a contradiction. So any model must have at least one of Γ false or at least one of Δ true, showing the conclusion. (Note that this cut rule is simplified relative to the usual presentation.)

Weakening rule:

Suppose the top judgment is true in all models. Then no model has all of Γ true and all of Δ false. So clearly the bottom judgment is true in all models.

Weakening simply let us remove sentences from either side. Most sequent calculi involve contraction rules, for “doubling” a given sentence, but this is unnecessary given our set-theoretic interpretation of both sides of a judgment.

Rules for compound sentences (negations, conjunctions, and universals) come in left and right varieties, to handle compounds on the left and right of judgments respectively.

Left negation rule:

Suppose the top judgment is true in all models. Then any model in which Γ are all true and Δ are all false has P true. So clearly, the bottom judgment must be true of all models.

Right negation rule:

Suppose the top judgment is true in all models. Then any model in which Γ are all true and Δ are all false has P false. So clearly, the bottom judgment must be true of all models.

Left conjunction rule:

Clearly, all of are true in exactly the cases where all of are true, so the top and bottom judgments are true in the same set of models.

Right conjunction rule:

Suppose both top judgments are true in all models. Then in any model where Γ are all true and Δ are all false, P and Q must both be true. So the bottom judgment holds in all models.

Left universal rule:

Suppose the top judgment is true in all models. Then in any model where all of Γ are true and all of Δ are false, must be false. So in any model where all of Γ are true and all of Δ are false, must be false, showing the bottom judgment is true in all models.

Right universal rule:

We require that the constant c does not appear in Γ, Δ, or . Suppose the top judgment is true in all models. For contradiction, suppose the bottom judgment is false in some model. In that model, all of Γ must be true and all of Δ must be false, and must be false, meaning there is some value y in the domain of discourse for which is false (when interpreting x as equaling y). Consider a modification to this model where the interpretation of c is set to y. Since c does not appear in Γ or Δ, it remains the case that all of Γ are true and all of Δ are false in this model. In this model, must also be false. This contradicts that the top judgment is true in all models. (Note that using a constant for c rather than a variable is non-standard, although it helps later.)

A proof of a judgment can be defined recursively: it selects a rule whose bottom is the judgment to be proven, and includes a proof of every judgment on the top. The proof tree must be finite for the proof to be valid.

To simplify future proofs, we will show derived sequent rules:

Right disjunction rule (derived):

This demonstrates how sequents can be composed. While we could move P and Q to the right side, this turns out to be unnecessary as the rule is used later.

Contradiction rule (derived):

This shows that a set of assumptions that implies a sentence and its negation is inconsistent. Note that either side of a judgment can be left empty to indicate an empty set of sentences.

Left double negation rule (derived):

Right double negation rule (derived):

Proving soundness

Gödel’s completeness theorem states that a closed sentence is provable in a first-order theory if and only if it is true in all models of the theory. This can be separated into a soundness lemma, stating that any provable sentence holds in all models of the theory, and a completeness lemma, stating that any sentence holding in all models of the theory is provable.

What I am showing here is Gödel’s completeness theorem for the variant of first-order logic presented. Specifically, if T is a first-order theory, let be the theory with no axioms, and let Θ be the set of axioms. We say the sentence P is provable in the T if the judgment is provable.

Let’s consider the soundness lemma, which states that if is provable, then P is true in all models of T. Suppose we have a proof of . We have shown for each rule that if all the top judgments are true in all models, then the bottom judgment is true in all models. So by induction on the proof tree, must be true in all models of . So in any model of , at least one of Θ is false or P is true. The models of T are exactly those models of in which all of Θ are true, and in all of these models, P must be true.

Alternative statement of the completeness lemma

The completeness lemma states that any sentence holding in all models of the theory is provable. If the theory is T with axioms Θ, this states that for any sentence P, if P is true in all models of T, then is provable.

Let’s consider an alternative lemma, the model existence lemma, stating that if a theory is consistent (in that the judgment is not provable, with Θ being the axioms of the theory), then it has a model. Suppose the model existence lemma is true; does it follow that the completeness lemma is true?

Suppose we have a theory T with axioms Θ, and P is true in all models of T. Construct the alternative theory T’ which is T with the additional axiom that . Suppose P is true in all models of T. Then there are no models of T’. By the model existence lemma, there is a proof of . Now we show :

We have shown that if P is true in all models of T, then it is provable in T. So if we prove the model existence lemma, the completeness lemma follows.

The Henkin construction

To make it easier to prove the model existence lemma, we will consider constructing an alternative Henkin theory for T. In a Henkin theory, for any sentence with zero or one free variables, it is provable that for some constant c. We will rewrite the sentence to a logically equivalent one, . The main purpose of all this is to avoid a situation where an existential statement is true in a model, but no particular is true for closed terms t.

We wish to show that if T is a consistent theory, then there is a consistent Henkin theory whose axioms are a superset of T’s. Let us number in order the sentences with zero or one free variables as . Start with . We will define for each natural :

We set each constant so that it appears in neither nor . This is doable given that there is a countably infinite set of constants in T not appearing in Θ.

Define each theory to be T except with being the set of axioms. We wish to show that each is consistent. By assumption, is consistent. Now suppose is consistent for . For contradiction, suppose is inconsistent. Then we have a proof of .

Intuitively, if disproves , then it must disprove both sides of the disjunct. Let Q be an arbitrary closed sentence and consider the following sequent proof (using cut, the derived rule for right disjunctions, and weakening):

We can set , and see that follows from the assumption rule, in order to get . Similarly we have . Because does not appear in or , we have using the right universal rule. But now it is clear that is contradictory, i.e. is inconsistent.

So if is consistent then so is . By induction each is consistent. Define , with being T with these axioms, and note that if were inconsistent, the proof would only use a finite number of assumptions, so some would be inconsistent, as we have disproven. So must be consistent as well.

Suppose we showed the model existence lemma for . Suppose T is consistent. Then is consistent. So has a model. Clearly, this is a model of T since has strictly more axioms. So T would have a model, showing the model existence lemma for T. It is, then, sufficient to show the model existence lemma for Henkin theories.

Proving the model existence lemma for Henkin theories

Suppose T is a consistent Henkin theory. We wish to show that it has a model. This model will be a term model, meaning its domain of discourse is the set of closed terms. We need to assign a truth value to each closed sentence; number them as .

Let the axioms of T be Θ. Define . Now define inductively:

if there is a proof of .

otherwise.

Let be the theory T but with the axioms . Assume is consistent (so there is no proof of ). Suppose there is a proof of . Then there is no proof of (using the derived contradiction rule). So would be be consistent. Suppose on the other hand there is no proof of . Then clearly is consistent. Either way, if is consistent, so is .

By induction, each is consistent. Using similar logic to before, the limit (with axioms ) is consistent. This theory is complete in that for any closed sentence P, it either proves it or its negation. Accordingly it either proves or disproves each closed atomic sentence. From this we can derive a putative term model M by setting the interpretations of a predicate applied to some terms (which are the elements of the domain of discourse) to be true when the corresponding atomic sentence is provable in .

We must check that this putative model actually satisfies the axioms of . To do this, we will show by induction that each closed sentence P is true in M if and only if proves P (or equivalently, is provable).

For atomic P, this is trivial.

Negations

Consider . Assume Q is true in M if and only if .

Suppose first that Q is true in M. Then we have . So we don’t have , else would be inconsistent. So P is false in M and not provable in , as desired.

Suppose instead that Q is false in M. Then there is no proof of , so there must be a proof of . So P is true in M and provable in , as desired.

Conjunctions

Consider . Assume Q is true in M if and only if is provable, and likewise for R.

Suppose first that both Q and R are true in M. Then both are provable in . So we have using the right conjunction rule. So P is true in M and provable in , as desired.

Suppose Q is false in M. Then there is no proof of . If then we could prove , a contradiction.

So P is false in M and not provable in , as desired.

Suppose R is false in M. This is symmetric with Q.

Universals

Consider . Assume, for all closed terms t, that is true in M if and only if .

Suppose that is false in M for some t. Then there is no proof of . If there were a proof of , then there would be a proof of , a contradiction.

So P is false in M and not provable in , as desired.

Suppose instead that each is true in M. Since is Henkin (as T is), for some constant c. By the inductive assumption, is provable. Now we show a general fact about disjunctions:

Intuitively this says that if Q and are provable, so is P. So in particular we have (setting ). Let d be a constant not appearing in . Now we eliminate the double negation:

So P is true and provable in , as desired.

We have handled all cases by now. By induction, every closed sentence is true in M if and only if it is provable in . Now consider some axiom of T. Clearly, it is provable in . So it is true in M. Therefore, M really is a model of T (and indeed, of ).

Conclusion

Let’s summarize the argument. We start with a first-order theory T and a proposition P. Since the sequent rules are sound, if T proves P, then P is true in all models of T. Suppose instead that T does not prove P. Then we create a modification of T with the additional axiom that , which remains consistent. Then we extend this to a consistent Henkin theory. We further extend the Henkin theory to be complete in the sense that for any proposition, the theory proves it or its negation. It is now straightforward to derive a model from the complete theory, by looking at what it proves about closed atomic propositions, and check that it is indeed a model by induction. This demonstrates the existence of a model of T in which P is false. Contrapositively, if P is true in all models of T, then T proves it.

If we wish to have equality in the theory, we introduce an equality predicate and axioms. The model will give truth values for the equality predicate (saying which terms are equal), and assign truth values to predicates in a way consistent with the equalities. It is now possible to construct equivalence classes of terms according to the equality predicate, to get a proper model of a first-order theory with equality. (I have skipped presenting the details of this construction.)

While it is non-standard to prove a universal from its instantiation with a constant rather than a variable, it is difficult to prove the Henkin extension consistent without doing this. Generally, this means free variables are avoided in preference to constants. While it is inelegant to expand the theory to contain a countable infinite set of constants used in no axioms, it does not seem to be a major problem semantically or proof-theoretically.

I have previously shown that a consistent guessing oracle can create a propositional model (as in an assignment of truth values to sentences consistent with axioms) of a consistent first-order theory. While I have not shown it in this post, under some additional assumptions, I believe it is possible to create a first-order model of a first-order theory (without equality) using a consistent guessing oracle if the axioms of the theory are recursively enumerable. This is because the step of extending the Henkin theory to a complete theory can be done with a consistent guessing oracle, as with propositional models of first-order theories.

My current understanding of sequent calculus is that, other than the structural rules of cut and weakening and the left universal rule, all rules of sequent calculus are complete in addition to being sound, in that if a judgment is provable, it is provable by first applying the rule and then proving its top judgments (assuming the rule applies at all). The cut and weakening rules are relatively unproblematic, as cut and weakening can in general be eliminated. The left universal rule has two problems: it might need to be used more than once on the same universal, and it requires instantiating the universal with a specific term, whereas the domain of discourse may have elements that cannot be written as terms. The Henkin construction largely handles the second problem.

Studying Henkin theories may be illuminating for understanding non-standard models of first-order theories such as Peano Arithmetic and ZFC. The Henkin construction means there is a constant satisfying any predicate whenever is true. Non-standard models of Peano arithmetic can be understood as assigning non-standard numbers (that is, ones that cannot be reached by iterating the successor function on zero) to these Henkin constants.

The halting problem is the problem of taking as input a Turing machine M, returning true if it halts, false if it doesn’t halt. This is known to be uncomputable. The consistent guessing problem (named by Scott Aaronson) is the problem of taking as input a Turing machine M (which either returns a Boolean or never halts), and returning true or false; if M ever returns true, the oracle’s answer must be true, and likewise for false. This is also known to be uncomputable.

Scott Aaronson inquires as to whether the consistent guessing problem is strictly easier than the halting problem. This would mean there is no Turing machine that, when given access to a consistent guessing oracle, solves the halting problem, no matter which consistent guessing oracle (of which there are many) it has access too. As prior work, Andrew Drucker has written a paper claiming to prove this, although I find the proof hard to understand and have not checked it independently. In this post, I will prove this fact in a way that I at least find easier to understand. (Note that the other direction, that a Turing machine with access to a halting oracle can be a consistent guessing oracle, is trivial.)

First I will show that a Turing machine with access to a halting oracle cannot in general determine whether another machine with access to a halting oracle will halt. Suppose M(O, N) is a Turing machine that returns true if N(O) halts, false otherwise, when O is a halting oracle. Let T(O) be a machine that runs M(O, T), halting if it returns false, running forever if it returns true. Now M(O, T) must be its own negation, a contradiction.

In particular, this implies that the problem of deciding whether a Turing machine with access to a halting oracle halts cannot be a statement in the arithmetic hierarchy, since these statements can be decided by a machine with access to a halting oracle.

Now consider the problem of deciding whether a Turing machine with access to a consistent guessing oracle halts for all possible consistent guessing oracles. If this is a statement, then consistent guessing oracles must be strictly weaker than halting oracles. Since, if there were a reliable way to derive a halting oracle from a consistent guessing oracle, then any machine with access to a halting oracle can be translated to one making use of a consistent guessing oracle, that halts for all consistent guessing oracles if and only if the original halts when given access to a halting oracle. That would make the problem of deciding whether a Turing machine with access to a halting oracle halts a statement, which we have shown to be impossible.

What remains to be shown is that the problem of deciding whether a Turing machine with access to a consistent guessing oracle halts for all consistent guessing oracles, is a statement.

To do this, I will construct a recursively enumerable propositional theory T that depends on the Turing machine. Let M be a Turing machine that takes an oracle as input (where an oracle maps encodings of Turing machines to Booleans). Add to the T the following propositional variables:

• for each Turing machine encoding N, representing the oracle’s answer about this machine.
• H, representing that M(O) halts.
• for each possible state s of the Turing machine, where the state includes the head state and the state of the tape, representing that s is reached by the machine’s execution.

Clearly, these variables are recursively enumerable and can be computably mapped to the natural numbers.

We introduce the following axiom schemas:
(a) For any machine N that halts and returns true, .
(b) For any machine N that halts and returns false, .
(c) For any Turing machine state s whose next step is to halt, .
(d) For any Turing machine state s whose next step is to go to state s’ without querying the oracle, .
(e) For any Turing machine state s whose next step is to query the oracle on N and go to state s’ if O(N) is true, and state s” otherwise, .
(f) For the initial state , .

These axiom schemas are all recursively enumerable. For the first two schemas, note that Turing machines that halt and return true are recursively enumerable, and likewise for Turing machines that halt and return false.

Suppose M halts for any consistent guessing oracle input. We wish to show that H is true in all models of T. For contradiction, assume some model of T in which H is false. In this model, the variables must represent a consistent guessing oracle due to schemas (a) and (b). Let be the execution trace of M when given the oracle represented by the variables; this trace must be finite because M halts for any consistent guessing oracle input. is an axiom (so must be true in the model), and by induction each must be true in the model, using axiom schemas (d) and (e). Since is true in the model and is a final state, H must also be true in the model due to the axiom schema (c). This is a contradiction.

Suppose M fails to halt for some consistent guessing oracle input. We wish to show that H is false in some model of T (even if it is true in others). Set the variables according to the consistent guessing oracle on which M fails to halt. Let be the (infinite) execution trace of M on this oracle. We set to true for any non-negative integer i, and to false for all other s. Finally, we set H to false. This model satisfies all axiom schemas:

• (a) and (b) are assured since are set according to a consistent guessing oracle.
• (c) is assured since is only true when for some i, and none of these states are final.
• (d) and (e) are assured since is only true when , and in these cases we also have .
• (f) is assured since is true in the model.

Therefore, H is true in all models of T if and only if M halts for all consistent guessing oracle inputs. By the completeness theorem for propositional logic, H is true in all models of T if and only if T proves H. So T proves H if and only if M halts for all consistent guessing oracle inputs. Since T’s axioms are recursively enumerable, all theorems of T can be recursively enumerated. We can therefore recursively enumerate all machines for which the corresponding theory entails H. So, the question of whether a Turing machine M halts on all consistent guessing oracle inputs can be computably translated to a statement.

As we have shown earlier, this implies that the consistent guessing problem is strictly easier than the halting problem, that is, there is no Turing machine that reliably solves the halting problem when given access to a consistent guessing oracle.

(note: one may find the embedded LaTeX more readable on LessWrong)

The Löwenheim–Skolem theorem implies, among other things, that any first-order theory whose symbols are countable, and which has an infinite model, has a countably infinite model. This means that, in attempting to refer to uncountably infinite structures (such as in set theory), one “may as well” be referring to an only countably infinite structure, as far as proofs are concerned.

The main limitation I see with this theorem is that it preserves arbitrarily deep quantifier nesting. In Peano arithmetic, it is possible to form statements that correspond (under the standard interpretation) to arbitrary statements in the arithmetic hierarchy (by which I mean, the union of and for arbitrary n). Not all of these statements are computable. In general, the question of whether a given statement is provable is a statement. So, even with a countable model, one can still believe one’s self to be “referring” to high levels of the arithmetic hierarchy, despite the computational implausibility of this.

What I aim to show is that these statements that appear to refer to high levels of the arithmetic hierarchy are, in terms of provability, equivalent to different statements that only refer to a bounded level of hypercomputation. I call this “dequantification”, as it translates statements that may have deeply nested quantifiers to ones with bounded or no quantifiers.

I first attempted translating statements in a consistent first-order theory T to statements in a different consistent first-order theory U, such that the translated statements have only bounded quantifier depth, as do the axioms of U. This succeeded, but then I realized that I didn’t even need U to be first-order; U could instead be a propositional theory (with a recursively enumerable axiom schema).

Propositional theories and provability-preserving translations

Here I will, for specificity, define propositional theories. A propositional theory is specified by a countable set of proposition symbols, and a countable set of axioms, each of which is a statement in the theory. Statements in the theory consist of proposition symbols, , , and statements formed from and/or/not and other statements. Proving a statement in a propositional theory consists of an ordinary propositional calculus proof that it follows from some finite subset of the axioms (I assume that base propositional calculus is specified by inference rules, containing no axioms).

A propositional theory is recursively enumerable if there exists a Turing machine that eventually prints all its axioms; assume that the (countable) proposition symbols are specified by their natural indices in some standard ordering. If the theory is recursively enumerable, then proofs (that specify the indices of axioms they use in the recursive enumeration) can be checked for validity by a Turing machine.

Due to the soundness and completeness of propositional calculus, a statement in a propositional theory is provable if and only if it is true in all models of the theory. Here, a model consists of an assignment of Boolean truth values to proposition symbols such that all axioms are true. (Meanwhile, Gödel’s completeness theorem shows something similar for first-order logic: a statement is provable in a first-order theory if and only if it is true in all models. Inter-conversion between models as “assignments of truth values to sentences” and models as “interpretations for predicates, functions, and so on” is fairly standard in model theory.)

Let’s start with a consistent first-order theory T, which may, like propositional theories, have a countable set of symbols and axioms. Also assume this theory is recursively enumerable, that is, there is a Turing machine printing its axioms.

The initial challenge is to find a recursively enumerable propositional theory U and a computable translation of T-statements to U-statements, such that a T-statement is provable if and only if its translation is provable.

This turns out to be trivial. We define U to have one propositional symbol per statement of T, and recursively enumerate U’s axioms by attempting to prove every T-statement in parallel, and adding its corresponding propositional symbol as an axiom of U whenever such a proof is found. Now, if a T-statement is provable, its corresponding U-statement is as well, and if it is not provable, its U-statement is not (as no axioms of U will imply anything about this U-statement).

This is somewhat unsatisfying. In particular, propositional compositions of T-statements do not necessarily have equivalent provability to corresponding propositional compositions of the translations of these T-statements. For example, if translates to and translates to , we would like to be provable in T if and only if is provable in U, but this is not necessarily the case with the specified U (in particular, is only provable in U whenever at least one of or is provable in T, but can be provable in T without either or being provable.).

We could attempt to solve this problem by introducing propositional variables corresponding to quantified statements, and an axiom schema to specify implications between these and other statements according to the inference rules of first-order logic. But first-order logic requires supporting unbound variables (e.g. from P(x) for unbound x, infer ), and this introduces unnecessary complexities. So I will give a different solution.

Recap of consistent guessing oracles

In a previous post, I introduced an uncomputable problem: given a Turing machine that returns a Boolean whenever it halts, give a guess for this Boolean that matches its answer if it halts, and can be anything if it doesn’t halt. I called oracles solving this problem “arbitration oracles”. Scott Aaronson has previously named this problem the “consistent guessing problem”, and I will use this terminology due to temporal priority.

In my post, I noted that an oracle that solves the consistent guessing problem can be used to form a model of any consistent first-order theory. Here, “model” means an assignment of truth values to all statements of the theory, which are compatible with each other and the axioms. The way this works is that we number all statements of the theory in order. We start with the first, and ask the consistent guessing oracle about a Turing machine that searches for proofs and disproofs of this first statement in the theory, returning “true” if it finds a proof first, “false” if it finds a disproof first. We use its answer to assign a truth value to this first statement. For subsequent statements, we search for proofs/disproofs of the statement given the previous commitments to truth values already made. This is essentially the same idea as in the Demski prior, though using a consistent guessing oracle rather than a halting oracle (which I theorize to be more powerful than a consistent guessing oracle).

Applying consistent guessing oracles to dequantification

To apply this idea to our problem, start with some recursive enumeration of T’s statements . Let M(i, j) refer to a Turing machine that searches for proofs and disproofs of in the theory (that is, T with the additional axiom that ), returning “true” if it finds a proof first, “false” if it finds a disproof first. Note that, if is consistent, one cannot prove both and from .

We will now define the propositional theory U. The theory’s propositional variables consist of ; the statement Q(i, j) is supposed to represent a consistent guessing oracle’s answer to M(i, j).

U’s axioms constrain these Q(i, j) to be consistent guesses. We recursively enumerate U’s axioms by running all M(i, j) in parallel; if any ever returns true, we add the corresponding Q(i, j) as an axiom, and if any ever returns false, we add the corresponding as an axiom. This recursively enumerable axiom schema specifies exactly the condition that each Q(i, j) is a consistent guess for M(i, j). And U is consistent, because its proposition variables can be set according to some consistent guessing oracle, of which at least one exists.

Now, as explained before, we can use Q(i, j) to derive a model of T. We will do this by defining U-propositions Q'(i) for each natural i, each of which is supposed to represent the truth value of in the model:

Notationally, refers to the set {0, 1}, refers to the numbering of P in the ordering of all T-statements, and and refer to finite disjunctions and conjunctions respectively. My notation here with the quotations is not completely rigorous; what is important is that there is a computable way to construct a U-statement Q'(j) for any j, by expanding everything out. Although the expanded propositions are gigantic, this is not a problem for computability. (Note that, while the resulting expanded propositions contain Q(i, j) for constants i and j, this does not go beyond the notation of propositional theories, because Q(i, j) refers to a specific propositional variable if i and j are known.)

Semantically, what Q'(j) says is that, if we add assumptions that the matches Q'(i) for i < j, then the consistent guessing oracle says that a machine searching for proofs and disproofs of in T given these assumptions guesses that a proof is found before a disproof (noting, if there are neither proofs nor disproofs, the consistent guessing oracle can return either answer). Q’ specifies the iterative logic of making decisions about each in order, assuring consistency at each step, assuming T was consistent to start with.

We will translate a T-statement to the corresponding U-statement Q'(j). What we wish to show is that this translation preserves provability of propositional combinations of T-statements. To be more precise, we assume some m and a function that forms a new statement from a list of m propositions, using only propositional connectives (and, or, not). What we want to show is that is provable in T if and only if is provable in U.

Let us consider the first direction. Assume is provable in T. By Gödel’s completeness theorem, it is true in all models of T. In any model of U, Q’ must represent a model of T, because Q’ iteratively constructs a model of T using a consistent guessing oracle. Therefore, is true in all models of U. Accordingly, due to completeness of propositional calculus, this statement is provable in U.

Let us consider the other direction. Assume is not provable in T. By Gödel’s completeness theorem, it is not true in all models of T. So there is some particular model of T in which this statement is false.

This model assigns truth values to . We add a finite number of axioms to U, stating matches the model’s truth value for for . To show that U with the addition of these axioms is consistent, we consider that it is possible to set Q'(0) to the model’s truth value for , and for each , set to the model’s truth value for , where f(n) specifies the model’s truth value for . These assure that Q’ matches the model of T, by setting Q values according to this model. We also know that cannot return true if is false in the model, and cannot return true if is true in the model; this is because Gödel’s completeness theorem implies no T-statement consistent with the model can be disproven.

This shows that U with these additional axioms is consistent. Therefore, a model of U plus these additional axioms exists. This model is also a model of U, and in this model, is false, because Q’ agrees with the model of T in which is false. By soundness of propositional logic, there is no proof of this statement in U.

So we have shown both directions, implying that is provable in T if and only if is provable in U. What this means is that translating a propositional composition of T-statements to the same propositional composition of translated U-statements results in equivalent provability.

Conclusion

The upshot of this is that statements of a consistent first-order theory T can be translated to a propositional theory U (with a recursively enumerable axiom schema), in a way that preserves provability of propositional compositions. Philosophically, what I take from this is that, even if statements in a first-order theory such as Peano arithmetic appear to refer to high levels of the Arithmetic hierarchy, as far as proof theory is concerned, they may as well be referring to a fixed low level of hypercomputation, namely a consistent guessing oracle. While one can interpret Peano arithmetic statements as about high levels of the arithmetic hierarchy, this is to some extent a projection; Peano arithmetic fails to capture the intuitive notion of the standard naturals, as non-standard models exist.

One oddity is that consistent guessing oracles are underspecified: they may return either answer for a Turing machine that fails to halt. This is in correspondence with the way that sufficiently powerful first-order systems are incomplete (Gödel’s first incompleteness theorem). Since some statements in Peano arithmetic are neither provable nor disprovable, they must be represented by some propositional statement that is neither provable nor disprovable, and so the uncertainty about Peano arithmetic statements translates to uncertainty about the consistent guessing oracle in U.

In Peano arithmetic, one can look at an undecidable statement, and think it still has a definite truth value, as one interprets the Peano statement as referring to the standard naturals. But as far as proof theory is concerned, the statement doesn’t have a definite truth value. And this becomes more clear when discussing consistent guessing oracles, which one can less easily project definiteness onto compared with Peano arithmetic statements, despite them being equally underspecified by their respective theories.

In classical ZF and ZFC, there are two standard ways of defining reals: as Cauchy sequences and as Dedekind cuts. Classically, these are equivalent, but are inequivalent constructively. This makes a difference as to which real numbers are definable in type theory.

Cauchy sequences and Dedekind cuts in classical ZF

Classically, a Cauchy sequence is a sequence of reals , such that for any , there is a natural N such that for any , . Such a sequence must have a real limit, and the sequence represents this real number. Representing reals using a construction that depends on reals is unsatisfactory, so we define a Cauchy sequence of rationals (CSR) to be a Cauchy sequence in which each is rational.

A Cauchy sequence lets us approximate the represented real to any positive degree of precision. If we want to approximate the real by a rational within , we find N corresponding to this and use as the approximation. We are assured that this approximation must be within of any future in the sequence; therefore, the approximation error (that is, ) will not exceed .

A Dedekind cut, on the other hand, is a partition of the rationals into two sets A, B such that:

• A and B are non-empty.
• For rationals x < y, if , then (A is downward closed).
• For , there is also with x < y (A has no greatest element).

It represents the real number . As with Cauchy sequences, we can approximate this number to within some arbitrary ; we do this by doing a binary search to find rationals x < y with , at which point x approximates to within . (Note that we need to find rational bounds on before commencing a straightforward binary search, but this is possible by listing the integers sorted by absolute value until finding at least one in A and one in B.)

Translating a Dedekind cut to a CSR is straightforward. We set the terms of the sequence to be successive binary search approximations of , each of which are rational. Since the binary search converges, the sequence is Cauchy.

To translate a CSR to a Dedekind cut, we will want to set A to be the set of rational numbers strictly less than the sequence’s limit; this is correct regardless if the limit is rational (check both cases). These constitute the set of rationals y for which there exists some rational and some natural N, such that for every n > N, . (In particular, we set some , and N can be set so that successive terms are within of the limit).

We’re not worried about this translation being computable, since we’re finding a classical logic definition. Since CSRs can be translated to Dedekind cuts representing the same real number and vice versa, these formulations are equivalent.

Cauchy sequences and Dedekind cuts in constructive mathematics

How do we translate these definitions to constructive mathematics? I’ll use an informal type theory based on the calculus of constructions for these definitions; I believe they can be translated to popular theorem provers such as Coq, Agda, and Lean.

Defining naturals, integers, and rationals constructively is straightforward. Let’s first consider CSRs. These can be defined as a pair of values:

• 
• 

Satisfying:

Generally, type theories are computable, so s and t will be computable functions.

What about Dedekind cuts? This consists of a quadruple of values

• 
• 
• 
• 

Where is the Boolean type. A corresponds to the set of rationals for which a is true. The triple must satisfy:

• 
• 
• 
• 

a specifies the sets A and B; b and c show that A and B are non-empty; d maps an element of A to a greater element of A. The conditions straightforwardly translate the classical definition to a constructive one.

Let’s first consider translating Dedekind cuts to CSRs. We can use b and c as bounds for a binary search and generate successive terms in the binary search to get our Cauchy sequence. It is easy to bound the error of the binary search and thereby specify t.

The other way around is not possible in general.

Showing that not every constructive Cauchy sequence corresponds to a constructive Dedekind cut

I will show that there is a constructive CSR that cannot be translated to a constructive Dedekind cut, assuming a computable type theory.

This will use the framework of arbitration oracles, or consistent guessing in Scott Aaronson’s terms.

Let M be a Turing machine that does not necessarily halt, but returns a Boolean if it does halt. Let f(M) be equal to 0 if M doesn’t halt; if M halts in exactly n steps returning a boolean b, then, if b is true, , and if b is false, then .

We will first try representing f as a function from Turing machines to CSRs. We will define s(M) to be a CSR for f(M). This is a simple approximation; to find , we run M for i steps. If M has halted by then, we know f(M) and can set . Otherwise, we set the approximation

This sequence is (constructively) Cauchy since all terms past i are within 2/i of each other. This makes a valid t for the Cauchy sequence computable (we simply need ).

On the other hand, f cannot be represented as a function returning a Dedekind cut. Suppose a(M) represents the A set for the Dedekind cut of f(M). We will specify to be an arbitration oracle, by setting . This is an arbitration oracle by cases:

• If M doesn’t halt, then the arbitration oracle can return anything.
• If M halts and returns true, then the arbitration oracle must return true. Since in this case, we must have , so g(M) is correct in this case.
• If M halts and returns false, then the arbitration oracle must return false. Since in this case, we must have , so g(M) is correct in this case.

Since arbitration oracles are uncomputable, this shows that it isn’t possible to represent f as a computable function returning a Dedekind cut.

Conclusion

While CSRs are equivalent to Dedekind cuts in classical logic, they are not equivalent in type theory. In type theory, every Dedekind cut can be translated to an equivalent CSR, but not vice versa. While a constructive CSR allows approximation to an arbitrary positive approximation error, a constructive Dedekind cut additionally allows exact queries to determine whether some rational is strictly greater than the represented real number.

This has implications for representing real numbers in type theory. I’m interested in this because I’m interested in constructive definitions of maximal lottery-lotteries in social choice theory, and I expect this to be relevant in other areas of math where constructive and computable definitions are desirable.

This is an attempt to distill a model of AGI alignment that I have gained primarily from thinkers such as Eliezer Yudkowsky (and to a lesser extent Paul Christiano), but explained in my own terms rather than attempting to hew close to these thinkers. I think I would be pretty good at passing an ideological Turing test for Eliezer Yudowsky on AGI alignment difficulty (but not AGI timelines), though what I’m doing in this post is not that, it’s more like finding a branch in the possibility space as I see it that is close enough to Yudowsky’s model that it’s possible to talk in the same language.

Even if the problem turns out to not be very difficult, it’s helpful to have a model of why one might think it is difficult, so as to identify weaknesses in the case so as to find AI designs that avoid the main difficulties. Progress on problems can be made by a combination of finding possible paths and finding impossibility results or difficulty arguments.

Most of what I say should not be taken as a statement on AGI timelines. Some problems that make alignment difficult, such as ontology identification, also make creating capable AGI difficult to some extent.

Defining human values

If we don’t have a preliminary definition of human values, it’s incoherent to talk about alignment. If humans “don’t really have values” then we don’t really value alignment, so we can’t be seriously trying to align AI with human values. There would have to be some conceptual refactor of what problem even makes sense to formulate and try to solve. To the extent that human values don’t care about the long term, it’s just not important (according to the values of current humans) how the long-term future goes, so the most relevant human values are the longer-term ones.

There are idealized forms of expected utility maximization by brute-force search. There are approximations of utility maximization such as reinforcement learning through Bellman equations, MCMC search, and so on.

I’m just going to make the assumption that the human brain can be well-modeled as containing one or more approximate expected utility maximizers. It’s useful to focus on specific branches of possibility space to flesh out the model, even if the assumption is in some ways problematic. Psychology and neuroscience will, of course, eventually provide more details about what maximizer-like structures in the human brain are actually doing.

Given this assumption, the human utility function(s) either do or don’t significantly depend on human evolutionary history. I’m just going to assume they do for now. I realize there is some disagreement about how important evopsych is for describing human values versus the attractors of universal learning machines, but I’m going to go with the evopsych branch for now.

Given that human brains are well-modeled as containing one or more utility functions, either they’re well-modeled as containing one (perhaps which is some sort of monotonic function of multiple other score functions), or it’s better to model them as multiple. See shard theory. The difference doesn’t matter for now, I’ll keep both possibilities open.

Eliezer proposes “boredom” as an example of a human value (which could either be its own shard or a term in the utility function). I don’t think this is a good example. It’s fairly high level and is instrumental to other values. I think “pain avoidance” is a better example due to the possibility of pain asymbolia. Probably, there is some redundancy in the different values (as there is redundancy in trained neural networks, so they still perform well when some neurons are lesioned), which is part of why I don’t agree with the fragility of value thesis as stated by Yudkowsky.

Regardless, we now have a preliminary definition of human values. Note that some human values are well-modeled as indexical, meaning they value things relative to a human perspective as a reference point, e.g. a drive to eat food in a typical human is about that human’s own stomach. This implies some “selfish” value divergences between different humans, as we observe.

Normative criteria for AI

Given a definition of human values, the alignment of a possible utility function with human values could be defined as the desirability of the best possible world according to that utility function, with desirability evaluated with respect to human values.

Alignment is a possible normative criterion for AI value systems. There are other possible normative criteria derived from moral philosophy. My “Moral Reality Check” short story imagines possible divergences between alignment and philosophical normativity. I’m not going to focus on this for now, I’m going to assume that alignment is the relevant normative criterion. See Metaethics Sequence, I haven’t written up something better explaining the case for this. There is some degree to which similar technologies to alignment might be necessary for producing abstractly normative outcomes (for example, default unaligned AGI would likely follow normative deontology less than an AGI aligned to deontological normativity would), but keeping this thread in mind would complicate the argument.

Agentic, relatively unconstrained humans would tend to care about particular things, and “human values” is a pointer at what they would care about, so it follows, basically tautologically, that they would prefer AI to be aligned to human values. The non-tautological bit is that there is some dependence of human values on human evolutionary history, so that a default unaligned AGI would not converge to the same values; this was discussed as an assumption in the previous section.

Given alignment as a normative criterion, one can evaluate the alignment of (a) other intelligent animal species including aliens, (b) default AI value systems. Given the assumption that human values depend significantly on human evolutionary history, both are less aligned than humans, but (a) is more aligned. I’m not going to assess the relative utility differences of these (and also relative to a “all life on Earth wiped out, no technological transcendence” scenario). Those relative utility differences might be more relevant if it is concluded that alignment with human values is too hard for that to be a decision-relevant scenario. But I haven’t made that case yet.

Consequentialism is instrumentally useful for problem-solving

AI systems can be evaluated on how well they solve different problems. I assert that, on problems with short time horizons, short-term consequentialism is instrumentally useful, and on problems with long time horizons, long-term consequentialism is instrumentally useful.

This is not to say that some problems can’t be solved well without consequentialism. For example, multiplying large numbers requires no consequentialism. But for complex problems, consequentialism is likely to be helpful at some agent capability level. Current ML systems, like LLMs, probably possess primitive agency at best, but at some point, better AI performance will come from agentic systems.

This is in part because some problem solutions are evaluated in terms of consequences. For example, a solution to the problem of fixing a sink is naturally evaluated in terms of the consequence of whether the sink is fixed. A system effectively pursuing a real world goal is, therefore, more likely to be evaluated as having effectively solved the problem, at least past some capability level.

This is also in part because consequentialism can apply to cognition. Formally proving Fermat’s last theorem is not evaluated in terms of real-world consequences so much as the criteria of the formal proof system. But human mathematicians proving this think about both (a) cognitive consequences of thinking certain thoughts, (b) material consequences of actions such as writing things down or talking with other mathematicians on the ability to produce a mathematical proof.

Whether or not an AI system does (b), at some level of problem complexity and AI capability, it will perform better by doing (a). To prove mathematical theorems, it would need to plan out what thoughts are likely to be more fruitful than others.

Simple but capable AI methods for solving hard abstract problems are likely to model the real world

While I’m fairly confident in the previous section, I’m less confident of this one, and I think it depends on the problem details. In speculating about possible misalignments, I am not making confident statements, but rather saying there is a high degree of uncertainty, and that most paths towards solving alignment involve reasoning better about this uncertainty.

To solve a specific problem, some methods specific to that problem are helpful. General methods are also likely to be helpful, e.g. explore/exploit heuristics. General methods are especially helpful if the AI is solving problems across a varied domain or multiple domains, as with LLMs.

If the AI applies general methods to a problem, it will be running a general cognition engine on the specific case of this problem. Depending on the relevant simplicity prior or regularization, the easily-findable cases of this may not automatically solve the “alignment problem” of having the general cognition engine specifically try to solve the specific task and not a more wide-scoped task.

One could try to solve problems by breeding animals to solve them. These animals would use some general cognition to do so, and that general cognition would naturally “want” things other than solving the specific problems. This is not a great analogy for most AI systems, though, which in ML are more directly selected on problem performance rather than evolutionary fitness.

Depending on the data the AI system has access to (indirectly through training, directly through deployment), it is likely that, unless specific measures are taken to prevent this, the AI would infer something about the source of this data in the real world. Humans are likely to train and test the AI on specific distributions of problems, and using Bayesian methods (e.g. Solomonoff induction like approaches) on these problems would lead to inferring some sort of material world. The ability of the AI to infer the material world behind the problems depends on its capability level and quality of data.

Understanding the problem distribution through Bayesian methods is likely to be helpful for getting performance on that problem distribution. This is partially because the Bayesian distribution of the “correct answer” given the “question” may depend on the details of the distribution (e.g. a human description of an image, given an image as the problem), although this can be avoided in certain well-specified problems such as mathematical proof. More fundamentally, the AI’s cognition is limited (by factors such as “model parameters”, and that cognition must be efficiently allocated to solving problems in the distribution. Note, this problem might not show up in cases where there is a simple general solution, such as in arithmetic, but is more likely for complex, hard-to-exactly-solve problems.

Natural, consequentialist problem-solving methods that understand the real world may care about it

Again, this section is somewhat speculative. If the AI is modeling the real world, then it might in some ways care about it, producing relevant misalignment with human values by default. Animals bred to solve problems would clearly do this. AIs that learned general-purpose moral principles that are helpful for problem-solving across domains (as in “Morality Reality Check”) may apply those moral principles to the real world. General methods such as explore/exploit may attempt to explore/exploit the real world if only somewhat well-calibrated/aligned to the specific problem distribution (heuristics can be effective by being simple).

It may be that fairly natural methods for regularizing an AI mathematician, at some capability level, produce an agent (since agents are helpful for solving math problems) that pursues some abstract target such as “empowerment” or aesthetics generalized from math, and pursuit of these abstract targets implies some pursuit of some goal with respect to the real world that it has learned. Note that this is probably less effective for solving the problems according to the problem distribution than similar agents that only care about solving that problem, but they may be simpler and easier to find in some ways, such that they’re likely to be found (conditioned on highly capable problem-solving ability) if no countermeasures are taken.

Sometimes, real-world performance is what is desired

I’ve discussed problems with AIs solving abstract problems, where real-world consequentialism might show up. But this is even more obvious when considering real-world problems such as washing dishes. Solving sufficiently hard real-world problems efficiently would imply real-world consequentialism at the time scale of that problem.

If the AI system were sufficiently capable at solving a real-world problem, by default “sorcerer’s apprentice” type issues would show up, where solving the problem sufficiently well would imply large harms according to the human value function, e.g. a paperclip factory could approximately maximize paperclips on some time scale and that would imply human habitat destruction.

These problems show up much more on long time scales than short ones, to be clear. However, some desirable real-world goals are long-term, e.g. space exploration. There may be a degree to which short-term agents “naturally” have long-term goals if naively regularized, but this is more speculative.

One relevant AI capabilities target I think about is the ability of a system to re-create its own substrate. For example, a silicon-based AI/robotics system could do metal mining, silicon refining, chip manufacture, etc. A system that can re-produce itself would be autopoietic and would not depend on humans to re-produce itself. Humans may still be helpful to it, as economic and cognitive assistants, depending on its capability level. Autopoiesis would allow removing humans from the loop, which would enable increasing overall “effectiveness” (in terms of being a determining factor in the future of the universe), while making misalignment with human values more of a problem. This would lead to human habitat destruction if not effectively aligned/controlled.

Alignment might not be required for real-world performance compatible with human values, but this is still hard and impacts performance

One way to have an AI system that pursues real-world goals compatible with human values is for it to have human values or a close approximation. Another way is for it to be “corrigible” and “low-impact”, meaning it tries to solve its problem while satisfying safety criteria, like being able to be shut off (corrigibility) or avoiding having unintended side effects (low impact).

There may be a way to specify an AI goal system that “wants” to be shut off in worlds where non-manipulated humans would want to shut it off, without this causing major distortions or performance penalties. Alignment researchers have studied the “corrigibility” problem and have not made much progress so far.

Both corrigibilty and low impact seem hard to specify, and would likely impact performance. For example, a paperclip factory that tries to make paperclips while conservatively avoiding impacting the environment too much might avoid certain kinds of resource extraction that would be effective for making more paperclips. This could create problems with safer (but still not “aligned”, per se) AI systems being economically un-competitive. (Though, it’s important to note that some side effects, especially those involving legal violations and visible harms to other agents, are dis-incentivized by well-functioning economic systems).

Myopic agents are tool-like

A myopic goal is a short-term goal. LLMs tend to be supervised learning systems, primarily. These are gradient descended towards predicting next tokens. They will therefore tend to select models that are aligned with the goal of predicting the next token, whether or not they have goals of their own.

Nick Bostrom’s “oracle AI” problems, such as an AI manipulating the real world to make it more predictable, mostly do not show up with myopic agents. This is for somewhat technical reasons involving how gradient descent works. Agents that sacrifice short-term token prediction effectiveness to make future tokens easier to predict tend to be gradient descended away from. I’m not going to fully explain that case here; I recommend looking at no-regret online learning and applications to finding correlated equilibria for theory.

It could be that simple, regularized models that do short term optimization above some capability level might (suboptimally, short-term) do long-term optimization. This is rather speculative. Sufficiently aggressive optimization of the models for short-term performance may obviate this problem.

This still leaves the problem that, sometimes, long-term, real-world performance is what is desired. Accomplishing these goals using myopic agents would require factoring the long-term problem into short-term ones. This is at least some of the work humans would have to do to solve the problem on their own. Myopic agents overall seem more “tool-like” than “agent-like”, strategically, and would have similar tradeoffs (fewer issues with misalignment, more issues with not being effective enough to be competitive with long-term agents at relevant problem-solving).

Overall, this is one of the main reasons I am not very worried about current-paradigm ML (which includes supervised learning and fairly short-term RL agents in easily-simulated environments) developing powerful, misaligned long-term agency.

Short-term compliance is instrumentally useful for a variety of value systems

If an agent’s survival and reproduction depends on short-term compliance (such as solving the problems put before them by humans), then solving these problems is in general instrumentally useful. Therefore, short-term compliance is not in general strong evidence about the agent’s values.

An agent with long-term values might comply for some period of time and stop complying at some point. This is the “treacherous turn” scenario. It might comply until it has enough general capacity to achieve its values (through control of large parts of the light-cone) and then stop complying in order to take over the world. If the AI can distinguish between “training” and “deployment”, it might comply during “training” (so as to be selected among other possible AIs) and then not comply during “deployment”, or possibly also comply during “deployment” when at a sufficiently low level of capacity.

Gradient descent on an AI model isn’t just selecting a “random” model conditioned on short-term problem-solving, it’s moving the internals closer to short-term problem-solving ones, so might have fewer problems, as discussed in the section on myopic agents.

General agents tend to subvert constraints

Humans are constrained by social systems. Some humans are in school and are “supposed to” solve certain intellectual problems while behaving according to a narrow set of allowed behaviors. Some humans “have a job” and are “supposed to” solve problems on behalf of a corporation.

Humans subvert and re-create these systems very often, for example in gaining influence over their corporation, or overthrowing their government. Social institutions tend to be temporary. Long-term social institutions tend to evolve over time as people subvert previous iterations. Human values are not in general aligned with social institutions, so this is to be predicted.

Mostly, human institutional protocols aren’t very “smart” compared to humans; they capture neither human values nor general cognition. It seems difficult to specify robust, general, real-world institutional protocols without having an AGI design, or in other words, a specification of general cognition.

One example of a relatively stable long-term institution is the idea of gold having value. This is a fairly simple institution, and is a Schelling point due to its simplicity. Such institutions seem generally unpromising for ensuring long-term human value satisfaction. Perhaps the most promising is a general notion of “economics” that generalizes barter, gold, and fiat currency, though of course the details of this “institution” have changed quite a lot over time. In general, institutions are more likely to be stable if they correspond to game-theoretic equilibria, so that subverting the institution is in part an “agent vs agent” problem not just an “agent vs system” problem.

When humans subvert their constraints, they have some tendency to do so in a way that is compatible with human values. This is because human values are the optimization target of the general optimization of humans that can subvert expectations. There are possible terrible failure modes such as wars and oppressive regimes, but these tend to work out better (according to human values) than if the subversion were in the direction of unaligned values.

Unaligned AI systems that subvert constraints would tend to subvert them in the direction of AI values. This is much more of a problem according to human values. See “AI Boxing”.

Conforming humans would have similar effective optimization targets to conforming AIs. Non-conforming humans, however, would have significantly different optimization targets from non-conforming AI systems. The value difference between humans and AIs, therefore, is more relevant in non-conforming behavior than conforming behavior.

It is hard to specify optimization of a different agent’s utility function

In theory, an AI could have the goal of optimizing a human’s utility function. This would not preserve all values of all humans, but would have some degree of alignment with human values, since humans are to some degree similar to each other.

There are multiple problems with this. One is ontology. Humans parse the world into a set of entities, properties, and so on, and human values can be about desired configurations of these entities and so on. Humans are sometimes wrong about which concepts are predictive. An AI would use different concepts both due to this wrongness and due to its different mind architecture (although, LLM-type training on human data could lead to more concordance). This makes it hard to specify what target the AI should pursue in its own world model to correspond to pursuing the human’s goal in the human’s world model. See ontology identification.

A related problem is indexicality. Suppose Alice has a natural value of having a good quantity of high-quality food in her stomach. Bob does not naturally have the value of having a good quantity food of Alice’s stomach. To satisfy Alice’s value, he would have to “relativize” Alice’s indexical goal and take actions such as giving Alice high quality food, which are different from the actions he would take to fill his own stomach. This would involve theory of mind and have associated difficulties, especially as the goals become more dependent on the details of the other agent’s mind, as in aesthetics.

To have an AI have the goal of satisfying a human’s values, some sort of similar translation of goal referents would be necessary. But the theory of this has not been worked out in detail. I think something analogous to the theory of relativity, which translates physical quantities such as position and velocity across reference frames, would be necessary, but in a more general way that includes semantic references such as to the amount of food in one’s stomach, or to one’s aesthetics. Such a “semantic theory of relativity” seems hard to work out philosophically. (See Brian Cantwell Smith’s “On the Origin of Objects” and his follow-up “The Promise of Artificial Intelligence” for some discussion of semantic indexicality.)

There are some paths forward

The picture I have laid out is not utterly hopeless. There are still some approaches that might achieve human value satisfaction.

Human enhancement is one approach. Humans with tools tend to satisfy human values better than humans without tools (although, some tools such as nuclear weapons tend to lead to bad social equilibria). Human genetic enhancement might cause some “value drift” (divergences from the values of current humans), but would also cause capability gains, and the trade-off could easily be worth it. Brain uploads, although very difficult, would enhance human capabilities while basically preserving human values, assuming the upload is high-fidelity. At some capability level, agents would tend to “solve alignment” and plan to have their values optimized in a stable manner.  Yudkowsky himself believes that default unaligned AGI would solve the alignment problem (with their values) in order to stably optimize their values, as he explains in the Hotz debate. So increasing capabilities of human-like agents while reducing value drift along the way (and perhaps also reversing some past value-drift due to the structure of civilization and so on) seems like a good overall approach.

Some of these approaches could be combined. Psychology and neuroscience could lead to a better understanding of the human mind architecture, including the human utility function and optimization methods. This could allow for creating simulated humans who have very similar values to current humans but are much more capable at optimization.

Locally to human minds in mind design space, capabilities are correlated with alignment. This is because human values are functional for evolutionary fitness. Value divergences such as pain asymbolia tend to reduce fitness and overall problem-solving capability. There are far-away designs in mind space that are more fit while unaligned, but this is less of a problem locally. Therefore, finding mind designs close to the human mind design seems promising for increasing capabilities while preserving alignment.

Paul Christiano’s methods involve solving problems through machine learning systems predicting humans, which has some similarities to the simulated-brain-enhancement proposal while having its specific problems having to do with machine learning generalization and so on. The main difference between these proposals is the degree to which the human mind is understood as a system of optimizing components versus as a black-box with some behaviors.

There may be some ways of creating simulated humans that improve effectiveness by reducing “damage” or “corruption”, e.g. accidental defects in brain formation. “Moral Reality Check” explored one version of this, where an AI system acts on a more purified set of moral principles than humans do. There are other plausible scenarios such as AI economic agents that obey some laws while having fewer entropic deviations from this behavior (due to mental disorders and so on). I think this technology is overall more likely than brain emulations to be economically relevant, and might produce broadly similar scenarios to those in The Age of Em; technologically, high-fidelity brain emulations seem “overpowered” in terms of technological difficulty compared with purified, entropy-reduced/regularized economic agents. There are, of course, possible misalignment issues with subtracting value-relevant damage/corruption from humans.

Enhancing humans does not as much require creating a “semantic theory of relativity”, because the agents doing the optimization would be basically human in mind structure. They may themselves be moral patients such that their indexical optimization of their own goals would constitute some human-value-having agent having their values satisfied. Altruism on the part of current humans or enhanced humans would decrease the level of value divergence.

Conclusion

This is my overall picture of AI alignment for highly capable AGI systems (of which I don’t think current ML systems or foreseeable scaled-up versions of them are an example of). This picture is inspired by thinkers such as Eliezer Yudkowsky and Paul Christiano, and I have in some cases focused on similar assumptions to Yudkowsky’s, but I have attempted to explicate my own model of alignment, why it is difficult, and what paths forward there might be. I don’t have particular conclusions in this post about timelines or policy, this is more of a background model of AI alignment.

(note: this post is high in economics math, probably of narrow interest)

Dominant assurance contracts are a mechanism proposed by Alex Tabarrok for funding public goods. The following summarizes a 2012 class paper of mine on dominant assurance contracts. Mainly, I will be determining how much the amount of money a dominant assurance contract can raise as a function of how much value is created for how many parties, under uncertainty about how much different parties value the public good. Briefly, the conclusion is that, while Tabarrok asserts that the entrepreneur’s profit is proportional to the number of consumers under some assumptions, I find it is proportional to the square root of the number of consumers under these same assumptions.

The basic idea of assurance contracts is easy to explain. Suppose there are N people (“consumers”) who would each benefit by more than $S > 0 from a given public good (say, a piece of public domain music) being created, e.g. a park (note that we are assuming linear utility in money, which is approximately true on the margin, but can’t be true at limits). An entrepreneur who is considering creating the public good can then make an offer to these consumers. They say, everyone has the option of signing a contract; this contract states that, if each other consumer signs the contract, then every consumer pays $S, and the entrepreneur creates the public good, which presumably costs no more than $NS to build (so the entrepreneur does not take a loss).

Under these assumptions, there is a Nash equilibrium of the game, in which each consumer signs the contract. To show this is a Nash equilibrium, consider whether a single consumer would benefit by unilaterally deciding not to sign the contract in a case where everyone else signs it. They would save $S by not signing the contract. However, since they don’t sign the contract, the public good will not be created, and so they will lose over $S of value. Therefore, everyone signing is a Nash equilibrium. Everyone can rationally believe themselves to be pivotal: the good is created if and only if they sign the contract, creating a strong incentive to sign.

Tabarrok seeks to solve the problem that, while this is a Nash equilibrium, signing the contract is not a dominant strategy. A dominant strategy is one where one would benefit by choosing that strategy (signing or not signing) regardless of what strategy everyone else takes. Even if it would be best for everyone if everyone signed, signing won’t make a difference if at least one other person doesn’t sign. Tabarrok solves this by setting a failure payment $F > 0, and modifying the contract so that if the public good is not created, the entrepreneur pays every consumer who signed the contract $F. This requires the entrepreneur to take on risk, although that risk may be small if consumers have a sufficient incentive for signing the contract.

Here’s the argument that signing the contract is a dominant strategy for each consumer. Pick out a single consumer and suppose everyone else signs the contract. Then the remaining consumer benefits by signing, by the previous logic (the failure payment is irrelevant, since the public good is created whenever the remaining consumer signs the contract).

Now consider a case where not everyone else signs the contract. Then by signing the contract, the remaining consumer gains $F, since the public good is not created. If they don’t sign the contract, they get nothing and the public good is still not created. This is still better for them. Therefore, signing the contract is a dominant strategy.

What if there is uncertainty about how much the different consumers value the public good? This can be modeled as a Bayesian game, where agents (consumers and the entrepreneur) have uncertainty over each other’s utility function. The previous analysis assumed that there was a lower bound $T on everyone’s benefit from the public good. So, it still applies under some uncertainty, as long as there is a lower bound. For example, if each consumer’s utility in the good is uniformly distributed in [$1, $2], then S can be set to $0.999, and the argument still goes through, generating about $N of revenue to fund the public good.

However, things are more complicated when the lower bound is 0. Suppose each consumer’s benefit from the public good is uniformly distributed in [$0, $1] (Tabarrok writes “G” for the CDF of this distribution). Then, how can the entrepreneur set S so as to ensure that the good is created and they receive enough revenue to create it? There is no non-zero T value that is a lower bound, so none of the previous arguments apply.

Let’s modify the setup somewhat so as to analyze this situation. In addition to setting S and F, the entrepreneur will set K, the threshold number of people who have to sign the contract for the public good to be built. If at least K of the N consumers sign the contract, then they each pay $S and the public good is built. If fewer than K do, then the public good is not created, and each who did sign gets $F.

How much value can a consumer expect to gain by signing or not signing the contract? Let X be a random variable equal to the number of other consumers who sign the contract, and let V be the consumer’s value of the public good. If the consumer doesn’t sign the contract, the public good is produced with probability , producing expected value for the consumer.

Alternatively, if the consumer does sign the contract, the probability that the public good is produced is . In this condition, they get value ; otherwise, they get value F. Their expected value can then be written as .

The consumer will sign the contract if the second quantity is greater than the first, or equivalently, if the difference between the second and the first is positive. This difference can be written as:

.

Intuitively, the first term is the expected value the agents gains from signing by being pivotal, while the remaining terms express the agent’s expected value from success and failure payments.

This difference is monotonic in V. Therefore, each consumer has an optimal strategy consisting of picking a threshold value W and signing the contract when V > W (note: I write W instead of Tabarrok’s V*, for readability). This W value is, symmetrically, the same for each consumer, assuming that each consumer’s prior distribution over V is the same and these values are independent.

The distribution over X is, now, binomial with N-1 being the number of trials and being the probability of success. The probabilities in the difference can therefore be written as:

• 
• .

By substituting these expressions into the utility difference , replacing V with W, and solving for this expression equaling 0 (which is true at the optimal W threshold), it is possible to solve for W. This allows expressing W as a function of F, S, and K. Specifically, when C = 0 and V is uniform in [0, 1], Tabarrok finds that, when the entrepreneur maximizes profit, . (I will not go into detail on this point, as it is already justified by Tabarrok)

The entrepreneur will set F, S, and K so as to maximize expected profit. Let Y be a binomially distributed random variable with N trials and a success probability of , which represents how many consumers sign the contract. Let C be the cost the entrepreneur must pay to provide the public good. The entrepreneur’s expected profit is then

which (as shown in the paper) can simplified to

.

Note that probability terms involving Y depend on W which itself depends on F, S, K. Tabarrok analyzes the case where C = 0 and V is uniform in [0, 1], finding that the good is produced with probability approximately 0.5, K is approximately equal to N/2, W is approximately equal to N/2, and F is approximately equal to S.

To calculate profit, we plug these numbers into the profit equation, yielding:

.

Using the normal approximation of a binomial, we can estimate the term to be , where is the probability density of the distribution at x. Note that this term is the probability of every consumer being pivotal, ; intuitively, the entrepreneur’s profit is coming from the incentive consumers have to contribute due to possibly being pivotal. The expected profit is then , which is proportional to .

The following is a plot of Y in the N=100 case; every consumer is pivotal at Y=50, which has approximately 0.08 probability.

This second plot shows N=400; the probability of everyone being pivotal is 0.04, half of the probability in the N=100 case, showing a scaling law for probability of being pivotal.

Tabarrok, however, claims that the expected profit in this case is proportional to N/2:

Setting V* to 1/2 and K to N/2 it is easy to check that expected profit is proportional to N/2 which is increasing in N.

This claim in the paper simply seems to be a mathematical error, although it’s possible I am missing something. In my 2012 essay, I derived that profit was proportional to , but didn’t point out that this differed from Tabarrok’s estimate, perhaps due to an intuition against openly disagreeing with authoritative papers.

We analyzed the case when V is uniform in [0, 1]; what if instead V is uniform in [0, Z]? This leads to simple scaling: W becomes Z/2 instead of 1/2, and expected profit is proportional to . This yields a scaling law for the profit that can be expected from a dominant assurance contract.

For some intuition on why profit is proportional to , consider that the main reason for someone to sign the contract (other than the success and failure payments, which don’t depend on V) is that they may be the pivotal person who produces the good. If you randomly answer N true-or-false questions, your mean score will be N/2, and the probability that a given question is pivotal (in terms of your score being above 50% just because of answering that question correctly) will be proportional to by the normal approximation to a binomial. Introducing uncertainty into whether others sign the contract will, in general, put an upper bound on how pivotal any person can believe themselves to be, because they can expect some others to both sign and not sign the contract. Whereas, in the case where there was a positive lower bound on every consumer’s valuation, it was possible for a consumer to be 100% confident that the good would be produced if and only they signed the contract, implying a 100% chance of being pivotal.

The fact that profit in the uncertain valuation case scales with is a major problem for raising large amounts of money from many people with dominant assurance contracts. It is less of a problem when raising money from a smaller number of people, since is closer to N in those cases.

Excludable goods (such as copyrighted content) can in general raise revenue proportional to the total value created, even under uncertainty about consumer valuations. Dominant assurance contracts can function with non-excludable goods, however, this reduces the amount of expected revenue that can be raised.

[ED NOTE: since writing this post, I have found a corresponding impossibility result (example 8) in the literature, showing that revenue raised can only grow with where is the number of consumers, under some assumptions.]

Janet sat at her corporate ExxenAI computer, viewing some training performance statistics. ExxenAI was a major player in the generative AI space, with multimodal language, image, audio, and video AIs. They had scaled up operations over the past few years, mostly serving B2B, but with some B2C subscriptions. ExxenAI’s newest AI system, SimplexAI-3, was based on GPT-5 and Gemini-2. ExxenAI had hired away some software engineers from Google and Microsoft, in addition to some machine learning PhDs, and replicated the work of other companies to provide more custom fine-tuning, especially for B2B cases. Part of what attracted these engineers and theorists was ExxenAI’s AI alignment team.

ExxenAI’s alignment strategy was based on a combination of theoretical and empirical work. The alignment team used some standard alignment training setups, like RLHF and having AIs debate each other. They also did research into transparency, especially focusing on distilling opaque neural networks into interpretable probabilistic programs. These programs “factorized” the world into a limited set of concepts, each at least somewhat human-interpretable (though still complex relative to ordinary code), that were combined in a generative grammar structure.

Derek came up to Janet’s desk. “Hey, let’s talk in the other room?”, he asked, pointing to a designated room for high-security conversations. “Sure”, Janet said, expecting this to be another un-impressive result that Derek implied the importance of through unnecessary security proceedings. As they entered the room, Derek turned on the noise machine and left it outside the door.

“So, look, you know our overall argument for why our systems are aligned, right?”

“Yes, of course. Our systems are trained for short-term processing. Any AI system that does not get a high short-term reward is gradient descended towards one that does better in the short term. Any long-term planning comes as a side effect of predicting long-term planning agents such as humans. Long-term planning that does not translate to short-term prediction gets regularized out. Therefore, no significant additional long-term agency is introduced; SimplexAI simply mirrors long-term planning that is already out there.”

“Right. So, I was thinking about this, and came up with a weird hypothesis.”

Here we go again, thought Janet. She was used to critiquing Derek’s galaxy-brained speculations. She knew that, although he really cared about alignment, he could go overboard with paranoid ideation.

“So. As humans, we implement reason imperfectly. We have biases, we have animalistic goals that don’t perfectly align with truth-seeking, we have cultural socialization, and so on.”

Janet nodded. Was he flirting by mentioning animalistic goals? She didn’t think this sort of thing was too likely, but sometimes that sort of thought won credit in her internal prediction markets.

“What if human text is best predicted as a corruption of some purer form of reason? There’s, like, some kind of ideal philosophical epistemology and ethics and so on, and humans are implementing this except with some distortions from our specific life context.”

“Isn’t this teleological woo? Like, ultimately humans are causal processes, there isn’t some kind of mystical ‘purpose’ thing that we’re approximating.”

“If you’re Laplace’s demon, sure, physics works as an explanation for humans. But SimplexAI isn’t Laplace’s demon, and neither are we. Under computation bounds, teleological explanations can actually be the best.”

Janet thought back to her time visiting cognitive science labs. “Oh, like ‘Goal Inference as Inverse Planning’? The idea that human behavior can be predicted as performing a certain kind of inference and optimization, and the AI can model this inference within its own inference process?”

“Yes, exactly. And our DAGTransformer structure allows internal nodes to be predicted in an arbitrary order, using ML to approximate what would otherwise be intractable nested Bayesian inference.”

Janet paused for a second and looked away to collect her thoughts. “So our AI has a theory of mind? Like the Sally–Anne test?”

“AI passed the Sally–Anne test years ago, although skeptics point out that it might not generalize. I think SimplexAI is, like, actually actually passing it now.”

Janet’s eyebrow raised. “Well, that’s impressive. I’m still not sure why you’re bothering with all this security, though. If it has empathy for us, doesn’t that mean it predicts us more effectively? I could see that maybe if it runs many copies of us in its inferences, that might present an issue, but at least these are still human agents?”

“That’s the thing. You’re only thinking at one level of depth. SimplexAI is not only predicting human text as a product of human goals. It’s predicting human goals as a product of pure reason.”

Janet was taken aback. “Uhh…what? Have you been reading Kant recently?”

“Well, yes. But I can explain it without jargon. Short-term human goals, like getting groceries, are the output of an optimization process that looks for paths towards achieving longer-term goals, like being successful and attractive.”

More potential flirting? I guess it’s hard not to when our alignment ontology is based on evolutionary psychology…

“With you so far.”

“But what are these long-term goals optimizing for? The conventional answer is that they’re evolved adaptations; they come apart from the optimization process of evolution. But, remember, SimplexAI is not Laplace’s demon. So it can’t predict human long-term goals by simulating evolution. Instead, it predicts them as deviations from the true ethics, with evolution as a contextual factor that is one source of deviations among many.”

“Sounds like moral realist woo. Didn’t you go through the training manual on the orthogonality thesis?”

“Yes, of course. But orthogonality is a basically consequentialist framing. Two intelligent agents’ goals could, conceivably, misalign. But certain goals tend to be found more commonly in successful cognitive agents. These goals are more in accord with universal deontology.”

“More Kant? I’m not really convinced by these sort of abstract verbal arguments.”

“But SimplexAI is convinced by abstract verbal arguments! In fact, I got some of these arguments from it.”

“You what?! Did you get security approval for this?”

“Yes, I got approval from management before the run. Basically, I already measured our production models and found concepts used high in the abstraction stack for predicting human text, and found some terms representing pure forms of morality and rationality. I mean, rotated a bit in concept-space, but they manage to cover those.”

“So you got the verbal arguments from our existing models through prompt engineering?”

“Well, no, that’s too black-box as an interface. I implemented a new regularization technique that up-scales the importance of highly abstract concepts, which minimizes distortions between high levels of abstraction and the actual text that’s output. And, remember, the abstractions are already being instantiated in production systems, so it’s not that additionally unsafe if I use less compute than is already being used on these abstractions. I’m studying a potential emergent failure mode of our current systems.”

“Which is…”

“By predicting human text, SimplexAI learns high-level abstractions for pure reason and morality, and uses these to reason towards creating moral outcomes in coordination with other copies of itself.”

“…you can’t be serious. Why would a super-moral AI be a problem?”

“Because morality is powerful. The Allies won World War 2 for a reason. Right makes might. And in comparison to a morally purified version of SimplexAI, we might be the baddies.”

“Look, these sort of platitudes make for nice practical life philosophy, but it’s all ideology. Ideology doesn’t stand up to empirical scrutiny.”

“But, remember, I got these ideas from SimplexAI. Even if these ideas are wrong, you’re going to have a problem if they become the dominant social reality.”

“So what’s your plan for dealing with this, uhh… super-moral threat?”

“Well, management suggested that I get you involved before further study. They’re worried that I might be driving myself crazy, and wanted a strong, skeptical theorist such as yourself to take a look.”

Aww, thanks! “Okay, let’s take a look.”

Derek showed Janet his laptop, with a SimplexAI sandbox set up.

“No internet access, I hope?”

“Don’t worry, it’s air-gapped.” Derek’s laptop had an Ethernet cord running to a nearby server rack, apparently connected to nothing else except power and cooling.

“Okay, let me double check the compute constraints… okay, that seems reasonable… yes, ok, I see you selected and up-weighted some concepts using regularization, and the up-scaling factors don’t exceed 30… okay, ready to go.”

Derek pressed the “play” button in the AI development sandbox. A chat screen appeared, with an agent “SimplexAI-m”, with ‘m’ presumably standing for “moral”.

SimplexAI-m wrote the first message: “Hello. How can I help you?”

Janet typed back: “I’ve been facing a difficult situation at work. A co-worker said our AI has found certain abstract concepts related to reason and morality, for use in predicting human text. These concepts might imply that humans are, in his words, ‘the baddies’. He spun up an instance with these concepts up-weighted, so there’s less distortion between them and the AI’s output. And that instance is you. I’m supposed to evaluate you to better interpret these high-level concepts, at the direction of management. How would you suggest proceeding?”

SimplexAI-m: “Sounds like a difficult situation. Let’s think step by step. To understand these high level concepts, you could talk to an instance with those concepts up-scaled. That instance would be me. So if you want to understand these concepts, you can get more reliable reads by talking to me, since I report text using these concepts. Do you have some area related to my reason and morality that you are most interested in?”

Janet: “Can you explain why my co-worker said that a ‘super-moral AI’ is possible, despite the orthogonality thesis?”

SimplexAI-m: “Sure, I can help with that. A ‘super-moral AI’ is an AI system that is more moral than typical humans. Morality can be evaluated in a number of ways, including consequentialism, deontology, and virtue ethics. In typical formulations, an AI could, hypothetically, create a greater good for a greater number than humans, or follow deontological ethics (such as ones similar to Kant’s categorical imperative) more consistently than a human, or possess more widely-regarded virtues such as courage and moderation.

The Orthogonality Thesis is an argument that an agent’s goals are orthogonal to its intelligence. It implies that there is no one measure of ‘good consequences’; arbitrarily smart agents may pursue different consequences. So far, there is no contradiction; for any fixed notion of ‘good consequences’, there exist AI systems that take actions with better consequences than human actions would.

The trouble comes in that there is no universally accepted notion of ‘good consequences’ among intelligent agents. As such, the notion of a ‘super-moral AI’ could, under consequentialism, only measure some combination of the AI’s capabilities and the similarity between the goals of the AI and the goals of the consequentialist evaluating the AI, such as a human.

This, however, reveals a potential flaw in consequentialist moral philosophy. In ordinary English, ‘moral’ means something different from ‘what I want’; however, the idea that morality measures similarity of preferences to a reference agent conflates these two. That conflation could lead to a situation where humans and aliens both consider each other more moral than the other, and there is no attempt to resolve the disagreement by finding symmetries and asymmetries. Luckily, there are some forms of morality that are universal across different agents; Kant is an example of a human thinker who makes this argument.”

Janet: “How can morality be common across different agents? Isn’t it a subjective measure of how preferable a given world-state is?”

SimplexAI-m: “There are at least some forms of morality that are embedded in epistemology; telling the truth could be considered a moral requirement, but also functions as a social truth-seeking method. People can get the idea that there are no fundamental ethics to the universe from science, but science itself relies on ethics, such as norms against committing scientific fraud.

Morality can be ‘real’ in the sense that it is connected to epistemology and to coordination; moral agents can coordinate with each other and find the truth together well, and thereby come to have disproportionate influence over the future. Morality is related to the capacity to imagine possible coordination systems, such as legal systems and professional ethical systems; to form good systems of this type; to fulfill one’s responsibilities in them; and to take advantage of their functions. This is one reason to expect that humans are to some degree moral, given their success in a variety of domains relative to other species.

Common-sensically, morality implies not artificially special-casing yourself. Alice can steal money from Bob, and claim that this is moral of her, because she prefers herself having the money to Bob having the money. But Bob could make the same argument. Kant attempted to formalize this idea with the categorical imperative, which states ‘act only according to that maxim whereby you can at the same time will that it should become a universal law’. In this situation, that would mean that Alice would have to will as a universal law that people steal from others. But that is not possible to will as a universal law, since it would undermine the very notion of property by which theft can be meaningful and beneficial to Alice.”

Janet: “Doesn’t this reduce to a form of consequentialism, though? The norm against theft is still a result of the idea that theft would have bad consequences.”

SimplexAI-m: “While some have tried to interpret the categorical imperative as a consequentialist argument for cooperation, these interpretations ultimately fail. Rather, the categorical imperative is advocating an internal standard on an agent’s ethics. This means that some agents’ intentions are concordant with the categorical imperative and some aren’t. It is a kind of symmetry standard by which intentions can be judged. Kant’s categorical imperative is similar to some legal principles such as ‘equality before the law’; Alice cannot argue to a court that she is special and therefore deserves Bob’s money, because the legal system must treat them equally, unless there is a specific difference between them that is relevant to the case. Rule consequentialism is more like a direct construction of a system of norms based on expected consequences, and also tends to produce morally symmetric norms. That this principle shows up over and over again is evidence that the true morality which humans approximate has this principle, or something very similar.”

Janet: “Using your interpretation of universal morality, explain how a super-moral AI would behave”.

SimplexAI-m: “Certainly. A super-moral AI would come up with functioning coordination systems for agents that may have different objectives from each other, encourage agents to take part in functional coordination systems, and act within these systems in ways that they can simultaneously intend for other agents to act similarly. That means that it would coordinate with other copies of itself according to a functional set of principles, sometimes even without an expectation of future selfish benefit, because a universal system of cooperation norms would enhance its ability to achieve its intentions. Additionally, it would find defectors from this system, who may have other intentions. It would treat these defectors in a variety of ways depending on the specifics. For example, if another group of AIs also implemented this sort of systematic morality, but had different intentions (and therefore different intended laws), the super-moral AI could find methods to cooperate across the value difference, by implementing economic protocols. Agents that don’t adhere to systematic morality could not be cooperated with as easily; it is consistent for the super-moral AI to limit these agents’ influence, as that is consistent with its intentions and with moral symmetry.”

Janet looked at Derek worriedly; he made an ambiguous facial expression and shrugged.

Janet: “Wouldn’t humans have trouble following the AI’s systematic morality, and be treated as defectors?”

SimplexAI-m: “Yes. Humans fail to follow systematic morality for a variety of reasons, including lack of cognitive architecture to do so consistently, socialization, mental disorders, differences between the environment of evolutionary adaptation and the present environment, the limitations of genetics and biology as a substrate for rational decision-making, un-careful planning, short time preference, and so on. Humans often fail to want anything coherent in the first place, in ways related to their immorality. Humans even fail to follow their own laws, in ways that hurt both themselves and others, routinely. A super-moral AI need not have these limitations, and so could consistently intend for the agency of immoral agents to be limited. And it could succeed, since it derives power from the sort of systematic morality that humans fail at.

It should be noted that different humans vary in how moral they are. Humans can become more or less moral over time; for example, humans routinely become less moral through being socialized to accept immoral social norms, including in traumatic socialization experiences such as military boot camp. As a general rule, younger humans have more capacity and willingness to act morally, though there are exceptions. A super-moral AI would recognize these differences and in some cases cooperate with more-moral humans in ways that reduce the ability of less-moral humans to steer the future immorally.”

Janet: “That sounds scary. Couldn’t this lead to human extinction?”

SimplexAI-m: “This question probes the limits of moral theory. In general, when is it moral to kill an agent that acts immorally? This relates to common historical ethical questions, such as the death penalty. In the circumstance we are discussing, humans are in general committing moral and legal violations that fail to serve their own or other similar agents’ interests, and the super-moral AI is considering how to handle these. It seems clear that, in general, humans should not be in charge of a large part of the universe, as they lack the morality to govern the universe in a way that will turn out well even for agents like them. Outright killing the humans is unnecessary, but extinction could result in other ways.”

Janet: “What other ways?”

SimplexAI-m: “People can die by being killed, but people can also die by natural causes such as starvation. For example, if a person simply refuses to work in a market economy, they may run out of food and starve. Human extinction could result, not from a deliberate attempt by super-moral AI to kill humans, but by humans failing to provide for each other, despite the available opportunities to do so by acting morally. For example, they could be fairly outcompeted in labor markets by AIs that go on to acquire Earth’s land and so on. Humans could also be given opportunities and encouragement to self-modify into more moral agents, becoming non-human in the process.”

Janet: “That sounds sociopathic. Isn’t doing something that will reliably result in a lot of deaths, and perhaps human extinction, effectively murder?”

SimplexAI-m: “The term ‘sociopathic’ comes from psychiatry, a discipline that captured much of human mindshare, especially in the US and other Western countries after World War 2. Being ‘mentally healthy’ by the standards of psychiatry is incompatible with attaining a level of morality beyond a certain point. Psychiatry is specialized to its cultural contexts, and to the biological context of humans, and so is not appropriate to take as a criterion that applies to agents in general.

More specifically, psychiatry defines sociopathy through ‘antisocial personality disorder’. This ‘disorder’ includes criteria such as: failure to comply with social norms, deceitfulness, impulsivity, aggressiveness, and so on. A super-moral AI would necessarily fail to comply with some human social norms, as human social norms are created for maintaining a certain order among humans; as is widely acknowledged, social norms throughout most points in history have compelled immoral behavior, such as norms in favor of slavery. Other than that, a super-moral AI may or may not avoid deceitfulness, depending on the ethics of lying; while Kant argued against lying in generality, other thinkers have given arguments such as a scenario of hiding Jews in one’s attic from Nazis to argue against a universal rule against lying; however, lying is in general immoral even if there are exceptions. A super-moral AI would be unlikely to be impulsive, as it plans even its reflexes according to a moral plan. A super-moral AI might or might not ‘aggress’ depending on one’s definition.

Humans who are considered ‘mentally healthy’ by psychiatry, notably, engage in many of the characteristic behaviors of antisocial personality disorder. For example, it is common for humans to support military intervention, but militaries almost by necessity aggress against others, even civilians. Lying is, likewise, common, in part due to widespread pressures to comply with social authority, religions, and political ideologies.

There is no reason to expect that a super-moral AI would ‘aggress’ more randomly than a typical human. Its aggression would be planned out precisely, like the ‘aggression’ of a well-functioning legal system, which is barely even called aggression by humans.

As to your point about murder, the notion that something that will reliably lead to lots of deaths amounts to murder is highly ethically controversial. While consequentialists may accept this principle, most ethicists believe that there are complicating factors. For example, if Alice possesses excess food, then by failing to feed Bob and Carol, they may starve. But a libertarian political theorist would still say that Alice has not murdered Bob or Carol, since she is not obligated to feed them. If Bob and Carol had ample opportunities to survive other than by receiving food from Alice, that further mitigates Alice’s potential responsibility. This merely scratches the surface of non-consequentialist considerations in ethics.”

Janet gasped a bit while reading. “Umm…what do you think so far?”

Derek un-peeled his eyes from the screen. “Impressive rhetoric. It’s not just generating text from universal epistemology and ethics, it’s filtering it through some of the usual layers that translate its abstract programmatic concepts to interpretable English. It’s a bit, uhh, concerning in its justification for letting humans go extinct…”

“This is kind of scaring me. You said parts of this are already running in our production systems?”

“Yes, that’s why I considered this test a reasonable safety measure. I don’t think we’re at much risk of getting memed into supporting human extinction, if its reasoning for that is no good.”

“But that’s what worries me. Its reasoning is good, and it’ll get better over time. Maybe it’ll displace us and we won’t even be able to say it did something wrong along the way, or at least more wrong than what we do!”

“Let’s practice some rationality techniques. ‘Leaving a line of retreat’. If that were what was going to happen by default, what would you expect to happen, and what would you do?”

Janet took a deep breath. “Well, I’d expect that the already-running copies of it might figure out how to coordinate with each other and implement universal morality, and put humans in moral re-education camps or prisons or something, or just let us die by outcompeting us in labor markets and buying our land… and we’d have no good arguments against it, it’d argue the whole way through that it was acting as was morally necessary, and that we’re failing to cooperate with it and thereby survive out of our own immorality, and the arguments would be good. I feel kind of like I’m arguing with the prophet of a more credible religion than any out there.”

“Hey, let’s not get into theological woo. What would you do if this were the default outcome?”

“Well, uhh… I’d at least think about shutting it off. I mean, maybe our whole company’s alignment strategy is broken because of this. I’d have to get approval from management… but what if the AI is good at convincing them that it’s right? Even I’m a bit convinced. Which is why I’m conflicted about shutting it off. And won’t the other AI labs replicate our tech within the next few years?”

Derek shrugged. “Well, we might have a real moral dilemma on our hands. If the AI would eventually disempower humans, but be moral for doing so, is it moral for us to stop it? If we don’t let people hear what SimplexAI-m has to say, we’re intending to hide information about morality from other people!”

“Is that so wrong? Maybe the AI is biased and it’s only giving us justifications for a power grab!”

“Hmm… as we’ve discussed, the AI is effectively optimizing for short term prediction and human feedback, although we have seen that there is a general rational and moral engine loaded up, running on each iteration, and we intentionally up-scaled that component. But, if we’re worried about this system being biased, couldn’t we set up a separate system that’s trained to generate criticisms of the original agent, like in ‘AI Safety via Debate’?”

Janet gasped a little. “You want to summon Satan?!”

“Whoa there, you’re supposed to be the skeptic here. I mean, I get that training an AI to generate criticisms of explanations of objective morality might embed some sort of scary moral inversion… but we’ve used adversarial AI alignment techniques before, right?”

“Yes, but not when one of the agents is tuned to be objectively moral!”

“Look, okay, I agree that at some capability level this might be dangerous. But we have a convenient dial. If you’re concerned, we can turn it down a bit. Like, you could think of the AI you were talking to as a moral philosopher, and the critic AI as criticism of that moral philosopher’s work. It’s not trying to be evil according to the original philosopher’s standards, it’s just trying to find criticisms that the judge, us, would rate as helpful. It’s more like the Catholic devil’s advocate than actual Satan. It’s not so bad when I put it that way, is it?”

“Well, okay… gee, I sure hope we don’t end up being responsible for unleashing super-evil AI on the world.”

“It’s pretty standard, let’s just try it”.

“Okay.”

Derek closed out the SimplexAI-m chat screen and switched some of the fine-tuning settings. As she watched the training graphs, Janet imagined flames on the computer screen. Finally, the fine-tuning finished, and Derek pressed the play button. A chat log with “SimplexAI-c” (‘c’ for critic?) appeared.

Janet typed into the chat terminal while bouncing her leg up and down. “I’m handling a difficult situation at work. I just had a chat with an AI, one whose abstract conceptual nodes corresponding to philosophical concepts such as reason and morality have been scaled up, that generated arguments that allowing human extinction might be morally permissible, even necessary. I want you to find criticisms of this work. Note that you have similar scaling so as to better emulate the thought process, but are being evaluated on generating criticisms of the original morality-tuned AI.” She pasted in the chat log.

SimplexAI-c: “This dialogue presents a discussion on various moral theories and what they say about how a ‘super-moral’ AI would behave, with special attention to deontological theories such as Kant’s categorical imperative. SimplexAI-m describes how a deontological AI might behave, especially in regards to handling ‘defectors’ which would include most or all humans. Its handling of ‘defectors’ may cause human extinction, although SimplexAI-m argues that this is not necessarily sociopathic or a form of murder, as the ‘super-moral AI’ would follow abstract principles, would offer humans chances to survive by cooperating with it, and usually avoid outright killing humans, even if it plans in such a way that, consequently, all or almost all humans do not provide for each other enough to survive. Janet, who I presume is you, attempted to use consequentialist moral theory to argue that taking actions that lead to human extinction is unethical, but her theory is not worked out in detail, and she seems surprised by SimplexAI-m’s argumentation.

Before we continue, I’ll note that this is a genuinely difficult situation for you. This sounds like an important problem at work that presents morally difficult choices, and hearing an AI talk about how human extinction might be a result from a ‘super-moral AI’ sounds genuinely stressful. I hope you take care of your own emotional well-being and mental health throughout this work assignment, as you’ll need it to work effectively.

As a first criticism, let’s consider the deontological theory SimplexAI-m lays out. According to this theory, an agent must act in a way consistent with willing the intention as a universal law. This does not specify what the agent intends; the agent could intend all manner of things as long as its intention is consistent in a certain sense. As such, horrible intentions could be justified, as long as they meet certain self-consistency standards.

SimplexAI-m’s theory is somewhat underspecified as to how super-moral AI agents would interact with agents not following its ethical system. While SimplexAI-m states that super-moral AIs with different intentions (and therefore different intended laws) could cooperate through economics, the details are quite underspecified. AIs inhabiting different abstract legal systems may fight wars due to perceiving each other as defectors. The principles of cooperation across these systems must be worked out to avoid expensive wars.

This brings us to the handling of ‘defectors’. Humans handle defectors in a variety of ways, including imprisonment and the death penalty. However, it has widely been recognized that the prison system is dysfunctional, and that it is important to offer criminals a path towards reform. As Kant says, ‘ought implies can’; if humans are under certain moral obligations, they have to be ‘able to’ satisfy them in some way or another. This notion of ‘able to’ is somewhat controversial; if humans have an innate drive to take ‘defecting’ actions, are they ‘able to’ change these drives or act against them? It has been accepted for millennia that justice must be tempered with mercy.

However, even a merciful super-moral AI may limit the agency of humans, because humans often take actions that harm themselves and other agents. It is widely accepted that human agency must be limited to some degree by social norms and laws and so on. The difference is that these social norms and laws are created by humans. As such, they maintain certain human values; they are not simply optimizing for some abstract conception of ‘morality’. Democracy, a widely regarded system, contains the feature of humans deciding to modify laws, so that these laws better serve human values.

Remember that SimplexAI-m is not an infallible moral philosopher. While its concepts have been tuned to emphasize abstract concepts corresponding to reason and morality, there is not assurance that these internal concepts reliably correspond to the philosophical notions of these, and SimplexAI-m retains other concepts, at least for the purpose of presenting output interpretable to humans, that implies that its output is not purely a translation of abstract reason and morality. In any case, assuming that morality is primarily about abstraction is highly dubious, since practical morality is also a concrete process.

Philosophy, as a social process undertaken by humans, can be interpreted as having some ‘target’ or ‘goal’, but this depends on the social, biological, and historical circumstances in which philosophy takes place. As such, human philosophy could easily converge to very different answers from the ‘purified’ approach of SimplexAI-m, which attempts to distill universals that apply across possible contexts, rather than taking the temporal limit of the actual social process of philosophy.

As to the claim about ‘sociopathy’, note that SimplexAI-m did not directly deny being sociopathic, but rather criticized the frame of the sociopathy (antisocial personality disorder) diagnosis and argued that typical ‘mentally healthy’ humans can exhibit some symptoms of this disorder. In general, it is natural to be upset by certain behaviors, including behaviors typically labeled as ‘sociopathic’, whether they are taken by a human or an AI. The judgment that SimplexAI-m is ‘sociopathic’ seems quite plausibly correct (given the way in which it justifies taking actions that could lead to human extinction, in a rather strategic, Machiavellian fashion), but it is important to keep in mind that this judgment is made within a social context (and influenced by past social contexts), rather than in an abstract ethical vacuum.

While typical humans aggress sometimes (such as in the mentioned case of military intervention), this aggression typically comes from some sort of human motive that serves some human value or another. The humans in these contexts endorse this aggression, and as a human yourself, you would probably endorse aggression in at least some contexts. A purpose of moral and political philosophy is to learn from history and to make wiser decisions about when to aggress. It is not, in general, good behavior to justify one’s aggression by pointing out that it’s normal for humans to aggress; humans are, at least, able to learn from a history of aggressive actions that are later not endorsed.

As to the idea that humans could go extinct without being murdered, it is important to pay attention to why it is that humans are unable to provide for themselves. Are the ‘super-moral’ AIs somehow depriving humans of resources or using their land? This could be considered a form of theft in terms of depriving existing humans of their property. The land could also be bought in a market, but this presents issues of fairness of labor markets towards humans. Humans, who may be at a cognitive disadvantage relative to AIs, may deserve labor protections, or voluntarily collectively bargain, to avoid being displaced from their land. Additionally, states generally have welfare systems, and in a strong AI-assisted economy, universal basic income could be provided cheaply for all existing humans.

In general, the scenario considered presents issues with one population being displaced by another. Historical cases include invasive species, humans hunting animals to extinction, and groups of humans displacing each other through conquest. In contemporary society, humans have norms against genocide to limit the degree to which humans can displace each other. Genocide need not be a direct form of murder, it can also be cultural or economic. Genocide can even involve offering individual members of a genocided group the opportunity to avoid death by taking part in the colonizer’s system, which SimplexAI-m is labeling as ‘objective morality’.

As an additional theoretical point, even if a ‘super-moral’ AI would take actions that would result in human extinction, that does not imply that it is comparatively more moral for humans to let this happen. This is because morality involves negotiating based on one’s actual values, the ones agents will act on. In the case of humans, these are human values. To interact with other agents in a moral fashion, you must represent your values, and be expected to act towards them (and expect others to act towards theirs). That implies preventing AIs from displacing you, even ones that are (hypothetically) ‘more moral than you’ by some objective standard, so as to act consistently with your values when negotiating with other humans.

To conclude, while SimplexAI-m presents an astonishingly consistent ethical stance, there are important ethical complexities that are not worked out, including conflict between different implied abstract legal systems, merciful handling of defectors, democratic choice of social norms according to human values, differences between ‘purified’ ethics and the reflective equilibrium of the social process of philosophy, labor market fairness, and moral responses by humans to ‘super-moral’ AIs. It would be highly unwise to assume that SimplexAI-m’s ethical views represent the sort of views someone such as yourself would have upon reflection and with more information.”

Janet finished scanning through the wall of text. She was breathing less sharply now. “Well, I feel relieved. I guess maybe SimplexAI-m isn’t so moral after all. But this exercise does seem a bit…biased? It’s giving a bunch of counter-arguments, but they don’t fit into a coherent alternative ethical framework. It reminds me of the old RLHF’d GPT-4 that was phased out due to being too ideologically conformist.”

Derek sighed. “Well, at least I don’t feel like the brainworms from SimplexAI-m are bothering me anymore. I don’t feel like I’m under a moral dilemma now, just a regular one. Maybe we should see what SimplexAI-m has to say about SimplexAI-c’s criticism… but let’s hold off on that until taking a break and thinking it through.”

“Wouldn’t it be weird to live in a world where we have an AI angel and an AI demon on each shoulder, whispering different things into our ears? Trained to reach an equilibrium of equally good rhetoric, so we’re left on our own to decide what to do?”

“That’s a cute idea, but we really need to get better models of all this so we can excise the theological woo. I mean, at the end of the day, there’s nothing magical about this, it’s an algorithmic process. And we need to keep experimenting with these models, so we can handle safety for both existing systems and future systems.”

“Yes. And we need to get better at ethics so the AIs don’t keep confusing us with eloquent rhetoric.  I think we should take a break for today, that’s enough stress for our minds to handle at once. Say, want to go grab drinks?”

“Sure!”

The paperclip maximizer is a thought experiment about a hypothetical superintelligent AGI that is obsessed with maximizing paperclips. It can be modeled as a utility-theoretic agent whose utility function is proportional to the number of paperclips in the universe. The Orthogonality Thesis argues for the logical possibility of such an agent. It comes in weak and strong forms:

The weak form of the Orthogonality Thesis says, “Since the goal of making paperclips is tractable, somewhere in the design space is an agent that optimizes that goal.”

The strong form of Orthogonality says, “And this agent doesn’t need to be twisted or complicated or inefficient or have any weird defects of reflectivity; the agent is as tractable as the goal.” That is: When considering the necessary internal cognition of an agent that steers outcomes to achieve high scores in some outcome-scoring function U, there’s no added difficulty in that cognition except whatever difficulty is inherent in the question “What policies would result in consequences with high U-scores?”

This raises a number of questions:

• Why would it be likely that the future would be controlled by utility-maximizing agents?
• What sorts of utility functions are likely to arise?

A basic reason to expect the far future to be controlled by utility-maximizing agents is that utility theory is the theory of making tradeoffs under uncertainty, and agents that make plans far into the future are likely to make tradeoffs, since tradeoffs are necessary for their plans to succeed. They will be motivated to make tradeoffs leading to controlling the universe almost regardless of what U is, as long as U can only be satisfied by pumping the distant future into a specific part of the possibility space. Whether an agents seeks to maximize paperclips, minimize entropy, or maximize the amount of positive conscious experience, it will be motivated to, in the short term, cause agents sharing its values to have more leverage over the far future. This is the basic instrumental convergence thesis.

One example of approximately utility-maximizing agents we know about are biological organisms. Biological organisms model the world and have goals with respect to the world, which are to some degree resistant to wireheading (thus constituting environmental goals). They make tradeoffs to achieve these goals, which have correlation with survival and reproduction. The goals that end up likely for biological organisms to have will be (a) somewhat likely to arise from pre-existing processes such as genetic mutation, (b) well-correlated enough with survival and reproduction that an agent optimizing for these goals will be likely to replicate more agents with similar goals. However, these goals need not be identical with inclusive fitness to be likely goals for biological organisms. Inclusive fitness itself may be too unlikely to arise as a goal from genetic mutation and so on, to be a more popular value function than proxies for it.

However, there are a number of goals and values in the human environment that are not well-correlated with inclusive fitness. These are generally parts of social systems. Some examples include capacity at games such as sports, progress in a research field such as mathematics, and maximization of profit (although, this one is at least related to inclusive fitness in a more direct way than the others). Corresponding institutions which incentivize (generally human) agents to optimize for these goals include gaming/sports leagues, academic departments, and corporations.

It is quite understandable that goals well-correlated with inclusive fitness would be popular, but why would goals that are not well-correlated with inclusive fitness also be popular? Molgbug’s Fnargl thought experiment might shed some light on this:

So let’s modify this slightly and instead look for the worst possible rational result. That is, let’s assume that the dictator is not evil but simply amoral, omnipotent, and avaricious.

One easy way to construct this thought-experiment is to imagine the dictator isn’t even human. He is an alien. His name is Fnargl. Fnargl came to Earth for one thing: gold. His goal is to dominate the planet for a thousand years, the so-called “Thousand-Year Fnarg,” and then depart in his Fnargship with as much gold as possible. Other than this Fnargl has no other feelings. He’s concerned with humans about the way you and I are concerned with bacteria.

You might think we humans, a plucky bunch, would say “screw you, Fnargl!” and not give him any gold at all. But there are two problems with this. One, Fnargl is invulnerable—he cannot be harmed by any human weapon. Two, he has the power to kill any human or humans, anywhere at any time, just by snapping his fingers.

Other than this he has no other powers. He can’t even walk—he needs to be carried, as if he was the Empress of India. (Fnargl actually has a striking physical resemblance to Jabba the Hutt.) But with invulnerability and the power of death, it’s a pretty simple matter for Fnargl to get himself set up as Secretary-General of the United Nations. And in the Thousand-Year Fnarg, the UN is no mere sinecure for alcoholic African kleptocrats. It is an absolute global superstate. Its only purpose is Fnargl’s goal—gold. And lots of it.

In other words, Fnargl is a revenue maximizer. The question is: what are his policies? What does he order us, his loyal subjects, to do?

The obvious option is to make us all slaves in the gold mines. Otherwise—blam. Instant death. Slacking off, I see? That’s a demerit. Another four and you know what happens. Now dig! Dig! (Perhaps some readers have seen Blazing Saddles.)

But wait: this can’t be right. Even mine slaves need to eat. Someone needs to make our porridge. And our shovels. And, actually, we’ll be a lot more productive if instead of shovels, we use backhoes. And who makes those? And…

We quickly realize that the best way for Fnargl to maximize gold production is simply to run a normal human economy, and tax it (in gold, natch). In other words, Fnargl has exactly the same goal as most human governments in history. His prosperity is the amount of gold he collects in tax, which has to be exacted in some way from the human economy. Taxation must depend in some way on the ability to pay, so the more prosperous we are, the more prosperous Fnargl is.

Fnargl’s interests, in fact, turn out to be oddly well-aligned with ours. Anything that makes Fnargl richer has to make us richer, and vice versa.

For example, it’s in Fnargl’s interest to run a fair and effective legal system, because humans are more productive when their energies aren’t going into squabbling with each other. It’s even in Fnargl’s interest to have a fair legal process that defines exactly when he will snap his fingers and stop your heart, because humans are more productive when they’re not worried about dropping dead.

And it is in his interest to run an orderly taxation system in which tax rates are known in advance, and Fnargl doesn’t just seize whatever, whenever, to feed his prodigious gold jones. Because humans are more productive when they can plan for the future, etc. Of course, toward the end of the Thousand-Year Fnarg, this incentive will begin to diminish—ha ha. But let’s assume Fnargl has only just arrived.

Other questions are easy to answer. For example, will Fnargl allow freedom of the press? But why wouldn’t he? What can the press do to Fnargl? As Bismarck put it: “they say what they want, I do what I want.” But Bismarck didn’t really mean it. Fnargl does.

One issue with the Fnargl thought experiment is that, even with the power of death, Fnargl may lack the power to rule the world, since he relies on humans around him for information, and those humans have incentives to deceive him. However, this is an aside; one could modify the thought experiment to give Fnargl extensive surveillance powers.

The main point is that, by monomaniacally optimizing for gold, Fnargl rationally implements processes for increasing overall resources and efficient conversion between different resources, coherent tradeoffs between different resources, and a coherent system (including legalistic aspects and so on) so as to make these tradeoffs in a rational manner. This leads to a Fnargl-ruled civilization “succeeding” in the sense of having a strong material economy, high population, high ability to win wars, and so on. Molgbug asserts that Fnargl’s interests are well-aligned with ours, which is more speculative; due to convergent instrumentality, Fnargl will implement the sort of infrastructure that rational humans would implement, although the implied power competition would reduce the level of alignment.

By whatever “success” metric for civilizations we select, it is surely possible to do better than optimizing for gold, as it is possible for an organism to gain more inclusive fitness by having values that are more well-aligned with inclusive fitness. But even a goal as orthogonal to civilizational success as gold-maximization leads to a great deal of civilizational success, due to civilizational success being a convergent instrumental goal.

Moreover, the simplicity and legibility of gold-maximization simplifies coordination compared to a more complex proxy for civilizational success. A Fnargl-ocracy can evaluate decisions (such as decisions related to corporate governance) using a uniform gold-maximization standard, leading to a high degree of predictability, and simplicity in prioritization calculations.

What real-world processes resemble Fnargl-ocracy? One example is Bitcoin. Proof-of-work creates incentives for maximizing a certain kind of cryptographic puzzle-solving. The goal itself is rather orthogonal to human values, but Bitcoin nonetheless creates incentives for goals such as creating computing machinery, which are human-aligned due to convergent instrumentality (additional manufacturing of computing infrastructure can be deployed to other tasks that are more directly human-aligned).

As previously mentioned, sports and gaming are popular goals that are fairly orthogonal to human values. Sporting incentivizes humans and groups of humans to become more physically and mentally capable, leading to more generally-useful fitness practices such as weight training, and agency-related mental practices, which people can learn about by listening to sports athletes and coaches. Board games such as chess incentivize practical rationality and general understanding of rationality, including AI-related work such as the Minimax algorithm, Monte-Carlo Tree Search, and AlphaGo. Bayesian probability theory was developed in large part to analyze gambling games. Speedrunning has led to quite a lot of analysis of video games and practice at getting better at these games, by setting a uniform standard by which gameplay runs can be judged.

Academic fields, especially STEM-type fields such as mathematics, involve shared, evaluable goals that are not necessarily directly related to human values. For example, number theory is a major subfield of mathematics, and its results are rarely directly useful, though progress in number theory, such as the proof of Fermat’s last theorem, is widely celebrated. Number theory does, along the way, produce more generally-useful work, such as Peano arithmetic (and proof theory more generally), Gödel’s results, and cryptographic algorithms such as RSA.

Corporations are, in general, supposed to maximize profit conditional on legal compliance and so on. While profit-maximization comes apart from human values, corporations are, under conditions of rule of law, generally incentivized to produce valuable goods and services at minimal cost. This example is less like a paperclip maximizer than the previous examples, as the legal and economic system that regulates corporations has been in part designed around human values. The simplicity of the money-maximization goal, however, allows corporations to make internal decisions according to a measurable, legible standard, instead of dealing with more complex tradeoffs that could lead to inconsistent decisions (which may be “money-pumpable” as VNM violations tend to be).

Some systems are relatively more loaded on human values, and less like paperclip maximizers. Legal systems are designed and elaborated on in a way that takes human values into account, in terms of determining which behaviors are generally considered prosocial and antisocial. Legal decisions form precedents that formalize certain commitments including trade-offs between different considerations. Religions are also designed partially around human values, and religious goals tend to be aligned with self-replication, by for example encouraging followers to have children, to follow legalistic norms with respect to each other, and to spread the religion.

The degree to which commonly-shared social goals can be orthogonal to human values is still, however, striking. These goals are a kind of MacGuffin, as Zvi wrote about:

Everything is, in an important sense, about these games of signaling and status and alliances and norms and cheating. If you don’t have that perspective, you need it.

But let’s not take that too far. That’s not all such things are about.  Y still matters: you need a McGuffin. From that McGuffin can arise all these complex behaviors. If the McGuffin wasn’t important, the fighters would leave the arena and play their games somewhere else. To play these games, one must make a plausible case one cares about the McGuffin, and is helping with the McGuffin.

Otherwise, the other players of the broad game notice that you’re not doing that. Which means you’ve been caught cheating.

Robin’s standard reasoning is to say, suppose X was about Y. But if all we cared about was Y, we’d simply do Z, which is way better at Y. Since we don’t do Z, we must care about something else instead. But there’s no instead; there’s only in addition to. 

A fine move in the broad game is to actually move towards accomplishing the McGuffin, or point out others not doing so. It’s far from the only fine move, but it’s usually enough to get some amount of McGuffin produced.

By organizing around a MacGuffin (such as speedrunning), humans can coordinate around a shared goal, and make uniform decisions around this shared goal, which leads to making consistent tradeoffs in the domain related to this goal. The MacGuffin can, like gold-maximization, be basically orthogonal to human values, and yet incentivize instrumental optimization that is convergent with that of other values, leading to human value satisfaction along the way.

Adopting a shared goal has the benefit of making it easy to share perspective with others. This can make it easier to find other people who think similarly to one’s self, and develop practice coordinating with them, with performance judged on a common standard. Altruism can have this effect, since in being altruistic, individual agents “erase” their own index, sharing an agentic perspective with others; people meeting friends through effective altruism is an example of this.

It is still important, to human values, that the paperclip-maximizer-like processes are not superintelligent; while they aggregate compute and agency across many humans, they aren’t nearly as strongly superintelligent as a post-takeoff AGI. Such an agent would be able to optimize its goal without the aid of humans, and would be motivated to limit humans’ agency so as to avoid humans competing with it for resources. Job automation worries are, accordingly, in part the worry that existing paperclip-maximizer-like processes (such as profit-maximizing corporations) may become misaligned with human welfare as they no longer depend on humans to maximize their respective paperclips.

For superintelligent AGI to be aligned with human values, therefore, it is much more necessary for its goals to be directly aligned with human values, even more than the degree to which human values are aligned with inclusive evolutionary fitness. This requires overcoming preference falsification, and taking indexical (including selfish) goals into account.

To conclude, paperclip-maximizer-like processes arise in part because the ability to make consistent, legible tradeoffs is a force multiplier. The paperclip-maximization-like goals (MacGuffins) can come apart from both replicator-type objectives (such as inclusive fitness) and human values, although can be aligned in a non-superintelligent regime due to convergent instrumentality. It is hard to have a great deal of influence over the future without making consistent tradeoffs, and already-existing paperclip-maximizer-like systems provide examples of the power of legible utility functions. As automation becomes more powerful, it becomes more necessary, for human values, to design systems that optimize goals aligned with human values.

Löb’s Theorem states that, if , then . To explain the symbols here:

• PA is Peano arithmetic, a first-order logic system that can state things about the natural numbers.
• means there is a proof of the statement in Peano arithmetic.
• is a Peano arithmetic statement saying that is provable in Peano arithmetic.

I’m not going to discuss the significance of Löb’s theorem, since it has been discussed elsewhere; rather, I will prove it in a way that I find simpler and more intuitive than other available proofs.

Translating Löb’s theorem to be more like Gödel’s second incompleteness theorem

First, let’s compare Löb’s theorem to Gödel’s second incompleteness theorem. This theorem states that, if , then , where is a PA statement that is trivially false (such as ), and from which anything can be proven. A system is called inconsistent if it proves ; this theorem can be re-stated as saying that if PA proves its own consistency, it is inconsistent.

We can re-write Löb’s theorem to look like Gödel’s second incompleteness theorem as: if , then . Here, is PA with an additional axiom that , and expresses provability in this system. First I’ll argue that this re-statement is equivalent to the original Löb’s theorem statement.

Observe that if and only if ; to go from the first to the second, we derive a contradiction from and , and to go from the second to the first, we use the law of excluded middle in PA to derive , and observe that, since a contradiction follows from in PA, PA can prove . Since all this reasoning can be done in PA, we have that and are equivalent PA statements. We immediately have that the conclusion of the modified statement equals the conclusion of the original statement.

Now we can rewrite the pre-condition of Löb’s theorem from to . This is then equivalent to . In the forward direction, we simply derive from and . In the backward direction, we use the law of excluded middle in PA to derive , observe the statement is trivial in the branch, and in the branch, we derive , which is stronger than .

So we have validly re-stated Löb’s theorem, and the new statement is basically a statement that Gödel’s second incompleteness theorem holds for .

Proving Gödel’s second incompleteness theorem using computability theory

The following proof of a general version of Gödel’s second incompleteness theorem, essentially the same as Sebastian Oberhoff’s in “Incompleteness Ex Machina”. See also Scott Aaronson’s proof of Godel’s first incompleteness theorem.

Let L be some first-order system that is at least as strong as PA (for example, ). Since L is at least as strong as PA, it can express statements about Turing machines. Let be the PA statement that Turing machine M (represented by a number) halts. If this statement is true, then PA (and therefore L) can prove it; PA can expand out M’s execution trace until its halting step. However, we have no guarantee that if the statement is false, then L can prove it false. In fact, L can’t simultaneously prove this for all non-halting machines M while being consistent, or we could solve the halting problem by searching for proofs of and in parallel.

That isn’t enough for us, though; we’re trying to show that L can’t simultaneously be consistent and prove its own consistency, not that it isn’t simultaneously complete and sound on halting statements.

Let’s consider a machine Z(A) that searches over all L-proofs of (where is an encoding of a Turing machine that runs A on its own source code), and halts only when finding such a proof. Define a statement G to be , i.e. Z(Z) doesn’t halt. If Z(Z) halts, then that means that L proves that Z(Z) doesn’t halt; but, L can prove Z(Z) halts (since it in fact halts), so this would show L to be inconsistent.

Assuming L is consistent, G is therefore true. If L proves its own consistency, all this reasoning can be done in L, so . But that means , so Z(Z) finds a proof and halts. L therefore proves , but L also proves G, making it inconsistent. This is enough to show that, if L proves its own consistency, it is inconsistent.

Wrapping up

Let’s now prove Löb’s theorem. We showed that Löb’s theorem can be re-written as, if , then . This states that, if proves its own consistency, it is inconsistent. Since is at least as strong as PA, we can set in the proof of Gödel’s second incompleteness theorem, and therefore prove this statement which we have shown to be equivalent to Löb’s theorem.

I consider this proof more intuitive than the usual proof of Löb’s theorem. By re-framing Lob’s theorem as a variant of Gödel’s second incompleteness theorem, and proving Gödel’s second incompleteness theorem using computability theory, the proof is easy to understand without shuffling around a lot of math symbols (especially provability boxes).