FOL in mathlib

Stream: general

[Mario Carneiro]

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]

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]

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]

@Aaron Anderson has been working on this as well

[Mario Carneiro]

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]

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

[Reid Barton]

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]

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]

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]

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]

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]

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]

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

[Aaron Anderson]

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]

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]

Which definitions are you referring to?

[Reid Barton]

#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]

@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]

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]

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]

Can you suggest any text about it?

[Mario Carneiro]

there were a couple papers about flypitch by Jesse and Floris

[Mario Carneiro]

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

[Mario Carneiro]

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

[Alexandre Rademaker]

Thank you very much