axioms and rules of inference

Stream: Type theory

[Paige Thomas]

Can type theory be expressed using a set of axioms and rules of inference in the same manner that set theory can? Is there a way to translate a proof in Lean to an enumeration of steps, where each is either an instance of an axiom or the result of applying a rule of inference to previous steps?

[Henrik Böving]

Yes, the inference rules are basically just the typing rules, this is a well known idiom known as the "curry howard correspondence". For some introductory material you can check out e.g. https://github.com/JLimperg/dtt-seminar-2024/releases/latest/download/notes.pdf or https://www.danielgratzer.com/courses/type-theory-s-2024/lecture-notes.pdf

For the specific constructions used by Lean's type theory you can take a look at #leantt

[Paige Thomas]

@Henrik Böving Thank you. Out of curiosity, is there by any chance a tool available that will take a Lean proof and translate it to a listing of the application of each axiomatic typing rule?

[Henrik Böving]

Well internally Lean is turned into a lambda calculus term that gets type checked by essentially applying the inference rules in an efficient way to check if the lambda term represents a prope proof. So that tool is quite literally Lean itself.

[Paige Thomas]

I guess I mean something that will print an enumerated list of the inference rules that are applied in order.

[Bulhwi Cha]

Kayla Thomas said:

Can type theory be expressed using a set of axioms and rules of inference in the same manner that set theory can?

You might want to take a look at lean.mm1: https://github.com/digama0/mm0/blob/8aba8acf9f524d8f4a0401f78dba1348a3a41f2b/examples/lean.mm1.

[Paige Thomas]

@Bulhwi Cha Thank you.