What to read to learn logic?

Stream: new members

[Ignat Insarov]

The common presentation style of mathematical literature skims over _«nitty-gritty»_ formalities of logic. This is unfortunately reflected in my own lack of understanding — it is often that I trust the proof assistant without really understanding what it does _«under the hood»_, and even if I can prod it into accepting my proof, I am unhappy.

What can I read to better understand how proofs work on the most tedious and pedantic level?

I want to get an intuition of where excluded middle or decidability are required, see examples of how to build natural numbers, functions and tuples from the ground up, how quantifiers work in hypotheses and goals, and so on. Ideally I should like to see how all this works in the setting of Lean, where we have types rather than sets, and why it leads to the same results as the mathematics based on set theory.

I already understand how proofs work overall and I am comfortable working with a proof assistant.

[Andrew Ashworth]

You should do all the exercises in Theorem Proving in Lean

[Andrew Ashworth]

also avoid tactics and construct your proofs in term mode (unless eq.subst is uncooperative, then you might need rw)

[Andrew Ashworth]

You will either understand all the tedious and pedantic detail by the end, or will have given up in frustration at all the tedious and pedantic detail, so it's a win/win situation no matter which way you end up

[Chris B]

Ignat Insarov said:

What can I read to better understand how proofs work on the most tedious and pedantic level?

You can read Mario's paper and/or poke around in one of the kernel implementations to see what's at like the ring 0 of Lean. There's also Peter Dybjer's paper if you really want to get into the theory behind the inductive stuff. At the end of the day, users write an expression e which they claim is of type T, Lean infers the type of e and checks whether the result is definitionally equal to T.

[Ignat Insarov]

So, Mario's paper says (before becoming too technical for me to follow) that Lean's type theory is equivalent to ZFC. So how can I invoke the axiom of choice? Does this mean that I can construct the law of excluded middle?

[Kevin Buzzard]

Lean's type theory is equivalent to ZFC + infinitely many universes. The axiom of choice and the law of the excluded middle are proved in core Lean. The axiom of choice is docs#classical.axiom_of_choice and LEM is docs#classical.em . You can search for what is in the library using the API documentation and this gives you links to the source code where you can read the proofs.

[Kevin Buzzard]

And yes, LEM is proved via Dionescu's argument.

[Ignat Insarov]

I see an axiom here.

axiom choice {α : Sort u} : nonempty α → α

The presence of this axiom makes me suspect that the law of excluded middle may require this axiom and may be non-provable without it.

[Johan Commelin]

Sure, it's an axiom. Just like in ZFC.

[Ignat Insarov]

The paper Sets in Types, Types in Sets by Benjamin Werner, referred to by the Mario paper above, says that the axiom of choice has to be assumed.

[Kevin Buzzard]

And making it an axiom is indeed assuming it.

[Ignat Insarov]

Yes, what I mean to say is that it is not inherent to the Lean verification engine.

[Kevin Buzzard]

The statement "Lean's type theory is equivalent to ZFC + infinitely many universes" means "core Lean plus the axioms defined in core Lean, is equivalent to ..."

[Kevin Buzzard]

There are three axioms, each explained in the last chapter of #tpil

[Johan Commelin]

In some sense "what to read to learn logic" suggests that there is only 1 logic. (Un)fortunately, there a dozens.

[Johan Commelin]

See https://en.wikipedia.org/wiki/Brouwer%E2%80%93Hilbert_controversy if you like fighting mathematicians.

[Ignat Insarov]

I know. I have been skimming some introductions to substructural logics and so on.

[Ignat Insarov]

Now I want to put my house in order and understand what specific logic I have my proofs done with.

[Ignat Insarov]

My understanding so far is that:

Classical ← Constructive → Intuitionistic

For example, in Classical there are discontinuous functions ℝ → ℝ, in Intuitionistic there are none, and Constructive does not care either way. Lean with the core libraries makes the choice to the left, but it seems that Lean without the core libraries is in the middle, either by coincidence or by design.

[Johan Commelin]

@Ignat Insarov The mere presence of axiom doesn't imply that the whole library is classical. You can mix both things in one library.

[Ignat Insarov]

Whichever way it is, my problem is the lack of skill needed to appreciate all these flavours. For example, we see that Lean with the axiom of choice is equivalent to set theory with axiom of choice. Is Lean without said axiom equivalent to some other flavour of set theory? How do I even begin to investigate this question?

[Ignat Insarov]

None of my education so far prepared me to wrestle with questions of this kind.

[Johan Commelin]

Same here. But I personally don't really care.

[Patrick Massot]

Same here except that I really don't care.

[Reid Barton]

Ignat Insarov said:

Whichever way it is, my problem is the lack of skill needed to appreciate all these flavours. For example, we see that Lean with the axiom of choice is equivalent to set theory with axiom of choice. Is Lean without said axiom equivalent to some other flavour of set theory? How do I even begin to investigate this question?

I think we don't know much about this question. For example I don't think we even really know that core Lean doesn't prove LEM. Here under core Lean I'm including all the fancy parts like definitional proof irrelevance for Prop and large elimination rules.

But presumably the expectation would be that core Lean is comparable to a set theory that's formulated in a constructive first-order logic, such as CZF set theory.

[Reid Barton]

People who care about formalization in a specific constructive framework would presumably rather use a different proof assistant (e.g. Coq) whose relationship to that framework is better understood, so to some extent there's a chicken-and-egg problem

[Mario Carneiro]

That would be a cool result; unfortunately I don't know much about how to prove e.g. CZF doesn't prove LEM

[Lucas Teixeira]

In response to the original post, this book might be of interest:

https://www.amazon.com/Type-Theory-Formal-Proof-Introduction/dp/110703650X

I've read the first couple of chapters, and I really enjoy it. I find it remarkably clear (thus far).

[Mac]

Unlike some of the mathematicians here, I do care a lot about this stuff. (Maybe that comes from my primarily CS/Philosophy background?) However, I have not had a lot of formal training in the nitty gritty details of complex logic systems like Lean, so I cannot really provide good resources in that regard. My approach in the past has generally be to just roll-my-own by a building a logic from the ground up and seeing what I can prove (and looking up things I stumble upon them). I have learned a lot of what I know now from such explorations.

[Cody Roux]

Mario Carneiro said:

That would be a cool result; unfortunately I don't know much about how to prove e.g. CZF doesn't prove LEM

Realizability models!

But it's finicky.