(PDF) Knowledge, proof and the Knower

Knowledge, proof and the Knower Walter Dean & Hidenori Kurokawa

&

May 16, 2009 Abstract The Knower Paradox demonstrates that any theory T which 1) extends Robinson arithmetic Q, 2) includes a predicate K(x) intended to formalize “the formula with godel number x is known by agent i,” and 3) contains certain elementary epistemic principles involving K(x) is inconsistent. The purpose of this paper is to show how this paradox may be redeveloped within a system of quantified explicit modal logic in the tradition of Artemov [4] and Fitting [10], [11] which we argue allows for a more faithful formulation of some of the epistemic principles on which it is based. Along the way, we isolate a principle – the Uniform Barcan Formula [UBF] – which we show is required to derive an explicit counterpart of the axiom U (i.e. K(!K(!ϕ") → ϕ")) which was used in the original formulation of the Paradox. We argue that since there are independent epistemic reasons to be suspicious of UBF, the paradox may be resolved by abandoning this principle (and thereby U as well). 1 Introduction A simplified formulation of Montague and Kaplan’s [19] Paradox of the Knower is as follows: if a predicate K(x), intended to express that the sentence with godel-number x is known by an agent i, is adjoined to an arithmetic theory Z sufficiently strong to formal- ize reasoning about its own syntax (e.g. Robinson arithmetic [Q]) and it is assumed that knowledge implies truth – i.e. T K(!ϕ") → ϕ and that this fact is known – i.e. U K(!K(!ϕ") → ϕ") – then the resulting theory T is inconsistent. The derivation of a contradiction passes through the fact that the existence of self-referential statements about the predicate K(x) such as (1) i) δ ↔ K(!¬δ") ii) δ ↔ ¬K(!δ") 1 will be provable in T . Such statements respectively receive the interpretations δ is true iff i knows δ to be false and δ is true iff i does not know δ. As such, the Knower is conventionally taken to reflect a conflict between certain intuitively evident principles about knowledge and the possibility of accommodating epistemic self-reference within a single theory for reasoning about knowledge. Montague and Kaplan [M&K] originally presented the Knower as a zero-day or ‘instan- taneous’ version of the Hangman Paradox wherein a judge issues a decree of the form i knows that this decree is false. If we let δ stand for the proposition expressed by this state- ment, then it is evident that δ is true iff i knows ¬δ – i.e. if δ satisfies (1i). The situation envisioned by the original formulation of the Knower is thus one in which the existence of self-referential statements about knowledge comes about through linguistic stipulation. Others (e.g. Tymoczko [22], Burge [7] and Koons [14]) have argued that since epistemic self-reference can arise in a variety of other mechanisms, it would be arbitrary to exclude statements like (1i,ii) from the scope of an epistemic theory. M&K accommodate this obser- vation by proposing that knowledge should be treated as a predicate of sentences and that this predicate be adjoined to an arithmetic background theory Z to which the G¨odel-Carnap Fixed Point Theorem applies. But as we will see below, the same arguments can readily be formulated in the traditional framework of epistemic modal logic provided that appropriate fixed point formulas are either assumed as premises or added systematically in, e.g., the style of Smorynski diagonalization operators [20].1 M&K’s original strategy in setting out the paradox was to seek a minimal set of epistemic principles which can be shown to lead to a contradiction in the presence of epistemic self- reference. In addition to T and U, they also assumed a closure principle I which states (roughly) that if ϕ → ψ is derivable in T , and ϕ is known, then so is ψ. The epistemic motivation of T, U ought to be clear: T expresses the factivity of knowledge (i.e. that knowledge of ϕ entails its truth) and U expresses that this feature of knowledge is known. T is almost universally accepted as a conceptual truth about knowledge. But in this case, i can presumably come to know that U is true simply by reflecting on the meaning of “knows that.” Although the justification of T and U appear to be closely linked in this way, the con- sensus about the epistemic significance of the Knower seems to be that principle U ought ´ e [9].2 The argument typically adduced to be rejected – c.f., e.g., Anderson [1], Cross [8], Egr´ against U turns on the fact that the following instance of this principle (2) K(!K(!⊥") → ⊥") ≡ K(!¬K(!⊥")") expresses that i knows that his reasoning is consistent. But as long as T is recursively axiomatizable and sufficiently strong to show that K(x) shares certain features of traditional 1 This latter observation glosses over the significance which Montague [18] assigned to the Knower –i.e. that since self-reference is a feature of even very weak arithmetic systems, the inconsistency of these systems with T and U shows that we must reject Quine’s view that sentential operators like “knows that” and “necessarily” should be treated as predicates of sentences. But we now know that in treating these operators as modalities, we do not necessarily escape self-reference. For instance, a modal analogue to the arithmetic Fixed Point Theorem obtains for the provability logic GL in the form of the De Jongh-Sambin Fixed Point Theorem. For a discussion of the Knower in the context of modal provability logic, see [9]. 2 arithmetic proof predicates, it follows by an argument which mirrors the proof of G¨odel’s Second Incompleteness Theorem that a statement like (2) cannot be derived in T as long as T is and consistent. It has been argued on this basis (e.g. by Anderson [1]) that the outer occurrence of K in U cannot be taken to express knowledge which is on the same ‘level’ as the inner occurrence. We do not so much object to the view that U is problematic, as much as we find the ar- gument just sketched for this conclusion lacking in epistemic motivation. For if self-reference really is an integral part of our everyday conception of knowledge, then it seems that a satisfactory resolution of the Knower should not be grounded in the specifically arithmetic features of the system we adopt in order to ensure the existence of statements like (1i,ii).3 Our primary goal in this paper will thus be to adduce an independently motivated argument for rejecting U. In order to do this, we will reconstruct the Knower in a system of explicit modal logic known as the Quantified Logic of Proofs (QLP) due to Fitting [10], [11]. When reformulated in this setting, it becomes clear that an additional principle beyond those assumed by M&K is required in order to derive a contradiction and that this principle is also needed in order to underwrite U. In demonstrating this, it will be useful to take as our starting point a streamlined version of the Knower based on a latter presentation of Montague [18]. In this case, the axioms U and I are dropped in favor of a rule – which we will refer to as the internalization principle – which subsumes them both: Int T % ϕ ∴ T % K(!ϕ") Montague’s result can now be stated as follows: Proposition 1.1. Let T ⊇ Q, and let be K(x) a predicate of LT which satisfies T and Int. Then T is inconsistent. Proof : Apply the Fixed Point Theorem to find a sentence δ such that FP T % δ ↔ ¬K(!δ") We may now reason in T as follows: 1) T % ¬K(!δ") → δ FP 2) T % K(!δ") → ¬δ FP 3) T % K(!δ") → δ T 4) T % ¬K(!δ") 2), 3) 5) T %δ 1), 4) 6) T % K(!δ") Int 5) 7) T %⊥ 4), 6) 2 The caveat “epistemic” reflects the fact that soon after M&K’s original derivation of the Knower, it was realized that the properties they assumed of K(x) also held for a variety of other “truth-like” predicates such as necessity – c.f., e.g., Montague [18], McGee [16] and Friedman & Sheard [12]). In this broader context, arguments in favor of dropping T have also been advanced – cf., e.g., [17]. 3 It bears noting in this regard that the argument summarized in the previous paragraph requires that Second Incompleteness Theorem (or equivalently L¨ob’s Theorem) is provable in T . This is straightforwardly true in the case of PA. But the situation is much more subtle for Q – cf. [5]. This highlights the extent to which Anderson’s argument relies on arithmetic considerations in addition to epistemic ones. 3 In order to motivate the use of QLP in reconstructing this derivation, it will be useful to begin by considering the epistemic rationale for adopting Int. Such a principle presumably reflects the fact that if the statement ϕ is derivable in T , then i can come to know ϕ by constructing a proof of this statement himself by reasoning in T . This principle thus embodies the view that if we are to view T as a medium for reasoning about i’s knowledge, then derivability in T must be understood as a means by which i can not only extend his knowledge, but also that by proving a statement ϕ in T , he thereby gains justification for ϕ. As such, we take it to be implicit in the formulation of the Knower that knowledge requires proof. A related issue which this observation helps to expose is that since the class of statements which are derivable in T will inevitably outstrip those which i will have explicitly derived at any given time, the epistemic notion described implicitly by the hypotheses of Proposition 1.1 is not precisely that of knowledge, but closer to a conception of knowability grounded in deductive provability.4 But since to say that ϕ is provable just is to say that there exists a proof of ϕ. This suggests that a faithful interpretation of the meaning of K(x) in Proposition 1.1 ought to resemble (3) K(!ϕ") $ there exists a proof of ϕ in T One obvious means of attempting to formalize such an interpretation is to think of K(x) not as a primitive predicate, but rather as defined using a conventional arithmetic proof predicate P roofZ (x, y) for Z. This would in turn suggest defining K(x) as follows: (4) K(!ϕ") =df ∃xP roofZ (x, !ϕ") The problem with adopting such a definition is that its consistency with T and Int will de- pend quite sensitively on the details of how P roofZ (x, y) is defined and also on the strength of Z. In particular, if provably in Z, P roofZ (x, y) satisfies the G¨odel-L¨ob-Bernays condi- tions on proof predicates, it follows by a well-known argument that the provability principle analogous to T – i.e. the so-called reflection axiom ∃xP roofZ (x, !ϕ") → ϕ – cannot be consistently adjoined to Z.5 If, on the other hand, we think of epistemic self-reference as a phenomenon which arises independently of our decision to represent i’s reasoning using an arithmetic theory, then nothing about the formulation of the Knower requires that the notion of provability be analyzed arithmetically. This suggests the possibility of formalizing (3) using a system for reasoning about informal proofs and provability. QLP is such a system. This theory descends from Artemov’s LP (the Logic of Proofs) which in turn descends from G¨odel’s [13] use of the modal logic S4 to provide a provability interpretation for intuitionistic proposal logic. QLP inherits from LP statements of the form t : ϕ (which are known as explicit modalities) subject to the intended interpretation 4 This observation in turn raises the question whether the paradox can be resolved by simply abandoning Int or similar closure principles like I. Such a strategy has been advocated by Maitzen [15]. However, Cross [8] has shown that a paradox analogous to the Knower can be formulated on the basis of a knowledge predicate which fails to satisfy substantial closure conditions. 5 Cf. Boolos [6], p. 63. 4 (5) t : ϕ $ t is a proof of ϕ Herein t is a potentially complex expression known as a proof term intended to denote an informal proof. In addition to explicit modalities, QLP also possess first-order quantifiers intended to range over informal proofs. In this system, a statement of the form (∃x)x : ϕ thus receives the intended interpretation “there exists a proof of ϕ,” which thereby provides us with a means of formalizing the right hand side of (3). Our goal in the rest of this paper will be demonstrate that when the Knower is recon- structed in QLP, we discover that an additional epistemic principle is required in order to legitimate the application of Int at line 6) in the derivation of Proposition 1.1. Since this principle underwrites the transposition of a proof quantifier across an explicit modality, it is known as the Uniform Barcan Formula [UBF]. We will suggest in Section 3 below that there are a variety of reasons – both technical and conceptual – to regard UBF with suspicion. In addition, we will also see that it is precisely such a principle which is required in order to internalize a proof of the QLP analogue of T – i.e. Tq (∃x)x : ϕ → ϕ to derive the QLP analogue of U – i.e. Uq (∃y)y : ((∃x)x : ϕ → ϕ) As such, we will argue that the source of the inconsistency highlighted by the Knower Paradox is not located in U itself, but rather in the principle UBF on which it depends. Such a resolution provides not only the desired epistemic rationale for rejecting U, but it also points towards a system wherein epistemic self-reference, factivity and a limited form of internalization may be consistently accommodated. 2 QLP and the explicit reconstruction of the Knower The language of QLP is similar to that of propositional modal logic. However, rather than a single modal operator !, QLP possesses an infinite family of so-called explicit modalities consisting of a proof term t followed by the operator symbol “:” (which is intended to express “is a proof of”). The class of QLP proof terms is specified by the grammar t := xi | ai (x) | !t | t1 · t2 | t1 + t2 | (t∀x) x1 , x2 , . . . are known as proof variables, a1 (x), a2 (x), . . . as primitive proof terms. !, ·, + and (·∀·) denote proof operations respectively called proof checker (unary), application (binary), sum (binary) and uniform verifier (binary). The class of formulas and sentences of QLP is defined as follows: Definition 2.1. If P0 , P1 , . . . are propositional letters, then the class of formulas of LP is specified by the grammar ϕ := ⊥ | Pi | ϕ1 ∧ ϕ2 | ϕ1 ∨ ϕ2 | ϕ1 → ϕ2 | ¬ϕ1 | t : ϕ | (∀x)ϕ(x) | (∃x)ϕ(x). 5 The free variables of proof terms and formulas are respectively defined in the same manner as those of terms and formulas in first-order logic with the exception that in uniform verifier terms of the form (t∀x), x is considered bound. As usual, a sentence is taken to be a formula with no free variables. We now present a Hilbert-style proof system for QLP, presenting first the axioms and then rules. Definition 2.2. The axioms of LP are as follows: LP1 all tautologies of classical propositional logic LP2 t : (ϕ → ψ) → (s : ϕ → t · s : ψ) LP3 t:ϕ→ϕ LP4 t : ϕ →!t : t : ϕ LP5 t : ϕ → t + s : ϕ and s : ϕ → t + s : ϕ QLP1 (∀x)ϕ(x) → ϕ(t), for any proof term t that is free for x in ϕ(x) QLP2 ϕ(t) → (∃x)ϕ(x), for any proof term t that is free for x in ϕ(x) QLP3 (∀x)(ψ → ϕ(x)) → (ψ → (∀x)ϕ(x)), where x +∈ FV(ψ) QLP4 (∀x)(ϕ(x) → ψ) → ((∃x)ϕ(x) → ψ), where x +∈ FV(ψ) UBF (∀x)t(x) : ϕ(x) → (t∀x) : (∀x)ϕ(x) Axioms LP2, LP3 and LP4 will be respectively recognized as explicit versions of the S4 axioms K, T and 4 wherein !s have been replaced with explicit modalities. These axioms can be taken to display functional dependencies between occurrences of S4-!s, read in accordance with G¨odel’s [13] informal provability interpretation (cf. Artemov [4] for details). UBF corresponds to the Uniform Barcan Formula mentioned above. It expresses that if for all x, the proof term t(x) serves as a proof of ϕ(x), then the uniform verifier term (t∀x) serves as a proof of (∀x)ϕ(x). A primitive term specification is a mapping F which assigns to each primitive proof term a a (possibly empty) set of formulas F(a) such that if ϕ ∈ F(a), then FV(a) = FV(ϕ). F is axiomatically injective if for all (and only) instances ϕ of the QLP axioms, there exists a unique primitive proof term a such that ϕ ∈ F(a). We will henceforth assume that we are working with a fixed axiomatically injective constant specification F. Definition 2.3. If Γ is a finite set of formulas, then the derivability relation Γ % ϕ for QLP is now given by specifying the following rules: RQLP1 If ϕ ∈ Γ, then Γ % ϕ. RQLP2 If Γ % ϕ → ψ and Γ % ϕ, then Γ % ψ. RQLP3 If % ϕ(x), then % (∀x)ϕ(x). RQLP4 If ϕ is an instance of a QLP axiom, then Γ % ϕ. RQLP5 If ϕ is an instance of one of LP1-LP5 and ϕ(x1 , . . . , xn ) ∈ F(a(x1 , . . . , xn )), then % a(x1 , . . . , xn ) : ϕ(x1 , . . . , xn ). RQLP5 is known as the axiom internalization rule and is meant to reflect the idea that if ϕ(x1 , . . . , xn ) is an instance of an axiom, then a(x1 , . . . , xn ) serves as a name for a justification of this axiom provided that ϕ(x1 , . . . , xn ) ∈ F(a(x1 , . . . , xn )). 6 RQLP5 should be contrasted with the internalization rule Int which we have suggested above implicitly represents the fact that there is a proof of any statement derivable in T . While this does not hold in virtue of any basic rule in QLP, much of the interest of this and related systems of explicit modal logic derives from the fact that they are able to internalize their own proofs in the manner reflected in the following theorem. Theorem 2.1. Constructive Internalization Theorem (Artemov [4], Fitting [10]) Suppose that x1 : ϕ1 , . . . , xn : ϕn % ψ. Then there exists a proof term t(x1 , . . . , xn ) such that x1 : ϕ1 , . . . , xn : ϕn % t(x1 , . . . , xn ) : ψ Something must finally be said about the status of self-referential statements such as FP with respect to QLP. Since this system has no mechanism for reasoning about its own syntax, there is no reason to expect that anything like the Fixed Point Theorem holds for QLP. In fact QLP derivability bears a close relationship to S4 derivability in a sense which is made precise by the following: Theorem 2.2. Embedding Theorem (Fitting [10]) Define the mapping (·)∃ between the language of S4 and QLP as follows: (Pi )∃ = Pi for Pi a propositional letter; (·)∃ commutes with propositional connectives; (!A)∃ = (∃x)x : A∃ . Then S4 % A if and only if QLP % A∃ . It is easy to see that S4 is incompatible with the existence of a modal version of a statement like FP in the strong sense that S4 % ¬!(A ↔ ¬!A) for all modal formulas A.6 One straightforward means of seeing this is to take !(A ↔ ¬!A) as a reductio assumption, and proceeding as follows: Proposition 2.1. For all A, S4 % ¬!(A ↔ ¬!A) Proof : Reasoning in S4: 0) !(A ↔ ¬!A) % A ↔ ¬!A T 1) !(A ↔ ¬!A) % ¬!A → A 2) !(A ↔ ¬!A) % !A → ¬A 3) !(A ↔ ¬!A) % !A → A T 4) !(A ↔ ¬!A) % ¬!A 2), 3) 5) !(A ↔ ¬!A) % A 1), 4) 6) !(A ↔ ¬!A) % !A Necessitation 5) 7) !(A ↔ ¬!A) % ⊥ 4), 6) 8) % ¬!(A ↔ ¬!A) 0) - 7) 6 Although the 4 axiom (i.e. transitivity) is required to justify the form of the Necessitation rule employed in Proposition (2.1) (i.e. if all formulas in Γ are of the form !B, then Γ % A ∴ Γ % !A) this feature of the derivation is eliminable as ¬!(A ↔ ¬!A) is already a theorem of the modal logic T which contains only the normality and reflection axioms. We have elected to employ S4 rather than T in our exposition to simplify the exposition of results about QLP such as Theorem 2.2. We have also extended the results presented here to cover versions of the Knower Paradox based on a belief operator (similar to that employed by Thomason [21]) in which an axiom similar to 4 is assumed. 7 It is notable that the right hand side of lines 1)-7) of this derivation have exactly the same form as the derivation given in Proposition 1.1. The foregoing derivation thus can be taken as a modal reconstruction of the Knower Paradox. Formulated in this context, it demonstrates the inconsistency of adding an instance of a modal analog of FP of the form !(A ↔ ¬!A) together with the reflection axiom and necessitation rule of S4.7 It is now straightforward to transform the previous S4 derivation into a QLP derivation: 0) y : (ϕ ↔ ¬(∃x)x : ϕ) % ϕ ↔ ¬(∃x)x : ϕ LP3 1) y : (ϕ ↔ ¬(∃x)x : ϕ) % ¬(∃x)x : ϕ → ϕ 2) y : (ϕ ↔ ¬(∃x)x : ϕ) % (∃x)x : ϕ → ¬ϕ 3) y : (ϕ ↔ ¬(∃x)x : ϕ) % (∃x)x : ϕ → ϕ derivable in QLP 4) y : (ϕ ↔ ¬(∃x)x : ϕ) % ¬(∃x)x : ϕ 2), 3) 5) y : (ϕ ↔ ¬(∃x)x : ϕ) % ϕ 1), 4) 6) y : (ϕ ↔ ¬(∃x)x : ϕ) % t(y) : ϕ for some t(y) via Theorem 2.1 6" ) y : (ϕ ↔ ¬(∃x)x : ϕ) % (∃x)x : ϕ QLP3 7) y : (ϕ ↔ ¬(∃x)x : ϕ) % ⊥ 4), 6’) 8) % ¬y : (ϕ ↔ ¬(∃x)x : ϕ) 0) - 7) 9) % (∀y)¬y : [ϕ ↔ ¬(∃x)x : ϕ] RQLP4 10) % ¬(∃y)y : [ϕ ↔ ¬(∃x)x : ϕ] With the exception of the quantifier steps 8)-10), this derivation also shares the structure of Proposition 1.1. However, as presented the argument is an enthymeme as neither steps 3) nor step 6) correspond to QLP axioms nor are they derivable from the preceding steps by QLP rules. The first of these gaps is filled in as follows: i) %x:ϕ→ϕ LP3 ii) % (∀x)(x : ϕ → ϕ) RQLP4 iii) % (∀x)(x : ϕ → ϕ) → ((∃x)x : ϕ → ϕ) QLP4 iv) % (∃x)x : ϕ → ϕ 2), 3) In order to construct the term t(y) used at step 6), i)-iv) must now be internalized in the manner suggested by Theorem 2.1. This may be accomplished as follows: v) %x:ϕ→ϕ LP3 vi) % r(x) : (x : ϕ → ϕ) RQLP3 vii) % (∀x)r(x) : (x : ϕ → ϕ) RQLP2 viii) % (∀x)r(x) : (x : ϕ → ϕ) → (r(x)∀x) : (∀x)(x : ϕ → ϕ) UBF ix) % (r(x)∀x) : (∀x)(x : ϕ → ϕ)) 3), 4) x) % q : (∀x)(x : ϕ → ϕ) → ((∃x)x : ϕ → ϕ) RQLP3 xi) % q · (r(x)∀x) : ((∃x)x : ϕ → ϕ) LP2, 5), 6) 7 If after G¨odel [13] we interpret the ! operator of S4 as expressing informal provability, !(A ↔ ¬!A) can be interpreted as stating the informal provability of a fixed point statement. While Proposition 2.1 demonstrates that such statements are incompatible with S4, it is easy to see that no inconsistency arises if we assume the weaker statement A ↔ ¬!A as in this case the application of the Necessitation rule at line 6) would not be licensed. This might initially seem to threaten the parallelism between Propositions 1.1 and 2.1. But note that in the context of Proposition 1.1 FP is not an additional principle assumed in order to derive a contradiction. Rather, it is an instance of the Diagonal Lemma which is provable in T itself. As such, the arithmetic analog of !(A ↔ ¬!A) (i.e. K(!δ ↔ ¬K(!δ")")) will also be derivable in T via Int. 8 It is now routine to internalize steps 0) - 5) in the original derivation so as to construct the term t(y).8 What is of more immediate interest is that since Tq appears in the derivation of 10) above, its derivation must consequently be internalized to construct the term t(y) at line 6). This leads to line xi), which immediately implies Uq via existential generalization (i.e. QLP2). Another notable fact about the derivation v)-xi) is that it appears to depend on UBF. For although Tq can be derived via i)-iv), there appears to be no way of internalizing this proof without transposing the universal quantifier in vii) across the explicit modality. This is in fact the case: Theorem 2.3. Let QLP− denote the axiom system consisting of QLP without UBF and LQLP− be the language of QLP without the uniform verifier symbol (·∀·). Then QLP % + ϕ, then QLP− +% (∃y)y : ((∃x)x : ϕ → ϕ) This result – which demonstrates the non-conservativity of QLP over QLP− – can readily be established using the so-called evidential semantics for QLP presented by Fitting [10], [11] . It immediately follows that xi) in the foregoing derivations could not be derived without the aid of UBF. If we do not assume this principle, there is no way of constructing the proof term t(y) required by 6). As such, we take Theorem 2.3 to demonstrate that when knowledge is understood in terms of proof in the manner we have suggested, UBF is required in order to reconstruct the Knower. What remains to be seen is what sort of independent consideration can be brought to bear on the acceptability of this principle. 3 UBF, consistency and internalization In this section, we will discuss two distinct sorts of considerations which we take to argue against the epistemic acceptability of UBF. The first of these derives from an attempt to make sense of this principle relative to the informal provability interpretation of explicit modalities. The second consideration represents an attempt to understand the arithmetic significance of UBF by attempting to construct an arithmetic semantics for QLP. Consider again the interpretation which takes an explicit modality t : ϕ expresses that t is an informal proof or other form of justification of ϕ. This interpretation allows us to provide an epistemic motivation for axioms LP2, LP3 and LP4. For instance, if t is an informal proof of ϕ it then follows that ϕ must be true.9 And if t denotes a proof ϕ → ψ, and s a proof of ϕ, then it follows that there exists a proof of ψ – i.e. that compromised of 8 Specifically the required form is of the form t(y) ≡ (a1 · y) · ((b · (q · (r(x)∀x))) · (a2 · y)) where r(x) and q are primitive proof terms which justify the formulas displayed in the derivation and a1 , a2 and b are primitive proof terms for propositional tautologies. 9 This of course presupposes that the notion of informal proof which we are attempting to capture is one according to which proofs provide an indefeasible form of justification for the statements which they verify. This is presumably true of mathematical proofs (both informal and formal) but not for other forms of everyday forms of evidence based on sense data, inductive or abductive inference, etc. 9 t, followed by s, followed by one application of MP with conclusion ψ. In QLP, such a proof is denoted by the complex proof term t · s.10 Of course there is nothing special about the proof terms t and s mentioned in the pre- ceding examples. Accordingly, many intuitively valid principles about informal proof may naturally be formulated using quantifiers – e.g. (6) a) (∀x)[x : ϕ → ϕ]11 b) (∀x)(∀y)[x : (ϕ → ψ) → (y : ϕ → x · y : ψ)] It should thus also be apparent that the quantifier axioms and rules of QLP which underwrite the derivability of such examples also express valid principles about informal proof. As such, there appears to be no conceptual difficultly in envisioning a calculus of informal provability which contains quantifiers intended to range over proofs. Now consider the acceptability of UBF – which we reproduce here for reference – on the informal proof interpretation: UBF (∀x)t(x) : ϕ(x) → (t∀x) : (∀x)ϕ(x) Recall the gloss of this principle provided above: if for all x, the proof term t(x) serves as a proof of ϕ(x), then the uniform verifier term (t∀x) serves as a proof of (∀x)ϕ(x). In order to get a better impression of the meaning of the antecedent of such a statement, it is useful to consider a specific instance in which x occurs free in ϕ(x). An illustrative example is provided by taking ϕ(x) = x : P → P – i.e. an instance of LP3 with P an atomic formula. To make the case yet more concrete, suppose P symbolizes a specific empirical proposition – e.g. that a particular substance p contained cyanide. Also suppose we are considering a class of empirical tests T by which P might be confirmed. For instance x1 ∈ T might test p’s appearance under UV light, x2 ∈ T p’s reaction with iron sulfate, etc.12 And suppose in addition we were concerned with verifying whether each of the tests in T was accurate in the sense of producing no false positives – a proposition which can be expressed in QLP as x : P → P . In such a case we can presumably also envision a uniform procedure t(x) which would, when presented with a specific test, produced a verification that this test was accurate. For instance, on input x1 , t(x) might return a demonstration invoking principles from quantum theory, on input x2 , t(x) might return a demonstrate invoking principles from electrochemistry, etc. Were such a function to exist, (∀x)t(x) : (x : P → P ) would be true. If UBF expressed a valid principle about informal proof, then in the situation just de- scribed there must exist a single proof denoted by (t∀x) which would verify (∀x)(x : P → P ). But it certainly does not seem to follow from what we mean when we speak about informal proofs that such a higher-order verification must exists, even given that we have individually 10 For more on the use of LP as a medium for reasoning about the informal notion of justification, see[3] and [2]. 11 Note that (∃x)x : ϕ → ϕ ≡ Tq follows from (6a) in the manner illustrated by i)-iv) above. Since the informal gloss of this statement (i.e. “If ϕ is provable, then ϕ is true”) may seem fundamental to our conception of informal than which can be given for LP3, one might reasonably wonder why it is the latter principle and not the former which is adopted as an axion of QLP. The arithmetic examples below provide some insight why it is the latter which we take as to be the axiom and the former the theorem. 12 Cf. [23]. 10 verified that all of the tests in T are accurate. On this basis, it appears that UBF lacks the same degree of self evidence possessed by the other axioms of QLP. Another sort of case can be built against UBF by considering in more detail why this principle leads to inconsistency in the presence of self-reference while the other axioms of QLP do not. In order to do this, we will now demonstrate that while there is a natural way of arithmetically interpreting the language of QLP− so that all its theorems all come out as true in the standard model N , adjoining UBF to QLP− allows us to prove statements whose interpretations are not arithmetically valid. An arithmetic interpretation is a mapping (·)◦ from LQLP − into an arithmetic language La such that QLP− proof terms are interpreted as codes of arithmetic proofs, QLP− quantifiers are interpreted as ranging over such codes, and such that statements of the form t : ϕ are interpreted as asserting that t◦ is the code of an arithmetic proof of ϕ◦ . Our goal will be to formulate (·)◦ in such a way that the images of the theorems of QLP− are true in the standard model N . In order to do this, we now embark on a series of definitions, borrowing as many details as possible from [4] and [6]. We assume that La contains terms f0 , f 1 , . . . which represent all primitive recursive functions. We will fix Z = PA as the background arithmetic theory and also fix a multi-conclusion proof predicate Prf(x, y) which is provably ∆1 in PA and such that for every arithmetic formula ϕ (7) PA % ϕ if and only if for some n ∈ N, N |= Prf(n, !ϕ"). As described in [4] we will also assume that T (n) = {k | N |= Prf(n, k)} is finite and that for n, m there is a k such that T (n) ∪ T (m) ⊆ T (k). It follows from the fact that Prf(x, y) is provably ∆1 that the set of P = {n | N |= ∃yPrf(n, y)} is recursive. There is hence a computable function p : N → N which enumerates P injectively – i.e. P = {p(n) | n ∈ N} and if p(n) = p(m), then n = m. Let p be a name for a La -representation of this function. Such a function will be used to interpret proof variables. In particular, if we assume that the official names for proof variables in LQLP− are x0 , x1 , . . . and the official names for arithmetic variables in La are y0 , y1 , . . ., then we set (xi )◦ = p(yi ). In the case that xi occurs in a QLP− formula ϕ(xi ), this will mean that yi will occur free in (ϕ(xi ))◦ inside an arithmetic term of the form p(yi ). Our next task is to specify an arithmetic interpretation for primitive proof terms. Re- call that we are working with a fixed, axiomatically injective primitive term specification F. Thus for each instance of a QLP− axiom ϕ, there is some primitive proof term a such that ϕ ∈ F(a) and FV(a) = FV(ϕ). We wish statements of the form a(x1 , . . . , xn ) : ϕ(x1 , . . . , xn ) to get mapped to arithmetic open sentences which are true for all numerical substitution instances of their free variables. This means that the image of a primitive proof term must itself be a function mapping numbers into codes of proofs. For instance, if ϕ(x1 , . . . , xn ) is an instance of an axiom of QLP− and we have defined (·)◦ so that (ϕ(x1 , . . . , xn ))◦ is an open sentence of La provable in PA, then the interpretation of a(x1 , . . . , xn ) must be a function aϕ(x1 ,...,xn ) ϕ(x◦1 , . . . , x◦n ) such that for every assignment of QLP− terms to x1 , . . . , xn , aϕ(x1 ,...,xn ) returns the code of an arithmetic proof of the image of the corresponding substi- tution instance of ϕ(x1 , . . . , xn ). We will refer to such functions as axiom functions. Once we have verified that the axioms of QLP− are themselves valid under (·)◦ , then it is routine to find a family of primitive recursive functions with the desired properties. 11 Finally, we must provide a means of interpreting the proof operations ·, + and ! of LQLP− . This can be accomplished in the same manner as Artemov’s original arithmetic interpretation of LP via the use of three functions m(x, y), p(x, y) and c(x). These functions are defined to operate on codes of proofs so that m(t◦ , s◦ ) returns the least godel-number of a proof containing all instances of ψ such that !ϕ → ψ" ∈ T (t◦ ) and !ϕ" ∈ T (s◦ ), p(t◦ , s◦ ) returns the least godel number of a proof containing T (t◦ ) and T (s◦ ) and c(t◦ ) returns the least godel-number of a proof k which has Prf(t◦ , !ϕ") ∈ T (k) for all !ϕ" ∈ T (t◦ ). As is shown in [4], these functions are primitive recursive and will hence be represented by arithmetic terms m, a and c. Putting these pieces together, we may now specify how (·)◦ is defined on proof terms: - x◦i = p(yi ) - if ϕ(x1 , . . . , xn ) ∈ F(a(x1 , . . . , xn )), then (a(x1 , . . . , xn ))◦ = aϕ(x1 ,...,xn ) (x◦1 , . . . , x◦n ) - (t · s)◦ = m(t◦ , s◦ ), (t + s)◦ = a(t◦ , s◦ ), (!t)◦ = c(t◦ ) Such an interpretation may be extended to the entire language of LQLP− as follows: - (Pi )◦ is some fixed closed sentence of La - (ϕ → ψ)◦ = ϕ◦ → ψ ◦ , (¬ϕ)◦ = ¬ϕ◦ - ((∀x)ϕ)◦ = (∀x)ϕ◦ , ((∃x)ϕ)◦ = (∃x)ϕ◦ - t : ϕ(xk1 , . . . , xkm ) = Prf(t◦ , su(x◦km , k m , . . . , su(x◦2 , k 2 , su(x◦1 , k 1 , !ϕ(x◦k1 , . . . , x◦km )")) . . .)) See [6] for the definition of su(y1 , . . . , yn ). In order to illustrate the manner in which the axiom functions are defined, it will be useful to consider an example. Let P be a propositional letter and consider again the following instance of axiom LP3: (8) x:P →P First note that the image of (8) under (·)◦ is (9) Prf(p(y), !P ◦ ") → P ◦ where y is an arithmetic variable. Although this is an open arithmetic sentence, it is easy to see that for all n ∈ N, (10) PA % Prf(p(n), !P ◦ ") → P ◦ For note that we have either i) N |= Prf(p(n), !P ◦ ") or ii) N +|= Prf(p(n), !P ◦ "). In the first case, Prf(p(n), !P ◦ ") is a true ∆1 -sentence and hence p(n)N is indeed the godel number of a proof of P ◦ in PA. Hence PA % P ◦ , meaning that (10) holds. In the second case, Prf(p(n), !P ◦ ") is a false ∆1 -sentence and hence PA % ¬Prf(p(n), !P ◦ ") and (10) again holds. The foregoing reasoning is uniform in n in the sense that not only is each substitution instance of (10) provable, but the argument just rehearsed demonstrating this fact can itself be formalized in PA. From this it follows that there is a computable function which for every n, returns the godel number of a proof demonstrating (10) in PA. It is this function which we take as the axiom function ax:P →P . Using the foregoing example as a model, it is now routine to show that the interpretations of the other QLP− axioms are all true in N and that the rules preserve truth. We thus have following: 12 Proposition 3.1. (Arithmetic soundness of QLP− ) If QLP− % ϕ, then N |= ϕ◦ . The foregoing example also foreshadows why it is not possible to extend an arithmetic interpretation to all of QLP. For note that taking ϕ ≡ ⊥ in the derivation v)-xi) above shows that (11) QLP % t : (∀x)(x : ⊥ → ⊥) where t ≡ q · (ax:⊥→⊥ ∀x) contains the uniform verifier symbol. Were we able to extend the given interpretation of QLP− to the full language of QLP including the uniform verifier symbol, then this statement would get mapped to the La statement (12) Prf(t◦ , !(∀y)¬Prf(p(y), !⊥")") where t◦ corresponded to a closed arithmetic term. (12) would hence express that (t◦ )N ∈ N is the godel number of a proof of (∀y)¬Prf(p(y), !⊥") in PA. But assuming that PA is consistent, the existence of such a number in the standard model would violate G¨odel’s Second Incompleteness Theorem. These observations can readily be put together with the internal provability of L¨ob’s Theorem in PA to show the following: Theorem 3.1. Let S = {ϕ◦ | ϕ ∈ LQLP− and QLP % ϕ}. PA ∪ S is inconsistent. Proof. It follows from (11) that (13) QLP % (∃y)y : (∀x)¬x : ⊥ The arithmetic interpretation of (13) – i.e. (14) (∃y)Prf(p(y), !(∀y)¬Prf(p(y), !⊥")") is thus in S. However, an easy modification of the traditional proof of L¨ob’s Theorem (cf., e.g, [6], p. 56) shows that (15) PA % (∃y)Prf(p(y), !(∀y)¬Prf(p(y), !⊥")") → ∃yPrf(p(y), !⊥") Since (14) is thus also in S, it follows that PA ∪ S % ∃yPrf(p(y), !⊥"). But since QLP % (∃x)x : ⊥ → ⊥, S % ((∃x)x : ⊥ → ⊥)◦ = ∃yPrf(p(y), !⊥") → ⊥. Putting these two facts together, we have PA ∪ S % ⊥. This result demonstrates that even if we restrict attention to statements not containing the uniform verifier symbol itself, the arithmetic interpretations of statements provable with the aid of UBF is still inconsistent with PA (or, more generally, any arithmetic theory strong enough to derive L¨ob’s Theorem). Theorem 3.1 is obviously based on the same sorts of arithmetic considerations which motivate Anderson’s resolution of the Knower discussed in Section 1. As such we do not take this result to condemn UBF on epistemic grounds alone. However, the proof of this result does shine some light on the relationship which this principle bears to consistency statements. For consider the following instance of UBF: 13 (16) (∀x)r(x) : (x : ⊥ → ⊥) → /r(x)∀x0 : (∀x)(x : ⊥ → ⊥) As we have seen, the antecedent of this conditional is derivable in QLP− and receives the arithmetical interpretation (17) ∀y[Prf(ax:⊥→⊥ (y), !Prf(y, !⊥") → ⊥"] Assuming that PA is consistent, this statement expresses a fact which is true in the standard model – i.e. for all codes of proofs y in the standard model, there exists a proof (which may be found uniformly), that y is not a proof of ⊥. However, the consequent of (16) receives (12) as its arithmetic interpretation. As we have seen, this statement expresses that PA proves its own consistency and is hence false in the standard model. Thus while UBF does not itself express either consistency or the provability of consistency itself, it is responsible for mediating an inference from an expression of one to an expression of the other in the language of QLP. We take the foregoing considerations to suggest that dropping UBF from the system we use to reason about informal provability is a well motivated means of resolving the Knower Paradox. As is clear from Theorem 2.3, the cost of this omission is losing the general validity of the Constructive Internalization Theorem, a fact which was already noted by Fitting [10]. However, even without UBF in the system, it is easily verified that that Constructive Internalization still applies for all statements derivable in QLP− without the Universal Generalization rule RQLP3. In addition it may be shown that the existence of (provably) self-referential formulas having the form of (1ii) is compatible with QLP− in the following sense: Proposition 3.2. The theory QLP− + {(∃y)y : (P ↔ ¬(∃x)x : P ) | P atomic} is consistent.13 Abandoning UBF thus allows us to formulate a system in which factivity and self-reference are preserved, while retaining internalization for a wide range of formulas. References [1] C. A. Anderson. The paradox of the knower. The Journal of Philosophy, 80(6):338–355, 1983. [2] S. Artemov. Justification logic. Technical report 2007019, CUNY Ph.D. Program in Computer Science, 2007. [3] S. Artemov and E. Nogina. On epistemic logic with justification. In R. Meyden, editor, Theoretical Aspects of Rationality and Knowledge. Proceedings of the Tenth Conference (TARK 2005), pages 279– 294, 2005. The proof of this Proposition, like that of Proposition 2.3, required the use of a relational semantics for 13 QLP presented by Fitting [10], [11] which we have elected not to reproduce here. We expect to extend to Proposition 3.2 by showing that fixed point formulas for arbitrary statements can be consistently added to QLP− via a device like Smorynski’s diagonalization operator [20]. 14 [4] S. N. Artemov. Explicit provability and constructive semantics. The Bulletin of Symbolic Logic, 7(1):1– 36, 2001. [5] A. Bezboruah and J. C. Shepherdson. G¨odel’s second incompleteness theorem for Q. The Journal of Symbolic Logic, 41(2):503–512, 1976. [6] G. Boolos. The Logic of Provability. Cambridge University Press, 1993. [7] T. Burge. Epistemic paradox. Journal of Philosophy, 81:5–29, 1984. [8] C. Cross. The paradox of the knower without epistemic closure. Mind, New Series, 110(438):319–333, 2001. ´ e. The knower paradox in the light of provability interpretations of modal logic. Journal of Logic, [9] P. Egr´ Language, and Information, 14(1):13–48, 2005. [10] M. Fitting. Quantified LP. Technical report, CUNY Ph.D. Program in Computer Science Technical Report TR-2004019, 2004. [11] M. Fitting. The logic of proofs, semantically. Ann. Pure Appl. Logic, 132(1):1–25, 2005. [12] H. Friedman and M. Sheard. An axiomatic approach to self-referential truth. Annals of Pure and Applied Logic, 33:1–21, 1987. [13] K. G¨odel. An interpertation of intuitionistic propositional calculus. In S. Feferman et al., editors, Kurt G¨ odel. Collected Works, volume I, pages 144–195. Oxford University Press, 1986. [14] R. Koons. Paradoxes of belief and strategic rationality. Cambridge University Press, 1992. [15] S. Maitzen. The knower paradox and epistemic closure. Synthese, 114(337-354), 1998. [16] V. McGee. How truthlike can a predicate be? A negative result. Journal of Philosophical Logic, 14:399–410, 1985. [17] V. McGee. Truth, Vaugeness and Paradox. Hackett Publishing Company, 1991. [18] R. Montague. Syntactic treatment of modalities, with corollaries on reflexion princples and finite axiomatizability. In R. Thomason, editor, Formal Philosophy. Yale University Press, 1974. [19] R. Montague and D. Kaplan. A paradox regained. Notre Dame Journal of Formal Logic, 1:79–90, 1960. [20] C. Smorynski. Self-Reference and Modal Logic. Springer-Verlag, Berlin, 1985. [21] R. Thomason. A note of the syntactic treatment of modality. Synthese, 44:371–395, 1980. [22] T. Tymoczko. An unsolved puzzel about knowledge. Philosophical Quarterly, 34:437–458, 1984. [23] Wikipedia. Cyanide. http://en.wikipedia.org/wiki/Cyanide, 2009. 15