modal logic on top of Lean's logic?

Stream: new members

[Matt Diamond]

I was wondering if it's possible to prove theorems of modal logic by defining necessity as an opaque function with the type Prop → Prop and adding axioms like so:

import Mathlib

opaque Necessary (A : Prop) : Prop

notation:max "□" p:40 => Necessary p

axiom necessitation {A : Prop} : A → □A
axiom distribution {A B : Prop} : □(A → B) → (□A → □B)

However, my understanding of necessitation is that it's a kind of meta-logical rule, saying that if a theory entails A, then it also entails □A, which is technically different from saying "this theory entails the implication A → □A". Otherwise necessitation would imply modal axiom 4.

Does this mean that the only way to prove anything about modal logic in Lean is to define a notion of logical system from scratch, like in https://github.com/FormalizedFormalLogic/Foundation? Or is there some part of modal logic that can be formalized the "easy way" by simply adding axioms on top of Lean's logical system?

[Bjørn Kjos-Hanssen]

I suppose you could add another function Provable and then the axioms become

opaque Necessary (A : Prop) : Prop
opaque Provable (A : Prop) : Prop

notation:max "□" p:40 => Necessary p
notation:max "⊢" p:40 => Provable p

axiom necessitation {A : Prop} : ⊢ A → ⊢ □A
axiom distribution {A B : Prop} : ⊢ (□(A → B) → (□A → □B))

But this is really just a toy setup because it allows you to express undesired things like □(⊢A),
and doesn't allow for negative result like "S4 doesn't imply S5".

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Matt Diamond said:

I was wondering if it's possible to prove theorems of modal logic by defining necessity as an opaque function with the type Prop → Prop and adding axioms like so:

import Mathlib

opaque Necessary (A : Prop) : Prop

notation:max "□" p:40 => Necessary p

axiom necessitation {A : Prop} : A → □A
axiom distribution {A B : Prop} : □(A → B) → (□A → □B)

However, my understanding of necessitation is that it's a kind of meta-logical rule, saying that if a theory entails A, then it also entails □A, which is technically different from saying "this theory entails the implication A → □A". Otherwise necessitation would imply modal axiom 4.

Does this mean that the only way to prove anything about modal logic in Lean is to define a notion of logical system from scratch, like in https://github.com/FormalizedFormalLogic/Foundation? Or is there some part of modal logic that can be formalized the "easy way" by simply adding axioms on top of Lean's logical system?

My fuzzy understanding is that this cannot be done precisely because of the trouble with necessitation that you point out. There are type-theoretic renderings of modal logic, but all the ones I know involve some kind of extension of the system. A nice paper in this area is Fitch-Style Modal Lambda Calculi. It's simply-typed, but this approach has been extended to DTT.

[Matt Diamond]

Do we have anything about Kripke semantics in Mathlib? I've been playing around with Kripke Frames/Models in Lean, deriving various "axioms" from frame conditions, and it's been pretty easy to work with so far

[Miyahara Kō]

Not in Mathlib, but in FormalizedFormalLogic.

[Matt Diamond]

Ah okay, I'll take a look there. Thanks!