**H**is the Godel code of formula H):

|- F1 <-> ~T(

**F2**)|- F2 <-> ~T(

**F1**)(loosely speaking, each statement is equivalent to the claim that the other is false). Now, given the F1 and F2 instances of the T-schema, we have:

|- F1 <-> ~ F2

Symmetry considerations suggest, however, that F1 and F2 ought to have the same truth value. Hence the 'paradox'.

The question I will set before you today is this. Assume we are working in a consistent extension of Q, and given a predicate P(x), consider two statements G1 and G2 such that:

|- G1 <-> P(

**G2**)|- G2 <-> P(

**G1**)Under what conditions is it the case that:

|- G1 <-> G2

In other words, when can we prove the symmetry claim?

Here is a start: If P is a provability predicate, then we can prove G1 <-> G2 (actually, we can prove both G1 and G2 individually!)

Harder?: With the set-up the same as the above, consider a 'Sorensen n-cycle':

|- G1 <-> P(

**G2**)|- G2 <-> P(

**G3**)|- G3 <-> P(

**G4**): : : : : : :

|- Gn-1 <-> P(

**Gn**)|- Gn <-> P(

**G1**)Under what conditions can we prove:

|- G1 <-> G2

|- G2 <-> G3

: : : : : : :

|- Gn-1 <-> Gn

|- Gn <-> G1

Again, P being a provability predicate is sufficient.

Have at it.

[Important Disclaimer: I do not have a general solution to this. I do have some partial results that I will dole out if the question attracts sufficient interest.]

[Edited to correct typo noted by Shane]

I was never convinced by the 'symmetry considerations' argument for the sameness of truth-value for F1 and F2. In other words, it's not that I rejected the idea outright, but the symmetry argument alone seemed to me not to be sufficient. So it will be interesting to see which assumptions must hold for |- G1 <-> G2 . If they are in the slight bit contentious, I'd probably be happy to ditch some of them and stick to the idea that F1 and F2 do not have the same truth-value after all! :)

ReplyDeleteSo I'm looking forward to people's replies here :) (Too lazy and too busy to look for a solution myself...)

Is the following right?

ReplyDeleteP-out or P-in would get you the equivalences. And if you have the equivalences, then neither P-out nor P-in can fail for any G_i.

Best,

Sam

I will chime in with some thoughts later, but wanted to point out a small typo:

ReplyDelete"|- G2 <-> P(

G2)" I believe should read "|- G2 <-> P(G1)"Sam,

ReplyDeleteI am not sure I am following your reasoning. Can you put it in symbols (always easier for a hack like me!)

Roy

Hi Roy,

ReplyDeleteSuppose we have P(G_i) --> G_i for each i<=n. Then as G_i-1 --> P(G_i), G_i-1 --> G_i. By similar reasoning we also have G_n --> G_1. So, we have G_i <--> G_m for any i,m <=n.

A similar argument shows that G_i --> P(G_i) for each i<= n implies that G_i <--> G_m for any i,m<=n.

Conversely suppose that we have G_i <--> G_m for any i,m <=n, and suppose that for some G_i, G_i & ~P(G_i). Then by the original equivalences, we have G_i-1 <--> P(G_i) and by the new equivalences we'd have G_i-1 <--> G_i. Putting that together with our supposition yields G_i & ~G_i.

The argument from P(G_i) & ~G_i to contradiction is similar.

Hope that helps.

Please do say if I've got the rules of the puzzle wrong.

Best,

Sam

Sam,

ReplyDeleteOkay, so what you have shown is (I am going to restrict my attention to the n = 2 case) that if:

(a) |- G1 <-> P(G2)

(b) |- G2 <-> P(G1)

Then:

(c) |- G1 <-> G2

If and only if:

(d) |- P(G1) <-> G1

(e) |- P(G2) <-> G2

This provides an exact answer to P(x)'s behavior w.r.t. G1 and G2. But what about general principles (i.e. not specific to G1 and G2)?

Your result shows that if P(x) satisfies either of the following general rules, then we can prove the equivalence (c):

(f) |- P(F) -> F

(g) |- F -> P(F)

My claim about P being a provability predicate can now be understood in the following way: Even if P(x) fails to satisfy one or both of (f) and (g) generally, if it is a provability predicate then it will be able to prove the 'relevant biconditionals for G1 and G2, and will therefore still allow us to prove the equivalence (c).

So a version of the problem still remains: What other general principles involving P(x) (but not mentioning G1 and G2 specifically) will allow us to prove the equivalence (c)?

Replace P("A") by []A and use modal logic:

ReplyDelete- from A infer []A

- the scheme [](A -> B) -> [](A -> B)

- the scheme []A -> [][]B.

As Roy says, these give you what you want (they're the modal versions of the properties of provability predicates). The SEP entry on provability logic is here:

http://plato.stanford.edu/entries/logic-provability/

Sam, note that (in this scenario), a provability predicate doesn't satisfy a local reflection principle like (f) (or (g)), which are too strong. E.g., if [] represents provablity in T, and T proves []A -> A, then, by Lob's Theorem, T proves A. If T1 and T2 contain something like Q (or ISigma_1), and P(x) is a provability predicate for T1, then T2 will prove all instances of the scheme P("A") - > A only if T2 is stronger than T1.

For example, let P_n(x) mean "x is a theorem of ISigma_n". Then PA proves the local reflection scheme P_n("A") -> A.

[Proof: PA proves the reflection scheme for logical provability: all instances of Val("A") -> A. So, PA proves Val("ISigma_n -> A") -> (ISigma -> A). But ISigma_n is a single sentence provable in PA, so, PA proves Val("ISigma_n -> A") -> A. But since Val("ISigma_n -> A") just means "A is provable in ISigma_n", PA proves P_n("A") -> A. Here it's essential that PA be logically stronger than ISigma_n: PA has to be "essentially reflexive".]

So, for provability logic, while [] satisfies some weaker principles, it won't satisfy local reflection []A -> A, unless the provability implicit in [] (e.g., provability in ISigma_n) is different from the notion of provability in the theory you're examining (e.g., provability in PA).

Hi, Roy,

ReplyDeleteThat's really helpful. I just have one more question, if that's ok.

You said in your original post that you don't have a general solution to the problem raise. I was just wondering what form a general solution would take?

One concern is just to see which general principles will entail the equivalences. But simply listing these doesn't seem to be in itself a general solution (without further contraints the list would be very long!!).

Any help would be great,

Sam

Hi Jeff,

Thanks for this.

I didn't think that P /had/ to be a provability predicate, just that a provability predicate is one way to get the equivalences. Of course, if P does have to be a provability predicate, then I of course agree that adding general reflection would be both unnecessary and trivialising.

But there are (uninteresting!) examples of reflection for some P. For instance, if we have Q, then "\phi --> P(`\phi')" where P is interpreted as `is a formula' will do the trick.

Or am I missing something?

Thanks again,

Sam

Hey,

ReplyDeleteSorry, that wasn't an example of reflection!!

I mean to say the following:

If P is interpreted as `is not a formula', then we have ``P(`\phi') --> \phi.

Best,

Sam

OK. Here is the sort of result I have in mind:

ReplyDeleteLet:

P_1(F) = P(F)

P_n+1(F) = P(P_n(F))

Assume we have an n-Sorensen cycle for P:

|- F1 <-> P(F2)

|- F2 <-> P(F3)

: : : : : : : :

|- Fn <-> P(F1)

Now, assume that:

(a) For any G, H, if |- G <-> H, then |- P(G) <-> P(H)

(b) There are positive integers k, j, m, n where m and n are co-prime such that, for any G:

|- P_k(G) -> P_k+m(G)

|- P_j+n(G) -> Pj(G)

Then:

|- F1 <-> F2

|- F2 <-> F3

: : : : : : :

|- Fn <-> F1

Hi Sam, yes, you're right. What you suggest works in giving P("A") -> A. Q proves Form("A"), for each formula A. So, Q proves ~Form("A") -> A, for each formula A.

ReplyDeleteOn the other hand, Form(x) *is* a provability predicate, for it satisfies the HB-conditions,

If PA proves A, then PA proves Form("A")

PA proves Form("A") -> Form("Form("A")")

PA proves Form("A -> B") -> (Form("A") -> Form("B")

By Lob's Theorem, if PA proves Form("A")-> A, then PA proves A. So, PA only proves Form("A") -> A for its theorems. Lob's Theorem also shows that ~Form("A") is not a provability predicate.

(I don't know of a name for the converse of reflection: I.e., A -> Prov("A"), which is a kind of completeness scheme, I suppose.)

Oops - typo.

ReplyDeleteI meant: "Lob's Theorem also shows that ~Form(x) is not a provability predicate."