The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Sunday, November 29, 2015 02:40:11 AM Emilio Jesús Gallego Arias wrote:
> Hello Jeffrey,
> 
> "Terrell, Jeffrey" 
> <jeffrey.terrell AT kcl.ac.uk>
>  writes:
> > Does anyone know of a Coq proof that propositional logic is decidable?
> 
> If you are looking for a more compact solution you could just build an
> interpretation from propositional formulae to bool; decidability then
> follows.
> 
> A quick example building such a function is attached below.

I read the question as being about proving the decidability of whether some 
context proves a certain proposition in some formal system representing 
intuitionstic propositional logic - or equivalently, the decidability of 
whether some given formula is a theorem (axiom-free) in the system.  So, for 
example, along the lines of what the Coq "tauto" tactic does based on the 
LJT* 
system.

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.
-- 
Daniel Schepler