forked from vezwork/modallogic
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathindex.html
285 lines (283 loc) · 21.2 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
<!DOCTYPE html>
<html>
<head>
<meta charset="utf-8">
<title>Dynamic Epistemic Logic Playground</title>
<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/4.0.0/css/bootstrap.min.css" integrity="sha384-Gn5384xqQ1aoWXA+058RXPxPg6fy4IWvTNh0E263XmFcJlSAwiGgFAW/dAiS6JXm" crossorigin="anonymous">
<link rel="stylesheet" href="css/app.css">
</head>
<body>
<div id="page-container">
<a href="https://github.com/vezwork/modallogic"><img class="github-link" src="img/blacktocat-32.png" title="Fork me on GitHub"></a>
<h1>Dynamic Epistemic Logic Playground</h1>
<section id="app">
<div id="mode-select" class="btn-group">
<button class="btn btn-primary active" onclick="setAppMode(MODE.EDIT)">
<i class="icon-pencil icon-white"></i> Edit Model
</button>
<button class="btn btn-primary" onclick="setAppMode(MODE.EVAL)">
<i class="icon-eye-open icon-white"></i> Evaluate Formula
</button>
</div>
<div id="app-body">
<div class="panel tab-content">
<div id="edit-pane" class="tab-pane active">
<div class="agent-btns">
Current agent:<br>
<div class="btn-group">
<button class="btn btn-secondary active" onclick="setCurrentAgent(0)">a</button>
<button class="btn btn-secondary" onclick="setCurrentAgent(1)">b</button>
<button class="btn btn-secondary" onclick="setCurrentAgent(2)">c</button>
<button class="btn btn-secondary" onclick="setCurrentAgent(3)">d</button>
<button class="btn btn-secondary" onclick="setCurrentAgent(4)">e</button>
</div>
</div>
<div class="var-count mt-3">
Number of propositional variables:<br>
<div class="btn-group">
<button class="btn btn-secondary" onclick="setVarCount(1)">1</button>
<button class="btn btn-secondary active" onclick="setVarCount(2)">2</button>
<button class="btn btn-secondary" onclick="setVarCount(3)">3</button>
<button class="btn btn-secondary" onclick="setVarCount(4)">4</button>
<button class="btn btn-secondary" onclick="setVarCount(5)">5</button>
</div>
</div>
<div class="alert alert-info">
<div class="selected-node-id">No world selected</div>
<table class="propvars inactive">
<tbody>
<tr class=""><td class="var-name">p:</td><td class="var-value"><div class="btn-group">
<button class="btn btn-small btn-success" onclick="setVarForSelectedNode(0,true)">True</button>
<button class="btn btn-small btn-danger" onclick="setVarForSelectedNode(0,false)">False</button>
</div></td></tr>
<tr class=""><td class="var-name">q:</td><td class="var-value"><div class="btn-group">
<button class="btn btn-small btn-success" onclick="setVarForSelectedNode(1,true)">True</button>
<button class="btn btn-small btn-danger" onclick="setVarForSelectedNode(1,false)">False</button>
</div></td></tr>
<tr class="inactive"><td class="var-name">r:</td><td class="var-value"><div class="btn-group">
<button class="btn btn-small btn-success" onclick="setVarForSelectedNode(2,true)">True</button>
<button class="btn btn-small btn-danger" onclick="setVarForSelectedNode(2,false)">False</button>
</div></td></tr>
<tr class="inactive"><td class="var-name">s:</td><td class="var-value"><div class="btn-group">
<button class="btn btn-small btn-success" onclick="setVarForSelectedNode(3,true)">True</button>
<button class="btn btn-small btn-danger" onclick="setVarForSelectedNode(3,false)">False</button>
</div></td></tr>
<tr class="inactive"><td class="var-name">t:</td><td class="var-value"><div class="btn-group">
<button class="btn btn-small btn-success" onclick="setVarForSelectedNode(4,true)">True</button>
<button class="btn btn-small btn-danger" onclick="setVarForSelectedNode(4,false)">False</button>
</div></td></tr>
</tbody>
</table>
</div>
</div>
<div id="eval-pane" class="tab-pane">
<div class="eval-input">
Enter a formula:
<input type="text" placeholder="e.g., (p -> K{a}p)">
<button class="btn btn-primary" onclick="evaluateFormula()">Evaluate</button>
or
<button class="btn btn-dark" onclick="announceFormula()">[📣]Announce</button>
</div>
<div class="eval-output inactive">
</div>
<div class="instructions">
<ul class="unstyled pl-4">
<li>
When entering a formula:
<ul class="pl-2">
<li>use <code>~A</code> for $\lnot{}A$</li>
<li>use <code>(A & B)</code> for $(A\land{}B)$</li>
<li>use <code>(A | B)</code> for $(A\lor{}B)$</li>
<li>use <code>(A -> B)</code> for $(A\rightarrow{}B)$</li>
<li>use <code>K{a,b,c}A</code> for $K_{a,b,c}A$</li>
<li>use <code>[A]B</code> for $[A]B$</li>
</ul>
</li>
</ul>
</div>
</div>
</div>
<div style="position: absolute; bottom: 10px; left: 310px; z-index: 10;">
<i style="color: gray;" id="checks-title">loading...</i><br>
<input type="checkbox" class="form-check-input ml-1" id="reflexive-check" disabled>
<label class="form-check-label ml-4" for="reflexive-check">Reflexive</label><br>
<input type="checkbox" class="form-check-input ml-1" id="symmetric-check" disabled>
<label class="form-check-label ml-4" for="symmetric-check">Symmetric</label><br>
<input type="checkbox" class="form-check-input ml-1" id="transitive-check" disabled>
<label class="form-check-label ml-4" for="transitive-check">Transitive</label>
</div>
<div class="graph"></div>
<div class="current-formula inactive"></div>
</div>
</section>
<section class="text-section">
<h2>Editing Instructions</h2>
<ul class="unstyled">
<li class="mb-1">Click in the open space to <strong>add a world</strong></li>
<li class="mb-1">Drag between worlds to <strong>add a transition for the current agent</strong></li>
<li class="mb-1">Ctrl-drag a world to <strong>move</strong> graph layout</li>
<li class="mb-1">Click a world or a transition to <strong>select</strong> it</li>
<li class="mb-1">
When a world is selected:
<ul>
<li><strong>R</strong> toggles reflexivity for the current agent</li>
<li><strong>Delete</strong> removes the world</li>
</ul>
</li>
<li class="mb-1">
When a transition is selected:
<ul>
<li><strong>L</strong>(eft), <strong>R</strong>(ight), <strong>B</strong>(oth) change direction</li>
<li><strong>Delete</strong> removes the transition</li>
</ul>
</li>
<li class="mb-1">Copy the URL from your browser's URL bar to share your model!</li>
</ul>
</section>
<section class="text-section">
<h2>Examples</h2>
<ul>
<li><a href="https://vezwork.github.io/modallogic/index.html?model=;AqS?formula=(p-q)&(q-p)">A simple classical logic example. Does $p = q$?</a></li>
<li><a href="https://vezwork.github.io/modallogic/index.html?model=;AqS?formula=p|~p">A tautology is a formula which is true no matter what the propositional variables are set to.</a></li>
<li><a href="https://vezwork.github.io/modallogic/index.html?model=ApS1a,0a,;AS0a,1a,?formula=K{a}p|(K{a}(~p))">Agent $a$ doesn't know that $p$ is true or that $p$ is false.</a></li>
<li><a href="https://vezwork.github.io/modallogic/index.html?model=ApqS1a,0a,2b,0b,1b,4a,;ApqS0a,1a,2b,1b,0b,4a,;ApqS0b,1b,2b,2a,;;AS1a,0a,4a,4b,?formula=K{a}K{b}p">$a$ knows that $b$ knows that $p$ is true.</a></li>
<li><a href="https://vezwork.github.io/modallogic/index.html?model=;ApS2b,3a,1b,1a,;AS1b,2a,2b,;ApqS1a,3a,3b,?formula=[p&~K{b}p](p&~K{b}p)">Announcing the formula $p \land \lnot K_b p$ makes it false! (strange)</a></li>
</ul>
</section>
<section class="text-section">
<h2>What is (Epistemic) Logic?</h2>
Epistemic Logic is way of formally reasoning about knowledge.
In order to understand how Epistemic logic works, let's start with classical logic and build
up from there.
<h3>Classical Logic and Formulas</h3>
<p>
In classical logic we start with propositional variables, our propositional
variables are $p$, $q$, $r$, $s$, and $t$. Each propositional variable can either be
true or false. For example we can say $p$ is false, written as $\lnot p$, and let's say
$q$ is true, written just as $q$.
</p>
<svg viewbox="-50 -20 100 50" height="80" style="margin: 0 auto; display: block;">
<g><circle class="node" r="15" style="fill: rgb(44, 170, 255); stroke-width: 3px; stroke: black;"></circle><text x="0" y="4" class="id" fill="white">0</text><text x="18" y="4" class="shadow">¬p, q</text><text x="18" y="4">¬p, q</text></g>
</svg>
<p>
Alongside propositional variables, we have the classical logical connectives:
<ul>
<li>$\lnot A$ (not) which is true when $A$ is false,</li>
<li>$A \land B$ (and) which is true when both $A$ and $B$ are false,</li>
<li>$A \lor B$ (or) which is true when $A$ is true or $B$ is true, or their both true,</li>
<li>and $A \rightarrow B$ (conditional) which is true if $B$ is true whenever $A$ is true.</li>
</ul>
We can apply the logical connectives, along with parantheses,
to propositional variables to build up complex formulas. For example
<a href="https://vezwork.github.io/modallogic/index.html?model=;AqS?formula=(p-q)&(q-p)">$(p \rightarrow q) \land (q \rightarrow p)$ is a formula which is true when $p = q$</a>,
or <a href="https://vezwork.github.io/modallogic/index.html?model=;AqS?formula=p|~p">$p \lor \lnot p$ is a formula which is always true!</a>
<div class="alert alert-primary mt-3">
pro tip: $(p \rightarrow q) \land (q \rightarrow p)$ can
be written shorthand as <code>(p <-> q)</code> in the playground.
</div>
</p>
<h3>Worlds, Agents, and Epistemic Logic</h3>
<p>
Epistemic Logic is designed for reasoning about the knowledge of someone (we call that someone an agent).
We might imagine that an agent does not know whether they are in a situation where
$p$ is true, or a situation where $p$ is not true, i.e. $\lnot p$.
We express situations as worlds.
We express an agent's knowledge by drawing relations (arrows) between worlds. These worlds
and agent relations together are called a model.
</p>
<p>
Here's <a href="https://vezwork.github.io/modallogic/index.html?model=ApS1a,0a,;AS0a,1a,">an example model</a> for when an agent $a$ doesn't know if they are in
a situation where $p$, or a situation where $\lnot p$:
<svg viewbox="290 200 100 100" width="300" height="100" style="display: block; margin: 0 auto;">
<defs><marker id="mid-arrow-a" viewBox="-2 -5 10 10" refX="0" markerWidth="10" markerHeight="10" orient="0"><text class="agent-text agent-a">a</text></marker></defs>
<defs><marker id="end-arrow-a" viewBox="0 -5 10 10" refX="6" markerWidth="4" markerHeight="4" orient="auto"><path d="M0,-5L10,0L0,5" class="agent-a"></path></marker></defs>
<defs><marker id="start-arrow-a" viewBox="0 -5 10 10" refX="4" markerWidth="4" markerHeight="4" orient="auto"><path d="M10,-5L0,0L10,5" fill="#000" class="agent-a"></path></marker></defs>
<g><path class="link agent-a" d="M255.32746765464503,269.9349482346648Q287.66351853041107 269.967473900772,319.9995694061771 269.9999995668793Q352.3356202819432 270.0325252329866,384.6716711577092 270.0650508990939" style="marker-end: url("#end-arrow-a"); marker-mid: url("#mid-arrow-a"); marker-start: url("#start-arrow-a");"></path><path class="link agent-a" d="M234.32747827813984,269.9138251035397Q219.57956117754583 254.6638598185298,234.82747827813984 239.9138251035397Q250.07539537873384 254.6638598185298,235.32747827813984 269.9138251035397" style="marker-start: url("#start-arrow-a"); marker-end: url("#end-arrow-a"); marker-mid: url("#mid-arrow-a");"></path><path class="link agent-a" d="M405.6716605342144,270.08617403021896Q390.9237434336204 254.83620874520906,406.1716605342144 240.08617403021896Q421.41957763480843 254.83620874520906,406.6716605342144 270.08617403021896" style="marker-start: url("#start-arrow-a"); marker-end: url("#end-arrow-a"); marker-mid: url("#mid-arrow-a");"></path></g>
<g><g class="" transform="translate(234.32747827813984,269.9138251035397)"><circle class="node" r="15" style="fill: rgb(44, 170, 255);"></circle><text x="0" y="4" class="id" fill="white">0</text><text x="18" y="4" class="shadow">p</text><text x="18" y="4">p</text></g><g transform="translate(405.6716605342144,270.08617403021896)"><circle class="node" r="15" style="fill: rgb(255, 127, 14); stroke-width: 3px; stroke: transparent;" transform=""></circle><text x="0" y="4" class="id" fill="white">1</text><text x="18" y="4" class="shadow">¬p</text><text x="18" y="4">¬p</text></g></g>
</svg>
</p>
<p>
When you enter a classical formula into the playground, the formula is evaluated at each world as if that
world was just a classical logic by itself. Epistemic logic introduces a new logical connective which takes advantage of agents' relations
between worlds:
<ul>
<li>$K_b A$ (knowledge of an agent $b$) which is true at a world when $A$ is true at all worlds connected to that
world by $b$ arrows.</li>
<li>along with $K_{a,b,c} A$ which is shorthand for $K_a A\land K_b A\land K_c A$.</li>
</ul>
Now, I understand if this definition isn't intuitive, it's not obvious what $K_b A$ has
to do with knowledge. In order to start intuitively understanding, let's consider our previous
example.
We can write a formula to check whether an agent $a$ knows that they are in
a situation where $p$ or that they know they are in a situation where $\lnot p$:
<div class="mt-2 mb-2" style="display: block; text-align: center;"><a href="https://vezwork.github.io/modallogic/index.html?model=ApS1a,0a,;AS0a,1a,?formula=K{a}p|(K{a}(~p))">$K_a p \lor K_a \lnot p$.</a></div>
This formula is false, by definition of $K_a$, at both worlds because they are each connected to both a world
where $p$ is false and a world where $p$ is true.
<svg viewbox="290 200 100 100" width="300" height="100" style="display: block; margin: 0 auto;">
<defs><marker id="mid-arrow-a" viewBox="-2 -5 10 10" refX="0" markerWidth="10" markerHeight="10" orient="0"><text class="agent-text agent-a">a</text></marker></defs>
<defs><marker id="end-arrow-a" viewBox="0 -5 10 10" refX="6" markerWidth="4" markerHeight="4" orient="auto"><path d="M0,-5L10,0L0,5" class="agent-a"></path></marker></defs>
<defs><marker id="start-arrow-a" viewBox="0 -5 10 10" refX="4" markerWidth="4" markerHeight="4" orient="auto"><path d="M10,-5L0,0L10,5" fill="#000" class="agent-a"></path></marker></defs>
<g><path class="link agent-a" d="M255.32746765464503,269.9349482346648Q287.66351853041107 269.967473900772,319.9995694061771 269.9999995668793Q352.3356202819432 270.0325252329866,384.6716711577092 270.0650508990939" style="marker-end: url("#end-arrow-a"); marker-mid: url("#mid-arrow-a"); marker-start: url("#start-arrow-a");"></path><path class="link agent-a" d="M234.32747827813984,269.9138251035397Q219.57956117754583 254.6638598185298,234.82747827813984 239.9138251035397Q250.07539537873384 254.6638598185298,235.32747827813984 269.9138251035397" style="marker-start: url("#start-arrow-a"); marker-end: url("#end-arrow-a"); marker-mid: url("#mid-arrow-a");"></path><path class="link agent-a" d="M405.6716605342144,270.08617403021896Q390.9237434336204 254.83620874520906,406.1716605342144 240.08617403021896Q421.41957763480843 254.83620874520906,406.6716605342144 270.08617403021896" style="marker-start: url("#start-arrow-a"); marker-end: url("#end-arrow-a"); marker-mid: url("#mid-arrow-a");"></path></g>
<g><g class="" transform="translate(234.32747827813984,269.9138251035397)"><circle class="node" r="15" style="fill: #ff9896;"></circle><text x="0" y="4" class="id" fill="white">0</text><text x="18" y="4" class="shadow">p</text><text x="18" y="4">p</text></g><g transform="translate(405.6716605342144,270.08617403021896)"><circle class="node" r="15" style="fill: #ff9896; stroke-width: 3px; stroke: transparent;" transform=""></circle><text x="0" y="4" class="id" fill="white">1</text><text x="18" y="4" class="shadow">¬p</text><text x="18" y="4">¬p</text></g></g>
</svg>
In an intuitive sense, agent $a$ does not know what $p$ is because they cannot distinguish between
the world where $p$ is true and the world where $p$ is false.
</p>
<p>
If you add more than one agent you can reason about one agent's knowledge of
another agent's knowledge e.g. <a href="https://vezwork.github.io/modallogic/index.html?model=ApqS1a,0a,2b,0b,1b,4a,;ApqS0a,1a,2b,1b,0b,4a,;ApqS0b,1b,2b,2a,;;AS1a,0a,4a,4b,?formula=K{a}K{b}p">$K_a K_b p$, $a$ knows that $b$ knows that $p$ is true.</a>
</p>
<p>
Finally, for the sake of representing knowledge, in Epistemic logic it is expected that all agent's relations between worlds are
equivalence relations, i.e. each agent's relation is:
<ul>
<li><b>reflexive</b>, so each world is related to itself;</li>
<li><b>symmetric</b>, if a world $0$ is related to a world $1$, then world $1$ is also related to world $0$;</li>
<li>and <b>transitive</b>, if a world $0$ is related to a world $1$, and world $1$ is related to world $2$ then
world $0$ has to be related to world $2$ as well.
</li>
</ul>
</p>
<h3>Dynamic Epistemic Logic - Public Announcement</h3>
<p>
Dynamic Epistemic Logic introduces announcement, a mechanism for publicly announcing facts that
become the knowledge of all agents. Given a formula $A$, a public announcement removes all
worlds where $A$ is not true.
</p>
<p>
Dynamic Epistemic Logic also introduces a logical connective:
<ul>
<li>$[A]B$ (public announcement of $A$) which is true at a world if $B$ is true after $A$ is announced, or if the world
is removed by the announcement.</li>
</ul>
Try out the announcement button and the announcement connective in the playground.
</p>
</section>
<section class="text-section">
<h2>Project Information</h2>
<p>
This project is based on the open-source <a href="http://rkirsling.github.io/modallogic/">Modal Logic Playground</a> by <a href="https://github.com/rkirsling">Ross Kirsling</a>.
The Epistemic Logic Playground was made by <a href="https://elliot.website">Elliot Evans</a>.
Special thanks to my non-classical logic instructors Richard Zach and Audrey Yap, as well
as my classmates Jaxson, Parker, Koray, Alejandro, and Tina who provided feedback on this project.
</p>
<p class="mb-4">
More resources on Epistemic Logic and this project:
<ul>
<li><a href="https://github.com/vezwork/modallogic">This project on GitHub</a></li>
<li><a href="https://github.com/vezwork/modallogic/issues/new">Having issues with this project or have a suggestion? Submit an issue here!</a></li>
<li><a href="https://plato.stanford.edu/entries/dynamic-epistemic/appendix-A-kripke.html">Kripke models for modal logic (Stanford Encyclopedia of Philosophy)</a></li>
</ul>
</p>
</section>
</div>
</body>
<script type="text/x-mathjax-config">MathJax.Hub.Config({ tex2jax: { inlineMath: [['$','$']] } });</script>
<script type="text/javascript" async
src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.7/MathJax.js?config=TeX-MML-AM_CHTML">
</script>
<script src="lib/d3.min.js"></script>
<script src="lib/formula-parser.min.js"></script>
<script src="js/MPL.js"></script>
<script src="js/app.js"></script>
</html>