Comparing expressive power of various first order languages

Stream: new members

[David Pratten]

Hi All,

I'm evaluating various theorem proving environments for database theory work. Lean is, naturally, on the list. To assist my selection of a tool, I have a concrete use case which I would be interested in the communities response to.

I'm curious as to the recommended path in Lean for comparing the expressive power of various first order languages. I'd like to leverage Lean's native syntax and input methods to the greatest degree.

For example one language that is interesting to my project is 'conjunctive queries' from database theory which amongst other restrictions doesn't admit disjunction or negation.

One approach might be to start with a meta-programmed implementation of FOL hosted in Lean that mirrors the built-in FOL. Are there other approaches?

Once we had a hosted FOL, I imagine one could instantiate various restricted versions of the hosted language, as required, then prove theorems both within and about them?

If this is the recommended approach, is there a standard hosted FOL to start from?

Thoughts?

David

[Mark Fischer]

David Pratten said:

comparing the expressive power of various first order languages. I'd like to leverage Lean's native syntax and input methods to the greatest degree.

[...]

one language that is interesting to my project is 'conjunctive queries'

Chapter 3 of Theorem Proving in Lean 4 starts with a description of Propositions as Types that might be enlightening.

You can probably introduce types that model your desired language and then prove things with/about them. I don't think you'd need any meta-programming, but you can effectively build your logic using all the same tools Lean uses to build FOL (Lean's Prop universe enjoys some compiler support, but I think the support is for speed/ergonomics and not for expressiveness).

I'm not sure what hurdles you may encounter, but assuming familiarity with Dependent Type Systems, you might be able to get a feel for it yourself in an afternoon or two. If you're not familiar with any system like Lean, Agda, Idris, Coq, etc then there's a bit of a learning curve but it's a fun adventure in my opinion.