Bio

Jaime Sevilla is a mathematics and computer engineering undergrad student at the Universidad Complutense de Madrid, Spain.

He is headed toward becoming a researcher in safe artificial intelligence. He is a summer fellow of the Machine Intelligence Research Institute and an alumni of the Center for Applied Rationality. He has spoken at several conferences about artificial intelligence, rationality and effective altruism, as well as organized several workshops and activities related to those fields.

He has also led a couple of entrepreneurship-related projects as a startup leader, and has won several math contests and programming hackathons.

His study interests lie in logic, computability, complexity, probability, machine learning and the theoretical foundations of artificial intelligence, among other things.

Project: Modal Logic in the Wolfram Language

Modal logic extends propositional logic by introducing a new operator, □, symbolizing necessity.

The goal of this project is to implement utilities to express and manipulate statements of modal logic within the Wolfram Language, together with tools to reason about their correctness, simplification and semantic representation of such statements in relation to the most famous formal system of modal logic, GL.

The reason why we focus on this system is twofold. In the first place, GL is decidable, which allows us to build a collection of functions that could potentially be used to reason about its theorems with full generality. Perhaps more interestingly, Solovay’s arithmetical adequacy theorems show us a direct relationship between theorems of GL and provability in PA: a sentence of modal logic is a theorem of GL if and only if Peano arithmetic proves every substitution instance of the statement. This is a very powerful result that can be used to reason effectively about tricky, self-referential statements in PA, via the fixed-point theorems of GL.

For this project, we have implemented the following:

• Syntax for modal logic statements
• A semantic GL theorem prover
• Kripke chain visualization
• Fixed-point finder for the special case with only one variable and for the general unrestricted case
• Transformation of letterless sentences of modal logic to equivalent truth-functional compounds in GL

As applications for modal logic, this work may be relevant for the formalization of unambiguous smart contracts, automatic theorem proving in PA and game theory research applications in the context of self-referential, or mutually-referential, agents.

To showcase the potential of our work, we implement Modal Kombat, a game theoretical application of modal logic in which two programs with access to each other’s source code are confronted with a prisoners’ dilemma situation.

References

[1] G. Boolos, The Logic of Provability, Cambridge: Cambridge University Press, 1995.

[2] P. LaVictoire, “An Introduction to Löb’s Theorem in MIRI Research,” expository note, 2015. intelligence.org/files/lob-notes-IAFF.pdf.

Favorite 3-Color 2D Totalistic Cellular Automaton

Rule 875035732