Zulip Chat Archive

Stream: new members

Topic: Creating Theories


Newell Jensen (Mar 05 2022 at 18:47):

I am new to lean and have played around with it but I still haven't wrapped my head around whether or not it is possible to use lean to create your own axiomatic theories. For example, let's say I want to create a propositional calculus that is built from a couple logical connectives together with modus ponens and a handful of axioms. Is it possible to reason with lean within this scope?

I tried seeing if this had already had been asked in the past but didn't have too much luck so apologize if this is something that has come up from time to time. Cheers and thanks (hoping to carve out more time in the future to really start using lean more).

Jakub Kądziołka (Mar 05 2022 at 18:53):

you can do that by defining the logic you're interested in and using Lean as a meta-logic

Jakub Kądziołka (Mar 05 2022 at 18:53):

then you'll be proving theorems of the form "X is provable in [your logic]"

Jakub Kądziołka (Mar 05 2022 at 18:55):

I think you could even define the syntax such that this amounts to putting a turnstile before the theorem statement

Newell Jensen (Mar 05 2022 at 18:58):

@Jakub Kądziołka Thanks for the reply. Any pointers in navigating the meta-programming documentation? Also not sure, but would this be something that might be easier in lean 4 vs lean 3?

Newell Jensen (Mar 05 2022 at 19:01):

An example is probably all I would need to get me started (would at least save me some time stumbling around at least) so if you are aware of any I am interested to hear. Thanks again.

Yaël Dillies (Mar 05 2022 at 19:13):

This has nothing to do with "metaprogramming" as in "writing tactics. You might want to check out Flypitch.

Chris B (Mar 05 2022 at 19:20):

There's also this thread, there are probably similar ones in the "Type Theory" stream. There's another project called mm0 that's more directly aimed at this kind of thing; the author has an intro/tutorial video: https://www.youtube.com/watch?v=A7WfrW7-ifw

Newell Jensen (Mar 05 2022 at 21:48):

Thanks everyone. Seems metamath or mm0/mm1 are what I actually need as doing this in lean is a bit harder. Cheers.


Last updated: Dec 20 2023 at 11:08 UTC