Theorem
-------
[~Liar => [Ruins <=> Yes]]
& [Liar => [Ruins <=> ~Yes]]
& [~Liar => [Yes' <=> Yes]]
& [Liar => [Yes' <=> ~Yes]]
=> [Ruins <=> Yes']
where:
Liar = villager is a liar
Ruins = tourist points to road to ruins
Yes = answer is yes to direct question (Is this the road to the ruins?)
Yes' = answer to yes indirect question (If I asked you if this was the road to the ruins, would you say yes?)
Notation
--------
~ = NOT-operator
& = AND-operator
| = OR-operator
=> = IMPLIES-operator
<=> = IF-AND-ONLY-IF-operator
This prove was written with the aid of DC Proof 2.0 (download at http://www.dcproof.com )
Proof
-----
Suppose...
1 [~Liar => [Ruins <=> Yes]]
& [Liar => [Ruins <=> ~Yes]]
& [~Liar => [Yes' <=> Yes]]
& [Liar => [Yes' <=> ~Yes]]
Premise
Splitting this premise...
2 ~Liar => [Ruins <=> Yes]
Split, 1
3 Liar => [Ruins <=> ~Yes]
Split, 1
4 ~Liar => [Yes' <=> Yes]
Split, 1
5 Liar => [Yes' <=> ~Yes]
Split, 1
'=>'
Prove: Ruins => Yes'
Suppose...
6 Ruins
Premise
Two cases:
7 Liar | ~Liar
Or Not
Case 1
Prove: Liar => Yes'
Suppose...
8 Liar
Premise
Apply original premise
9 Ruins <=> ~Yes
Detach, 3, 8
10 [Ruins => ~Yes] & [~Yes => Ruins]
Iff-And, 9
11 Ruins => ~Yes
Split, 10
12 ~Yes => Ruins
Split, 10
Apply previous premise
13 ~Yes
Detach, 11, 6
Apply original premise
14 Yes' <=> ~Yes
Detach, 5, 8
15 [Yes' => ~Yes] & [~Yes => Yes']
Iff-And, 14
16 Yes' => ~Yes
Split, 15
17 ~Yes => Yes'
Split, 15
Apply previous result
18 Yes'
Detach, 17, 13
Case 1
As Required:
19 Liar => Yes'
4 Conclusion, 8
Case 2
Prove: ~Liar => Yes'
Suppose...
20 ~Liar
Premise
Apply original premise
21 Ruins <=> Yes
Detach, 2, 20
22 [Ruins => Yes] & [Yes => Ruins]
Iff-And, 21
23 Ruins => Yes
Split, 22
24 Yes => Ruins
Split, 22
Apply previous premise
25 Yes
Detach, 23, 6
Apply original premise
26 Yes' <=> Yes
Detach, 4, 20
27 [Yes' => Yes] & [Yes => Yes']
Iff-And, 26
28 Yes' => Yes
Split, 27
29 Yes => Yes'
Split, 27
Apply previous result
30 Yes'
Detach, 29, 25
Case 2
As Required:
31 ~Liar => Yes'
4 Conclusion, 20
Join previous results
32 [Liar => Yes'] & [~Liar => Yes']
Join, 19, 31
Apply Cases Rule
33 Yes'
Cases, 7, 32
'=>'
As Required:
34 Ruins => Yes'
4 Conclusion, 6
'<='
Prove: Yes' => Ruins
Suppose...
35 Yes'
Premise
Two cases:
36 Liar | ~Liar
Or Not
Case 1
Prove: Liar => Ruins
Suppose...
37 Liar
Premise
Apply original premise
38 Yes' <=> ~Yes
Detach, 5, 37
39 [Yes' => ~Yes] & [~Yes => Yes']
Iff-And, 38
40 Yes' => ~Yes
Split, 39
41 ~Yes => Yes'
Split, 39
42 ~Yes
Detach, 40, 35
Apply original premise
43 Ruins <=> ~Yes
Detach, 3, 37
44 [Ruins => ~Yes] & [~Yes => Ruins]
Iff-And, 43
45 Ruins => ~Yes
Split, 44
46 ~Yes => Ruins
Split, 44
Apply previous premise
47 Ruins
Detach, 46, 42
Case 1
As Required:
48 Liar => Ruins
4 Conclusion, 37
Case 2
Prove: ~Liar => Ruins
Suppose...
49 ~Liar
Premise
Apply original premise
50 Yes' <=> Yes
Detach, 4, 49
51 [Yes' => Yes] & [Yes => Yes']
Iff-And, 50
52 Yes' => Yes
Split, 51
53 Yes => Yes'
Split, 51
Apply previous premise
54 Yes
Detach, 52, 35
55 Ruins <=> Yes
Detach, 2, 49
56 [Ruins => Yes] & [Yes => Ruins]
Iff-And, 55
57 Ruins => Yes
Split, 56
58 Yes => Ruins
Split, 56
Apply previous results
59 Ruins
Detach, 58, 54
Case 2
As Required:
60 ~Liar => Ruins
4 Conclusion, 49
Join previous results
61 [Liar => Ruins] & [~Liar => Ruins]
Join, 48, 60
Apply Cases Rule
62 Ruins
Cases, 36, 61
'<='
As Required:
63 Yes' => Ruins
4 Conclusion, 35
Join previous results
64 [Ruins => Yes'] & [Yes' => Ruins]
Join, 34, 63
Apply Iff-And Rule
65 Ruins <=> Yes'
Iff-And, 64
As Required:
66 [~Liar => [Ruins <=> Yes]]
& [Liar => [Ruins <=> ~Yes]]
& [~Liar => [Yes' <=> Yes]]
& [Liar => [Yes' <=> ~Yes]]
=> [Ruins <=> Yes']
4 Conclusion, 1