Sunday, 20 March 2011

On Adding a Validity Predicate to PA

This note was occasioned by reading JC Beall & Julien Murzi's manuscript, "Two Flavors of Curry's Paradox" concerning the possibility of reconstructing a Curry-style paradox within a theory of validity.

Under certain circumstances, the theory is consistent, as it can be interpreted inside Peano arithmetic, $PA$. Suppose we begin with $PA$ in its usual first order language $\mathcal{L}$ with $=, 0, S, +$ and $\times$. Suppose that $\vdash$ stands for ordinary first-order deducibility. "$P$ is a derivation of $B$ from $A$" means "$P$ is a finite sequence $(P_0, ..., P_n)$ where $P_n$ is $B$, and each $P_i$ is either a logical axiom, or is $A$, or is obtained from previous formulas by Modus Ponens". The relation "$P$ is a derivation of $B$ from $A$" is decidable. So, it can be strongly represented in $PA$ by a recursive formula, $\mathbf{Proof}(x, y, z)$, in such a way that:
  • (i) If $P$ is a derivation of $B$ from $A$ then $PA \vdash \mathbf{Proof}(\ulcorner P \urcorner, \ulcorner A \urcorner, \ulcorner B \urcorner)$.
and
  • (ii) If $P$ is not a derivation of $B$ from $A$ then $PA \vdash \neg \mathbf{Proof}(\ulcorner P \urcorner, \ulcorner A \urcorner, \ulcorner B \urcorner)$.
Write $\mathbf{Val}(\ulcorner A \urcorner, \ulcorner B \urcorner)$ to mean: "there is a derivation of $B$ from $A$".
Then (i) guarantees that we have a version of (V-Intro):
  • (V-Intro) $\text{If } A \vdash B, \text{ then } PA \vdash \mathbf{Val}(\ulcorner A \urcorner, \ulcorner B \urcorner)$.
[This doesn't say that $PA$ itself is closed under this introduction rule. If that were so, we would have a version of Montague's Paradox.]

Next, as $PA$ is sound, if $PA \vdash \mathbf{Val}(\ulcorner A \urcorner, \ulcorner B \urcorner)$, then $\mathbf{Val}(\ulcorner A \urcorner, \ulcorner B \urcorner)$ is true --- that is, $A \vdash B$. So, we have a version of (V-Elim):
  • (V-Elim) $\text{If } PA \vdash \mathbf{Val}(\ulcorner A \urcorner, \ulcorner B \urcorner), \text{ then } A \vdash B$.
Finally, the difficult part. A property of $PA$ is that, for every $\mathcal{L}$-sentence $A$:

(iii) $PA \vdash A \rightarrow \mathbf{Con}(A)$.

where $\mathbf{Con}(A)$ means: "there is no derivation of $0 = 1$ from $A$".

[Update, 6 April: This is a non-trivial result about $PA$. (See Hajek/Pudlak, 1993, Metamathematics of First-Order Arithmetic, p. 108.) It is intimately related to the fact that $PA$ is reflexive - $PA$ proves the consistency of any of its finitely axiomatized subtheories. The proof of (iii) in Hajek/Pudlak uses partial truth definitions, first to show that $I\Sigma_k$ proves the consistency of all true $\Pi_{k+1}$-sentences.]

So,

(iv) $PA \vdash \neg(A \rightarrow B) \rightarrow \mathbf{Con}(\neg(A \rightarrow B))$.

So,

(v) $PA \vdash \neg \mathbf{Con}(\neg(A \rightarrow B)) \rightarrow (A \rightarrow B)$.

The validity of the inference in logic from $A$ to $B$ can be expressed by saying that the sentence $\neg (A \rightarrow B)$ is not consistent. This in fact can be proved in $PA$ itself,

(vi) $PA \vdash \mathbf{Val}(\ulcorner A \urcorner, \ulcorner B \urcorner) \leftrightarrow \neg \mathbf{Con}(\neg (A \rightarrow B))$.

So, we get a version of the scheme (V-Out):
  • (V-Out) $PA \vdash \mathbf{Val}(\ulcorner A \urcorner, \ulcorner B \urcorner) \rightarrow (A \rightarrow B)$.
[Relatedly, $PA$ proves the local reflection scheme for logic: if $\mathbf{Prov}_{\emptyset}(x)$ means "$x$ is a theorem of logic", then $PA$ proves all instances of $\mathbf{Prov}_{\emptyset}(\ulcorner A \urcorner) \rightarrow A$.]

So, $PA$ itself is a consistent theory that already contains a theory of validity with versions of (V-Intro), (V-Elim) and (V-Out).

Application to Curry's Paradox:
The example discussed in Beall & Murzi concerns a validity-Curry sentence, a sentence $C$ which says "I am inconsistent". In the case of $PA$, choose $C$ such that,

(vii) $PA \vdash C \leftrightarrow \mathbf{Val}(\ulcorner C \urcorner, \ulcorner \bot \urcorner)$.

where $\bot$ is some contradiction (e.g., $0 \neq 0$). Using property (V-Out), we get:

(viii) $PA \vdash C \rightarrow (C \rightarrow \bot)$.

[Note: this is where we are about to use something like "contraction", as $C \rightarrow (C \rightarrow \bot)$ is equivalent in classical logic to $C \rightarrow \bot$.]

Thus,

(ix) $PA \vdash \neg C$.

So, since $PA$ is sound, $C$ is not true. This tells us that $\mathbf{Val}(\ulcorner C \urcorner, \ulcorner \bot \urcorner)$ is not true. In other words, $C$ is consistent. In particular, it is not the case that $\bot$ is derivable in logic from $C$. This is why we cannot apply (V-Intro). Rather, $\bot$ is derivable in $PA$ itself from $C$, and $PA$ is stronger than logic. From (vii) and (ix), $PA \vdash \neg \mathbf{Val}(\ulcorner C \urcorner, \ulcorner \bot \urcorner)$. So:

(x) $PA \vdash \mathbf{Con}(C)$.

Beall & Murzi (ms) give a derivation of a contradiction from a sentence like $C$, but their derivation uses a different version of (V-Intro). Suppose $V$ is a theory of validity (including arithmetic) such that:
  • $V$ permits diagonalization.
  • $V$ proves each instance of the scheme (V-Out).
  • $V$ has the following form of the (V-Intro) rule:
  • (V-Intro)* $\text{If } V, A \vdash B, \text{ then } V \vdash \mathbf{Val}(\ulcorner A \urcorner, \ulcorner B \urcorner)$.
Then, following Beall & Murzi's derivation, $V$ is inconsistent:
  1. $V \vdash C \leftrightarrow \mathbf{Val}(\ulcorner C \urcorner, \ulcorner \bot \urcorner)$.
  2. $V \vdash \mathbf{Val}(\ulcorner C \urcorner, \ulcorner \bot \urcorner) \rightarrow (C \rightarrow \bot)$.
  3. $V, C \vdash \mathbf{Val}(\ulcorner C \urcorner, \ulcorner \bot \urcorner)$.
  4. $V, C \vdash C \rightarrow \bot$.
  5. $V, C \vdash \bot$.
  6. $V \vdash \mathbf{Val}(\ulcorner C \urcorner, \ulcorner \bot \urcorner)$.
  7. $V \vdash C$.
  8. $V \vdash \bot$.
The crucial step that might be considered problematic is (6), which invokes the strong introduction rule (V-Intro)* to infer $\mathbf{Val}(\ulcorner C \urcorner, \ulcorner \bot \urcorner)$ from a derivation of $\bot$ from $C$ in the theory $V$ itself. But the derivation of $\bot$ from $C$ inside $V$ surely doesn't imply that the inference of $C$ to $\bot$ is logically valid.

Abstracting from the interpretation of $\mathbf{Val}$, this seems to me to be closely related to a version of Montague's Paradox: a theory which contains an "absolute knowability" predicate satisfying an (Intro) rule and an (Out) scheme.

[Update 1, 16 April: LaTeX-ified.]

[Update 2, 24 April: Since the issue of logical derivability is crucial here, I've changed occurrences of $0=1$ (which is normally used in discussion of consistency for systems of arithmetic) to $\bot$, which stands for a genuine contradiction, say $0 \neq 0$.]

14 comments:

  1. Thanks much for these comments, Jeff. Indeed, the validity paradox we discuss is closely related to the Montague-Kaplan-Myhill Paradox, or Paradox of the Knower, and absolute knowability (I talk about this and Myhill 1960 in a follow up to the paper with Jc I have recently drafted).

    Concerning the step from 5 to 6, I tend to take the validity predicate to express a broader notion of validity (although we don't really say as much in the paper). At any rate, what you suggests seem to point to a hierarchical approach to v-curry - one on which validity predicates are always added on the top of deductive systems, so to speak. I think I like this approach; this is very likely the way to go if we're classical logicians. Incidentally, Myhill's 'Levels of implication' (1975) may point in that direction, although I haven't had a chance to get a hold of this paper yet (I must read it, and it may be a good idea to discuss it at some point in our reading group!).

    ReplyDelete
  2. OK: 'what you suggest seems to point'

    ReplyDelete
  3. Hi Julien - I don't know Myhill's paper, so yes, let's discuss that (I'm not in Munich this week though). Right, you and JC are treating validity as a broader notion than logical (e.g., first-order) implication. So, (V-Intro)* yields Val("A", "B") given a derivation of B from A in the theory of validity+arithmetic.

    ReplyDelete
  4. Hi Jeff,

    Julien suggested I post here with a few thoughts on this, to see what you think, if you get time.

    I take it the sticking point between your suggestion and Julien and JC's is that the notion of validity they use is broader that logical validity. In particular, their Valid-In rule will apply to derivations which might have used that very rule itself (or of course Valid-Out).

    One way around this is to say that Valid-In cannot properly be applied to derivations which include applications of Valid-In. But I think we can allow them this broader notion of validity and simply restrict Valid-Out to an axiom form.

    So, I propose the following theory T (which includes PA). We have an axiom:

    (Val-Out) A & Val(A, B) --> B

    for all A, B in the language of arithmetic plus the predicate Val(x, y). In addition we have a sequent rule:

    (Val-In) A |- B
    ---------
    |- Val(A, B)

    where the derivation from A to B might have used applications of Val-In.

    Then I claim that there is a relation |-* which is closed under classical consequence and satisfies Val-In. Moreover I claim that there is an extension of the standard model of arithmetic N to include an extension for Val(x, y) which satisfies Val-Out and for which |-* is sound,

    Proof: First we define an extension for Val(x, y) recursively in the following way:

    Val_0 = { : A |-_c B} where |-_c is classical consequence.

    Val_n+1 = { : A |-_Val_n B} where A |-_Val_n B just in case we can derive B from A classically using any Val(C, D) for in Val_n as an extra premise.

    Then we take our deduction relation |-* to be the union of all the Val_n's. We also make the union of the Val_n's our extension of Val(x, y), which we add to N. Call the resulting model N*

    Now we want to show (1) that Val-In holds of |-*, (2) that Val-Out holds in N*, and (3) that if A |-* B, then if N* |= A, N* |= B.

    For (1), suppose that A |-* B. Then there is some Val_n which contains . Given our definition of the Val_n's, <0, Val(A, B)> will be in Val_n+1, and thus |-* Val(A, B) as required.

    For (2), suppose that A and Val(A, B) are true in N* and B is not true in N*. Then there is a least n such that for some C, D, is in Val_n, C is true in N*, and D is not. As is in Val_n, there is a classical proof of D from C which might use Val(P, Q) for any in some Val_m where m < n. But, by hypothesis all such Val(P, Q) are true in N*, so as C is true in N*, so is D. Contradiction.

    For (3), any proof in |-* will be classical except for the possible use of Val(A, B) for in some Val_n as extra premises. As all such are in the extension of Val(x, y) in N*, the proofs will be effectively classical in N*.

    It is open to Julien and JC to claim that Val-Out is inadequate in axiom form. In particular, they might claim that their notion of validity is such that Val-Out is itself valid, an thus can be used in proofs without stating it as an explicit assumption (much like we do with A --> (B --> A), say).

    But no matter how general their notion of validity is, it mustn't include all truths (otherwise it looks like we've just got another paradox of truth). That is, there must be truths A such that ~Val(0, A). Given that there are such, I don't see why we can't claim that Val-Out is one of them.

    Of course, just because Val-Out is about validity, doesn't means it should be valid itself.

    Best,
    Sam

    ReplyDelete
  5. Hi,

    For some reason, the post deleted lots of ordered pairs in the proof I gave. So here it is again, this time using [A, B] for the ordered pair of A and B.


    Proof: First we define an extension for Val(x, y) recursively in the following way:

    Val_0 = {[A, B] : A |-_c B} where |-_c is classical consequence.

    Val_n+1 = {[A, B] : A |-_Val_n B} where A |-_Val_n B just in case we can derive B from A classically using any Val(C, D) for [C, D] in Val_n as an extra premise.

    Then we take our deduction relation |-* to be the union of all the Val_n's. We also make the union of the Val_n's our extension of Val(x, y), which we add to N. Call the resulting model N*

    Now we want to show (1) that Val-In holds of |-*, (2) that Val-Out holds in N*, and (3) that if A |-* B, then if N* |= A, N* |= B.

    For (1), suppose that A |-* B. Then there is some Val_n which contains [A, B]. Given our definition of the Val_n's, [0, Val(A, B)] will be in Val_n+1, and thus |-* Val(A, B) as required.

    For (2), suppose that A and Val(A, B) are true in N* and B is not true in N*. Then there is a least n such that for some C, D, [C, D] is in Val_n, C is true in N*, and D is not. As [C, D] is in Val_n, there is a classical proof of D from C which might use Val(P, Q) for any [P, Q] in some Val_m where m < n. But, by hypothesis all such Val(P, Q) are true in N*, so as C is true in N*, so is D. Contradiction.

    For (3), any proof in |-* will be classical except for the possible use of Val(A, B) for [A, B] in some Val_n as extra premises. As all such [A, B] are in the extension of Val(x, y) in N*, the proofs will be effectively classical in N*.

    Best,
    Sam

    ReplyDelete
  6. Thanks, Sam.

    The principles you give are:

    (Val-Out) A & Val(A, B) --> B

    (Val-In) A |- B
    ---------
    |- Val(A, B)

    But aren't these just what I called the scheme (V-Out) and the rule (V-Intro)? If so, one gets the inconsistency as outlined above (and in Julien and JC's article).

    For (V-Out) is the scheme:

    Val(A, B) -> (A -> B)

    which is equivalent to your formulation:

    A & Val(A, B) -> B

    And your (Val-In) seems to be what I call (V-Intro) above. That is, an introduction rule saying that if B is derivable from A (possibly using other V-principles), then we can infer Val(A, B).

    [On the notation, I follow Friedman & Sheard and others in saying "in" and "out" for schemes, and "intro" and "elim" for rules. So, e.g., (T-In) is the scheme : A -> True("A"), while (T-Intro) is the rule that when you've derived A, you can infer True("A").]

    So, my question is: is your rule (Val-In) not the same as the rule (V-Intro) I mentioned above?

    ReplyDelete
  7. Hi Jeff,

    Sorry about the notation! I agree the Friedman & Sheard convention is a useful one.

    I'm pretty sure that my Val-In is not the same as V-Intro. So, V is a theory of validity. Let's say that V is my theory T. In particular, it has as an axiom my Val-Out. So V-intro would give us the following instance:

    V |- Val-Out (for some A, B), then V |- Val(0, Val-Out)

    And, of course, I accept the antecedent. But I explicitly claim that Val-Out is not valid. So V-intro had better not be my Val-In!

    The difference is that I do not allow V in the antecedent - there are principles of validity which are not themselves valid.

    What do you think?

    Best,
    Sam

    ReplyDelete
  8. Hi Sam, thanks - yes, I get it better now.

    [Actually, I should have said (V-Intro)* above - which is the fully self-applicative rule. This, with (V-Out), gives inconsistency. The weaker rule (V-Intro), on the other hand, is consistent.]

    Call your (Val-In) "(Val-Intro)" instead - as it's a rule not a scheme. So, your theory has (V-Out) and (Val-Intro).
    There are three systems now:

    (i) (V-Out) plus (V-Intro) - this is consistent.
    (ii) (V-Out) plus (V-Intro)* - this is inconsistent.
    (iii) (V-Out) plus (Val-Intro) - this is consistent.

    (Val-Intro) is clearly a bit stronger than (V-Intro) as it allows the inference of Val(A,B) based on reasoning using the (Val-Intro) rule itself. It's basically a necessitation rule, analogous to having, from a derivation of A (in the modal logic), infer []A.

    "I do not allow V in the antecedent - there are principles of validity which are not themselves valid."

    Right - yes, that was my original point too. So, to infer Val(A,B), I required a derivation of B from A using only logic (and not the theory of validity itself). But your rule (Val-Intro) is a bit stronger than (V-Intro): it says that if there is a derivation of B from A using logic and applications of (Val-Intro), then infer Val(A,B). I think your consistency proof is correct for T. It allows iteration of the Val(.,.) predicate so long as the derivations only use the (Val-Intro) rule.

    However, your theory T counts certain things as valid that one might argue are not valid. For example, A is derivable from A in logic; so, T proves Val(A,A) using (Val-Intro). But because Val(A,A) is derivable from the empty set using logic and (Val-Intro), T proves Val(\emptyset, Val(A,A)).
    So,

    T |- Val(\empyset, Val(A, A)).

    But is the inference from emptyset to Val(A,A) itself really valid? My inclination is to say that it is an inference licensed by a rule of the theory of validity, rather than a merely logical rule. So, the inference isn't valid.

    I would want to have things like Val(ValA,A), Val(A,A)). But should we want Val(\empyset, Val(A, A)) as a theorem?

    ReplyDelete
  9. Hi Jeff,

    I agree completely. I certainly don't think that Val(A, A) is itself a logical truth. Whether it's valid in this context will depend on the notion of validity, of course, and it's not completely clear to me what notion Julien and JC have in mind. In any case, I'm also inclined to think that Val(A, A) isn't valid either.

    To be clear, the point of T was not to offer a genuine theory of validity, but to offer a slight weakening of Julien and JC's theory which was consistent. For me this raises one thought and one question:

    (1) The v-curry requires more than c-curry, in that in order to derive c-curry (in classical logic, say) we only need accept T(A) <--> A for all A, whereas for v-curry we need to accept not only V-Out but that V-Out is valid.

    (2) Given that some truths A are not valid, what reason have we to think that V-Out is? Any more than, say, set-theoretic replacement.

    Best,
    Sam

    ReplyDelete
  10. Sorry, (1) is not strictly true, of course. We don't need the full T-schema to get in to trouble and neither do we need the full V-Out.

    Sam

    ReplyDelete
  11. Yes, all that sounds right - the theory you describe is a bit like closing PA under the (T-Intro) rule (and the (T-Elim) rule, if you like). So, if we weaken (V-Intro)* to your version (Val-Intro), we get a consistent theory, with an extension for Val(.,.) defined by the induction you give.
    Right, I agree - the instances of the scheme (V-Out) shouldn't be regarded as valid themselves.
    Thanks for the comments, Sam.

    ReplyDelete
  12. Thanks for the comments to you both!

    Don't we get a hierarchical theory of validity at this point? The upshot seems to be that the validity rules for 'valid' are not valid; yet, if we accept them, we may still want to say that they're valid in some sense. And so on.

    I wonder whether this way out of the problem sits well with the revisionary thought that truth isn't stratified - if validity and truth are both key semantic concepts, then arguably they should be treated in the same way etc.

    ReplyDelete
  13. Hey Julien,

    I haven't thought too much about the need to treat both the truth and validity predicates in a non-hierarchical fashion (though my inclination is to treat them both as non-hierarchical).

    However, prima facie it's not clear to me that the theory with V-Out and Val-Intro is hierarchical. Indeed it includes all instances of V-Out, not just for those A, B which do not include the validity predicate, say. The same goes for Val-Intro.

    But you suggest a different route from V-Out/Val-Intro to some kind of hierarchy. I take it the idea is some kind of reflection principle for validity. Something like:

    (1) If we accept A, then we should accept Val(A).

    And, I think, unless 'valid' is to mean 'true', (1) cannot in general hold. For instance, I think there is /no/ sense of valid under which 'there is a chair in my room' is valid.

    What we need, it seems to me, is some notion of validity which, on the one hand, doesn't satisfy (1), and on the other, gives us that V-Out is not simply true but valid. I just can't see what would play this role.

    What do you think?

    Best,
    Sam

    ReplyDelete
  14. Hi Julien,

    "The upshot seems to be that the validity rules for 'valid' are not valid; yet, if we accept them, we may still want to say that they're valid in some sense."

    I think I'm with Sam. The weak validity rule (V-Intro) (which can be interpreted inside PA) is sound. But the stronger validity rule (V-Intro)* is not sound (it generates derivations of untruths from true assumptions). So, I don't think validity behaves analogously to truth. It's natural to desire of a truth theory something like: If A is true, then "A is true" is true, etc., etc. But it's not natural to require: if A is valid, then "A is valid" is valid.

    More generally, I think we have a consistent theory of validity with three ingredients
    (a) the scheme (V-Out).
    (b) the rule (V-Intro).
    (c) the rule (V-Elim).

    The step I identify as problematic in the post concerning the Curry sentence is the one that uses the much stronger rule (V-Intro)*. Here's another example. Suppose B is one of the non-logical axioms of the validity theory V. Presumably, the inference from any *tautology* to B is not valid. Now, for any formula A,

    (i) V, A->A |- B

    So, using (V-Intro)*,

    (ii) V |- Val(A->A, B).

    But the inference from the tautology A->A to B isn't valid. So, it seems that the rule (V-Intro)* is not sound.

    Is there some notion of validity on which (V-Intro)*) might be sound? We have three basic explications of validity,

    (Modal) "A : B" is valid iff it's impossible for A to be true and B to be false.
    (Semantic) "A : B" is valid iff any model of A is a model of B.
    (Syntactic) "A : B" is valid iff B is derivable from A.

    In (Modal), the notion of possibility has to be logical, so that "1+1=2 : 2+2=4" counts as invalid. We could introduce modification (e.g., allow only standard 2nd-order models for (Semantic) or allow infinitely long derivations for (Syntactic).]

    But none of these notions seems to support the strong rule (V-Intro)*. The theorems we get in the theory of validity may be true, but they're not (usually) themselves valid.

    ReplyDelete