An interpreter for set theory + first order logic

Stream: new members

[Patrick Thomas]

Is it possible to construct a sort of interpreter that takes a formulation strictly in set theory and first order logic and translates it to a formulation in Lean? That is, the only things given in the formulation to be interpreted are the axioms of set theory and first order logic, and the interpreter checks that those are all that are used, and then translates them into type theory as implemented by Lean in order to check them? I hope to learn type theory, and I am trying to, but I keep running into the issue that all of the books, including the one I am currently using to learn type theory, seem to give definitions and proofs using set theory. I usually try to formalize these to check my understanding and proofs, and perhaps it might be easier to do using something like this.

[Mario Carneiro]

Sure. This is more or less what the metamath -> Lean translator does, mapping proofs in ZFC into proofs about the Set type in lean

[Mario Carneiro]

But it probably isn't that helpful if you don't already have formal set theory content to translate from

[Mario Carneiro]

Also, it isn't always exactly what you want; translating into idiomatic type theory often means using more types than the unityped set theory version

[Mario Carneiro]

If you include this stuff, translating into type theory becomes a much more heuristic affair, and I would recommend just learning how to do it by hand

[Jason Rute]

@Patrick Thomas If you are just formalizing regular mathematics (i.e. not ZFC set theory), then usually the translation isn't too difficult when you get the hang of it. I'd recommend looking at the conversation at the end of #general > Type theory of Lean.

[Jason Rute]

Juho Kupiainen said:

I feel it would be useful to have a guide for how to formalize math that was previously defined in set theory.

[Jason Rute]

Reid Barton said:

The one line summary is Type = set, set = subset.

[Patrick Massot]

Patrick Massot said:

Juho Kupiainen said:

I feel it would be useful to have a guide for how to formalize math that was previously defined in set theory.

The main trick is to realize you are lying to yourself. The math you are thinking of have not been "previously defined in set theory". They have been defined outside of any formal foundation. However they are usually expressed using a vocabulary that is inspired by set theory, but this is a very superficial connection with set theory. When using Lean you can mostly ignore foundational details (unless you want to formalize computer science). You'll get used to it very quickly.

[Patrick Thomas]

Jason Rute said:

Patrick Thomas If you are just formalizing regular mathematics (i.e. not ZFC set theory), then usually the translation isn't too difficult when you get the hang of it. I'd recommend looking at the conversation at the end of #general > Type theory of Lean.

What is the delineation between regular mathematics and ZFC set theory?

[Kevin Buzzard]

A lot of the questions that set theorists think about are not mathematics but metamathematics. For example the proof of the independence of the continuous hypothesis is a result about the existence of models of mathematics.

[Reid Barton]

You can do regular mathematics without knowing the axioms of ZFC

[Kevin Buzzard]

Proof: Gauss and Euler were doing it before the axioms had even been invented.

[Patrick Thomas]

I guess I still feel like I'm stuck in a bit of a bootstrap issue, needing to learn type theory to use type theory to formalize my learning of type theory. This probably isn't unique to type theory, I would likely have the same issue with learning set theory using Metamath or Mizar. Probably what I am really looking for are more textbooks that use definitions, theorems and proofs that are already formalized, like Software Foundations in Coq. Are there more textbooks like that out there? Any hope that people are writing them?

[Chris B]

https://leanprover.github.io/logic_and_proof/
https://github.com/blanchette/logical_verification_2020
https://github.com/ImperialCollegeLondon/formalising-mathematics

[Patrick Thomas]

Thank you. Are there any that aim at teaching the foundational theory of type theory and computing?

[Patrick Thomas]

That is, aimed at teaching the theory behind assistants like Lean (lambda calculus, etc.) rather than how to use the assistants.

[Patrick Massot]

No

[Patrick Thomas]

Is that because it is thought to be not worth doing, can't be done, or just hasn't been done yet?

[Chris B]

TPIL has an introductory section on type theory, and the Lean team wrote this paper about elaboration which IMO is like the heart of a proof assistant. There are plenty of good educational resources discussing nuts and bolts of the typed lambda calculus, but the "why" of the foundational stuff pretty quickly gets into ultra-specialist territory that looks like mario's thesis or the Dybjer paper describing the theory behind Lean's inductive types.

[David Thrane Christiansen]

A couple of books that might work for you, depending on the way in which you want to learn the theory and which aspects you want to learn about, include "Type Theory and Formal Proof" by Nederpelt and Guevers, the first chapter of the Homotopy Type Theory book, "Programming in Martin-Löf's Type Theory" by Nordström, Petersson and Smith, the chapter on dependent types in "Advanced Topics in Types and Programming Languages" (chapter 2, by Aspinall and Hofmann), or "The Little Typer" that I wrote with Dan Friedman. What works for you will depend a lot on your background, goals, and learning style.

[Scott Morrison]

The first section of the homotopy type theory book is I think very good! Make sure you stop reading when they start talking about univalence, though. :-)

[Scott Morrison]

It's quite pleasant to read if you're used to reading mathematics, and is describing a foundation that to a mathematician's eyes is "close enough" to Lean's.

[Jason Rute]

Patrick Thomas said:

Thank you. Are there any that aim at teaching the foundational theory of type theory and computing?

See Good introductory book to type theory? on MathOverFlow. However, as I said there, I personally think the getting one's hands dirty with a theorem prover is one of the better ways to learn type theory.

[Patrick Thomas]

I was hoping for texts on type theory that had been formalized, but thank you.

[Reid Barton]

Trying to learn type theory by formalizing type theory in type theory (or by studying formalizations of type theory in type theory) sounds like pretty much the most difficult possible way to go about it

[Jason Rute]

Patrick Thomas said:

I guess I still feel like I'm stuck in a bit of a bootstrap issue, needing to learn type theory to use type theory to formalize my learning of type theory. This probably isn't unique to type theory, I would likely have the same issue with learning set theory using Metamath or Mizar. Probably what I am really looking for are more textbooks that use definitions, theorems and proofs that are already formalized, like Software Foundations in Coq. Are there more textbooks like that out there? Any hope that people are writing them?

I not sure what "use type theory to formalize my learning of type theory" means, but I would caution against it. Lean's type theory is a list of finite rules (plus axioms for classical mathematics). They are not the same rules and axioms as first order logic, but is is still in the same spirit of finite symbol manipulation. While it is not uncommon in metamathematics, to say use a first order theory like Peano arithmetic or ZFC set theory to prove properties about itself, however, I have a few observations about this approach: (1) One first learns Peano arithmetic (or ZFC) and how to use it for proofs, before one proves metamathematical properties about Peano arithmetic (or ZFC). (2) Metamath of a system is much harder than learning that system. (3) If one uses that same system to do the metamath (say using ZFC to prove stuff about the axioms of ZFC), then one quickly runs into Godel's incompleteness theorem. The same would happen in Lean.

Also dependent type theory is sort of like a program language. While it is possible to say write a Java compiler in Java, this is not how one usually learns Java. And while it is common to have a CS course where one writes a Scheme interpreter in Scheme, I would still argue that learning Scheme comes far earlier in that course that using Scheme to construct Scheme, and the point of that course isn't to learn Scheme, but to learn programming language theory. (Even Turing's paper first developed Turing machines and some examples before using Turing machines to run Turing machines.)

Specifically for Lean, I can't imagine what formalizing your learning of type theory would mean except to build your own proof checker, or at least parts of it. This is not easy at all, but is doable and others have done it. To do this one would have to really understand the foundations of Lean, like the full details of expressions and the Lean export format. Also, this is usually coded in another language like C++, Rust, Haskell, etc. Lean4 does have a proof checker written in Lean4, but I don't know if there is one not using unsafe code. While one could also theoretically do all or most of this in pure safe Lean, it would be a lot of work getting all the data types to work etc. More than that, what would you be proving about Lean? While Mario's thesis is devoted to the meta theory of Lean (including its consistency), none of that is needed to know how to use Lean. And most or none of it is formalized. Formalizing Mario's thesis would itself be a thesis.

[Jason Rute]

Reid Barton said:

Trying to learn type theory by formalizing type theory in type theory (or by studying formalizations of type theory in type theory) sounds like pretty much the most difficult possible way to go about it

I need to learn to be more succinct.

[Reid Barton]

I was thinking about the "learn X by writing a compiler for X in X" analogy also.

[Jason Rute]

I'm also going to hedge my above comments. If for example, if there is a book doing this for Coq (I don't know what is in Software Foundations for example), this surprises me less than if one existed for Lean. The reason is that Coq is more often used to prove properties of algorithms than Lean. Right now Lean is used more to prove mathematical theorems found in pure math. So if this does exist in Coq (and I'm not saying it does) and you really want to learn it this way, I would recommend leaning Coq first. Then learning Lean should be far easier.

[Patrick Thomas]

I didn't mean that Software Foundations tries to teach the meta theory of Coq, just that it was an example of a formalized text, in the sense that the examples are actual proofs in Coq.

[Jason Rute]

Aren't the examples in TPIL (or any Lean tutorial) also actually proofs in Lean?

[Patrick Thomas]

I didn't mean to ask, is there something like SF for Lean, but instead, is there something like SF that teaches type theory.

[Jason Rute]

Ok, so you want a math text about type theory as a mathematical subject where all the theorems are formally proved, but it is also a readable introduction to the subject? I'm pretty sure your could replace "type theory" with almost any subject and you would get a negative answer. This is asking a lot. There are research papers formally proving properties of say Coq or HOL Light's foundations in Coq or HOL Light, but they are advanced research papers, not introductory texts.

[Patrick Thomas]

Yes, basically, I think. This is sort of the goal of using Lean for teaching though right? So it is something being developed?

[Reid Barton]

What Jason said except the text is even more unlikely to exist because I would expect most potential authors to think this is a pedagogically unsound approach to learning type theory, e.g., it is likely to create confusion between the object level and the meta level in addition to the points Jason made earlier.

[Reid Barton]

People who are interested in using Lean for teaching aren't using it to teach the syntax of type theory as an object-level theory. (For one thing, people who are into that sort of thing are mostly using other proof assistants.)

[Kyle Miller]

Here's an example of Lean for teaching I believe, and it's about basic real analysis, not type theory. I've heard a few anecdotes about teaching with Lean where type theory itself had been successfully ignored. I guess this is sort of like how in most math courses (undergraduate and graduate) ZFC is never even mentioned.

[Reid Barton]

They're using it to teach: either ordinary object-level mathematics, like real analysis or a + b = b + a; or "what is a proof" / "what does it mean to prove something"--but in the ordinary sense, not in the sense of how can we regard the syntax of a proof as a mathematical object itself.

[Mario Carneiro]

Jason Rute said:

I'm also going to hedge my above comments. If for example, if there is a book doing this for Coq (I don't know what is in Software Foundations for example), this surprises me less than if one existed for Lean. The reason is that Coq is more often used to prove properties of algorithms than Lean.

While I think that this is more likely for Coq, it is also more likely to be a formalization of only a fragment of Coq; full Coq is quite a bit more complicated than Lean, and an analogue of my thesis for Coq is, as far as I know, still an open problem (although there are some formalizations that get close, in particular "Coq Coq Correct!")

[Patrick Thomas]

Reid Barton said:

People who are interested in using Lean for teaching aren't using it to teach the syntax of type theory as an object-level theory. (For one thing, people who are into that sort of thing are mostly using other proof assistants.)

So there are people out there doing this sort of thing, just using other proof assistants?

[Patrick Thomas]

Do you run into the issue that you then have to check the meta theory, and then the meta meta theory...

[Reid Barton]

e.g. there is https://www.cs.nott.ac.uk/~psztxa/publ/tt-in-tt.pdf

[Reid Barton]

or http://www2.tcs.ifi.lmu.de/~abel/popl18.pdf

[Patrick Thomas]

Interesting. Do you think there is similar material at an introductory teaching level?

[Mario Carneiro]

Doesn't software foundations cover lambda calculus?

[Mario Carneiro]

If you want formalized DTT I don't think you can get much simpler than Altenkirch's article

[Mario Carneiro]

and quite frankly there is no way you can read that article unless you have a very strong grasp of type theory already

[Patrick Thomas]

Yes, SF covers lambda calculus, but I think stops at the STLC, at least from what I gather from the table of contents.

[Patrick Thomas]

At the moment I've started going through "Types and Programming Languages", which I think goes further, but is not formalized.

[Matthew Ballard]

Chris B said:

https://leanprover.github.io/logic_and_proof/
https://github.com/blanchette/logical_verification_2020
https://github.com/ImperialCollegeLondon/formalising-mathematics

+1 for https://github.com/blanchette/logical_verification_2020 for a great lean specific educational resource (along these lines, which I interpret as “more CSy but with real math still“)

[Anne Baanen]

Matthew Ballard said:

Chris B said:

https://leanprover.github.io/logic_and_proof/
https://github.com/blanchette/logical_verification_2020
https://github.com/ImperialCollegeLondon/formalising-mathematics

+1 for https://github.com/blanchette/logical_verification_2020 for a great lean specific educational resource (along these lines, which I interpret as “more CSy but with real math still“)

Be sure to check out the website for recorded lectures and some bonus information!

[Patrick Thomas]

Jason Rute said:

Patrick Thomas If you are just formalizing regular mathematics (i.e. not ZFC set theory), then usually the translation isn't too difficult when you get the hang of it. I'd recommend looking at the conversation at the end of #general > Type theory of Lean.

Supposing I did want to formalize ZFC set theory, does it make sense to do so in Lean?

[Scott Morrison]

src#Set

[Patrick Thomas]

(deleted)

[Patrick Thomas]

Is the full power of the calculus of constructions needed to formalize set theory and first order logic with equality? What is the simplest extension to the simply typed lambda calculus that is necessary to formalize most set theory based math? Lambda P?

[Scott Morrison]

See previous discussion at https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/inductive.20types.20.3D.20set.20theory.3F

[Patrick Thomas]

I'm not sure if I am asking the same thing. I don't think I mean what is the minimum lambda calculus to have the same power as zfc. I'm saying for example, did the author of the formalization of the book linked above need to full power of Coq, or could everything he stated and proved have been done with something simpler, like Lambda P. That is, could a simpler lambda calculus be used to encode first order logic with equality and formalize the axioms of zfc.

[Patrick Thomas]

From which then most of math can be done?

[Patrick Thomas]

Maybe the questions end up equating because in order to formalize the axioms of zfc, you need to same power as zfc?

[Patrick Thomas]

I guess put another way, can you use less type theory and do the same amount of math by using the axioms of zfc instead of inductive types.

[Mario Carneiro]

Of course. You don't need to do everything in type theory, and there are proof assistants based on set theory and the axioms of ZFC (metamath being the one I am most familiar with), and in those proof assistants "types" are a tacked-on notion at best, and are not at all foundational. Inductive types are constructed, not axiomatized, and you can prove the existence of a large class of inductive types in ZFC, similar to what lean implements "by fiat".

[Mario Carneiro]

The underlying foundation of a proof assistant is actually one of the less important reasons to pick one proof assistant over another. All foundations in common use are "good enough" for "most" math. The real differences are in the user interface, support for metaprogramming or tactics, and editor integration. That's where all the person-years of effort goes.

[Patrick Thomas]

Is Lambda P powerful enough to encode equality?

[Patrick Thomas]

That is, suppose that I want to code a simple proof checker, and I want to use the Curry Howard isomorphism for the logic and the statements of the axioms of set theory for the math. I believe that I need types that depend on terms to encode forall and exists, which is given by lambda P. Does lambda P give me equality as well, or do I need the full calculus of constructions to get it?

[Mario Carneiro]

I don't think even CoC gives you equality unless you add it explicitly

[Patrick Thomas]

Can I add it to just lambda P in the same way?

[Mario Carneiro]

as long as you can express types depending on terms, then Eq : A -> A -> Type is expressible

[Patrick Thomas]

What do I have to do to get the introduction and elimination rules for it?

[Mario Carneiro]

you just axiomatize them

[Patrick Thomas]

I see. Is that tricky, to axiomatize the substitution?

[Mario Carneiro]

Just take a look at the axioms for Eq in lean

[Mario Carneiro]

#print Eq.refl
-- constructor Eq.refl.{u} : ∀ {α : Sort u} (a : α), a = a

#print Eq.subst
-- theorem Eq.subst.{u} : ∀ {α : Sort u} {motive : α → Prop} {a b : α}, a = b → motive a → motive b

[Patrick Thomas]

I think I see. I'll give it a try. Thank you.

[Yaël Dillies]

Well actulaly Eq.subst isn't an axiom, right? It's a consequence of the recursor. Or did that change in Lean 4?

[Mario Carneiro]

You are correct, but Eq.rec has a complicated type and it's not necessary to make the point, especially if you don't have a complicated type system