Welcome to FormalizedFormalLogic Discussions!

[iehality]

👋 Welcome!

We’re using Discussions as a place to connect with other members of our community. We hope that you:

• Ask questions you’re wondering about.
• Share ideas.
• Engage with other community members.
• Welcome others and are open-minded. Remember that this is a community we
  build together 💪.

To get started, comment below with an introduction of yourself and tell us about what you do with this community.

[jkorb]

Hi, what an awesome project! I was, in fact, thinking of starting something similar before I found this.

I’m a logician working at Utrecht University and I have a series of BA and MA students in AI, who are keen on formally verifying formal logic results for their thesis projects. They have little previous experience, but a solid programming background.

Before we found this project, we were thinking of doing basic modal logic, but you already did that, as far as I can see. I was wondering: What would be good things to work on next? I was thinking of getting them started on something like dynamic epistemic logic, building on your modal logic work. Or maybe bisimulations?

In any case, no promises, but we’re keen on contributing and looking forward to hearing whether there’s interest and/or suggestions.

Feel free to reach out via mail if that’s easier.

Cheers

[SnO2WMaN]

Hello! Thank you for your interest on our project.

As the person responsible for the modal logic side of this project, I would like to share some future prospects. I plan to implement basic facts of provability logic (such as $\bf GL$), including Solovay's arithmetical completeness theorem and its applications, as well as calculi for modal logic, like sequent calculus.
In other words, I am focusing on standard modal logic with Box and Diamond. I am not currently considering logics with many modal operators, such as epistemic logic.

That being said, if any of you are interested in formalizing dynamic epistemic logic or similar, and wish to build upon our formalization, I would offer advice and guidance.

For your reference, here is a page that summarizes formalizations of modal logic by others, including in Lean: https://formalizedformallogic.github.io/Book/references.html#related-works

Best regards.

[fairflow]

hello! I'm Matthew Fairtlough; my undergraduate degree was in Mathematics and my PhD under Stan Wainer in proof theory, subrecursive hierarchies and tree-ordinals; I used a programming language approach to reformulate and generalise some classic results in proof theory. I went on to a postdoc position at Edinburgh University's LFCS where I used Lego to formalise abstract algebra and undertook some formal proofs about synchronous concurrent algorithms. I then took up a lectureship in theoretical computer science at Sheffield University, where I spent most of my limited research time together with my colleague Michael Mendler in developing proof theory, model theory and applications of a relatively unknown modal logic.
One set of axioms that characterizes the Lax modality (in intuitionistic propositional logic) is:
◯R : S → ◯S
◯M : ◯◯S → ◯S
◯F : (S → T) → (◯S → ◯T)
I'm new to Lean 4 (I hadn't heard of it at the start of this September!) but it rekindled my interest in formal mathematics and programming with dependent types; it was thrilling to discover a practical language that integrates programming with dependent types in such an elegant and, to a broad class of mathematicians, eminently usable formal system.
Thus far I've been learning theorem proving in Lean by developing some basic algebra over W-types with 0 (for which I am developing operations which would make them semi-near-rings following an old research proposal of mine). But I would like to work on proving existing results on Lax Logic and contribute something back to the Lean/mathlib/lean4-logic community. I'd really welcome some advice and guidance on this, especially as (a) I'd need to work in (super)intuitionistic framework for the object theory (I prefer constructive methods but am not opposed to using classical principles in metatheory) and (b) there's little in the library covering intuitionistic modal logics [and (c) I'm a beginner with Lean of course]. On the plus side, the Lax modality is very tractable from a technical perspective, having some straightforward proofs of soundness and completeness (via Kripke or more general topological models) and nice theoretical properties (subformula property, cut-elimination, finite model property, Gödel translations and so on). There is also an interesting class of context models which are sound and complete for the logic, contexts being things like C => _, D v _, C => (D v _) etc.

In developing the logic, we met some opposition from traditional logicians (I remember one review from such a person who said "it seems all wrong to me" which hardly seems like a fair and balanced opinion) so please forgive me if I give references:
The logic is variously known as Lax Logic (myself and Mendler), Computational Logic ([N., Bierman, G., & de Paiva, V. (1998))] Computational Types from a Logical Perspective. Journal of Functional Programming, 8(2), 177-193.](http://bit.ly/48Datcu)) or Geometric Logic as expounded by e.g Goldblatt.

[fairflow]

I've been studying the code/proofs for the modal and (super) intuitionistic logics. Going to take a little while for me to get familiar; the basic logic is as I explain above and I think you'll know very well how to use your framework to encode it. If I had a good look at that I think I can dive in and help with proofs. Kripke frames can be very simple: < has a subrelation <_m, ◯S is true at world w just in case for all u > w, exists v. with u <_m v satisfying S. There are some details with ◯false, it helps to have fallible worlds which are not in the codebase I think.

[fairflow]

And it's great you're on board with adding this to mathlib! thanks for your enthusiasm. Very exciting for me. Oh there's an issue with classical logic in that it collapses the modality: ◯S <-> S v ◯false but there are superintuitionistic logics which work fine. Which exactly I'd have to think about.

[iehality]

There are a few issues regarding mathlib. Currently, the plan to move FFL to mathlib is, in a sense, at a standstill. One reason for this is that FFL often undergoes significant changes, and I’d prefer to wait until it stabilizes to some extent. Additionally, from a practical standpoint, formal logic is highly dependent on its representation, so even if we create a library, it likely wouldn’t be used in the same way as conventional algebra libraries (For instance, there’s this comment here, which I largely agree with).

[fairflow]

Ah ok that's informative. I also had the same thoughts about decidability as expressed in this comment. And also about the plethora of typeclasses mentioned earlier in the discussion.

[iehality]

There are several reasons regarding numerous typeclasses.
First, concerning notation: the decision to avoid using Himp or HNot and instead use original type classes may be partly due to reusing assets from when the project was smaller. However, it also stems from a desire to clearly distinguish between semantics and syntax. Specifically, the notation for HImp is ⇨, but as far as I know, convention in logic typically uses a double arrow, like $\Rightarrow$, to represent implication in a semantic sense. Therefore I prefer to avoid this notation. (To be frank, I'm open to borrowing symbols from Heyting algebra for other notations, so this might happen in the future.)

Next, about other typeclasses: as Avigad noted, it is rare to manage various logical systems within a single project, such as FFL, in a consistent way, yet this approach has advantages.
Most logical systems contain common structures, like entailment $\vdash$ or models $\models$, as well as concepts like soundness and completeness. Using typeclasses allows us to define these abstractly. For example, we can prove that in systems stronger than intuitionistic logic, double negation elimination and the law of excluded middle are equivalent without specifying particular formula nor system. (this could be viewed as a kind of theorem schema) (Such codes are mainly done here). These results can then be applied to modal logic, intuitionistic first-order predicate logic, superintuitionistic logic, etc.

Additionally, this approach is useful when working with translations of different logics.

[00sqh]

Hi ,I am an undergraduate student at Fudan University in Shanghai interested in set theory. What an excellent job you have done with this project!

I have a few questions regarding the roadmap for the set theory library:

Given that there already seem to be mature, formalized concepts of definability, is it feasible to formalize Gödel's constructible universe L? Would it be accepted by the project? What do you anticipate the main technical hurdles to be?

I am also curious about the progress on formalizing the forcing theorem, which appears to be currently in development. Are there any outstanding tasks or open issues where I might be able to contribute?

What are the long-term plans for the set theory component? Specifically, I am wondering if the roadmap includes targeting consistency results involving the Axiom of Determinacy (AD), Dependent Choice (DC), or Large Cardinal axioms.

[iehality]

Hi, and thank you for your interest.

As for set theory, @tosiaki and @Convindix are currently working on formalizing transfinite recursion #799. Once that is in place (though it may still take some time) I expect that we can define L, and such a contribution would of course be very welcome.

For the same reason, I think formalizing forcing will also take some more time, since the definition of $\mathbb{P}$-name requires transfinite recursion. Even in the basic part of set theory, there are still many parts that are not yet sufficiently developed (ordinal arithmetic, cardinals, ...), so contributions in those areas would be helpful.

As for the roadmap, including the set theory, FFL does not really have a fixed one. (Our broad goal is to build a formalized catalogue of logic.) We would like to welcome as many results as possible, but I may not be able to review or maintain very specialized developments well enough. So for more niche topics, it might better to consider developing them as downstream projects.

[00sqh]

Thank you so much for the kind reply! I completely agree that transfinite recursion is exactly what's needed to formalize L. Additionally, I think some foundational work on the Lévy hierarchy (issue #663) is also necessary, since we'll need to relativize formulas to set-theoretic structures.

It looks like the work in #799 is progressing well, with the main theorem already formalized and currently undergoing refactoring (if I'm understanding the status correctly!). Since I'm not entirely sure how best to jump in right now, and given that Convindix is already working on that issue, perhaps I could help in tackling issue #663.

[Convindix]

@00sqh Hello, I'm glad you're interested in the repository! I was also thinking about formalizing L in the past, and I got some advice here on the Zulip, in case you find this helpful. (This was before I started using FormalizedFormalLogic, so some details may be Mathlib-specific instead.)