Fitch 的論證使有大量邏輯術語。即使是 SEPWiki 的介紹，也運用了一堆邏輯工具。對邏輯學有一定掌握的人，可以清楚看到整個推論過程，以及推論使用的規則和前提。我打算避用邏輯符號，但至少還要作三個約定，務求盡量減少誤解：一、我用「真命題」代替「真理」，因為後者常帶有人生雋語的意味，但「真命題」無此意味；二、我省掉「原則上可以」，改用「有可能」；三、我會盡量將「我們知道」省略成「知道」，令論證讀起來比較不拗口。

(A) 所有真命題都是有可能知道的
(B) 有些真命題還未有人知道

(C) 知道「 p 和 q 」可推論知道 p ，而且，知道 q
(D) 知道 p 可推論 p
(Simp) p 而且 q 可推論 p ；此外，  p 而且 q 可推論 q
(Conj) p , q 可推論 p 而且 q

1. 有可能知道「 P 為真，而且不知道 P 為真」

2. 知道「 P 為真，而且不知道 P 為真」（假設，為了做歸謬法）
3. 知道 P 為真，而且，知道不知道 P 為真 （根據2, C）
4. 知道不知道 P 為真（根據3, Simp）留意我一開始已約定：「知道 P 為真」是「我們知道 P 為真」。因此，「知道不知道 P 為真」其實是「我們知道我們不知道 P 為真」。
5. 不知道 P 為真（根據4, D）
6. 知道 P 為真（根據3, Simp）
7. 知道 P 為真，而且，不知道 P 為真（根據6, 5, Conj）

8. 不可能知道「 P 為真，而且不知道 P 為真」

#### 6 則留言:

1. I just find out this blog through a friend's Facebook sharing (of another entry of your blog). I find this paradox you explain here very interesting. I hope you don't mind my asking a question.

It seems that from (7), we don't get (8), but the negation of (2). If we want to get the modal claim (8), we need to infer from not-(2) to necessarily not-(2). But it seems that this is not a legitimate move in this context because we are under the scope of the assumption (1).

It's like, although the following inference is legit:

(1) P [Assumption]
(2) P [Taut. (1)]
(3) P --> P [C.P. (1), (2)]
(4) Necessarily, P --> P [Necessitation (3)]

the following inference is not legit:

(1) P & Q [Assumption]
(2) P [Simplification (1)]
(3) Necessarily, P [Necessitation (2)]

If I am right, we do not have the contradiction between (1) and (8) you need. Then, apparently there is no paradox. All we must say is:

(a) it is possible (for one) to know that (X and one does not know that X);
(b) one does not know that (X and one does not know that X).

I confess that my symbolic logic, including modal logic is all self-taught and I know I am not good at it. I suppose there is a good reason why this paradox is, and still is, around. So, I guess I must be wrong somewhere. Would you mind telling me where I got it wrong?

Thanks!!

Derek

2. hi Derek,

You are right that from (7) we cannot immediately get (8) according to formal logic. But given two more rules in epistemic logic, we can infer (8) from (7).

(C) If $⊢ p$, then $⊢□p$
(D) $□¬p ⊢ ¬◊p$

Here is the proof:
2. know “P and don't know P”

7. know P and don't know P <contradiction
8. don't know “P and don't know P” (2-7, by RAA)

Since 8 is a conclusion need no premise (it is discharged from the assumption (2)), it is a theorem. So, by (C)

9. necessarily don't know “P and don't know P” (from 8, (C))
10. not-possibly know “P and don't know P” (from 9, (D))

Two more clarifications. First, you cannot apply (C) in the following proof:

(1) P & Q [Assumption]
(2) P [by 1, Simp]
(3) Necessarily, P [by 2, C]

(2) is not a theorem, it is inferred from (1) and its assumption, i.e. (1), is not yet discharged. But (8) is different. It has been discharged from its assumption (2). (Compare: assume P, prove Q, then conclude "P→Q". In this case "P→Q" is a theorem, but "Q" is not a theorem) So your analogy is unlike the proof (2)-(8) in my note.

Second,
1. 有可能知道「 X 為真，而且不知道 X 為真」
is irrelevant to the proof from (2) to (8) in my note. (1) is a conclusion from (A) and (B). (2)-(7) is another proof for (8). So (1) is not an assumption of the proof (2)-(8).

I have also to confess that I have only taken an elementary logic class and an introductory class on computability. I didn't learn modal logic in class either. If you find any mistake, please correct me. Thank you!

3. Thanks so much for your detail reply. I have to apologize beforehand for the absurd length of the following follow up question (it is so long that I have to break it up into two replies).

You are right that (1) is irrelevant, and you can get (8) from (2). This might be a stupid question, but then you don't have (1) to get a contradiction between (1) and (8) -- the problem seems to be that both (1) and (8) involve proper name of a particular proposition, "X". I will try to articulate this worry a little bit more if you don't mind (again, I'm sorry for the length). Instead of using "X" as the proper name of the true but unknown proposition, I use "p".

First, the following is how I originally read the reasoning to the paradox [p.s. I do not know how to type logic symbols, so "Ax" is the universal quantifier, "Ex" the existential quantifier, "<>" the possibility operator, and "[]" the necessity operator. I hope it does not generate too much confusion]:

(1) Ax(x --> <>K(x)) [Assumption]
(2) Ex(x ^ ~K(x)) [Assumption]
(3) (p ^ ~K(p)) [EI (2)]
(4) (3) --> <>K((3)) [UI (1)]
(5) <>K(p ^ ~K(p)) [M.P. (3), (4)]
(6) K(p ^ ~K(p)) [Assumption]
(7) K(p) ^ K(~K(p)) [Distribution (6)]
(8) K(p) [Simplification (7)]
(9) K(~K(p)) [Simplification (7)]
(10) ~K(p) [knowledge implies truth]
(11) K(p) ^ ~K(p) [Conj. (8), (10)]
(12) ~K(p ^ ~K(p)) [R.A.A. (6), (11)]
(13) []~K(p ^ ~K(p)) [Nec. (12)]
(14) ~<>K(p ^ ~K(p)) [Taut. (13)]
(15) <>K(p ^ ~K(p)) ^ ~<>K(p ^ ~K(p)) [Conj. (5), (15)]
(16) ~Ex(x ^ ~K(x)) [R.A.A. (2), (15)]
(17) Ax(~(x ^ ~K(x))) [Taut. (16)]
(18) Ax(x --> K(x)) [Taut. (17)]
(19) Ax(x --> <>K(x)) --> Ax(x --> K(x)) [C.P. (1), (18)]

My original worry is that step (13) is not legit, for application of Nec is illegitimate inside the scope of the assumptions (1) and (2), as you have conceded. Now, your suggestion, which is completely correct, is that if we take step (6) to (14) out as an independent proof, then there is no problem:

(6) K(p ^ ~K(p)) [Assumption]
(7) K(p) ^ K(~K(p)) [Distribution (6)]
(8) K(p) [Simplification (7)]
(9) K(~K(p)) [Simplification (7)]
(10) ~K(p) [knowledge implies truth]
(11) K(p) ^ ~K(p) [Conj. (8), (10)]
(12) ~K(p ^ ~K(p)) [R.A.A. (6), (11)]
(13) []~K(p ^ ~K(p)) [Nec. (12)]
(14) ~<>K(p ^ ~K(p)) [Taut. (13)]

As you have said, it is now ok to apply the rule of necessitation on step (13) because the assumption (6) is discharged and there is no other assumption left -- (12) is a theorem.

4. Fair enough. But, the price is, now, without step (1) to (5), how are we suppose to reach the paradox? As shown in step (15), we need (5) to get the paradox. It seems to be an easy fix, but not quite so on closer look. Suppose we just insert step (1) to (5) after we get to (14) and get the following proof:

(6) K(p ^ ~K(p)) [Assumption]
(7) K(p) ^ K(~K(p)) [Distribution (6)]
(8) K(p) [Simplification (7)]
(9) K(~K(p)) [Simplification (7)]
(10) ~K(p) [knowledge implies truth]
(11) K(p) ^ ~K(p) [Conj. (8), (10)]
(12) ~K(p ^ ~K(p)) [R.A.A. (6), (11)]
(13) []~K(p ^ ~K(p)) [Nec. (12)]
(14) ~<>K(p ^ ~K(p)) [Taut. (13)]
(1) Ax(x --> <>K(x)) [Assumption]
(2) Ex(x ^ ~K(x)) [Assumption]
(3)* (q ^ ~K(q)) [EI (2)]
(4)* (3)* --> <>K((3)*) [UI (1)]
(5)* <>K(q ^ ~K(q)) [M.P. (3)*, (4)]

The problem seems to be it cannot be cut and paste straightforwardly, because the Existential Instantiation at step (3)* (and the original (3)) requires using a new name and "p" is a name already in use from the now earlier steps from (6) to (14). I.e. instead of (3), (4) and (5), we have to use (3)*, (4)* and (5)*. But then, with (5)* and (14), we get this:

(15)* ~<>K(p ^ ~K(p)) ^ <>K(q ^ ~K(q)) [Conj. (14), (5)*]

And (15)* is not of a contradictory form. That way, step (16) to (19) cannot go through and there is no reductio and no paradox. But I do not know how to get beyond step (14) to (19) if we are not to insert assumptions (1) and (2) after (14). So, we have a dilemma: if the assumptions are placed at the beginning, step (13) is not legit; if instead they are placed after (14), then now step (13) is legit but step (3) is not, which has to be replaced by (3)*.

How else can we get the paradox?

I apologize for the long follow-up question and am looking forward to your solution!

Derek

5. How stupid was I to have forgotten the existential universalization. I see that now. Thanks for your time!

Derek

6. hi Derek:

//My original worry is that step (13) is not legit, for application of Nec is illegitimate inside the scope of the assumptions (1) and (2), as you have conceded. Now, your suggestion, which is completely correct, is that if we take step (6) to (14) out as an independent proof, then there is no problem: //

1. It's nice to know that you have found another way to construct the paradox. But so far as I know your original proof doesn't have any mistake that would block the paradox.

Concerning your formal proof (1)-(19), as long as (12) has been discharge from all relevant assumptions, it is a theorem. In your proof, the only assumption relevant to (12) is (6). [In the subproof (6)-(12) you used only assumption (6), so other assumptions such as (1) and (2) are completely irrelevant to your subproof.] But you have discharged (6) from (12). It turned out that (12) is a theorem. Even though there are irrelevant assumptions (1) and (2) in the earlier line of proof, they do nothing to your subproof for establishing (12) as a theorem.

[So, what I meant by "(2)-(7) is another proof for (8)" in my earlier reply is that "(8) can be established as a theorem without assumption of (1)", but I didn't mean "there cannot be any irrelevant assumption preceding (8) in the lines of formal proof".]

Frankly, I am not familiar with the formal system you are using here, which should be most popular one. The natural deduction system I have learned in class is the one in Robert Causay's Logic, Sets and Recursion (2nd.). I guess you are using the system in Hausman, A. & Kahane, H. & Tidman, P. (2010) Logic and Philosophy A Modern Introduction. I just skimmed the rules in that book, and it seems that according to that system your indirect proof of the theorem (12) is not incorrect. So, if I have misunderstood your proof, please feel free to tell me.

2. A digression. If you want to use logical symbols on the web (e.g. your blog), you might be interested in this two websites

http://mathscribe.com/author/jqmath.html
http://mathscribetheblog.blogspot.hk/2011/03/jqmath-in-blogger.html