In The logic of provability, by G. Boolos, we are asked to ponder about this statement:

If this statement is consistent, then you will have an exam tomorrow, but you cannot deduce from this statement that you will have an exam tomorrow.

I tried formalizing it the following way:

Let $p$ stand for the whole statement, and $q$ is going to be true iff I have an exam tomorrow.

Then the paragraph is stating that: $$ p\leftrightarrow \diamond (p\rightarrow q)\wedge \neg\square(p\rightarrow q) $$

Solving the fixed point using any of the usual methods will give us that: $$ GL\vdash \boxdot [p\leftrightarrow A(p,q)]\implies \boxdot[p\leftrightarrow \bot] $$ Where $A(p,q)$ stands for the right hand side of the first formula.

Therefore, we can conclude by neccesitation and modus ponens that if $p$ and $q$ are suitable chosen statements of $PA$ satisfying the first formula then: $$ PA\vdash \neg p $$ Therefore we conclude that the statement is false under every interpretation of $PA$, and therefore it gives no information about $q$.

Is my reasoning correct? Is my conclusion pertinent?

  • $\begingroup$ How do you express "you will have an exam tomorrow" in the language of PA? $\endgroup$ – Henning Makholm Jul 19 '16 at 10:54
  • $\begingroup$ @HenningMakholm $q$ can be simply an arbitrary closed sentence such as $\exists x P(x)$. What I am concerned about is inferring whether $PA$ necessarily proves $q$ or its falsehood. $\endgroup$ – Jsevillamol Jul 19 '16 at 11:08
  • $\begingroup$ What does "$\boxdot$" mean? $\endgroup$ – user21820 Jul 19 '16 at 15:04
  • $\begingroup$ @user21820 $\boxdot A = \square A \wedge A$ $\endgroup$ – Jsevillamol Jul 19 '16 at 15:45

Take any consistent theory $T$ satisfying the provability conditions and the fixed point lemma.

Take any sentence $q$ over $T$. $\def\imp{\rightarrow}$ $\def\eq{\leftrightarrow}$ $\def\box{\square}$ $\def\diam{\lozenge}$

Your equation

By the fixed point lemma there is a sentence $p$ over $T$ such that $T \vdash p \eq \diam( p \imp q ) \land \neg \box( p \imp q )$.

Equivalently $T \vdash p \eq \neg \box( p \land \neg q ) \land \neg \box( \neg p \lor q )$.

Note that $T \vdash \box \neg p \imp \box( p \imp q )$ by (D1) and (D2).

Thus $T \vdash p \imp \neg \box \neg p$ and hence $T \vdash \box \neg p \imp \neg p$.

Therefore by Lob's theorem $T \vdash \neg p$.


Literal question

You translated the sentence wrongly. Literally, $T \vdash p \eq ( \diam p \imp q ) \land \neg \box( p \imp q )$. [$\diam$ before $\imp$!]

Equivalently $T \vdash p \eq ( \box \neg p \lor q ) \land \neg \box( p \imp q )$.

It so happens that the above reasoning works here too, giving $T \vdash \neg p$.

So your first claim is correct though I have no idea whether your reasoning is valid.

But I don't get your reasoning about $q$; how does $T \vdash \neg p$ imply anything about $q$? If you're just saying that the teacher is a liar, then I agree with you.

Probable intended question

The original sentence is ambiguous, and I first interpreted it with "but" binding first before "then".

In this case you want $T \vdash p \eq ( \diam p \imp q \land \neg \box( p \imp q ) )$. [$\diam$ first!]

Equivalently $T \vdash p \eq \box \neg p \lor q \land \neg \box( p \imp q )$.

If $T \vdash \neg p$, then $T \vdash \box \neg p$ by (D1) and hence $T \vdash p$, which is impossible.

Thus the teacher is making a consistent statement over $T$.

At this point it would be erroneous to reason as follows:

  $p$ is consistent. Thus $q$ is true and hence $p \imp q$. So we have deduced from $p$ that $q$ is true.

So this is probably the intended interpretation so that there is this 'paradox'. Once you write in terms of $\box$ it is clear that the error is right at the start, because $T$ is unable to prove $\neg \box \neg p$.

  • $\begingroup$ Oops! I made a typo in the formula. I meant to write the formula in Literal question. I agree that the conclusion is that the teacher is an inconsistent liar. I also agree that your Intended question is actually what the exercise was supposed to be about, and I agree that $p$ is consistent. I feel inclined to disagree with the conclusion, since in my way of seeing it the teacher is asserting that $p$ is true in the standard model, and in that model $\diamond p$ is also true, so $q$ follows. I however understand what you say. I guess it is up for interpretation?Thanks for your thorough answer. $\endgroup$ – Jsevillamol Jul 19 '16 at 18:25
  • 1
    $\begingroup$ @Jsevillamol: I think the point of the exercise is just that internal and external consistency are different. I'm curious to know how you computed the modal fixed point, since I've never learnt how to do that and I'm lazy to check your result. However, there's a far easier way to get the conclusion. If $\def\nn{\mathbb{N}}$$\nn \vDash \neg q$ and $\nn \vDash p$ then $\nn \vDash \box \neg p$ which is impossible. In fact, the same argument also shows that if $T \vdash \neg q$ then $T+p$ is $Σ_1$-unsound. $\endgroup$ – user21820 Jul 20 '16 at 4:44
  • 1
    $\begingroup$ I wrote some functions in the Wolfram Language to compute fixed points. You can access the code here. I do not explain how it is done, but Boolos exposes two methods in his book. The easy one when multiple sentence letters are present is to use $k$-decomposition. An explanation of the method and a proof of correctness can be found here. $\endgroup$ – Jsevillamol Jul 20 '16 at 13:01
  • 1
    $\begingroup$ @Jsevillamol: Okay since your comment suggests that computing modal fixed points isn't something easy to do by hand, I'm fine with just knowing it can be done. =) As for my comment, external consistency of $p$ over $T$ is the statement in the meta-system that $T \nvdash \neg p$, while internal consistency of $p$ over $T$ is the sentence $\neg \box_T \neg p$ over $T$. In this case the meta-system can prove that $p$ is externally consistent over $T$ but $T$ cannot prove internal consistency of $p$ over $T$. Makes sense? $\endgroup$ – user21820 Jul 20 '16 at 14:44
  • 1
    $\begingroup$ @Jsevillamol: Ah I do get the same final result, but it would be different if $H_2 = \box \bot$. Anyway thanks for showing me this! $\endgroup$ – user21820 Jul 21 '16 at 8:01

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.