THE POWER OF NAIVE TRUTH HARTRY FIELD As is well known, Kripke's 1975 xed point construction for truth based on the Strong Kleene semantics suggests a number of dierent axiomatized truth theories. A prominent division among them is between the external theories and the internal theories. Internal theories are, roughly, those whose only theorems are members of (some or all) xed points of Kripke's construction; whereas external theories provide a certain kind of external commentary on the xed points. The internal theories based on the Kleene semantics respect the naivety of truth: roughly, the equivalence between any sentence and the attribution of truth to it. (Also known as transparency.) The external theories don't respect naivety. Related to this, the internal theories seem more faithful to the intuitions behind the Kripke construction: as Halbach and Horsten put it (2006), the external theories are not sound with respect to Kripke's semantics in the straightforward sense (p. 677). Prima facie, these seem like strong points in favor of the internal theories. But as Halbach and Horsten argue in that paper, the standard internal theories are substantially weaker than their external counterparts in their non-truth-theoretic consequences. Halbach 2011 spells this out further, and while conceding the prima facie advantages of the internal theories over the external, says that the extra strength of the external theories (as regards non-truth-theoretic consequences) is a factor that far outweighs that. The same conclusion, on the same basis, is reached in Feferman 2012.1 I concede to these authors that the extra strength of the external theories is highly desirable. My aim in this paper is to show that this extra strength can be attained in an internal framework which still respects the naivety of truth. (That means that its logic must be non-classical; more on this in a moment.) I rst show how to achieve this in connection with the external theory KF+ (extended Kripke-Feferman), which has rst order Peano arithmetic as its basis: my strategy is to provide an internal theory INT, also based on rst order PA, in which KF+ can be interpreted. I then turn to Feferman's (1991) schematic extension of KF+, which I'll call S-KF+; I provide an analogous schematic internal theory, S-INT, in which S-KF+ can be interpreted. Feferman showed that classical predicative analysis can be interpreted in S-KF+, so when that deep result is combined with the (shallower) result to be presented we get a striking conclusion: 1Halbach and Horsten 2006 took a dierent view (p. 710 top): that while the prooftheoretic advantages of the external theories over the internal are striking, still the external theories are simply not satisfactory as theories of truth. 1 THE POWER OF NAIVE TRUTH 2 (*): One can do all of classical predicative analysis within a non-classical internal theory based on arithmetic. The situation is analogous for theories that add a truth predicate to richer theories such as ZFC (Zermelo-Fraenkel set theory with choice): this yields a predicative theory of self-applicative properties over the ZFC sets, which I think is a natural version of what Feferman (1991) calls the reective closure of ZFC. But I'll conne my attention here to the arithmetic case, where it's clearer what the target is (viz., predicative analysis). Feferman also repeatedly made a somewhat separate complaint against internal theories: one cannot carry out sustained ordinary reasoning within the logics they employ.2 The results of this paper also undercut much of the force of this. For my conclusion is really stronger than (*): since S-INT allows us to interpret S-KF+ (and by a very simple translation, as we'll see), and that in turn allows us to interpret predicative analysis, we get (**): One can carry out what is essentially the same reasoning as employed in the classical theory S-KF+ within a non-classical internal theory. The trick is that S-INT allows us to carve out a substantial classical core; within that substantial core it is possible to carry out whatever sustained ordinary reasoning we can carry out classically. Feferman's point about sustained ordinary reasoning outside the core remains; but the core is so substantial that I think much of the worry is undercut. 1. What Is to be Done? The basic idea will be to extend the usual internal theories by adding an extra predicate `Scl', read strongly classical. This predicate itself is to behave classically (in particular, it is to obey excluded middle).3 The truth predicate of the external theory is then to be interpreted within the corresponding internal theory, roughly as strongly classically true, that is, both true and strongly classical, which I will abbreviate as `Strue'. The laws governing `Scl' will be such that the dened predicate `Strue' also behaves classically (in particular, obeys excluded middle). As a result, classical logic 2It's easy to ascertain meta-theoretically what inferences they validate, but the need to go meta-theoretic is unattractive. 3It is this requirement that leads me to speak of strong classicality. In a truth theory within the internal logic I prefer, it's natural to regard a sentence x as classical if True(x) ∨ ¬True(x). But then we can never prove (or even legitimately assert) of a sentence B that it isn't classical: that would amount to asserting ¬[True(〈B〉)∨¬True(〈B〉)], which in the logic in question entails the contradiction ¬True(〈B〉) ∧ True(〈B〉), which in turn entails any absurdity one chooses. (We can't even prove or legitimately assert that there are non-classical sentences, on this denition of classicality.) To get around this, we want a notion of strong classicality for which the strong classicality of x entails True(x) ∨ ¬True(x), but not conversely; and for which we can prove of many sentences that they are strongly classical and of many others that they aren't. And to allow for the interpretation of the external theories, we want strong classicality to be a classical predicate. THE POWER OF NAIVE TRUTH 3 applies fully among sentences that only contain `true' in contexts of form strongly classical and true. Under basically this translation, all the laws of the external theory will be validated. This means that the proof-theoretic strength of the external theory is attained within the internal theory. I don't claim a lot of pre-theoretic clarity for the notion of strong classicality: indeed, it is a notion that can be lled out in various incompatible ways, and I will build into it only those features needed for the purpose of interpreting the external theories. For instance, the theory will be neutral as to whether truth-teller sentences, or sentences asserting that they are either true or not true, are strongly classical. But it is compatible with the theory to be presented to read `strongly classical' as grounded in the sense of (the Strong Kleene version of) Kripke 1975.4 How will the paradoxes be treated? Let's consider both a genuine Liar sentence λ, which asserts its own untruth, and an external Liar sentence λ∗, which asserts that it itself isn't both true and strongly classical (in whatever way that notion of strong classicality is lled out). Regarding the latter: (A): The internal theories will diagnose λ∗ as true but not strongly classical.5 This is reminiscent of, but seems far more attractive than, the treatment of the Liar sentence in external theories like KF+. In KF+(because `true' amounts to what the internal theory calls strongly classically true) the Liar sentence is asserted but simultaneously declared untrue. (As Halbach and Horsten say, KF+ disproves its own soundness (2006, p. 682).) The internal theories will treat λ very dierently from λ∗. INT and S-INT will employ the Strong Kleene logic K3, to be described shortly; it restricts excluded middle while keeping modus ponens for ⊃ (where ⊃ is dened in terms of ¬ and ∨ in the usual way). With this logic, (B): True(λ)∨¬True(λ) is not a theorem: indeed it is an anti-theorem, in the sense that it entails everything including absurdities like 0 = 1. The disjuncts are likewise anti-theorems; so one must reject them. Whereas the external theories declare a sentence stating its own untruth as not true, but assert it nonetheless, the internal theories reject the sentence and also reject its untruth, since its untruth is equivalent to the sentence itself. (They also reject its truth, which they take to likewise be equivalent.) I think this a much more appealing way to use `true': as many have argued, the equivalence of a sentence to the claim that it is true seems quite central to the uses to which a truth predicate is put. Be that as it may, the point will be to construct theories INT and S-INT that take such a naive truth predicate as basic, but dene (from it together with a predicate `Scl') a notion of strongly classical truth that works entirely 4Or rather: to read it this way when it is applied to sentences that don't themselves contain `strongly classical'. 5At least, as not strongly classical in the same sense as used in λ∗: see note 28. THE POWER OF NAIVE TRUTH 4 in accord with the external theory, and thus preserves the deductive power of the external theory. The view is somewhat reminiscent of Feferman 2008, which involves a theory of truth together with a separate predicate `Determinate' applicable to sentencess for which things work nicely. The dierence is that his truth theory is classical throughout, and things work nicely for determinate sentences means that truth is naive for them; whereas for me it's the reverse, we have naive truth everywhere and things work nicely means that instances of the formula obey excluded middle and hence are fully classical. I believe this latter view is preferable: on it, we get the full deductive power of the external theory within a philosophically attractive naive theory of truth.6 I think the view to be presented is one that should have been appealing to a slightly later time-slice of Feferman. For he says in 2012 (p. 189) that the notion of truth employed in KF(+) and S-KF(+) is not the philosophically signicant notion: he says that it doesn't really stand for truth, but for grounded truth in Kripke's sense.7 (Obviously he intended a qualication analogous to that in note 4 above.) But he provides no axiomatization of the philosophically signicant notion. The present paper can be viewed as lling out his suggestion, by simultaneously axiomatizing the philosophically signicant notion of truth and a notion of strong classicality that can but needn't be read as groundedness, so that something akin to grounded truth can be dened in a way that validates his axioms. That basically is the paper. The next section contains an explanation of the internal/external distinction and some details about the HalbachHorsten-Feferman argument; the rest of the paper gives the details of the response. 6See also Halbach and Fujimoto (in preparation): their theory, like Feferman 2008, is a classical truth theory with a separate determinateness predicate, in whose scope truth behaves naively. Interestingly, their axioms for determinateness are quite similar to mine for strong classicality. (We developed them independently, so I take this as a sign of their intuitive appeal.) Their system strikes me as rather more natural than Feferman's, both in its determinateness axioms and in its underlying truth theory. (Theirs, unlike Feferman's but like mine, contains all standard composition principles for truth; and it doesn't have the defect of declaring itself unsound, though it does fail to declare some of its theorems true.) The proof-theoretic strength of their system is strictly between that of KF and S-KF, but presumably a schematic variant matches that of S-KF, and hence of the theory S-INT to be presented below. Seeing their system does not change my verdict that it's best to attain that proof theoretic strength in a fully naive theory. 7By contrast, Halbach and Nicolai (2016) insist (p. 241 among other places) that the concept of truth employed in KF(+) is the same as that employed in the internal theories. Presumably this means that when the internal theory rejects the sentences that the external theory accepts, the dispute is genuine; which is what Feferman appears to have been denying. THE POWER OF NAIVE TRUTH 5 2. Internal and External Theories There are three main logics based on the Strong Kleene 3-valued evaluation rules.8 (I'll call the three Kleene values 0, 12 and 1, where 1 is the value we give to classical truths and 0 the value we give to classical falsehoods.) My favorite is the logic K3, that declares an inference valid when in every model where the premises have value 1, so does the conclusion. It is the dual to Priest's Logic of Paradox LP (Priest 1998), which declares an inference valid i in every model where the premises have non-0 value, so does the conclusion. S3 is the symmetric logic, whose valid inferences are those that are valid both in K3 and in LP: in other words, those where in every model the value of the conclusion is at least the minimum of the values of the premises. In K3, the law of excluded middle isn't valid, but the rule of explosion is. (That's the rule that contradictions imply anything; it's equivalent in the current context to the rule of disjunctive syllogism, A∨B,¬A ` B; which in turn is equivalent to Modus Ponens for ⊃.) In LP it's the other way around: excluded middle is valid, explosion (and Modus Ponens for ⊃) isn't. In S3 neither is valid; but their common content, the rule A ∧ ¬A ` B ∨ ¬B, is valid. I favor K3, but little will turn on this. Still, it's nice not to have to conduct the discussion in a general way, so I'll assume it for purposes of this paper.9 Whichever of these three logics one prefers, there are serious issues of expressive inadequacy: the logic does not contain conditionals adequate to our needs, or a satisfactory restricted universal quantier (for saying All A are B when A and B are non-classical formulas). Much of my work in recent years has been on extending K3 to address these limitations. In the present paper I want to avoid that: I'll work entirely within K3. Some things would be smoother with an added conditional, but the overall complexity would bury the basic idea. It's possible here to avoid added conditionals because once the strong classicality predicate is added, the task of recovering the proof-theoretic strength of external theories is done within the strongly classical part, and here the ordinary Kleene ⊃ suces. The additional conditional or conditionals are still important to the overall theory, e.g. for the theory of restricted quantication outside the strongly classical realm, but not for the part needed to respond to Halbach, Horsten and Feferman. 8I focus on Strong as opposed to Weak Kleene, both because the connectives and quantiers of the latter seem unnatural, and because as Saul Kripke pointed out to me, Weak Kleene is just a sublogic of Strong Kleene (one with quite limited expressive power). More specically, its disjunction is denable in Strong Kleene as (A ∧ B) ∨ (A ∧ ¬B) ∨ (¬A∧B), and its existential quantication (Kripke credits this to Brian Porter) as [∃xAx∧ ¬∃x(Ax ∧ ¬Ax)] ∨ [¬∃xAx ∧ ∃x(Ax ∧ ¬Ax)]. 9The problem of proof-theoretic strength that Halbach, Horsten and Feferman raise for internal theories based on Strong Kleene logic arises also for internal theories based on rather dierent logics such as Priest's LP, due to the restrictions imposed there on Modus Ponens. (See Picollo 2018.) The solution that I suggest to the problem in the case of Strong Kleene theories can easily be adapted to apply to LP-based theories. THE POWER OF NAIVE TRUTH 6 My internal theories will include a truth theory over Peano arithmetic, based on the logic K3. (The arithmetic enables us to develop a syntactic theory for sentences, taken to be the bearers of truth, via a Gödel numbering.) The truth theory will be naive, which means in part that for each sentence B of the language (including those containing `True'), it will prove each instance of these four rules: T-Elim: True(〈A〉) ` A ¬T-Introd: ¬A ` ¬True(〈A〉) T-Introd: A ` True(〈A〉) ¬T-Elim: ¬True(〈A〉) ` ¬A More generally, it means that for any sentence A, and any formula XA in which A is a subsentence, if XTrue(〈A〉) results from XA by replacing one or more occurrences of A by True(〈A〉) then XTrue(〈A〉) ` XA and XA ` XTrue(〈A〉). This follows inductively from the four listed rules together with the laws of K3. I'll refer to it as the intersubstitutability of True(〈A〉) with A in inference. Many generalizations about truth, e.g. compositional laws, will also be part of the theory; and the arithmetical induction rule will extend to formulas containing `True'. By standard techniques one can construct a Liar sentence λ; I'll use `Q' as an abbreviation of λ (or of its equivalent ¬True(l), where l is the numeral for the Gödel number of λ), and 〈Q〉 for l, so that (the sentence abbreviated as) Q is equivalent to ¬True(〈Q〉). By the equivalence, we have Q ` ¬True(〈Q〉), and ¬True(〈Q〉) ` Q. Combining these with the previous, we get Q ` ¬Q, and ¬Q ` Q. Classically these are inconsistent, but using the more modest rules of S3 they lead only to the conclusion Q ∨ ¬Q ` Q ∧ ¬Q. In the K3 that I prefer, we get the sharper conclusion Q ∨ ¬Q ` ⊥ where ⊥ is an absurdity (say, 0=1). Thus using naive truth in K3, Q ∨ ¬Q is an anti-theorem: it implies absurdities. Indeed the disjuncts Q and ¬Q are themselves anti-theorems. (If I'd used only the weaker S3, Q∨¬Q would not be an anti-theorem: it would still imply the contradiction Q ∧ ¬Q, but whereas in K3 contradictions imply absurdities, they don't in S3.) The fact that in K3 Q ∨ ¬Q is an anti-theorem does not mean that its negation is a theorem: ¬-Introduction is not a valid rule in K3. Indeed, not only is ¬(Q ∨ ¬Q) not a theorem, it is an anti-theorem of K3 too, since it is equivalent to Q ∧ ¬Q. THE POWER OF NAIVE TRUTH 7 What's called the Kripke-Feferman theory (KF) is sort of an external analog of the naive truth theory based on S3: where A1, ..., An ` B in S3, KF proves True(〈A1〉) ∧ ... ∧ True(〈An〉) ⊃ True(〈B〉).10 For instance, KF proves True(〈Q ∨ ¬Q〉) ⊃ True(〈Q ∧ ¬Q〉). KF+ adds to KF the principle (CONSIS): ¬∃x[True(x) ∧ True(neg(x))] (where when x is the Gödel number of a formula, neg(x) is the Gödel number of its negation; and when x isn't the Gödel number of a formula, neg(x) isn't either). This is an external analog of the explosion rule, so KF+ is an external analog of naive truth theory based on K3. KF + thus derives that ¬True(〈Q ∨ ¬Q〉), from which it derives ¬True(〈Q〉) and ¬True(〈¬Q〉). Halbach and Horsten showed that KF+ (and even KF) is powerful enough to interpret ramied analysis up to the ordinal ε0. And Feferman suggested a natural way to beef up KF or KF+ with schematic variables, to yield theories I'll call Schematic-KF and Schematic-KF+; and he showed that these allow the development of ramied analysis up to the much larger ordinal Γ0 (the Feferman-Schütte ordinal), i.e. what's called predicative analysis. Up until now, no internal theory based just on arithmetic has been able to match even KF: they have yielded only ramied analysis up to the much smaller level ωω. This has led Halbach (2011) and Halbach and Nicolai (2018) to not only question these particular internal theories but to strongly suggest that any theories based on non-classical logic are inadequate to mathematics (even if they assume excluded middle for standard mathematical predicates and restrict it only for `True'): e.g. the latter conclude their paper (p. 251) by saying We shouldn't expect that the eects of restricting classical logic for use with the truth predicate can be contained. It would be possible to contest the signicance of this argument from proof-theoretic strength. While we certainly want the results of ramied analysis of these higher levels, one might argue that this is just because we accept those results independently of the notion of truth: e.g., because we accept a standard set theory like ZFC, from which ramied analysis at all levels certainly follows. In that case, the real test isn't theories that add a truth theory to PA, but theories that add it to a much more powerful theory such as set theory. Presumably the results about excess strength carry over: adding truth in a KF-like (or KF+-like) way to ZFC will result in more consequences in the language of ZFC than adding it in a way that corresponds to extant internal theories. But it might be less obvious how important that is: if you think that ZFC already contains all the math you need, then even a weak internal extension of it certainly does. While this response is worth noting, I don't nd it satisfying. It does seem to me (along the lines of various papers by Feferman) that there is an 10The technical result of Halbach and Horsten 2006 shows that the converse fails. They say that KF can be viewed as the theory of the closed o Kripke construction that Kripke mentions late in his paper, though this is probably more true of the KF+ to be mentioned next. THE POWER OF NAIVE TRUTH 8 attractive project of reectively closing theories by adding truth predicates to them, and that the goal of such reective closures should be to capture predicative reasoning over those theories, which includes far more than adding extant internal theories can yield. (Indeed, it yields more than adding the non-schematic theories KF and KF+ can yield; but showing how to get up to ε0 in an internal framework is a clue for how to go farther.) So I think that the challenge to internal theories that these authors raise should be taken seriously. To this end, I'll begin (Section 3) by formulating a non-schematic internal theory INT, and show (Sections 4 and 5) that it is sucient to interpret KF+, thus getting ramied analysis up to ε0; in Section 6 I'll give a model-theoretic proof of its consistency.11 In Sections 7-9 I'll show that Feferman's use of schematic variables is equally available in an internal context, and leads to a consistent theory that interprets Schematic-KF+ and hence full predicative analysis. Section 10 sketches some extensions, and contains further remarks about the philosophical import of the results. 3. The Non-schematic Internal Theory INT I've divided the formalization of INT into four parts: the logic, the arithmetic, the truth theory, and the theory of strong classicality. The rst three will probably contain no surprises (together they are very similar to the theory PKF of Halbach and Horsten 2006, though with the addition of the Explosion rule), but it is important to be explicit, and to set the framework within which the fourth part is presented. 3.1. The logic. I start with a rather standard formalization of the logic K3. (The formalization is similar to the one in Wang 1961.) It is in the format of a Gentzen sequent system with single-formula consequents. The sequent symbol `⇒' is of course not part of the language. I assume the usual structural rules for⇒. (S3 is the same system except with (Explosion) weakened to A,¬A ⇒ B ∨ ¬B; simply dropping (Explosion) gives the 4valued logic FDE.) (∧-Ea): A ∧B ⇒ A (∧-Eb): A ∧B ⇒ B (¬∧-Ia): ¬A⇒ ¬(A ∧B) (¬∧-Ib): ¬B ⇒ ¬(A ∧B) (∧-I): A,B ⇒ A ∧B (¬∧-E): Γ,¬A⇒ C Γ,¬B ⇒ C Γ,¬(A ∧B)⇒ C (¬¬-I): A⇒ ¬¬A 11The explosion rule will be used only to derive the interpretation of CONSIS, so the analogous internal theory based on S3 will suce for KF; and that itself is known to interpret ramied analysis up to the ordinal ε0. That's why my choice to use K3 rather than S3 is inessential. (Consideration of LP would require a longer discussion.) THE POWER OF NAIVE TRUTH 9 (¬¬-E): ¬¬A⇒ A (Explosion): A,¬A⇒ B (∀-E): ∀xAx⇒ At (when the substitution of t for x is legitimate) (¬∀-I): ¬At⇒ ¬∀xAx (when the substitution of t for x is legitimate) (∀-I): Γ⇒ Ax Γ⇒ ∀xAx when x not free in any member of Γ (¬∀-E): Γ,¬Ax⇒ B Γ,¬∀xAx⇒ B when x not free in B or any member of Γ We dene ∨, ∃, ⊃ and ≡ from the others in the usual way, and we get the expected rules for them. It's easy to check that we have restricted conditional proof with side formulas: Restricted conditional proof: Γ⇒ A ∨ ¬A Γ, A⇒ B Γ⇒ A ⊃ B By induction on complexity, we also get an intersubstitutivity result: that if XB results from XA by substituting some or all occurrences of A in it by B, then from A ⇒ B, ¬B ⇒ ¬A, B ⇒ A and ¬A ⇒ ¬B, we can derive XA ⇒ XB (with the usual restrictions on substituting formulas with free variables into the scope of quantiers). Finally for identity we need (Re): ⇒ x = x (Subst of =): x = y,A(v/x) ⇒ A(v/y) when v is a variable and the substitutions of x and y for it are legitimate. We also need A0: ⇒ ∀x∀y(x = y ∨ ¬(x = y)). Instead of viewing this as a general logical axiom, we might prefer to think of a version restricted to where x and y are natural numbers as an arithmetic axiom. But in the context of theories built on PA, the only objects are natural numbers, so we have the unrestricted law either way (and it will make no dierence whether we regard it as logical or arithmetic). 3.2. The arithmetic. I'll employ this logic in connection with the standard language of rst-order Peano arithmetic, expanded to include two new 1place predicates `True' and `Scl'. Let L be this expanded language. (For deniteness, suppose that the arithmetic has `=' as its only predicate, and has the constant symbol `0' and the function symbols `suc', `+' and `*'. If we had more arithmetic predicates then we'd need to include analogs of A0 for them.) The axioms (beyond the instances of excluded middle) are the standard Peano axioms, except with the induction schema formulated in rule form: InductionRule: A(0) ∧ ∀x(A(x) ⊃ A(suc(x)))⇒ ∀xA(x). THE POWER OF NAIVE TRUTH 10 All formulas of L, even those with `True' and `Scl', are allowed as instances of A in this schema. (It's the possible presence of `True' that forces the retreat to rule form.) It's not hard to see that A0 together with the (other) logical laws implies universally generalized excluded middle for all formulas of the language of Peano arithmetic. So by restricted conditional proof, the usual conditional form of induction is derivable for all formulas of Peano arithmetic. Since the other laws of PA have been built in directly, we have full classical Peano arithmetic. 3.3. The compositional truth theory. To state the compositional rules for truth we need some primitive recursive syntactic operations, which can of course be dened in arithmetic as operations on Gödel numbers; so we can conservatively expand arithmetic to include function symbols for them. (This is all very standard, but I include it for reference as needed, and because some of the material required in stating it is also required for the compositional theory of strong classicality.) Let # be any specic number that isn't the Gödel number of anything. The function symbols we need are: neg(x), representing the function that takes the Gödel number of a formula of L to the Gödel number of its negation, and that takes the Gödel number of anything that isn't a formula of L into #; conj(x, y), representing the function that takes the Gödel numbers of two formulas of L to the numeral for the Gödel number of their conjunction, and that takes two numbers at least one of which isn't a formula of L into #; univ(v, x), representing the function that takes the Gödel numbers of a variable of L and a formula of L to the Gödel number of the result of universally quantifying that formula with that variable, and that takes two numbers into # unless the rst is the Gödel number of a variable of L and the second the Gödel number of a formula of L; subst(x, v, t), representing the function that takes the Gödel numbers of a formula, of a variable, and of a term to the Gödel number of the result of substituting the term for the variable in the formula; and that takes other triples of numbers to #; eq(x, y), representing the function that takes the Gödel numbers of two terms to the Gödel number of the equation between these terms (and that takes other pairs of numbers to #); num(x), representing the function that takes any number to the Gödel number of its corresponding numeral; SC(x), representing the function that takes the Gödel number of an expression x of L to the Gödel number of the corresponding atomic formula `Scl(num(x))' (and that takes other numbers to #); THE POWER OF NAIVE TRUTH 11 TR(x), representing the function that takes the Gödel number of an expression x of L to the Gödel number of the corresponding atomic formula `True(num(x))' (and that takes other numbers to #).12 There is also a primitive recursive relation that holds between two numbers if the rst is the Gödel number of a closed term that denotes the second; we can conservatively extend PA to include a predicate `denotes' that represents this. (I also include obvious predicates such as SENTL and CTerm (closed term) for the various syntactic categories in the full language L; I include the subscript for SENT because we'll later consider sublanguages with some predicates omitted (but the same closed terms, obviating the need of a subscript there). The compositional truth theory will come in six main parts: three corresponding to the three atomic predicates of L and three corresponding to the three primitive logical operations ¬, ∧ and ∀. (In the part for ∀ I make use of the fact that the language contains a closed term for everything in the intended model.) The parts corresponding to `=' and `Scl' will be single axioms; the other parts will each consist of four rules (T-Elim, ¬T-Introd, T-Introd and ¬T-Elim), special cases of the rules presented in Section 2. It would be possible (and more uniform) to present the parts corresponding to `=' and `Scl' that way too, and then use A0 and the S0 to be introduced later for the forms listed below;13 but in the interests of ease of comprehension and use I've adopted the simpler formulation below. (Teq): ⇒ ∀s∀t∀x∀y[s denotes x ∧ t denotes y ⊃ [True(eq(s, t)) ≡ x=y] (TSC): ⇒ ∀x[True(SC(x)) ≡ Scl(x)] (TTR-E): True(TR(x))⇒ True(x) (¬TTR-I): ¬True(x)⇒ ¬True(TR(x)) (TTR-I): True(x)⇒ True(TR(x)) (¬TTR-E): ¬True(TR(x))⇒ ¬True(x) (Tneg-E): True(neg(x))⇒ SENTL(x) ∧ ¬True(x) (¬Tneg-I): True(x)⇒ SENTL(x) ∧ ¬True(neg(x)) (Tneg-I): ¬True(x) ∧ SENTL(x)⇒ True(neg(x)) (¬Tneg-E): ¬True(neg(x)) ∧ SENTL(x)⇒ True(x) (Tconj-E): True(conj(x, y))⇒ True(x) ∧ True(y) (¬Tconj-I): ¬True(x) ∨ ¬True(y)⇒ ¬True(conj(x, y)) 12It is more common in the literature on KF to use a function symbol T. that represents the function taking a term t to the Gödel number of the corresponding atomic formula `True(t)', so that T. (num(x)) is TR(x). The use of TR rather than T. (and analogously for SC) simplies many formulations that follow, especially as regarding the function symbol H of Section 5. There is no formal signicance to the use of boldface and uppercase in SC and TR; I simply wanted to make the distinction between these function symbols and the correponding predicates leap out to the reader. 13That the biconditional formulation I've adopted implies the rule form uses Modus Ponens for ⊃. This is generally valid in K3; but the particular case involves formulas that provably obey excluded middle, so would be unproblematic even in S3. THE POWER OF NAIVE TRUTH 12 (Tconj-I): True(x) ∧ True(y)⇒ True(conj(x, y)) (¬Tconj-E): ¬True(conj(x, y))⇒ ¬True(x) ∨ ¬True(y) (Tuniv-E): True(univ(v, x)⇒ ∀y[CTerm(y) ⊃ True(subst(x, v, y))] (¬Tuniv-I): ¬True(univ(v, x)⇒ ∃y[CTerm(y) ∧ ¬True(subst(x, v, y))] (Tuniv-I): ∀y[CTerm(y) ⊃ True(subst(x, v, y))]⇒ True(univ(v, x)) (¬Tuniv-E): ∃y[CTerm(y) ∧ ¬True(subst(x, v, y))]⇒ ¬True(univ(v, x)). I'll also include the rather trivial T1: ⇒ ∀x[True(x) ⊃ SENTL(x)].14 (The induction rule for formulas involving `True' has already been included.) Though we can't derive the analog of (TSC) for `TR', we can use (TTR-I) and (¬TTR-I) to derive the weaker (TTR-Cor): True(x) ∨ ¬True(x)⇒ ∀x[True(TR(s)) ≡ True(x)] (which however does not suce to derive the corresponding quadruple of inference rules). Once we have the law (S-Main) for `Scl', given below, we'll be able to derive from this the generalization ⇒ ∀x(Scl(x) ⊃ [True(TR(x)) ≡ True(x)]). But this is getting ahead of ourselves. It is easily shown by induction on complexity than the general schemas of T-Elim, ¬T-Introd, T-Introd and ¬T-Elim given early in Section 2 all hold; which together with an intersubstitutivity result noted at the end of Subsection 3.1 implies intersubstitutivity of True(〈A〉) with A in inference. Related to this, we have that on the assumption that SENTL(x), True(neg(x)) is intersubstitutable in inference with ¬True(x) in all contexts. This tells us (in marked contrast to the case of KF) that for sentences, truth of negation (falsity) is just non-truth. It is because of this that ¬True(〈Q〉) is an anti-theorem of the K3-based theory (whereas it's a theorem of KF+). It's an anti-theorem because it's equivalent to True(〈¬Q〉), which in turn is equivalent to True(〈True(〈Q〉)), which in turn is equivalent to True(〈Q〉); so it's equivalent to the contradiction True(〈Q〉) ∧ ¬True(〈Q〉), and contradictions are anti-theorems of K3. 3.4. The compositional theory of strong classicality. I complete the specication of INT by giving the rules for the new predicate `Scl'. This will basically be a compositional theory, though it requires the use of the truth predicate. A central assumption will be excluded middle for `Scl': 14In a more general context than arithmetic it would be natural to weaken this, to allow truth to fully parameterized formulas, in eect pairs of formulas and assignments of objects to their variables; this would eectively absorb the notion of satisfaction into the notion of truth. In the context of arithmetic this has less obvious point since for every parameterized formula A(x1, ..., xn) there is a corresponding sentence A(x1, ..., ,xn), where the xi are numerals for the xi. (There's a slight redundancy in my formalization: given T1, the `SENTL(x)' conjuncts are unnecessary in the two Tneg rules in which they appear on the right; and given those rules, T1 could be restricted to atomic sentences and the results derived from the rest. Here and also later, I won't be concerned with eliminating such redundancies.) THE POWER OF NAIVE TRUTH 13 S0: ⇒ ∀x(Scl(x) ∨ ¬Scl(x)). Less central, I'll restrict the application of `Scl' to sentences:15 S1: ⇒ Scl(x) ⊃ SENTL(x). For atomic sentences I stipulate the following: (Seq): ⇒ Scl(eq(x, y)) (STR-i): ¬SENTL(x)⇒ Scl(TR(x)) (STR-ii): SENTL(x)⇒ [Scl(TR(x)) ≡ Scl(x)] (SSC-i): ¬SENTL(x) ⇒Scl(SC(x)) (SSC-ii): SENTL(x) ⇒[Scl(SC(x)) ≡ Scl(x)]. (Note the contrast between S1 and (STR-i). This is no violation of Intersubstitutivity since x isn't the Gödel number of a sentence.) The compositional axioms are as follows: (Sneg): ⇒ Scl(neg(x)) ≡ Scl(x)] (Sconj): ⇒ Scl(conj(x, y)) ≡ [(Scl(x) ∧ Scl(y)) ∨ (Scl(x) ∧ ¬True(x)) ∨ (Scl(y) ∧ ¬True(y))] (Suniv): ⇒ Scl(univ(v, x)) ≡ [∀y(CTerm(y) ⊃ Scl(subst(x, v, y))) ∨ ∃y(Scl(subst(x, v, y))∧ ¬True(subst(x, v, y))]. One nal law: (S-Main): ⇒ Scl(x) ⊃ (True(x) ∨ ¬True(x)). Some comments on these: (STR-ii) is natural given the naivety of truth. There's an obvious parallel between the SSC axioms and the STR axioms. 16 Regarding (SSC-ii), the direction Scl(x) ⊃ Scl(SC(x)) has an obvious appeal; the converse direction that ¬Scl(x) ⊃ ¬Scl(SC(x)) (when SENTL(x)) might seem less obviously desirable, but will be essential to the theory. (Sneg) encapsulates 15From it we could dene a notion Scl* of strong classicality for formulas: a formula is Scl* if all closed substitution instances are Scl. (This would capture the intuitive notion even outside the arithmetic context if we included parameterized instances, as suggested in the previous footnote.) An alternative strategy would take Scl* as the primitive; that would require adding a new axiom, that if a formula is Scl* then all substitution instances of it are too. All of this (and the truth theory too) would require complications in a language with a description operator, where the singular terms themselves can generate non-classicality. 16And two obvious disparallels between these and the corresponding T-axioms and Trules (i.e. TSC plus the four TTR rules). One is that for STR we can use axioms whereas for TTR we can't: this is because strongly classical will be assumed to obey excluded middle even in application to truth attributions. The other is that for the S-axioms we separately consider the case where what s denotes is not the Gödel number of a sentence, whereas we didn't for the T-rules. We didn't for the T-rules because we wanted the results ¬True(TR(s)) and ¬True(SC(s)) when ¬SENTL(x), and these follow from T1 and S1 by (¬TTR -I). But given T1 and S1, excluded middle is guaranteed for attributions of truth and strong classicality to terms that don't denote the Gödel numbers of sentences; this makes it natural to want Scl(TR(s)) and Scl(SC(s)) in this case, which requires the separation of casses (i) and (ii) in the SSC and the STR rules. THE POWER OF NAIVE TRUTH 14 the idea that `Scl' is to be neutral between truth and falsity. The motivating idea behind (Sconj) is that if at least one conjunct of a conjunction is both classical and false, the conjunction is classical as well as false. (`False' means `has a true negation' but since truth is naive, this is equivalent to `is an untrue sentence'.) (Suniv) makes universal quantication analogous to conjunction. The laws without (S-Main) are compatible with all sentences being strongly classical; (S-Main) excludes that, in the K3-based system, i.e. given (Explosion). It excludes it because for the usual Liar sentence λ, True(λ) ∨ ¬True(λ) is an anti-theorem (it implies everything); so (SMain) makes Scl(λ) also an anti-theorem; hence, given S0, ¬Scl(λ) is a theorem. A similar result holds (though by a dierent argument) for the external Liar sentence λ∗ that asserts that it isn't both true and strongly classical. For (S-Main) together with S0 entails that λ∗ is either not Sclassical, or Sclassical and true, or Sclassical and not true; but using naivety, the last two disjuncts are ruled out, so ¬Scl(λ∗) is also a theorem. (The example of the external Liar sentence shows that we cannot consistently have the converse of (S-Main). It will however hold for A that don't contain both `Scl' and `True'.) 4. Strongly classical truth in INT In Section 6 I will prove the consistency of INT. Before then, the main ocial goal is to interpret KF+ in INT; this will involve, among other things, singling out a certain class of sentences within the language L of INT as KFsentences. (I could say KF+-sentences, but KF+ and KF have the same language.) But the notion of strongly classical truth (Struth, where Strue(x) is dened as Scl(x)∧True(x)) is important even for L-sentences that aren't interpretations of KF-sentences: indeed it is probably ultimately more natural to develop ramied analysis up to ε0 directly in INT, using the notion of Struth, than to go via the KF+ interpretation. So it's worth studying the notion of Struth directly. And besides, there are some slightly technical issues about the interpretation of KF+ that I'd rather defer until the main ideas about Struth are on the table. That said, the laws of Struth I'll be demonstrating are closely analogous to standard laws of KF+, as given e.g. on p. 201 of Halbach 2011. I'll use a numbering for mine that corresponds to the numbers Halbach uses; there are gaps in my numbers since he has laws for ∨ and ∃ which I won't bother with given that they follow from the others given the denitions of these connectives. The following will be central: Lemma 1: ⇒ ∀x[Strue(x) ∨ ¬Strue(x)]. Proof. By (S-Main), Scl(x) obviously implies (Scl(x)∧True(x)) ∨ (Scl(x)∧ ¬True(x)), which implies (Scl(x) ∧ True(x)) ∨ ¬(Scl(x) ∧ True(x)), i.e. Strue(x) ∨ ¬Strue(x). That conclusion also follows from ¬Scl(x), so by THE POWER OF NAIVE TRUTH 15 S0 it follows without assumptions; and we can then use ∀-I to universally generalize.  Using Lemma 1 (and S0 again) one easily establishes Lemma 2: ⇒ ∀x[Scl(x) ⊃ (Strue(x) ≡ True(x))].17 (So by intersubstitutivity of `True', we have ⇒ Scl(〈A〉) ⊃ [Strue(〈A〉 ≡ A].) I next turn to the one result in this section whose proof requires Explosion; the proofs of the numbered Str-laws that follow would go through in the S3-based theory. 18 This is analogous to the axiom CONSIS of KF+ (the only axiom included in KF+ but not in KF). Str-CONSIS: ⇒ ¬∃x[Strue(x) ∧ Strue(neg(x))]. Proof. Strue(x) ∧ ¬Strue(x) ⇒ 0 = 1, by Explosion, and since we have excluded middle for the antecedent (using Lemma 1), we can apply restricted conditional proof. With ¬(0 = 1) we get ⇒ ¬(Strue(x) ∧ ¬Strue(x)). Universally generalize (and re-express using ∃).  Next, analogs of the KF axioms. The reader who doesn't want to wade through all this should probably still look at the proofs of Str5 and Str13, since the key ideas arise there. (An alternative to looking at Str5 is to look at the slightly simpler Str9.) Str1: ⇒ ∀s∀t∀x∀y[s denotes x ∧ t denotes y ⊃ (Strue(eq(s, t)) ≡ x=y)]. Proof. Strue(eq(s, t)) implies True(eq(s, t)) by denition, and that together with s denotes x ∧ t denotes y implies x = y by (Teq-E); so s denotes x ∧ t denotes y, Strue(eq(s, t))⇒ x = y. So using Lemma 1 and restricted conditional proof, (i) s denotes x, t denotes y ⇒ Strue(eq(s, t)) ⊃ x = y. For the converse, use (Seq) and the denition of `Strue' to get ¬Strue(eq(s, t))⇒ ¬True(eq(s, t)). Then by analogous reasoning to that in (i) (but using (¬Teq-E) instead of (Teq-E)), we get (ii) s denotes x ∧ tdenotes y ⇒ ¬Strue(eq(s, t)) ⊃ ¬(x = y). So the denotation premise implies the biconditional, and so by another restricted conditional proof and universal generalization we get the result.  Str2: ⇒ ∀s∀t∀x∀y(s denotes x ∧ t denotes y ⊃ [Strue(neg(eq(s, t))) ≡ ¬(x = y)]). 17Proof: Strue(x) ⇒ True(x) by denition of Strue, so by Lemma 1 and restricted conditional proof, ⇒ Strue(x) ⊃ True(x); so certainly (i) Scl(x)⇒ Strue(x) ⊃ True(x). Also Scl(x),¬Strue(x)⇒ ¬True(x) by denition of Strue, so by Lemma 1 and restricted conditional proof again, (ii) Scl(x) ⇒ ¬Strue(x) ⊃ ¬True(x). By (i) and (ii), Scl(x) ⇒ Strue(x) ≡ True(x); so by S0 and another conditional proof, followed by ∀-I, we get the result. 18This fact would be useful in extending the results of this paper to LP-based theories, since LP extends S3 but doesn't extend K3. THE POWER OF NAIVE TRUTH 16 Proof. Strue(neg(eq(s, t))) implies True(neg(eq(s, t))) by denition, and that together with s denotes x ∧ t denotes y implies ¬(x = y) by (TeqE); so as with Str1 we get (i) s denotes x ∧ t denotes y ⇒ Strue(neg(eq(s, t))) ⊃ ¬(x = y). Conversely, ¬(x = y) plus the denotation assumptions implies True(neg(eq(s, t)) by (Tneg) and (¬Teq-I), and they imply Scl(neg(eq(s, t))) by (Seq) and (Sneg). So (ii) s denotes x ∧ t denotes y ⇒ ¬(x = y) ⊃ Strue(neg(eq(s, t))). Apply restricted conditional proof and universal generalization to the conjunction of (i) and (ii).  Str3: ⇒ ∀x[Strue(neg(neg(x))) ≡ Strue(x)] Proof. (i) Strue(x)⇒ Scl(x)∧True(x), so using two applications of (Sneg) plus (Tneg-I) and (¬Tneg-I), Strue(x)⇒ Scl(neg(neg(x)))∧True(neg(neg(x))), i.e. Strue(x) ⇒ Strue(neg(neg(x))). By Lemma 1 and restricted conditional proof, ⇒ Strue(x) ⊃ Strue(neg(neg(x))). (ii) Strue(neg(neg(x)))⇒ Scl(neg(neg(x))) ∧ True(neg(neg(x))), so using two applications of (Sneg) together with and (Tneg-E) and (¬TnegE), Strue(neg(neg(x))) ⇒ Scl(x) ∧ True(x), i.e. Strue(neg(neg(x))) ⇒ Strue(x). By Lemma 1 and restricted conditional proof,⇒ Strue(neg(neg(x))) ⊃ Strue(x).  Str4: ⇒ ∀x∀y[Strue(conj(x, y)) ≡ Strue(x) ∧ Strue(y)] Proof. Again, we derive rule forms, then use restricted conditional proof and universal generalization. R to L rule: RHS implies Scl(x) ∧ Scl(y), so Scl(conj(x, y)) by (Sconj). RHS also implies True(x)∧True(y), so True(conj(x, y)) by truth rules. So Strue(conj(x, y)). L to R: LHS implies Scl(conj(x, y)), so by (Sconj), either Scl(x)∧Scl(y), or Scl(x)∧¬True(x), or Scl(y)∧¬True(y). But LHS also implies True(conj(x, y)), which implies True(x) and True(y), knocking out second and third disjuncts above. So Scl(x)∧Scl(y)∧True(x)∧True(y); i.e.Strue(x)∧Strue(y).  Str5: SENTL(x) ∧ SENTL(y)⇒ ∀x∀y[Strue(neg(conj(x, y))) ≡ Strue(neg(x))∨ Strue(neg(y))]. Proof. The restriction to sentences is unnecessary for the left to right of the biconditional, but is needed in the other direction. First I derive the following claims: (1a) ⇒ Strue(neg(x)) ⊃ Scl(neg(conj(x, y))) (1b) SENTL(y)⇒ Strue(neg(x)) ⊃ True(neg(conj(x, y))) For (1a), note that Strue(neg(x)) implies Scl(neg(x)), which implies Scl(x); and that Strue(neg(x)) also implies True(neg(x)), which implies ¬True(x); so by (Sconj), Scl(conj(x, y)), and hence Scl(neg(conj(x, y))). Now use Lemma 1 and restricted conditional proof to get (1a). THE POWER OF NAIVE TRUTH 17 For (1b), note that Strue(neg(x)) implies True(neg(x)), hence SENTL(x)∧ ¬True(x), hence SENTL(x) ∧ ¬True(conj(x, y)). But with SENTL(y) we get SENTL(conj(x, y)), so True(neg(conj(x, y))). Use Lemma 1 and restricted conditional proof to get (1b). Putting these together, we have SENTL(y)⇒ Strue(neg(x)) ⊃ Strue(neg(conj(x, y))). By a similar argument we get SENTL(x)⇒ Strue(neg(y)) ⊃ Strue(neg(conj(x, y))). From these we derive (1) SENTL(x)∧SENTL(y)⇒ Strue(neg(x))∨Strue(neg(y)) ⊃ Strue(neg(conj(x, y))). For the converse, I rst derive (2) ⇒ Strue(neg(conj(x, y))) ⊃ Strue(neg(x)) ∨ Strue(neg(y)). To do this, note rst that the antecedent requires that SENTL(neg(conj(x, y))), which obviously requires both SENTL(x) and SENTL(y). Next, given S0, we have that either (i) ¬Scl(x) ∧ ¬Scl(y), or (ii) Scl(x) ∧ ¬Scl(y), or (iii) ¬Scl(x) ∧ Scl(y), or (iv) Scl(x) ∧ Scl(y). If we suppose Strue(neg(conj(x, y))) we have Scl(conj(x, y)) (using (Sneg)). Using (Sconj), this rules out case (i), and allows us to expand cases (ii) and (iii) as follows: (ii*) Scl(x) ∧ ¬Scl(y) ∧ ¬True(x); (iii*) Scl(y) ∧ ¬Scl(x) ∧ ¬True(y). But since SENTL(x), case (ii*) yields Scl(neg(x))∧True(neg(x)), so Strue(neg(x)); analogously in (iii*), Strue(neg(y)). So in both these cases, Strue(neg(x)) ∨ Strue(neg(y)). In case (iv) we also get Strue(neg(x))∨Strue(neg(y)), again under the assumption that Strue(neg(conj(x, y))). For that assumption entails True(neg(conj(x, y))), which by the truth rules yields True(neg(x)) ∨ True(neg(y)), and by case (iv) assumptions this yields Strue(neg(x)) ∨ Strue(neg(y)). So by the four cases together, we have Strue(neg(conj(x, y)))⇒ Strue(neg(x))∨ Strue(neg(y)); so Lemma 1 and restricted conditional proof yield (2). Another restricted proof followed by universal generalization give the desired claim.  Str8: ⇒ ∀x[Strue(univ(v, x)) ≡ ∀y[CTerm(y) ⊃ Strue(subst(x, v, y))]] Proof. Again, I derive rule forms, then use restricted conditional proof and universal generalization. R to L rule: RHS implies both ∀y[CTerm(y) ⊃ Scl(subst(x, v, y))] and ∀y[CTerm(y) ⊃ True(subst(x, v, y))]. The rst implies Scl(univ(v, x)) by (Suniv), and the second implies True(univ(v, x)) by (Tuniv-I), and so the two together imply Strue(univ(v, x)). L to R: LHS implies both (i) Scl(univ(v, x)) and (ii) True(univ(v, x)). (ii) implies that ∀y[CTerm(y) ⊃ True(subst(x, v, y))]. By (Suniv), (i) implies that either ∀y[CTerm ⊃ Scl(subst(x, v, y))] or ∃y[Scl(subst(x, v, y)) ∧ ¬True(subst(x, v, y))]; but the second disjunct contradicts the conclusion from (ii). Using (ii) again with the remaining rst disjunct, we have ∀y[CTerm(y) ⊃ Strue(subst(x, v, y))].  Str9: ⇒ ∀x[Strue(neg(univ(v, x))) ≡ ∃y[CTerm(y) ∧ Strue(neg(subst(x, v, y)))]] THE POWER OF NAIVE TRUTH 18 Proof. Again, I derive rule forms, then use restricted conditional proof and universal generalization. R to L rule: Suppose that for some closed term y, Strue(neg(subst(x, v, y)). Then Scl(neg(subst(x, v, y)) and True(neg(subst(x, v, y)). So Scl(subst(x, v, y) and ¬True(subst(x, v, y)); so by (Suniv), Scl(univ(v, x)) and hence (i) Scl(neg(univ(v, x))). Scl(subst(x, v, y))also entails SENTL(subst(x, v, y)), so with ¬True(subst(x, v, y)) it entails True(neg(subst(x, v, y))); which then entails (ii) True(neg(univ(x, v, y))). By (i) and (ii) together, Strue(neg(subst(x, v, y))) entails Strue(neg(univ(v, x))). By ∃-Elim (equivalently, ¬∀-Elim), ∃y[CTerm(y)∧Strue(neg(subst(x, v, y))) entails Strue(neg(univ(v, x))). L to R rule: Strue(neg(univ(v, x))) implies both (i) Scl(neg(univ(v, x))) and (ii) True(neg(univ(v, x))). (i) implies Scl(univ(v, x)), which by (Suniv) implies that either (a) ∀y[CTerm(y) ⊃ Scl(subst(x, v, y))] or else (b) ∃y[CTerm(y)∧ [Scl(subst(x, v, y))∧¬True(subst(x, v, y)]]. (ii) implies that ∃y[CTerm(y)∧ ¬(True(subst(x, v, y)))]; given this, (a) above implies (b), so we've proved (b). But (given that everything Scl is a sentence, and the closure of Scl under negation), (b) implies that ∃y[CTerm(y) ∧ Scl(neg(subst(x, v, y))) ∧ True(neg(subst(x, v, y)))]; i.e. that ∃y[CTerm(y)∧Strue(neg(subst(x, v, y)))].  I now turn to laws of Struth that are analogs of Halbach's axiom KF12 and to some extent KF13; but I'll divide up KF13 and its analogs into three parts. (As we'll see, the task of interpreting KF12 and KF13 involves a major issue that doesn't arise for these analogs, and because of this, the analogy in 13c may be only partial.) Let STR represent the function taking the Gödel number of an expression x to the Gödel number of Scl(num(x)) ∧ True(num(x)) (and taking other numbers to #).19 (So STR(y) is equivalent to conj(SC(y),TR(y)).) Then Str12: ⇒ ∀x[Strue(STR(x)) ≡ Strue(x)] Proof. Since both sides of biconditional are bivalent by Lemma 1, it suces to establish the rule forms (1) Strue(STR(x))⇒ Strue(x) (2) Strue(x)⇒ Strue(STR(x)).20 (1): If Strue(STR(x)) then True(STR(x))), so Strue(x) by (TTR-E). (2): The premise implies True(STR(x)) by (TTR-I), so to get the conclusion we only need that Scl(STR(x)); which is equivalent to Scl(conj(SC(x),TR(x))). But the premise also implies Scl(x), so by L to R of (SSC-ii) and (STR-ii) 19If x is the Gödel number of a non-sentence, then this function takes it not to # but rather to the sentence that falsely attributes Struth to that non-sentence. 20Both these claims, and Str12 itself, would hold if `TR' were substituted for `STR'. Also note that (1) would hold with the weaker premise True(STR(s)); but the stronger premise is needed for going on to invoke conditional proof. THE POWER OF NAIVE TRUTH 19 it implies both Scl(SC(x)) and Scl(TR(x)). By (Sconj), this suces for Scl(conj(SCL(x),TR(x))); which is equivalent to Scl(STR(x)).  Str13a: ⇒ ∀x[Strue(neg(STR(x))) ∧ SENTL(x) ⊃ Strue(neg(x))] Proof. By Lemma 1, restricted conditional proof, and universal generalization, and the denition of Strue, it suces to prove these: (i) Strue(neg(STR(x)))⇒ Scl(neg(x)) (ii) SentL(x), Strue(neg(STR(x)))⇒ True(neg(x)). The premise of (i) implies Scl(neg(STR(x))), which implies Scl(STR(x)) by (Sneg), which amounts to Scl(conj(SC(x)),TR(x)). So by (Sconj), either (I) Scl(SC(x)) or (II) Scl(TR(x)). ((Sconj) gives more detailed information, but this is all that's needed.) But each of (I) and (II) imply Scl(x) (by (SSC-ii) and (STR-ii) respectively). So by (Sneg) again, Scl(neg(x)). As for (ii), Strue(neg(STR(x))) implies True(neg(STR(x))), which implies ¬Strue(x), i.e. ¬Scl(x) ∨ ¬True(x); and we've already established Scl(x), so ¬True(x). The truth rules plus SENTL(x) give True(neg(x)).  Str13b: ⇒ ∀x[Strue(neg(x)) ⊃ Strue(neg(STR(x)))]. Proof. (Again I prove the rule form, and conditionalize on the basis of Lemma 1.) Strue(neg(x)) implies both (A) True(neg(x)) and (B) Scl(neg(x)). (A) implies ¬True(x) by (¬Tneg-E); and hence ¬Strue(x) by denition of `Strue'. It also implies SENTL(neg(x)) and hence SENTL(x) and hence EXPRESSION(x), so SENTL(STR(x)); so (Tneg-I) yields True(neg(STR(x))). (B) implies Scl(x) by (Sneg), hence Scl(SC(x)) by (SSC-ii) and Scl(TR(x)) by (STR-ii). By (Sconj) these entail Scl(conj(SCL(x),TR(s))), which amounts to Scl(STR(x)). So by (Sneg) again, Scl(neg(STR(s))). This with the result of (A) yields Strue(neg(STR(x))).  Str13c: ∀x[¬SENTL(x) ⊃ Strue(neg(STR(x)))]. Proof. If ¬SENTL(x) then ¬Strue(x), so ¬True(STR(x)). But SentL(STR(x)), so True(neg(STR(x))). Also ¬SENTL(x) implies Scl(TR(x)) by (STR-i), and it implies ¬True(x) by T1 and hence ¬True(TR(x)) by (¬Tneg-I). That is, TR(x) is both strongly classical and untrue; so (Sconj) says that its conjunction with anything is strongly classical. In particular, Scl(conj(SC(s),TR(s))), i.e. Scl(STR(s))). So by (Sneg), Scl(neg(STR(s))).  Finally a useful pair of lemmas: Lemma 3A: ⇒ ∀x[Strue(STR(x)) ≡ Strue(TR(x))] Proof. Strue(TR(x)) means Scl(TR(x)) ∧ True(TR(x)); by (STR-ii) and the truth rules, that's equivalent to Scl(x)∧True(x), i.e. to Strue(x). And by Str12, Strue(STR(x)) is also equivalent to Strue(x). This establishes the biconditional.  THE POWER OF NAIVE TRUTH 20 Lemma 3B: ⇒ ∀x[Strue(neg(STR(x))) ≡ Strue(neg(TR(x)))] Proof. (i) If x isn't the Gödel number of an expression, then STR(x), TR(x), neg(STR(x)) and neg(TR(x)) each denote #; this implies the negations of each side of the bicondional, so the biconditional holds. (ii) If x is the Gödel number of a non-sentence, then STR(x) and TR(x) each denote strongly classical falsehoods, so neg(STR(s)) and neg(TR(s)) each denote strongly classical truths. So the biconditional holds. (iii) Suppose x is the Gödel number of a sentence. Strue(neg(TR(x))) means Scl(neg(TR(x))) ∧ True(neg(TR(x))); by (Sneg) and (STR-ii) and (Sneg) again, and the truth rules, that's equivalent to Scl(neg(x)) ∧ True(neg(x)), i.e. to Strue(neg(x)). By Str13a and b, Strue(neg(STR(x))) is also equivalent to Strue(neg(x)). This establishes the biconditional.  5. Interpreting KF+ in INT Here I show that INT interprets KF+, and thus by previous results (Halbach and Horsten 2006) interprets ramied analysis up to ε0. Most of the work for this was done in Section 4. There is an issue here about the goal. Halbach's axiomatization of KF includes what amounts to KF13c: ∀x[ ¬SENT k(x) ⊃ Truek(negk(TRk(x)))]. (The reader can ignore the subscript `k', but I think it helpful to use it for non-logical vocabulary in the language of KF prior to the reinterpretation that validates KF+ in INT. I'll soon introduce subscripts `KF ' for the reinterpretations that will validate KF+.) In KF+(though not KF) the consequent of this implies ¬Truek(TRk(x)), which together with KF12 implies ¬Truek(x); so Corollary to KF13c: ∀x[¬SENTk(x) ⊃ ¬Truek(x)]. If one accepts the Corollary (a KF analog of T1) then KF13c seems intuitively plausible. But as Halbach suggests (p. 199), neither KF13c or its corollary are needed for the proof-theoretic power of KF or KF+. Since the main aim here is to show that INT has all the proof-theoretic power of KF+, I will start out with a simple interpretation of the language of KF in INT that delivers all of KF+ except for KF13c; it doesn't deliver the corollary either. (It does deliver the analogs with SENTk replaced by SENTL. 21) Then I will briey sketch a more complicated interpretation that should yield the full KF+. The simple interpretation interprets `Truek(x)' as `Strue(x)', as long as x isn't the Gödel number of a formula of the language of KF that contains the function symbol TRk. It would be inapropriate to interpret `Truek(x)' as `Strue(x)' for other x, because a correct interpretation also needs to shift the denotation of terms in (the formula whose Gödel number is) x that contain TRk. So we need to introduce a function symbol H for a function 21This formulation assumes a Gödel numbering of L in KF, but that's unproblematic. THE POWER OF NAIVE TRUTH 21 that shifts the denotation of these terms. (That function is to be the identity except on formulas that containTRk.) `Truek(x)' will then be interpreted as `Strue(H(x))'. H is only applied to occurrences within the scope of Truek. The intuitive idea of H is that it replaces any formula containing TRk by the corresponding formula containing STR, to arbitrary depths of embedding; so that e.g. if x is a sentence not containing TRk, H maps TRk(TRk(x)) into STR(STR(x)). But as discussed in Halbach 2011 (pp. 36-38) in a more general setting, it's tricky to formalize this. (Because of self-referential uses of Truek, we can't do it by a simple induction on the depth of embedding.) To see the correct strategy, note that we want not only (i): `Truek(t)' is interpreted as `Strue(H(t))', but also (ii): the arithmetic function h that H stands for is the interpretation function induced by (i); where this means that (a) h is the identity on any number that isn't the Gödel number of a formula of the language of KF that contains Truek; (b) if n is the Gödel number of a formula of form Truek(t) then h(n) will be the Gödel number of the corresponding Strue(H(t)); and (c) h preserves the logical operations on formulas, e.g. if n is the Gödel number of a formula then h(neg(n)) = neg(h(n)). Given (b), there's an apparent circularity in demanding both (i) and (ii), but as Halbach observes, we can get an H satisfying these constraints via the version of Kleene's second recursion theorem for primitive recursive functions given in Hinman 1978 (p. 41). See Halbach for the details. One can easily check that since H satises (i) and (ii), we can derive ($): H(TRk(x)) = STR(H(x))). (Both sides denote h(Truek(x)).) This guarantees thatH does indeed translate the function symbol TRk as STR to arbitrary depths, in the way it ought to. Given the interpretation of `Truek(x)', there is an obvious strategy for interpreting `SENTk(x)' in a way that might validate KF: we dene in the arithmetic language a predicate AtFORMKF for the Gödel numbers of Lformulas that are either identities or of form of Scl(H(t)) ∧ True(H(t)); we then dene FORMULAKF and SENTKF from these in the standard way. By an easy induction on complexity, we then establish Lemma 4: ⇒ ∀x[SENTKF (x) ⊃ True(disj(x, neg(x)))], where of course disj represents disjunction. By the truth rules, this gives the schema SentKF (〈A〉) ⊃ A∨¬A. So INT validates the application of classical logic to KF-sentences. We thus need only that it validates the axioms (other than KF13c) under this simple interpretation. (By validating B under this THE POWER OF NAIVE TRUTH 22 interpretation, I mean that INT proves⇒ B∗ where B∗ is the interpretation of B.) And that the KF axioms other than 13c are validated is almost immediate given the corresponding Str theorems. For instance, • KF1 says that if s and t denotek x and y respectively, Truek(eq(s, t)) ≡ x=y). Under the interpretation, this says that if s and t denoteH(x) and H(y) respectively, Strue(eq(s, t)) ≡ H(x) =H(y)); and this is an instance of Str1. • KF3 is that for any sentence x of KF, Truek(negk(negk(x))) ≡ True(x). The proper interpretation of negk is just neg restricted to things that satisfy FORMULAKF , so the interpretation of this is in eect that if SENTKF (x) then Strue[H(neg(neg(x)))] ≡ Strue[H(x)]. But sinceH commutes with negation, this amounts to Strue[neg(neg(H(x)))] ≡ Strue[H(x)], which is an instance of Str3. • KF12 is ∀x[Truek(TRk(x)) ≡ Truek(x))]], so the interpretation of KF12 is ∀x[Strue(H(TRk(x))) ≡ Strue(H(x))]. By ($) this is equivalent to ∀x[Strue(STR(H(s))) ≡ Strue(H(x))], and that is an instance of Str12. The others are similar. In the case of KF13c and its corollary (given at the start of the section), the translation (and the fact that H preserves sentencehood and non-sentencehood) yields only the weak versions where ¬SENTk is replaced by ¬SENTL. For instance, if x is (the Gödel number of) the sentence True(〈0 = 0〉), then ¬SENTKF (x) since `True' occurs in x unconjoined with `Scl'; nonetheless TrueKF (x), i.e. Strue(H(x)), the H here being vacuous. As I've said, Halbach's KF13c isn't needed for the proof-theoretic power of KF+. So what I've established, in conjunction with Halbach and Horsten 2006, shows that INT suces to interpret ramied analysis up to ε0. If we want to interpret the full KF+, we can probably complicate the foregoing to achieve this. The basic idea is to dene AtFORMKF in a more complicated way than before, dene FORMULAKF and SENTKF from it in the usual way, and then interpret `TrueKF (x)' as `SENTKF (H(x)) ∧ Scl(H(x)) ∧ True(H(x))'. (The occurrence of H in the rst conjunct is redundant.) Because of the rst conjunct, the interpretation of `All truthsk are sentencesk' come out correct, and KF13c could easily be argued as well. The complication is in dening AtFORMKF . The atomic formulas of KF that aren't equations now need to be equivalent to L-formulas of form `FORMULAKF (x) ∧ Scl(H(x)) ∧ True(H(x))', but the rst conjunct is dened in terms of AtFORMKF , so the procedure looks circular. So we need to recast the denition of AtFORMKF as a more complicated kind of inductive denition. Again this will go by the recursion theorem. If it weren't for the H, a fairly simple use of the recursion theorem would allow for the denition of AtFORMKF (and hence FORMULAKF and SENTKF ), independent of the interpretation of `Truek'. We could then THE POWER OF NAIVE TRUTH 23 introduce the H needed for interpreting `Truek' by a separate use of the recursion theorem just as before. But given the need for H even in the interpretation of the predicate AtFormKF , things are more dicult: instead of two separate uses of the recursion theorem we need a single but more complicated one. I have little doubt that it can be provided, but I will leave that to those more expert in these matters than myself. I can take this attitude because the simple interpretation, though it doesn't yield KF-13c, suces for the proof-theoretic strength I've claimed. Indeed, if I were working from scratch rather than appealing to the results of Halbach and Horsten, I'd have skipped the interpretation of KF entirely, and directly interpreted RA<ε0 in INT: mimicing Halbach and Horsten's proof rather than simply appealing to the result. (The analog of KF13c in this setting is Str13c, which though not needed would be available if convenient.) The Str-theorems are more general than the corresponding KFaxioms, in that they apply to L-sentences that aren't the interpretations of KF-sentences, i.e. that have `True' in contexts other than `Scl(t)∧True(t)'; going by way of KF would be quite unnatural if proceeding from scratch. 6. Consistency of the non-schematic internal theory We need to prove INT consistent.22 Let INT0 be the part without the extra predicate `Scl'. Such a theory was in eect shown consistent by Kripke's well known xed point construction on a 3-valued model theory using Strong Kleene semantics, based on the standard model of arithmetic. Label the three values 0, 12 and 1, with 1 best, i.e. the value assigned to theorems, and 0 worst, i.e. assigned to negations of theorems. Call a sequent GOOD if it preserves value 1 at the minimal xed point (or at all xed points, it won't matter) of Kripke's construction, for all instantiations of the variables, in this model. The transition rules between sequences are the structural rules (which I haven't bothered to list) and the logical rules (¬∧-E), (∀-I), and (¬∀-E); these preserve GOODness. And the sequents that are axioms of the logic, arithmetic and truth theory are easily seen to be GOOD on the Kripke construction. (That includes all instances for the sequent giving the induction rule, even instances with `True': that's because we've taken the model to be standard.) So any sequent that is a theorem of INT0 is GOOD. A sequent A1, ..., An ⇒ B is naturally viewed as encoding the inference from the Ai to B (and a sequent of the special form ⇒ B as encoding the endorsement of B as a theorem). So another way to put this is: Kripke's construction shows that any inference that INT0 endorses preserves value 1 on all instantiations of the variables (at the minimal xed point, or at all of them); and in particular, any formula it endorses as a theorem has value 1 22Obviously this needs to be done in a stronger theory; a fairly weak classical set theory (with no additional truth predicate) suces. THE POWER OF NAIVE TRUTH 24 on all instantiations of the variables.23 Since some sentences don't get value 1 in all xed points (indeed in any non-trivial one), this shows that INT0 is Post-consistent; and indeed it is negation-consistent since no sentence of form A ∧ ¬A gets value 1 in any non-trivial xed point. But what about the full theory INT that includes the axioms for `Scl'? I will now provide a beefed up Kripke xed point construction, which proves the negation-consistency of the full INT in exactly the same way that the ordinary Kripke construction proves the consistency of its subtheory INT0. The trick is to run the Kripke construction twice over.24 In the rst run, we treat `Scl(x)' as equivalent to `SENTL(x)∧(True(x)∨¬True(x))'; so in this run, sentences of form `Scl(t)' get only values 12 or 1 unless the denotation of t isn't a sentence. We continue to a xed point Ω in the usual way. In the second run, we start o by closing o `Scl(x)' (but not `True(x)'): we start atomic sentences containing it with value 1 if they got value 1 at the xed point in the rst run, and 0 if they got value 12 or 0 at the xed point in the rst run. And we keep the values of `Scl(t)' xed throughout the second run. But the values of sentences of form `True(t)' vary in the second run, in the usual Kripkean way, until we reach a second xed point Ω∗. Every sentence that gets value 1 or 0 in the rst run gets the same value in the second, but some sentences that get value 12 in the rst run get another value in the second. Because of this, there will be sentences A such that A∨¬A gets value 1 in the second run even though Scl(〈A〉) gets value 0 in the second run.25 But the reverse can't happen: If Scl(〈A〉) gets value 1 in the second run, A ∨ ¬A does too. For those who prefer a more mathematical statement, here goes. For notational simplicity I initially state the construction for sentences only, rather than for formulas relative to a variable-assignment, exploiting the fact that the language contains a closed term for every object in the domain of the standard model. The construction will proceed from the standard model of arithmetic, by assigning to each (Gödel number of a) sentence of the language L and each ordinal σ ≤ ω1 * 2 a value in {0, 12 , 1}; where ω1 is the rst uncountable ordinal. (ω1 is big enough to serve as the rst xed point Ω in the sketch 23This is in marked contrast to external theories like KF+ prior to their reinterpretation in terms of strong classicality. In KF+ prior to reinterpretation, there are theorems such as ¬True(λ) where λ is an ordinary Liar sentences, and this gets value 1 2 in all Kripke xed points. There are also other sentences that get value 1 2 in all xed points that are anti-theorems of KF+: for instance, True(λ). The xed points thus don't adequately distinguish between sentences that KF+ takes to be good and sentences it takes to be bad. 24A referee has pointed out to me that this idea was used in Gupta and Martin 1984 in the context of adding a nonclassicality predicate to truth theory in Weak Kleene logic (on which, see note 8). 25A simple example is the external Liar λ∗. It and Scl(l∗) get value 1 2 throughout the rst run. At the start of the second run, |Scl(l∗)| is set at 0, so l∗ and hence disj(l∗, neg(l∗)) get value 1. THE POWER OF NAIVE TRUTH 25 above, and ω1 * 2 the second one Ω∗. If we generalized the procedure for other languages and other models, we'd go to c+ *2, where c is the maximum of the cardinalities of the domain of the model and the vocabulary of the language, and c+ is the rst ordinal of cardinality greater than c.) At every stage σ, |eq(s, t)|σ is 1 i s and t are Gödel numbers of the same closed term x; it's 0 otherwise. At every stage σ, |neg(x)|σ (when x is the Gödel number of a sentence) is 1− |x|σ; |conj(x, y)|σ (with a similar restriction) is min{|x|σ, |y|σ}; and |univ(v, x)|σ is min{|x(v/m)|σ : m a numeral}. The interesting thing is the values of the other atomic sentences. Following Kripke, we let |True(t)|σ for closed terms t be • 1 if t denotes (the Gödel number of) a sentence A for which (∃ρ < σ)(∀τ ∈ [ρ, σ))(|A|τ = 1) • 0 if either t denotes (the Gödel number of) a sentence A for which (∃ρ < σ)(∀τ ∈ [ρ, σ))(|A|τ = 0), or else t doesn't denote (the Gödel number of) a sentence of L • 12 otherwise. I formulate the clauses this way to make the consistency of the 1 and 0 clauses obvious, but once we've proved monotonicity as below, it will follow that the (∃ρ < σ)(∀τ ∈ [ρ, σ)) in them can be simplied to (∃τ < σ). In the same spirit as Kripke, we let |Scl(t)|σ be: • 1 if t denotes (the Gödel number of) a sentence A for which (∃τ < min(σ, ω1))(|A|τ ∈ {0, 1}) • 0 if either σ > ω1 and ¬(∃τ < ω1)(|A|τ ∈ {0, 1}), or else t doesn't denote (the Gödel number of) a sentence of L • 12 otherwise. In this case there is no initial worry of conict between the 1 and 0 clauses, so there's no need to resort to the (∃ρ < σ)(∀τ ∈ [ρ, σ)) formulation. Generalizing Kripke, all sentences of form True(t) or Scl(t) for which t denotes the Gödel number of a sentence get value 12 at stage 0. (For other t they get value 0.) Also, and crucially, we have monotonicity: letting u ≤K v (for u and v in {0,12 ,1}) mean that either u = 1 2 , or u = v = 0, or u = v = 1, then we can easily argue that for any sentence x of L, if τ < σ then |x|τ ≤K |x|σ .26 We can now extend Kripke's xed point argument to show the existence of double xed points. First, there can be only countably many changes prior to ω1, so there must be a σ < ω1 where for every sentence x, |x|σ+1 = |x|σ. So 26Suppose not; then there is a smallest σ, call it σ0, for which there is a sentence x that is a failure at σ in the sense that for some τ < σ, |x|τ is 0 or 1 and |x|σ 6= |x|τ . But x can't be of form True(t), since that would require that t denotes a sentence y that is a failure prior to σ0. And it can't be of form Sent(t), since if σ0 ≤ ω1 this would likewise require a failure prior to σ0, and since the only changes in valuation for Sent(t) when σ > ω1 are when σ is ω1 + 1 and go from value 1 2 to value 1. x also can't be an equality, since they never change in value as σ increases, so it can't be any atomic sentence. And the valuation rules for the Kleene connectives are such that no failure for atomic sentences implies no failure for any sentences. THE POWER OF NAIVE TRUTH 26 for any sentence of form True(s) where s denotes a sentence y, |True(s)|σ = |y|σ. Thus at a xed point value, truth is naive. Any later σ up through ω1 will give the same values as this σ gives, so for convenience we can choose ω1 as the ordinal Ω for the rst run xed point. At ω1 +1 the rule for `Scl' jolts the construction, but from there on it's basically just another Kripke construction with a dierent starting point, and thus produces another xed point prior to ω1 * 2; anything after, including ω1 * 2, is another xed point, so for convenience we can take ω1 * 2 as the ordinal Ω∗ for the second run xed point. From now on, only the values at Ω (=ω1) and Ω ∗ (=ω1 * 2) will matter. Truth behaves naively at both. At Ω, sentences of form Scl(t) where t denotes the Gödel number of a sentence get only values 12 and 1 at Ω; since there are some 12s, we do not have excluded middle for the formula Scl(v). At Ω∗, sentences of this form get only values 0 and 1 (1 if they got 1 at Ω, 0 if they got 12 at Ω); so at Ω ∗, ∀v(Scl(v) ∨ ¬Scl(v)) does get value 1. It remains to check in detail that all provable sequents of the internal theory are GOOD in a sense analogous to the one explained before: they preserve value 1 at Ω∗ for any instantiation of the variables, in this model. I'll write an instantiation of a formula A(u1, ..., un) by members x1, ..., xn of the domain as A(x1, ..., xn) (a notation which will only be used in the context where the instantiated formula is being evaluated in the model).27 The proof that the transition rules preserve GOODness, and that the sequent rules of logic, arithmetic, and truth theory are GOOD, is the same as before: here the shift to the second xed point changes nothing. Thus the only axiom-sequents that need checking are those governing `Scl'. Since there are no transition rules special to `Scl', I'll adopt the simplied formulation of inference rules and theorems introduced in the second paragraph of this section: so the task is to prove that the inference rules preserve value 1 in all instantiations, and that the theorems get value 1 in all instantiations. • We've already veried S0, excluded middle for `Scl'. (And induction for `Scl' is included in the arithmetic part.) 27In the current context, where every object in the domain gets a name, the value |A(x1, ..., xn)|σ of a parameterized formula at stage σ of the construction can be identied with the value |A(x1, ...,xn)|σ at σ of the sentence involving the corresponding numerals. In the more general case there is no such correspondence. (In that case, a proper treatment of quantication requires that the Kripke construction itself be done not in terms of sentences but of parameterized formulasor what is essentially the same, ordinary formulas relative to an assignment function for the variables. In the parameterized formula formulation, we need to take the Gödel number of a parameterized formula as a nite sequence of the ordinary Gödel number of the formula from which it was composed and the parameter values.) While what follows could be done in terms of the evaluation of the sentences A(x1, ...,xn), I nd it less confusing to think in terms of the values of parameterized formulas A(x1, ..., xn), as would be required in the more general case. THE POWER OF NAIVE TRUTH 27 • S1: If |¬SENTL(x)|Ω∗ = 1, then obviously x is not (the Gödel number of) a sentence of L. So by the valuation rule for Scl, |Scl(x)|σ is 0 at every stage of the construction and hence at Ω∗. • (Seq), stating the strong classicality of closed equations, is likewise validated: the rules give such equations value 0 or 1 at every stage of the construction, so the claim of their Sclassicality gets value 1 for each σ > 0 and hence at Ω∗. • (STR-i) and (SSC-i): Suppose that |¬SENTL(x)|Ω∗ is 1, so that x is not (the Gödel number of) a sentence of an L-sentence. By the valuation rules for `True' and `Scl', |True(x)|σ and |Scl(x)|σ are 0 for all σ; so by the valuation rules for `Scl', |Scl(TR(x))|σ and |Scl(SC(x))|σ are 1 for all σ > 0, and hence for Ω∗. • (STR-ii): Suppose that |SENTL(x)|Ω∗ is 1, so that x is an Lsentence. By the xed point property of Ω, |True(x)|Ω = |x|Ω, and indeed the same is true for all suciently large σ prior to Ω. So by the valuation rules for `Scl' and the xed point property, |Scl(TR(x))|Ω is the same as |Scl(x)|Ω (either 1 or 12). So |Scl(TR(x))|Ω∗ is the same as |Scl(x)|Ω∗ , and in this case either 1 or 0. So |Scl(TR(x)) ≡ Scl(x)|Ω∗ = 1. (Indeed, the biconditional has value 1 for any σ strictly greater than Ω.) • (SSC-ii): Again, from |SENTL(x)|Ω∗ = 1 we get that x is an Lsentence. If |x|Ω ∈ {0, 1} then |Scl(x)|Ω is 1 and hence |Scl(SC(x))|Ω is also 1; and if |x|Ω is 12 then |Scl(x)|Ω is 1 2 and hence |Scl(SC(x))|Ω is also 12 . Moving to Ω ∗, we get that if |x|Ω ∈ {0, 1} then |Scl(x)|Ω∗ and |Scl(SC(x))|Ω∗ are both 1 and otherwise they are both 0. So the biconditional Scl(SC(x)) ≡ Scl(x) has value 1 at Ω∗. (Indeed, it does at any σ > Ω.) • (Sneg): Obvious. • (Sconj): We show that at Ω∗, the formulas Scl(conj(x, y)) and (Scl(x)∧Scl(y))∨ (Scl(x)∧¬True(x))∨ (Scl(y)∧¬True(y)) have the same value, and it's never 0. That suces for the biconditional between them to have value 1 at Ω∗. (i) |Scl(conj(x, y))|Ω∗ is 1 if |conj(x, y)|Ω ∈ {0, 1}, and 0 otherwise. (Note shifts here and in rest of proof from Ω∗ to Ω.) Hence it's 1 i either |x|Ω and |y|Ω are both in {0, 1} or one of them is 0; i.e. if one of them is 0 or both are 1. And it's 0 otherwise. (ii-a) |Scl(x) ∧ Scl(y)|Ω∗ is 1 if |x|Ω and |y|Ω are both in {0, 1}; and 0 otherwise. (ii-b) |Scl(x) ∧ ¬True(x)|Ω∗ is 1 i |x|Ω = 0; similarly for y in place of x. So at Ω∗, the threedisjunct disjunction has value 1 i either |x|Ω and |y|Ω are both in {0,1}, or one of them is 0; and 0 otherwise. This is the same as the 1-condition in (i). And here too the disjunction has value 0 in all other cases. THE POWER OF NAIVE TRUTH 28 • (Suniv): Unless v is the Gödel number of a variable and x the Gödel number of a formula with only that variable free then obviously (the instantiations of) both sides have value 0 (at Ω∗ and everywhere else), so the biconditional is trivial when the condition isn't met. Assuming it is met, |∀y(CTerm ⊃ Scl(subst(x, v, y)))|Ω∗ is 1 i for every closed term t, the value of subst(x, v, t) at Ω is in {0, 1}. And |∃y(Scl(subst(x, v, y)) ∧ ¬True(subst(x, v, y))|Ω∗ is 1 i for some closed term t, the value of subst(x, v, t) at Ω is 0. So the value of the disjunction that's the RHS of (Suniv) is 1 i either for some closed term the value of subst(x, v, t) at Ω is 0, or else for every closed term the value of subst(x, v, t) at Ω is 1. And neither term of the disjunction can have value 12 , so the disjunction can't either. Clearly these are exactly the values one gets for |Scl(univ(v, x))|Ω∗ . Since the values at Ω∗ are the same and never 12 , the biconditional has value 1 at Ω∗. • (S-Main): |Scl(x)|Ω∗ is 0 or 1, and if 0 then |Scl(x) ⊃ (True(x) ∨ ¬True(x))|Ω∗ is obviously 1, so we need only consider the case where |Scl(x)|Ω∗ is 1. But in that case Scl(x) gets value 1 already at Ω, so True(x) ∨ ¬True(x) does too, and it retains this value at Ω∗. This completes the model-theoretic proof of the consistency of INT. 7. The schematic expansions of KF+ and INT Since it's known that KF+ (indeed, KF) can interpret RA<ε0 (ramied analysis up to ε0), the above results show that the internal theory we've been considering can consistently do so too. It would be nice to go further: to RA<α for larger α. An obvious way to do so, though not so attractive, is to introduce weaker and weaker strong classicality predicates. Pick an ordinal α (say Γ0) such that for each predicate β < α we have a satisfactory ordinal notation, and introduce a separate predicate Sclβ for each such β. Then iterate the Kripke construction through ω1 * α: whenever 1 ≤ β < α we close o Sclβ at ω1 * β.28 But it isn't altogether attractive to use a hierarchy of primitive predicates. (This would be an analog of Kripke's ghost of the Tarski hierarchy, though with strong classicality stratied instead of KF-like truth. Presumably each level of the ghost hierarchy, with an array of KF-like predicates Trueβ , would be interpretable in a theory with a corresponding array of predicates Sclβ .) There's a much better approach, which is an internal analog of the classical approach of Feferman 1991. Feferman noted that the standard presentation of induction in Peano arithmetic (or expansions of it like KF), as simply consisting of the set of rst order instances of the schema, doesn't really capture the intended strength. The intended strength is better represented 28There is then a hierarchy of external Liar sentences: for each β < α, a sentence declaring itself not both true and Sclβ . The theory would prove it true and Sclβ+1 though not Sclβ . THE POWER OF NAIVE TRUTH 29 as a schematic axiom: something like a second order axiom, but in a context where there are no second order quantiers. We have just a single unquantiable schematic variable P , and formulate induction in a classical setting using this variable as (Classical Schematic Induction): [P (0)∧∀x(P (x) ⊃ P (suc(x)))] ⊃ ∀xP (x). Of course, if we have these schematic variables, we will need a substitution rule for them. Will the schematic theory with this substitution rule be a mere conservative extension of the corresponding non-schematic theory? Feferman showed that this depends on the formulation of the substitution rule. If the legitimate substituends are restricted so that the schematic variable isn't allowed in the substituends, the extension is conservative. But what interested Feferman was an enhanced rule where the schematic variable can appear in the substituends. In arithmetic itself this makes no dierence. But Feferman observed that in the context of the theory KF (or KF+), the schematic theory with this substitution rule is highly non-conservative: instead of merely interpreting RA<ε0 , it gives full predicative analysis (RA<Γ0). There's no need to go through how it does this.29 As in the case of KF+, my strategy will be to show that whatever can be done in this theory S-KF+ can be done in an internal analog of it, which I'll call S-INT. S-INT will simply be a schematic version of the theory INT already presented; and I'll extend the strategy used with unschematic KF+, by showing that S-INT is consistent and can interpret S-KF+ within it.30 First I sketch Feferman's theory S-KF+. Its language L(P ) is the language of PA expanded to include both `True' and a unary schematic variable (i.e. unquantiable second order variable) `P '. Its formalization involves Ext 1: An arithmetic theory like that of KF, except with the Classical Schematic Induction given above in place of the usual rst order induction schema; Ext 2: All the axioms and rules of both rst order logic and KF+, understood to apply to formulas that contain `P ' as well as ones that don't. In the case of Axioms 5, 13a and 13c of KF+ we understand `SENTk' as formula of KF(P ) with no free variables other than `P '  29Feferman's argument is complicated, but its basic strategy is to show via schematic reasoning that if ramied analysis holds up to α then it holds up to Φ(α, 0), where Φ is the Veblen function; since Γ0 is the rst xed point of the function λαΦ(α, 0), this allows us to bootstrap our way up to RA<Γ0 . 30There's another extension of KF+ that yields full predicative analysis and beyond: Burgess's KFμ (2014), which incorporates within it a minimality axiom, expressing that the truths are just the sentences that get value 1 in the minimal xed point, i.e. what Kripke 1975 calls the grounded truths. I doubt that there's a way to nd a natural internal theory in which one can interpret this minimality axiom: that axiom seems to have a rather impredicative character beyond the reach of my sort of internal theory. (In my consistency proof I've used minimal xed points for convenience, but others would do: the theory of strong classicality in this paper is not commited one way or the other on the identication of the strongly classical with the grounded.) THE POWER OF NAIVE TRUTH 30 (P -sentence, for short). [Feferman actually uses KF instead of KF+, but the dierence won't matter.] Ext 3: A new pair of truth axioms: Let P represent the function taking the Gödel number of a term t to the Gödel number of the corresponding schematic formula `P (t)' (and taking other numbers to #). (Tschem-i): ⇒ ∀s[¬CTerm(s) ⊃ ¬True(P(s)] (Tschem-ii): ⇒ ∀s∀x[s denotes x ⊃ [True(P(s)) ≡ P (x)].31 Ext 4: An enhanced substitution rule. To formulate it, we need a notion of substituting a formula B(v) for `P ' in a schematic formula A(P ). (B(v) may contain free variables in addition to `v'; these may include `P '.) What this means is basically just that whenever a formula of form P (t) appears in A(P ) it is replaced by the corresponding B(v/t). (For the usual reasons, some replacement of bound variables in A(P ) may be required if they occur free in B(v); I won't bother to spell this out.) We can write the result of such a substitution as A(vB(v)). Feferman's enhanced rule is then: Feferman Rule: ` A(P ) ` A(vB(v)) if A(P ) doesn't contain `True'. B(v) is allowed to contain both `True' and `P '; as remarked, the allowance of `P ' in B is crucial to the proof-theoretic strength of the theory. I now turn to S-INT, the internal analog of S-KF+. Its language will be the language of INT expanded to include the new schematic variable; in other words, the language of S-KF expanded to include `Scl' (though with `True' understood dierently than in S-KF). Int 0: In line with the interpretation of schematic variables just mentioned, we include the new axiom (P-LEM): ⇒ ∀x(Px ∨ ¬Px). (This will of course mean that we need new restrictions in the substitution rule.) Int 1: We keep the Induction Rule of INT, but now allow the schematic variable `P ' in instances of the schema. So an instance of the induction rule is P (0) ∧ ∀x(P (x) ⊃ P (suc(x))⇒ ∀xP (x). Given P-LEM, this implies Classical Schematic Induction, so it might be thought that there's no need to use the rule form of Schematic Induction as basic. But because of the modication to be proposed in the Feferman substitution rule, the rule form strengthens Classical Schematic Induction: the latter wouldn't be enough to deliver all instances of the unschematic induction rule. 31One might be surprised at the inclusion of this in a classical theory, but Feferman interprets it as eectively saying that for any subset X of the natural numbers, `P (x)' is true relative to the assignment of X to `P ' i x ∈ X; on that interpretation, restrictions on (Tschem-ii) would be unwarranted. The restriction on A(P ) in the substitution rule below makes clear that there is no threat of paradox. THE POWER OF NAIVE TRUTH 31 Int 2: All the axioms and rules of both K3 and INT are understood to apply to formulas that contain `P ' as well as ones that don't. In the case of T1 and some of the S-rules, we understand `SENTL' as P -sentence, i.e. formula of L(P ) with no free variables other than `P ' . Int 3a: We add the truth axioms (Tschem-i) and (Tschem-ii) for the atomic `Pt'. (Instead of the latter we could use four rules of T-E, ¬T-I, T-I and¬T-E for P , but given (P-LEM) this is equivalent to adding (Tschem-ii).) Int 3b: We also need a corresponding pair of axioms for `Scl': (Sschematicvbl-i): ⇒ ∀s[¬CTerm(s) ⊃ ¬Scl(P(s)] (Sschematicvbl-ii): ⇒ ∀s[CTerm(s) ⊃ Scl(P(s)]. Int 4: For substitution rule I propose Modied Feferman Rule: ⇒ A(P ) ∀v(B(v) ∨ ¬B(v))⇒ A(vB(v)) ifA(P ) doesn't contain `True' or `Scl'. Again, there is no restriction on the substituting formula B(v) (as long as we ddle with the bound variables of A(P ) in case of clashes): it can contain `True' and `Scl', and also `P '. 8. Interpreting S-KF+ in S-INT The interpretation of S-KF+ in S-INT will be just like the interpretation of KF+ in INT: interpret the `True' of S-KF+ as strong truth, i.e. the conjunction of strong classicality and truth.32 Of course, this now applies not just to ordinary sentences but to P -sentences: i.e., formulas with no free variables other than `P '. We need to verify that this does indeed validate the axioms and rules of S-KF+, including its use of excluded middle across the board. But this involves little new: by and large the discussion of Sections 4 and 5 carries over without change when the formulas are schematic. Besides this there are only three things that need to be checked, and one of them, Classical Schematic Induction, has already been discussed. This leaves the (Tschem) axioms (Ext 3) and the Feferman Substitution Rule (Ext 4). Regarding the former, we've included corresponding (Tschem) axioms in S-INT, but we need the analogs with `Strue' for `True'. But given also the (Sschem) axioms of S-INT, this is a trivial consequence. As for the Feferman Substitution Rule, this involves A(P ) where A is in the schematic arithmetical language only (no additional predicates). By the analogous rule in S-INT, ` ∀v(B(v) ∨ ¬B(v)) ⇒ A(vB(v)). But for B(v) 32As we've seen there are really two interpretations, a simple one that doesn't deliver the inessential KF-13c and a more sophisticated one that does. For simplicity I've built my remarks here around the simple one, but with more complicated wording the point would extend to the other. THE POWER OF NAIVE TRUTH 32 in the restricted language L* built up from identities and formulas of form `Scl(t) ∧ True(t)', ` ∀v(B(v) ∨ ¬B(v)); so for such formulas, ` A(vB(v)). To summarize where we are, this result together with the powerful results of Feferman 1991 shows that all of predicative analysis can be carried out in the internal theory S-INT. That's the power of naive truth (or to be more accurate, of naive truth plus a strong classicality predicate). 9. Consistency of the schematic internal theory I turn nally to the consistency of S-INT. Here too little needs to be changed from the double Kripke construction of Section 5. We need to discuss how the model-theory applies to the schematic theory S-INT. This is analogous to how Feferman (1991) applied model theory in the case of S-KF+, but for clarity I spell this out. Let a standard schematic model MY,Z of the language of S-INT consist of the standard model M of arithmetic together with two functions Y and Z, each of which takes an arbitrary subset X of the domain of M (the natural numbers) to functions on the domain of M with values in {0,12 ,1}. For any X ⊆ M , let MY,Z(X) (equivalently, MY (X),Z(X)) be the 3-valued model of the language of S-INT that treats `P ' as an ordinary {0, 1}-valued predicate with extension X (i.e. it's evaluated by the characteristic function of X) and that evaluates `Scl' by Y (X) and `True' by Z(X). Then in any such MY,Z , and for any subset X of the domain ofM , every sentence in L(P ) gets a value in this 3-valued model. Of course this won't be a very useful assignment of values unless Y and Z are chosen properly. To choose a good Y and Z, we run the double Kripke construction of Section 5 in this general setting: we construct sequences Yσ and Zσ for ordinals σ ≤ ω1 * 2, by relativizing to X the rules for `True' and `Scl' given before. (The X is held xed in the construction.) That is: for each such σ, and subset X of the domain, and natural number n, [Yσ(X)](n) is • 1 i n is the Gödel number of a sentence A such that for some τ that precedes both σ and ω1, A gets value 0 or 1 in MYτ (X),Zτ (X), • 0 i either σ > ω1 and n is the Gödel number of a sentence A that gets only value 12 in any MYτ (X),Zτ (X) for which τ precedes both σ and ω1, or else n isn't the Gödel number of a sentence; • 12 otherwise. [Zσ(X)](n) is • 1 i n is the Gödel number of a sentence A such that for some interval just prior to σ, A gets value 1 relative to MYτ (X),Zτ (X), for each τ in the interval; • 0 i either n is the Gödel number of a sentence A such that for some interval just prior to σ, A gets value 0 relative to MYτ (X),Zτ (X), for each τ in the interval; or else n isn't the Gödel number of a sentence; • 12 otherwise. THE POWER OF NAIVE TRUTH 33 The argument from before then tells us that for each X, we get a 3-valued xed point model by assigning the extension X to `P ' and evaluating `Scl' and `True' by YΩ(X) and ZΩ(X), where Ω is ω1; similarly if we evaluate them by YΩ∗(X) and ZΩ∗(X), where Ω ∗ is ω1 * 2. (The ordinals at which the construction rst reach the two xed points will depend on the X; but since, for any X, the rst xed point is reached prior to ω1 and remains through ω1, and analogously for the second, we get the common xed points as claimed.) From now on the only two ordinals that will matter are Ω and Ω∗; for each X, we will evaluate all sentences, relative to any X, at both Ω and Ω∗. As before, it's the values at Ω∗ that are important for evaluating inferences, but those at Ω are needed for determining the extension of `Scl' at Ω∗ relative to X. We must state the good-making property that we want sequents of the schematic theory to have. Call a sequent UNIFORMLY GOOD if for every set X of natural numbers, the inference it encodes preserves the property of having value 1 relative to X at Ω∗, for all instantiations of the variables, in this model. The transition rules between sequents now include the Modied Feferman Rule, so a main task is to verify that this rule preserves UNIFORMGOODness. (The only other transition rules of the system are the structural rules that I haven't bothered to list, and the logical rules (¬∧-E), (∀-I), and (¬∀-E); that these ones preserve UNIFORM-GOODness is evident.) As for the sequent axioms themselves, all the ones whose P -free versions were shown GOOD for INT are obviously UNIFORMLY GOOD, since for sequents themselves (as opposed to transition rules between them) the schematic variable simply functions as a new predicate. (This handles what I earlier called Int 1 and Int 2 in my comparison to Feferman's schematic theory.) So besides the Modied Feferman substitution rule (Int 4), we need only consider the new sequent axioms of this theory, which are (P-LEM), (Sschem-i), (Sschem-ii), (Tschem-i) and (Tschem-ii) (which were Int 0, Int 3a and Int 3b). • That (P-LEM) is UNIFORMLY GOOD is trivial, since for any σ, |P (y)|Xσ is 1 if y ∈ X and 0 otherwise. • (Tschem-i) and (Sschem-i): If s isn't (the Gödel number of) a closed term then P(s) isn't a P-sentence, so for any X and any σ > 0, |True(P(s))|Xσ = 0 and |Scl(P(s))|Xσ = 0. So for any X and any σ > 0, |∀s[¬CTerm(s) ⊃ ¬True(P(s))]|Xσ = 1, and analogously with Scl(P(s)) for ¬True(P(s)), establishing that (Tschem-i) and (Sschem-i) are UNIFORMLY GOOD. • (Sschem-ii): If s is (the Gödel number) of a closed term, say for x, then P (s) is a sentence whose value for any X and σ is 1 if x ∈ X and 0 otherwise. In that case, for anyX and any σ > 0, |Scl(P(s))|Xσ = 1. THE POWER OF NAIVE TRUTH 34 So for any X and any σ > 0, |∀s[CTerm(s) ⊃ Scl(P(s))]|Xσ = 1. So (Sschem-ii) is UNIFORMLY GOOD. • (Tschem-ii): If s denotes x then P(s) is a sentence; so for any X and any σ > 0, |True(P(s))|Xσ = |P (x)|Xσ . This is 1 or 0 (depending on whether x ∈ X), so |True(P(s)) ≡ P(x)|Xσ = 1. So for any X and any σ > 0, |∀s∀x[s denotes x ⊃ [True(P(s)) ≡ P (x)]]|Xσ = 1, establishing that (Tschem-ii) is UNIFORMLY GOOD. • Finally the Modied Feferman Rule. Suppose that ⇒ A(P ) is UNIFORMLY GOOD, with A(P ) in the arithmetical language, i.e. not containing `True' or `Scl'. We need that for any given B(P, v), ∀v(B(P, v)∨¬B(P, v))⇒ A(vB(P, v)) is UNIFORMLY GOOD. Fix B(P, v), and for any set Y , letXY be {x : |B(P, x)|YΩ∗ = 1}. The only occurrences of `P ' in A(vB(P, v)) are within the B; and since A(P ) is in the arithmetical language, we have that for any σ, if |∀v(B(P, v)∨ ¬B(P, v))|Yσ = 1 then |A(vB(P, v))|Yσ = |A(P )|XYσ . The UNIFORM GOODNESS of A(P ) says that at σ = Ω∗ the right hand side is 1; so for any set Y of natural numbers, if |∀v(B(P, v) ∨ ¬B(P, v))|YΩ∗ = 1 then |A(vB(P, v))|YΩ∗ = 1. That completes the proof of the consistency of the internal theory S-INT. 10. Concluding remarks 10.1. Extensions. I mentioned early in the paper that for reasons independent of the proof-theoretic considerations that have been the topic of this paper, the logic K3 seems expressively inadequate: it lacks a conditional that is well-behaved in non-classical contexts, and relatedly, it lacks a well-behaved way of expressing restricted universal generalizations in non-classical contexts. Those defects didn't raise their heads in this paper because the idea of this paper was to add a new predicate that allowed us to maximize the classical contexts. But the work in the present paper does nothing to make the problems go away when we do deal with non-classical contexts. There thus remains the task of combining the added strong classicality predicate with the conditionals and the restricted quantier. I suspect that there is no diculty in doing this, though there are choices to be made and there might be some issue about which is best. Typical approaches to adding new conditionals (not only my own, as given for instance in Field 2016, but also earlier approaches such as Brady 1983) work by a macroconstruction consisting of a series of Kripke constructions, leading up to a privileged Kripke construction (in the case of my approach, at what are called reection ordinals).33 The simplest way to incorporate a strong classicality predicate would be to simply perform the kind of double Kripke construction considered here at the privileged stage. An alternative 33In earlier work I'd called them acceptable ordinals, but that was before Anil Gupta pointed out to me that my work proving their existence duplicated previous work establishing them under another name. THE POWER OF NAIVE TRUTH 35 approach would be to substitute the double Kripke construction for the single at each stage of the macroconstruction, not just the privileged stage, using the second half as the basis for later stages of the macroconstruction. (If one does that, then to avoid problems about the treatment of `Scl' at limit stages, it's probably best to make it behave in a Brady-like way despite the overall construction being revision-theoretic, as I advocated for propertyidentity in my 2018b. This would make fewer sentences involving the new conditionals strongly classical, but should improve the laws for the strong classicality predicate in this setting.) I should mention that on my currently preferred approach (2018a), which works from a semantics based on the unit interval [0,1] rather than on the 3-valued semantics, it is almost certainly possible to signicantly expand the present approach by adding not only a strong classicality predicate but also a weaker strong regularity predicate. Call a formula B regular if (> → B) ↔ B holds of it (where → is the conditional related to restricted quantication). A formula that obeys excluded middle is regular, but the converse is far from the case: indeed, in the theory of my 2018a, nearly all of the standard paradoxical sentences are regular. (The ones that can be handled with a naive truth predicate in ukasiewicz continuum-valued semantics are all regular.) Strong regularity is to be a bivalent property that guarantees regularity, in the same way that strong classicality is a bivalent property that guarantees excluded middle. Adding a strong regularity predicate in addition to a strong classicality predicate would not only greatly expand the domain in which classical logic holds (as done in this paper), but also supply a wider expanded domain in which ukasiewicz continuum-valued logic holds. But that is a matter for another time (and, I hope, another person). 10.2. Other morals. Many people, including myself in my 2008, have viewed internal theories based on non-classical logics and external theories like KF or KF+ or S-KF+ as competitors: they've assumed that choosing one of them involves rejecting the other. But of course this needn't be so: one could take one to be basic, and interpret the other within it. The task of interpreting the internal within the external is not promising: one could simply piggyback on the external, by taking A1, ..., An ` ∗B to mean that `KF True(〈A1〉) ∧ ... ∧ True(〈An〉) ⊃ True(〈B〉), but any attempt to do something similar in a more autonomous way results in a very weak internal theory. Any such approach would make it appear as if internal theories are merely impoverished versions of the external theories that interpret them. My approach in this paper has been the reverse: to interpret theories like KF+ or S-KF+ within internal theories. This approach seems to me better on two grounds. First, it accords with the idea (compellingly argued by many philosophers) that the most generally useful notion of truth (or perhaps the philosophically basic one) is naive. Second, the theory that this approach leads to is strictly stronger than the classical theory, in that it contains the latter within it. (I don't claim that it has greater proof-theoretic THE POWER OF NAIVE TRUTH 36 strength, i.e. that it proves more arithmetic sentences: I'm quite sure that it doesn't.) This is very much in contrast to the strong suggestion in Halbach 2011 and Halbach and Nicolai 2018 that non-classical theories are inherently impoverished. The approach here also shows that my rhetoric in my 2008 against external theories was misplaced: they are perfectly good theories. They aren't theories of truth in the philosophically most important sense, but they are good theories of a notion of strongly classical truth, which (though perhaps containing some arbitrary elements) is perfectly intelligible.34 References [1] Brady, Ross 1983. The Simple Consistency of a Set Theory Based on the Logic CSQ. Notre Dame Journal of Formal Logic 24: 431-49. [2] Burgess, John 2014. Friedman and the Axiomatization of Kripke's Theory of Truth. In Neil Tennant, ed., Foundational Adventures: Essays in Honor of Harvey M. Friedman. Pp. 125-48. [3] Feferman Solomon 1991. Reecting on Incompleteness. Journal of Symbolic Logic 56: 1-49. [4]  2008. Axioms for Determinateness and Truth. Review of Symbolic Logic 1: 204-217. [5]  2012. Axiomatizing Truth: Why and How? In (U. Berger, et al., eds.) Logic, Construction, Computation, Ontos Verlag, Frankfurt (2012), 185-200. [6] Field, Hartry 2008. Saving Truth from Paradox. Oxford University Press. [7]  2016. Indicative Conditionals, Restricted Quantication and Naive Truth. Review of Symbolic Logic 9: 181-208. [8] 2018a Properties, Propositions and Conditionals. Australasian Philosophical Review 4: xxxxx. [9] 2018b Reply to Zach Weber. Australasian Philosophical Review 4: xxxxx. [10] Gupta, Anil and Martin, Robert 1984. A Fixed Point Theorem for the Weak Kleene Valuation Scheme. Journal of Philosophical Logic 13: 131-5. [11] Halbach, Volker 2011. Axiomatic Theories of Truth. Cambridge University Press. [12] Halbach, Volker and Fujimoto, Kentaro (in preparation). Classical Determinate Truth I. [13] Halbach, Volker and Horsten, Leon 2006. Axiomatizing Kripke's Theory of Truth. Journal of Symbolic Logic 71: 677-712. [14] Halbach. Volker and Nicolai, Carlo 2018. On the Costs of Nonclassical Logic. Journal of Philosophical Logic 47: 227-57. [15] Hinman, Peter 1978. Recursion-Theoretic Hierarchies. Springer. [16] Kripke, Saul 1975. Outline of a Theory of Truth. Journal of Philosophy 72: 690-716. [17] Picollo, Lavinia 2018. Truth in a Logic of Formal Inconsistency: How classical can it get?, Logic Journal of the IGPL, jzy059, https://doi.org/10.1093/jigpal/jzy059. [18] Priest, Graham 1998. What's So Bad About Contradictions? Journal of Philosophy 95: 410-26. [19] Wang, Hao 1961. The Calculus of Partial Predicates and its Extension to Set Theory. Mathematical Logic Quarterly 7: 283-8. 34ACKNOWLEDGEMENTS