Start prove of completeness of Propositional Logic
Its soundness is almost proved. There are only some cases left.
Adequacy will take some effort still. The current proof is
nonconstructive, which is a shame (I wanted to use it as a SAT solver),
so I think I will prove it again constructively in the future.
Refactor and write sketch of get-CNF and get-DNF
Add DNF and CNF definitions, start new proof of Post's Theorem and refactor
The new proof is the one from the book, since I need that particular proof to
prove other theorems.
Begin proof of Post's Theorem
I define truth tables in order to prove Post's Theorem more easily but
get stuck proving the equivalence between tables and functions from
structures to booleans. Apart from that, Post's Theorem is proved, although
with a completely different proof than in the book.
Compile without K
First step to use Cubical Agda
Make some parameters explicit
Refactor Substitution definition
Previously we needed many implicit arguments to be passed around and
it was annoying. This way there are less. We could also add τ to the
tuple in Substitution and make it have only one argument.
Add substitutions
Added:
- Definition 3.7.1
- Example 3.7.2
Add until chapter 3.6
Lemma 3.6.1 is not fully proved, since it envolves a lot of boring
machinery, but it will eventually be proved.