A machine that knows its own code Samuel A. Alexander∗ † Department of Mathematics, the Ohio State University May 24, 2013 Abstract We construct a machine that knows its own code, at the price of not knowing its own factivity. 1 Introduction It is well known that a suitably idealized mechanical "knowing agent" capable of logic, arithmetic, and self-reflection, cannot know the index of a Turing machine that represents its own knowledge. See Lucas [7], Benacerraf [2], Reinhardt [10], Penrose [8], Carlson [4], and Putnam [9]. However, the proofs always involve (in various guises) the machine knowing its own factivity: that the machine satisfies K(Kφ → φ). We will relax this requirement and explicitly construct a machine that knows its own code. The construction resembles that of [4] and [6]. Our result should be compared with that of Carlson [4], who showed that a truthful knowing agent can know its own truth and know that it has some code, without knowing which code. A machine can know its own factivity as well as that it has some code (without knowing which), or it can know its own code exactly but not know its own factivity (despite actually being factive). This dichotomy in machine knowledge was first presented in the author's dissertation [1]. In Section 2, we discuss preliminaries. In Section 3, we construct a machine and prove that it knows its own code. 2 Preliminaries We will work in the language L of Epistemic Arithmetic of S. Shapiro [11]. This is the language of Peano arithmetic (with variables x, y, z, . . ., constant symbol 0, unary function symbol S for successor, and binary function symbols + and * for addition and multiplication), extended by a modal operator K for knowledge. The well-formed formulas of L (and their free variables φ 7→ FV (φ)) are defined in the usual way; a formula of the form K(φ) is called purely modal, and will be written Kφ if no confusion results. Formulas without free variables are sentences. Terms, substitutability, and the result φ(x|t) of substituting term t for variable x in φ, are defined in the obvious ways. We borrow the following semantics from T.J. Carlson [4] (pp. 54–55). We have reworded the definition in an equivalent form (except that Carlson allowed for multiple operators while we need only one). The intuition is that purely modal formulas should be treated as much like propositional atoms as possible. Definition 1. (The Base Logic) 1. If U is some set, an assignment into U is a function that maps variables of L into U . 2. If s is an assignment into U , x is a variable, and u ∈ U , s(x|u) shall mean the assignment into U that agrees with s except that it maps x to u. ∗Email: alexander@math.ohio-state.edu †2010 Mathematics Subject Classification: 03D80 1 3. An L -structure M consists of a first-order structure M0 for the first-order part of L , together with a function that takes one assignment s (into the universe of M0) and one purely modal formula Kφ, and outputs either True or False-in which case we write M |= Kφ[s] or M 6|= Kφ[s], respectively- satisfying the following three constraints: (a) Whether or not M |= Kφ[s] does not depend on s(x) if x is not a free variable of φ. (b) If ψ is an alphabetic variant of φ (meaning that ψ is obtained from φ by renaming bound variables so as to respect the binding of the quantifiers) then, for any assignment s, M |= Kφ[s] if and only if M |= Kψ[s]. (c) (Weak Substitution)1 If x and y are variables, Kφ is a modal formula, y is substitutable for x in φ, and s is an assignment, then M |= Kφ(x|y)[s] if and only if M |= Kφ[s(x|s(y))]. 4. From this, for any formula φ, M |= φ[s] and M 6|= φ[s] are defined in the usual inductive way. We say M |= φ if M |= φ[s] for every assignment s. 5. If Σ is a set of L -sentences and φ is an L -formula, we write Σ |= φ to indicate that for every L -structure M, if M |= Σ (meaning M |= σ for every σ ∈ Σ) then M |= φ. 6. An L -formula φ is valid if ∅ |= φ. Lemma 1. (Completeness and compactness) 1. The set of valid L -formulas is r.e. 2. For any r.e. set Σ of L -sentences, {φ : Σ |= φ} is r.e. 3. There is an effective procedure that, given (a Gödel number of) an r.e. set Σ of L -sentences, outputs (a Gödel number of) {φ : Σ |= φ}. 4. If Σ is a set of L -sentences and Σ |= φ, there is a finite set σ1, . . . , σn ∈ Σ such that 2 σ1 → * * * → σn → φ is valid. Proof. Straightforward. Definition 2. The axioms of Peano arithmetic for L consist of the axioms of Peano arithmetic, with the induction schema extended to L . To be precise, the axioms of Peano arithmetic for L are as follows. 1. ∀x(S(x) 6= 0). 2. ∀x∀y(S(x) = S(y) → x = y). 3. ∀x(x + 0 = x). 4. ∀x∀y(x + S(y) = S(x + y)). 5. ∀x(x * 0 = 0). 6. ∀x∀y(x * S(y) = x * y + x). 7. The universal closure of φ(x|0) → (∀x(φ → φ(x|S(x)))) → ∀xφ for any L -formula φ. Definition 3. • The pre-closure axioms of knowledge are given by the following schemata. – E1: The universal closure of Kφ whenever φ is valid. – E2: The universal closure of K(φ → ψ) → Kφ → Kψ. – E3: The universal closure of Kφ → φ. 1The full Substitution Lemma, where variable y is replaced by an arbitrary term t, is not generally valid in modal logic. 2Throughout the paper, A → B → C is shorthand for A → (B → C), and similar for longer implication chains. 2 – E4: The universal closure of Kφ → KKφ. • The axioms of knowledge consist of the pre-closure axioms of knowledge along with Kφ whenever φ is a pre-closure axiom of knowledge. • The axioms of epistemic arithmetic consist of the pre-closure axioms of knowledge along with Kφ whenever φ is a pre-closure axiom of knowledge or φ is an axiom of Peano arithmetic for L . • The axioms of knowledge mod factivity consist of the pre-closure axioms of knowledge along with Kφ whenever φ is an instance of E1, E2, or E4. • The axioms of epistemic arithmetic mod factivity consist of the pre-closure axioms of knowledge along with Kφ whenever φ is an instance of E1, E2, E4, or an axiom of Peano arithmetic for L . Definition 4. By Reinhardt's schema we mean the following schema ([10], p. 327) • ∃eK∀x(Kφ ↔ x ∈ We), whenever FV (φ) ⊆ {x}. Reinhardt demonstrated that a formalization of "I am a Turing machine and I know which one" cannot be consistent with epistemic arithmetic. To do this, he found a particular instance of Reinhardt's schema that was inconsistent with epistemic arithmetic. A truthful mechanical knowing agent that knows its own code necessarily knows all instances of Reinhardt's schema (for example, suppose φ is the formula "the xth Turing machine runs forever"; if I know my own code, I can deduce a code for the set of those n ∈ N such that I know the nth Turing machine runs forever). We will show that Reinhardt's schema is consistent (in fact, ω-consistent, by which we mean it has a structure with universe N where the symbols of Peano arithmetic are given the usual interpretations) with epistemic arithmetic mod factivity. This result should be compared with the main result of [4]. Along with the above schema, Reinhardt introduced ([10], p. 320) a weaker schema, Reinhardt's strong mechanistic thesis, K∃e∀x(Kφ ↔ x ∈ We). 3 Reinhardt conjectured, and Carlson proved4, that the strong mechanistic thesis is consistent with epistemic arithmetic. Thus we have a dichotomy: a truthful knowing machine can know it is some machine (but not which one), and also know itself to be truthful; alternatively, a truthful knowing machine can know precisely which machine it is, but not know itself to be truthful. 3 The Construction Definition 5. Suppose φ is an L -sentence and s is an assignment into N. We define φs to be the sentence φs = φ(x|s(x))(y|s(y)) * * * obtained by replacing each free variable in φ by a numeral for the natural number it is assigned to. For example, if s(x) = 0 and s(y) = 2, then (x = y)s is the sentence (0 = S(S(0))). The machine we construct will have the following form for a certain well-chosen set Σ. Definition 6. If Σ is a set of L -sentences, let MΣ be the L -structure with universe N, in which symbols of Peano arithmetic are interpreted in the usual way, and in which knowledge is interpreted so that for all L -formulas φ and assignments s into N, MΣ |= Kφ[s] iff Σ |= φ s. Lemma 2. For any Σ as in Definition 6, MΣ really is an L -structure. 3Reinhardt lists only ∃e∀x(Kφ ↔ x ∈ We), and K∃e∀x(Kφ ↔ x ∈ We) follows by the rule of necessitation. Clearly the latter formula is what is important. Reinhardt originally referred to this as the Post-Turing thesis, and later decided on the name strong mechanistic thesis (see [4] p. 54). 4This was accomplished using deep structural theorems on the ordinal numbers [3], later organized into patterns of resemblance [5]. 3 Proof. We must verify the conditions on MΣ |= Kφ[s] from Definition 1. Let s be an assignment into N. • (a) If x is not free in φ, then φs does not depend on s(x), so neither does Σ |= φs, so neither does MΣ |= Kφ[s]. • (b) An easy inductive argument shows that any time ψ is an alphabetic variant of φ, for any assignment s into N, ψs is an alphabetic variant of φs. Another easy induction shows that whenever ψ is an alphabetic variant of φ, ψ ↔ φ is valid, so certainly Σ |= φ ↔ ψ. It follows that (when ψ is an alphabetic variant of φ) MΣ |= Kφ[s] if and only if MΣ |= Kψ[s]. • (c) (Weak Substitution) Let x and y be variables. An easy inductive argument shows that for all assignments t into N and all formulas φ such that y is substitutable for x in φ, φ(x|y)t ≡ φt(x|t(y)). By definition MΣ |= Kφ(x|y)[s] if and only if Σ |= φ(x|y) s, which holds if and only if Σ |= φs(x|s(y)), which is true if and only if MΣ |= Kφ[s(x|s(y))]. Lemma 3. For any Σ as in Definition 6, any L -formula φ, and any assignment s, MΣ |= φ[s] if and only if MΣ |= φ s. Proof. By induction on formula complexity of φ. The most interesting case is when φ is Kφ0 for some formula φ0. Suppose MΣ |= Kφ0[s], so Σ |= φ s 0. If we let t be an arbitrary assignment, since φ s 0 is a sentence, φs0 ≡ (φ s 0) t and thus Σ |= (φs0) t. By definition this means MΣ |= Kφ s 0[t]. By arbitrariness of t, MΣ |= Kφ s 0. The converse is similar. Lemma 4. For any Σ as in Definition 6, MΣ satisfies all instances of E2. Proof. Let s be an assignment and suppose MΣ |= K(φ → ψ)[s] and MΣ |= Kφ[s]. This means Σ |= (φ → ψ)s and Σ |= φs. Clearly (φ → ψ)s ≡ φs → ψs, so by modus ponens, Σ |= ψs, so MΣ |= ψ[s]. Lemma 5. For any Σ as in Definition 6, MΣ satisfies the axioms of Peano arithmetic for L . Proof. Let M = MΣ. Let ψ be an axiom of Peano arithmetic. If ψ is any other axiom besides an instance of induction, M |= ψ because M has universe N and interprets the symbols of Peano arithmetic in the intended ways. But suppose ψ is a universal closure of φ(x|0) → (∀x(φ → φ(x|S(x)))) → ∀xφ. Let s be an assignment and assume M |= φ(x|0)[s] and M |= ∀x(φ → φ(x|S(x)))[s]. We must show M |= ∀xφ[s]. Since M |= φ(x|0)[s], Lemma 3 says M |= φ(x|0)s. Clearly φ(x|0)s ≡ φs(x|0), so M |= φs(x|0). For each m ∈ N, since M |= ∀x(φ → φ(x|S(x)))[s], in particular M |= φ → φ(x|S(x))[s(x|m)]. And thus, if M |= φ[s(x|m)], then M |= φ(x|S(x))[s(x|m)]. By Lemma 3, that last sentence can be rephrased: if M |= φs(x|m), then M |= φ(x|S(x))s(x|m); but clearly φ(x|S(x))s(x|m) ≡ φs(x|m+1), so in summary: • M |= φs(x|0). • For each m ∈ N, if M |= φs(x|m), then M |= φs(x|m+1). Therefore, by mathematical induction, M |= φs(x|m) for every m ∈ N. By Lemma 3, for all m ∈ N, M |= φ[s(x|m)]. So M |= ∀xφ[s], as desired. Lemma 6. Suppose Σ (as in Definition 6) is closed under K, by which we mean that for every φ ∈ Σ, Kφ ∈ Σ. Furthermore, assume Σ contains all instances of E1 and E2 from Definition 3. Then MΣ satisfies all instances of E4. Proof. Assume MΣ |= Kφ[s]. This means Σ |= φ s. By Lemma 1 there are finitely many σ1, . . . , σn ∈ Σ such that σ1 → * * * → σn → φ s is valid. Thus, the universal closure of K(σ1 → * * * → σn → φ s) is an instance of E1, hence in Σ. By repeated instances of E2 in Σ, Σ implies the universal closure of K(σ1 → * * * → σn → φ s) → Kσ1 → * * * → Kσn → Kφ s. It follows that Σ |= Kφs, so MΣ |= KKφ[s]. 4 Definition 7. By assigned validity we mean the following schemata of L -sentences: • φs, whenever φ is valid and s is any assignment. Lemma 7. For any Σ as in Definition 6, if Σ contains all instances of assigned validity, then MΣ satisfies all instances of E1. Proof. Suppose φ is valid and s is any assignment, we will show MΣ |= Kφ[s]. Since φ is valid, φ s is an instance of assigned validity, so Σ |= φs by assumption. Thus MΣ |= Kφ[s]. Definition 8. For every n ∈ N, let Σ(n) be the family of axioms consisting of the following L -schemata. 1. E1, E2, and E4. 2. The axioms of Peano arithmetic for L . 3. ∀x(Kφ ↔ 〈x, pφq〉 ∈ Wn), φ any L -formula with FV (φ) ⊆ {x}. • Here p•q denotes canonical Gödel number, • denotes numeral, and 〈•, •〉 abbreviates a definition (in Peano arithmetic) of a canonical computable bijection N2 → N. 4. Assigned validity. 5. Kφ, whenever φ is an instance of any of lines 1–4 or (recursively) 5. Lemma 8. For every n ∈ N and every φ ∈ Σ(n), φ is a sentence. Proof. By inspection. Lemma 9. There is a total computable function f : N → N such that for every n, Wf(n) = {〈m, pφq〉 ∈ N : φ is a formula with FV (φ) ⊆ {x} and Σ(n) |= φ(x|m)}. Proof. Follows from Lemma 1 and the Church-Turing Thesis. Corollary 10. There is an n ∈ N such that Wn = {〈m, pφq〉 ∈ N : φ is a formula with FV (φ) ⊆ {x} and Σ(n) |= φ(x|m)}. Proof. By Kleene's Recursion Theorem and Lemma 9. Proposition 11. Let n be as in Corollary 10. Then MΣ(n) |= Σ(n). Proof. For brevity, write Σ for Σ(n) and M for MΣ(n). Claim 1 M satisfies all instances of E1. By Lemma 7. Claim 2 M satisfies all instances of E2. By Lemma 4. Claim 3 M satisfies all instances of E4. By Lemma 6. Claim 4 M satisfies the axioms of Peano arithmetic for L . By Lemma 5. Claim 5 For any L -formula φ with FV (φ) ⊆ {x}, M satisfies ∀x(Kφ ↔ 〈x, pφq〉 ∈ Wn). Let s be an arbitrary assignment (say with s(x) = m), we must show M |= Kφ[s] if and only if M |= 〈x, pφq〉 ∈ Wn[s]. The following are equivalent: M |= Kφ[s] Σ |= φs (Definition of M) Σ |= φ(x|m) (Since FV (φ) ⊆ {x}) 〈m, pφq〉 ∈ Wn (By choice of n (Corollary 10)) M |= 〈m, pφq〉 ∈ Wn (Since M has standard first-order part) M |= (〈x, pφq〉 ∈ Wn) s (Since s(x) = m) M |= 〈x, pφq〉 ∈ Wn[s]. (By Lemma 3) 5 Claim 6 M satisfies all instances of assigned validity. Suppose φ is valid and s is an assignment, we must show M |= φs. By Lemma 3, it suffices to show M |= φ[s]. But this is immediate, because φ is valid. Claim 7 M |= Kφ whenever Kφ is an instance of line 5 from Definition 8. For any such Kφ, φ itself lies in Σ, so Σ |= φ. Let s be any assignment. By Lemma 8, φ is a sentence, thus φs = φ and so Σ |= φs, meaning M |= Kφ[s]. Theorem 12. Let n be as in Corollary 10. 1. MΣ(n) satisfies the axioms of epistemic arithmetic mod factivity. 2. MΣ(n) satisfies all instances of Reinhardt's schema, that is, ∃eK∀x(Kφ ↔ x ∈ We) whenever FV (φ) ⊆ {x}. 3. Additionally, there is a fixed m ∈ N such that MΣ(n) satisfies the schema K(Kφ ↔ pφq ∈ Wm), where φ ranges over L -sentences. Thus, the machine that knows the things known by MΣ(n) is a machine that knows its own code. Proof. (1). The only axiom schema that remains to be proven is E3, the universal closures of formulas of the form Kφ → φ. Suppose s is any assignment and MΣ(n) |= Kφ[s]. This means Σ(n) |= φ s. By Proposition 11, MΣ(n) |= Σ(n), therefore MΣ(n) |= φ s. By Lemma 3, MΣ(n) |= φ[s], establishing (1). (2) and (3). By combining lines 3 and 5 of Definition 8, Σ(n) contains K∀x(Kφ ↔ 〈x, pφq〉 ∈ Wn) whenever φ is an L -formula with FV (φ) ⊆ {x}. (2) and (3) follow. 4 Conclusion and Related Work A knowing machine (implicitly meaning, a knowing machine that knows its own factivity) cannot know its own code. Carlson showed that such a machine can know that it has some code (without knowing exactly which). Our result complements Carlson's: it is possible for a machine to know its code quite precisely, at the price of knowing its factivity (despite really being factive). In our dissertation [1] we explore related issues surrounding multiple interacting machines. Suppose ≺ is an r.e. well-founded partial ordering of N. • There are machines M0,M1, . . . such that each Mi knows precise codes of each Mj , and knows factivity of Mj when j ≺ i. • There are machines M0,M1, . . . such that each Mi knows precise codes of Mj when j ≺ i; factivity of Mj when j 1 i; and each Mi knows that each Mj has some code (without necessarily knowing which). • There are machines M0,M1, . . . such that each Mi knows precise codes of Mj (j ≺ i); factivity of Mj (j 1 i); a slight weakening of factivity of Mj (all j); and that Mj has some code (j 1 i). • But if ≺ is ill-founded, there are no such machines as above, provided the machines are also required to know rudimentary facts about computable ordinals. We are preparing a streamlined paper on these results for journal submission. 6 References [1] Alexander, S. (2013). The Theory of Several Knowing Machines. Dissertation, The Ohio State University. [2] Benacerraf, P. (1967). God, the Devil, and Gödel. The Monist, 51, 9–32. [3] Carlson, T.J. (1999). Ordinal arithmetic and Σ1 elementarity. Archive for Mathematical Logic, 38, 449–460. [4] Carlson, T.J. (2000). Knowledge, machines, and the consistency of Reinhardt's strong mechanistic thesis. Annals of Pure and Applied Logic, 105, 51–82. [5] Carlson, T.J. (2001). Elementary patterns of resemblance. Annals of Pure and Applied Logic, 108, 19–77. [6] Carlson, T.J. (2012). Sound Epistemic Theories and Collapsing Knowledge. Slides from the Workshop on The Limits and Scope of Mathematical Knowledge at the University of Bristol. [7] Lucas, J.R. (1961). Minds, machines, and Gödel. Philosophy, 36, 112–127. [8] Penrose, R. (1989). The Emperor's new mind: concerning computers, minds, and the laws of physics. Oxford University Press. [9] Putnam, H. (2006). After Gödel. Logic Journal of the IGPL, 14, 745–754. [10] Reinhardt, W. (1985). Absolute versions of incompleteness theorems. Noûs, 19, 317–346. [11] Shapiro, S. (1985). Epistemic and intuitionistic arithmetic. In Shapiro S. (ed), Intensional Mathematics, pp. 11–46. Elsevier.