Modal Logic in the Wolfram Language
This is the Community Post presenting the 2016 Summer Wolfram School Project of Jaime Sevilla, a Spanish student of math and computer engineering, assisted by Matthew Szudzik.
The project notebook with the code is attached to this post.
Modal Logic
One particular interesting kind of logic which is not widely known is modal logic, in which we study the notions of necessity and possibility by extending propositional calculus with a new operator, $\square$.
Between the modal logics, the most interesting one is Gödel-Löb logic, also known as provability logic or GL for short.
In GL we have as axioms all logical tautologies, such as $P\wedge \neg P$ and $\square A\implies A$, the distributive axioms, which are sentences of the form $\square [A\implies B]\implies (\square A \implies \square B)$, and the Gödel-Löb axioms, which correspond to sentences of the form $(\square A \implies A)\implies \square A$.
The rules of inference are modus ponens, which allows you to infer $B$ from $A\implies B$ and $A$, and necessitation, which lets you infer $\square A$ from $A$.
$GL$ is of particular interest because thanks to the Arithmetical Adecuacy Theorems of Solovay it can be interpreted to be talking about statements regarding provability predicates in Peano Arithmetic.
So for example, as $(\square \bot \implies \bot)\implies \square \bot$ is a theorem of GL (an axiom, actually) then we know that PA proves that $(Bew (\bot) \implies \bot)\implies Bew (\bot)$ (this is the formalization in arithmetic of Gödel's Second Incompleteness Theorem!).
Conversely, as $\neg \square \bot$ is not a theorem of GL, then we know that $\neg Bew(0/neq 1)$ is not a theorem of $PA$.
My project
During this Summer School I have been implementing basic tools to deal with provability logic in the Wolfram Language, and I have used them to show an interesting application in game theory.
The scope of the project is as follows: * Syntax for modal logic * Semantic evaluation of letterless sentences * Visualization of linear Kripke models * Normal forms of letterless sentences * Fixed point finder: special (for letterless sentences) and general version * An application of modal logic: Modal Kombat
In the following sections I will proceed to describe the functionality implemented, ending with an introduction to modal kombat and its applications to smart contracts.
Syntax for modal logic
Thanks to the symbolic nature of Wolfram Language, I could easily extend the language to include a new symbol for the $\square$ operator.
For example, we could enter Bew[A] [Implies] Bew[Bew[A]] To represent K4 axiom of provable necessitation; in other words, the sentence that represents that if you can prove that a sentence is true then you can prove that you can prove that the sentence is true (modal logic is by nature a tongue twister).
Some convenient abbreviations have been introduced as well. Con is short for $!Bew(False)$ and Possible(x) is short for !Bew(!x).
Semantic evaluation
When dealing with propositional logic, one of the first things we want to deal with is deciding whether a particular expression is true or false. Same with modal logic.
The semantics of modal logic are identical to that of the usual propositional logic (so True||False evaluates to True, while True && False evaluates to False, etc), but we have now to deal with the $\square$ operator.
For reasoning about that we have to think in terms of Kripke chain. A Kripke chain is a countable set of worlds enumerated from 0 to infinity. In each world the box operator will evaluate differently, according to the following rule: $\square A$, where $A$ is a letterless sentence, is true in the world $n$ iff $A$ is true in every world $i$ such that $i<n$.
For example, all sentences preceded with $\square$ are true in world $0$, since there is no previous world where the sentence boxed could be false.
The set of worlds in which a letterless sentence is true is called the trace of the sentence. A letterless sentence is a theorem of $GL$ iff its trace is equal to $\mathbb {N}$.
Also, traces have the property of being either finite or cofinite. Thus we only need to examine the Kripke chain in a finite number of worlds to know the trace; after one point the chain stabilizes and the sentence always evaluates to either true or false.
We can identify where it stabilizes by looking at the terms which have been evaluated to determine the evaluation of a letterless sentence in a world $k$. If the terms involved do not change nor receive different values from $k$ to $k+1$, then the chain stabilizes.
To identify where the trace stabilizes, one can use the function 'Stabilize', which returns the first world in which the chain stabilizes.
To receive a list of the terms involved in evaluating a given formula in world $i$ one can use the 'Terms' function.
Finally, GLEvaluation returns the truth value of a modal sentence in a particular world. GLEvaluation is a central piece of the project, and the optional parameter 'val' can be used for all sort of clever tricks regarding the semantical identification of fixed points, as we will see later.
'GL' is a commodity function that returns true if a letterless sentence is a theorem of $GL$; ie, if its trace is $\mathbb{N}$.
GL[Bew[Bew[False] \[Implies] False] \[Implies] Bew[False]]
Kripke Chain visualization
'WorldModel' displays a table representation of the Kripke chain, in which all terms involved appear with their corresponding truth values in each world.
By default it displays worlds until stability, but you can tweak how many worlds are displayed via the option "depth".
You can also add watches using the option "watches" to display additional terms you might be interested in. $$ \begin{array}{cccccc} \text{world= } & \square (\square (\text{False})) & \square (\text{False}) & \neg \square (\text{False}) & \square (\neg \square (\text{False})) & \square (\neg \square (\text{False}))\Rightarrow \square (\text{False}) \ 0 & \text{True} & \text{True} & \text{False} & \text{True} & \text{True} \ 1 & \text{True} & \text{False} & \text{True} & \text{False} & \text{True} \ 2 & \text{False} & \text{False} & \text{True} & \text{False} & \text{True} \ 3 & \text{False} & \text{False} & \text{True} & \text{False} & \text{True} \ \end{array} $$
We can also use FancyForm to render the Krike chain using more traditional notation.
$$ \begin{array}{ccccccccc} \text{world= } & p & \neg (p) & \square (\bot) & p\Rightarrow \square (\bot) & \neg (p)\Rightarrow \square (\bot) & \square (p\Rightarrow \square (\bot)) & \square (\neg (p)\Rightarrow \square (\bot)) & \square (\neg (p)\Rightarrow \square (\bot))\Rightarrow \square (p\Rightarrow \square (\bot)) \ 0 & \text{T} & \bot & \text{T} & \text{T} & \text{T} & \text{T} & \text{T} & \text{T} \ 1 & \text{T} & \bot & \bot & \bot & \text{T} & \text{T} & \text{T} & \text{T} \ 2 & \bot & \text{T} & \bot & \text{T} & \bot & \bot & \text{T} & \bot \ 3 & \text{T} & \bot & \bot & \bot & \text{T} & \bot & \bot & \text{T} \ \end{array} $$
Normal forms of letterless sentences
For every letterless modal sentence $S$ there is a truth functional compound $N$ of formulas of the type $\square^{n}\bot$ ( $\square^{n}$ means $\square$ nested $n$ times) such that $GL\vdash S\iff N$.
Using $NormalForm$ you can find such a sentence.
Fixed point finder
Consider a sentence of the form $p\iff A(p)$, where every occurence of $p$ in $A$ is in the scope of a $\square$ (we will say that $p$ is modalized in $A$). Then the fixed point theorem affirms that there exists a fixed point $H$ where $p$ does not appear in $H$ such that $GL\vdash (p\iff A(p))\then (p\iff H).
The function 'FixedPointFinder' computes a fixed point of such a sentence in the case that no other sentence letter aside from $p$ appears in $A$. For doing so, it uses semantic evaluation, substituting the $p$ when they are going to be evaluated by $A(p)$. That way we can compute the trace of $p$, and we can easily build a letterless sentence with the same trace using a truth functional compound of sentences of the form $\square^{n+1}\bot \wedge \neg \square^{n}\bot$, which is only true in the world $n$.
The process of computing the fixed point in this way can be visualized using WorldModel and adding the parameter val={p->A(p)}.
If we want to deal with the case where other sentence letter appears, then we can resort to GFixedPoint, which uses a more sophisticated algorithm to compute a fixed point in this more general case. There are whoever no pretty ways of visualizing what is going on in this case.
An application of modal logic: Modal Kombat
We are going to deal with a rather special prisonners dilemma situation. For those of you not familiar with this game theoretical situation, a prisonners dilemma is a scenario in which two partner thieves are given the option to either betray their companion (defect) in exchange of a reduced stance in jail, or remain silent and deal with their penalty (cooperate).
As you can see in the image, there are four possible outcomes. If we cannot reason about what the other person will choose, the rational outcome is to defect in a one-round prisoners dilemma. Sadly, this means that two rational agents end up in the defect-defect equilibrium, instead of the desired cooperate-cooperate.
Now we consider a prisoners dilemma where the players are program with access to a halting oracle (there are some related notions of finite character, but as the analysis of this uncomputable case is easier we will restrict ourselves to it), and that before taking their decision are given access to their opponent's source code. The range of possible strategies widens dramatically, as we can use the source code to predict what our opponent will try to do and try to get the best outcome possible for us!
We tackle now the problem of designing a program for this scenario. There are three criteria for optimality that we aim to achieve:
- Unexplotability: We want to never end in the cooperate-defect outcome (the sucker's payoff), in which we lose the most utility.
- Robust cooperation: Against as many opponents as possible, we want to achive mutual cooperation.
- Robust exploitation: Against as many opponents as possible we want to end in the defect-cooperate outcome in which we gain the most utility.
An special case of robust cooperation is self-cooperation: we want to achive cooperation when playing with a copy of ourselves.
One trivial way to desing an unexploitable program that achives self-cooperation is clique-bot, which collaborates only with programs whose source code is identical to their code.
However, we can do better than that. We are going to deal with programs which try to find mathematical proofs that their opponent is going to act in one way or another in hypothetical situations. Turns out that modal logic comes really handy to represent and reason about such programs.
For example, imagine a program, which we will call FairBot, which will colaborate with an opponent X if and only if there is a proof in Peano Arithmetic that X reciprocates in the collaboration. The pseudocode for this would be something akin to:
FairBot(X):
if Bew(X(FairBot)==Cooperate): return Cooperate
else return Defect
Which in turn can be represented by the modal formula $FB(X)\iff \square X(FB)$, where we interpret that $FB(X)$ collaborates if its trace in the kripke chain is cofinite (the technical justification is that then $GL+n$ for some $n$ will prove $FB(X)$. $GL+n$ is the $GL$ system plus $n$ consistency axioms).
Certainly, FairBot is unexploitable, and achieves cooperation with some simple opponents such as CooperateBot, who always cooperates.
One question arises: Does FairBot cooperate with itself? The answer is by no means obvious, and it is hard to reason about whether both bots will fall into an infinite regression of mutual simulation, waiting for the other to cooperate first in the simulation.
To solve the conundrum, we look at the substitution of FB into FB, which gives us $FB(FB)\iff \square FB(FB)$. As every occurence of FB(FB) is modalized, we are in a situation in which the fixed point lemma is applicable!
Thus we find that $GL\vdash FB(FB)\iff\square FB(FB) \implies FB(FB)\iff \top$. So FairBot does indeed cooperate with itself!
Is this result applicable somehow? Well, as smart contracts gain popularity, it becomes easier to imagine a future in which some smart contracts are set up to engage in trade with other contracts while looking for mutual cooperation guarantees via mathematical proofs. In that sort of scenario one could imagine techniques of modal logic such as the ones we just employed to prove that a certain smart contract is unexploitable and self-cooperative.
In the project I developed some commodity notation and functions to deal with modal programs such as FairBot. For example, FairBot is encoded as the following rule:
FairBot:= FB[x]->Bew[x[FB]]
And we can call ModalKombat(FairBot, FairBot) to get the result of the match.
We can also visualize a match using WorldModel[FB[CB], bots], for example:
$$ \begin{array}{cccc} \text{world= } & \text{CB}(\text{FB}) & \text{FB}(\text{CB}) & \square (\text{CB}(\text{FB})) \ 0 & \text{True} & \text{True} & \text{True} \ 1 & \text{True} & \text{True} & \text{True} \ \end{array} $$
Further improvements
The project has set a great basis for modal logic manipulations in Mathematica, but there is lots of room for improvement. Some tools which would be useful: * A general theorem prover for GL, maybe based on the method of trees or perhaps a semantical method * A way to build arbitrary Kripke models with arbitrary valuations over sentence letters, not only for GL but for other systems of modal logic.
Conclusion
The tools were developed with the purpose of help research and study of GL. I will be pleased if they were to find use by somebody wanting to better explain modal logic or another thing.
Feel free to leave a comment if you want me to clarify anything, and let me know if you are using those tools for a project of your own!
Before closing, I would like to thanks my mentor and the rest of the Wolfram team, as well as the participants of this edition of the Summer School, for letting me be part of such an awesome program with such an awesome crowd of people.
References
Attachments:
