An exploration of propositional logic and propositional calculus in Coq. In particular we explore the soundness and completeness results of the calculus with respect to the Boolean-valued semantics:
Theorem l_sound : forall S A, S |- A -> S ⊨ A.
Theorem l_complete : forall S A, S ⊨ A -> S |- A.
Currently no classical axioms are used, thus the proofs are fully constructive.
The repository contains the following files:
proplogic.v
- my developmentsproplogicST.v
- developments due to Steven Tschantzprop_equiv.v
- equivalence of the developments and examples of transporting results between them
A formalization of analogous results for first-order logic is planned.
$ make -f CoqMakefile