Lindenbaum-Tarski algebra

agda / cubical

An experimental library for Cubical Agda

https://agda.github.io/cubical/Cubical.README.html

Other

447 stars 136 forks source link

Lindenbaum-Tarski algebra #1012

Closed croos90 closed 1 year ago

croos90 commented 1 year ago

Lindenbaum-Tarski algebra of propostional logic.

Definition of provability
Properties of propositional logic
Biprovability relation
Definition of Lindenbaum-Tarski algebra
Lindenbaum-Tarski algebra is complemented distributive lattice, hence Boolean

felixwellen commented 1 year ago

I think it's fine like it is now (agreeing that a comment explaining the file contents would be great).

We can think about splitting off the logic-parts in our future refactoring that finally puts the logic related things in the library at a place where they are not completely unexpected ;-)