Creating Theories

Stream: new members

[Newell Jensen]

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]

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

[Jakub Kądziołka]

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

[Jakub Kądziołka]

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

[Newell Jensen]

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

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]

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

[Chris B]

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]

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