The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Tue, Mar 26, 2013 at 2:30 AM,  
<r.h.huijben AT student.tue.nl>
 wrote:
> I'm looking for a way to prove that something is not a tautology, but not
> necesarily a contradiction either. I have the following model:
[snip]
> This allows me to make terms like (A Person Walk). These terms represent 
> real
> world propositions and I would like to be able to prove them when they are
> true but also be able to show that they are unproveable when they are. For
> example the term ((A Woman Walk) ’Implies’ A Bird Fly) is clearly nonsense,
> but currently I am unable to prove that.
>
> I have tried a number of solutions (converting either IsTrue or Implies to
> inductive types, reconstructing everything into fixpoint operators etc.) but
> those only seemed to move the problem and I am kind of stuck here, so could
> you help me with this?

I'd approach this using a model type: something like

Class WorldModel : Type := {
  things : Set;
  truth_vals : Set;
  Woman Man Human ... : things -> truth_vals;
  ...
}.

(* Notation for model satisfying a condition. *)
Notation "M ⊧ P" := ((fun _:WorldModel => IsTrue P) M).

(* Notation for a condition being a tautology. *)
Notation "τ P" := (forall M:WorldModel, M ⊧ P).

Definition my_counterexample : WorldModel := {|
  things := unit;
  truth_vals := bool;
  Woman := fun _:unit => true;
  Bird := fun _:unit => false;
  Walk := fun _:unit => true
  Fly := fun _:unit => false
  ...
|}.
Proof.
(* prove axioms of the model here *)
Defined.

Lemma not_tauto : ~ τ (A Woman Walk 'Implies' A Bird Fly).
Proof.
intro is_tauto.
pose proof (is_tauto my_counterexample).  (* my_counterexample ⊧ A
Woman Runs ... *)
(* derive a contradiction *)
Qed.
-- 
Daniel Schepler