The Coq mailing list

[gallego AT cri.ensmp.fr (Emilio Jesús Gallego Arias)]

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.

Best regards,
Emilio

Require Import ssreflect ssrfun ssrbool eqtype ssrnat fintype finfun.

Section PL.

Variable (n : nat).

Inductive PropF : Type :=
| Var of 'I_n
| Bot
| Conj of PropF & PropF
| Disj of PropF & PropF
| Impl of PropF & PropF
.

Definition inter (v : {ffun 'I_n -> bool}) :=
  fix i p := match p with
             | Var i      => v i
             | Bot        => false
             | Conj p1 p2 => i p1 &&  i p2
             | Disj p1 p2 => i p1 ||  i p2
             | Impl p1 p2 => i p1 ==> i p2
             end.

Definition models (p : PropF) := [forall v, inter v p].

End PL.

About models.
(* models : forall n : nat, PropF n -> bool *)