Zulip Chat Archive

Stream: general

Topic: FOL in mathlib


Mario Carneiro (Sep 25 2020 at 13:09):

While updating the lean files from MM0, I have come to face once more the fact that everything outside mathlib bitrots; I was previously depending on flypitch but it's really not feasible to keep up such dependencies because the lean versions don't match up (it hasn't been updated since 3.4.2). But the FOL formalization in there is definitely useful for other stuff, so I would like to look (once more) into getting it into mathlib.

Are there any additional changes that should be made to FOL to make it fit in mathlib? This will probably be a new top level folder like proof_theory; any ideas on what the scope should be?

Rob Lewis (Sep 25 2020 at 13:14):

I'm definitely in favor. There have been more than a handful of people showing up here asking about FOL who we've directed to Flypitch. It would be great to have it local and up to date

Rob Lewis (Sep 25 2020 at 13:15):

We should be very careful with docs. Like it or not, people who think "Lean = logic" will be drawn to this file without necessarily understanding what it's doing. It needs to be clear e.g. that this is unconnected to the foundations of Lean, what a deep embedding is, etc

Johan Commelin (Sep 25 2020 at 13:15):

@Aaron Anderson has been working on this as well

Mario Carneiro (Sep 25 2020 at 13:16):

CC @Floris van Doorn @Jesse Michael Han Are there any lingering things that you wanted to update about the development? I recall there being some churn about dvector and dfin

Johan Commelin (Sep 25 2020 at 13:18):

Note also that in the lean-omin directory, Reid has developed "finvec". A nice api around fin n -> R.

Reid Barton (Sep 25 2020 at 13:29):

Yes, recently I tried to get it closer to mathlib readiness:
https://github.com/rwbarton/lean-omin/blob/master/src/for_mathlib/finvec.lean

Jesse Michael Han (Sep 25 2020 at 14:21):

IIRC floris would have preferred our FOL library to to use finvec over dvector.

bringing flypitch from 3.4.2 to 3.20 is not high on my to-do list at the moment, but i'm happy to accept PRs/endorse incorporating the code into mathlib

Adam Topaz (Sep 25 2020 at 15:21):

Reid Barton said:

Yes, recently I tried to get it closer to mathlib readiness:
https://github.com/rwbarton/lean-omin/blob/master/src/for_mathlib/finvec.lean

I would be very happy when this reaches mathlib! In case you're taking "requests", one of the main things that seems missing from mathlib is support for quotients, e.g. as in
https://github.com/flypitch/flypitch/blob/aea5800db1f4cce53fc4a113711454b27388ecf8/src/to_mathlib.lean#L321
https://github.com/flypitch/flypitch/blob/aea5800db1f4cce53fc4a113711454b27388ecf8/src/to_mathlib.lean#L331

Jeremy Avigad (Sep 25 2020 at 17:13):

Naming suggestion: call the folder "formal logic". Any deeply embedded logical system can go there. I prefer that to "proof theory" because it can include model theory and purely semantic developments as well.

Floris van Doorn (Sep 25 2020 at 17:20):

Yes, I'd like to use finvec instead of the non-standard dvector for the first-order logic file. But we can also port it to mathlib with dvector and port it to finvec once Reid merges his file.
Also note that if you just want to use fol.lean (and at most ~10 other files), there is a compiling version of that file on the branch lean-3.14.0, which should be a lot easier to port to the current version: https://github.com/flypitch/flypitch/blob/lean-3.14.0/src/fol.lean. I started porting flypitch to a (then) recent version of Lean, but fixing proofs later in the development was very painful :(

Aaron Anderson (Sep 25 2020 at 20:08):

Johan Commelin said:

Aaron Anderson has been working on this as well

My work so far has been at branch#fol-attempt. I have at least a basic proof of concept that flypitch structures can be ported with finvec, and a development of some basic model theory ideas that IIRC aren't in flypitch.

Aaron Anderson (Sep 25 2020 at 20:09):

I tried porting some of fol.lean, but got bogged down, I forget which lean version that was on.

Aaron Anderson (Sep 25 2020 at 20:10):

I could probably get a PR or two out of it just to get the ball rolling, but it'd be hard for me to port all of fol.lean without some help from people with more technical lean experience.

Alexandre Rademaker (Sep 28 2020 at 21:50):

Rob Lewis said:

We should be very careful with docs. Like it or not, people who think "Lean = logic" will be drawn to this file without necessarily understanding what it's doing. It needs to be clear e.g. that this is unconnected to the foundations of Lean, what a deep embedding is, etc

Yep, I would be one of those people. I am particular curious about what is the scope and goal of the definitions pointed by @Mario Carneiro .

Mario Carneiro (Sep 28 2020 at 21:51):

Which definitions are you referring to?

Reid Barton (Oct 04 2020 at 22:56):

#4406 has the most important parts of data.finvec. I'm not sure if the stuff related to set (finvec n R) is as generally useful so I'm going to hold off on it for now.

Alexandre Rademaker (Oct 09 2020 at 03:52):

@Mario Carneiro , I am talking about the file https://github.com/flypitch/flypitch/blob/master/src/fol.lean . I didn’t understand its content and scope

Mario Carneiro (Oct 09 2020 at 03:53):

The idea is to define what first order logic is, so that you can state and prove theorems in proof theory and model theory

Mario Carneiro (Oct 09 2020 at 03:53):

in particular, flypitch itself was concerned with proving the independence of the continuum hypothesis from the axioms of ZFC, which requires the notion of provability in ZFC to state

Alexandre Rademaker (Oct 09 2020 at 03:58):

Can you suggest any text about it?

Mario Carneiro (Oct 09 2020 at 03:58):

there were a couple papers about flypitch by Jesse and Floris

Mario Carneiro (Oct 09 2020 at 03:59):

https://github.com/flypitch/flypitch-itp-2019/releases/tag/1.1

Mario Carneiro (Oct 09 2020 at 04:00):

Also https://flypitch.github.io/assets/flypitch-cpp.pdf

Alexandre Rademaker (Oct 09 2020 at 04:00):

Thank you very much


Last updated: Dec 20 2023 at 11:08 UTC