Logic

[fredrik-bakke]

Some logic formalizations extracted from #1206.

Summary

• Create logic namespace
• Double negation elimination
  • Double negation stable propositions
  • Maps with double negation elimination and closure properties
  • Double negation stable embeddings and closure properties
• De Morgan's law
  • De Morgan types and De Morgan propositions
  • De Morgan maps and closure properties
  • De Morgan embeddings and closure properties
• Markov's principle and a strong version for finite types
• Some additional closure properties for decidable maps, decidable embeddings, decidable propositions...
• Diaconescu's theorem
  • The suspension of a proposition is a set

Initial work for #1069

[fredrik-bakke]

This PR is currently blocked on #1168.

[fredrik-bakke]

Turns out it's not directly blocked, there's just an overlap.

[EgbertRijke]

Sorry that this PR was left open for so long. I'll review it tomorrow or in the coming days. Could you get it up to date, if there is anything you wanted to change?

[fredrik-bakke]

Sorry that this PR was left open for so long. I'll review it tomorrow or in the coming days. Could you get it up to date, if there is anything you wanted to change?

I don't believe I want to add anything more to this PR, so review away. Thanks for taking on this huge PR!

[fredrik-bakke]

I just realized I want to factor "Markovian types" into a separate file. I will do so quickly. The rest can be reviewed in the meantime.

[EgbertRijke]

This is a very cool pull request!

[fredrik-bakke]

By the way @EgbertRijke, do you have an opinion on whether Markov's principle should be placed in foundation or the different principles of omniscience should be placed in logic?

[fredrik-bakke]

Would you want decidable types to be moved to the logic namespace? (not in this PR)

[fredrik-bakke]

I've addressed all of your comments now.

Would you want decidable types to be moved to the logic namespace? (not in this PR)

This question is relevant for where I should place the new module uniformly-decidable-type-families

[EgbertRijke]

By the way @EgbertRijke, do you have an opinion on whether Markov's principle should be placed in foundation or the different principles of omniscience should be placed in logic?

It would probably be fair to place them all in logic.

[EgbertRijke]

Would you want decidable types to be moved to the logic namespace? (not in this PR)

Hm.. that's a good question. I'm not sure where to draw the line between type theory and logic. The most obvious way to do it is that generic stuff about propositions should go in logic.

On the other hand, the Curry-Howard interpretation of logic into type theory also feels like logic, but perhaps I'd feel more comfortable about having the logic namespace mostly for proposition-level mathematics.

[EgbertRijke]

This pull request is a great advance for the library! Well done Fredrik!