The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

> (It'd be valuable to me to have someone critique my code.

I think having more code critique on coq-club is something that everyone would benefit from. (Did you use bullets?)

I would encourage you to start a new thread focused on the critique of your development.

On Sun, Nov 29, 2015 at 9:27 AM, Julian Michael <julianjohnmichael AT gmail.com> wrote:

 

I've recently played around with some development along those lines - defining
a natural deduction style proof system in Coq, and proving that it results in
a free Heyting algebra.  I haven't defined a decision procedure for it, much
less proved the completeness - which essentially reduces to cut elimination,
or perhaps as another way of putting it the possibility of reducing a lambda
_expression_ representation of a proof to a normal form.  Unfortunately, it's on
another machine I wouldn't be able to access until Monday, if you'd be
interested in seeing what I have so far.

I assumed the original question was about classical propositional logic. On a related note, I only recently started learning Coq and as an exercise I spent a bit of time trying to formalize the soundness and completeness of a natural-deduction style system with respect to 2-valued truth assignments, in the style of the proof by Kalmar (1935). Never quite finished, but it's mostly there if anyone's interested in taking a look. (It'd be valuable to me to have someone critique my code.) If such a proof is already around somewhere, though, let me know.