title: Defining a predicate without specifying its truth condition in Coq
body: <p>I'm trying to use Coq for some simple kinds of philosophical predicate logic. Suppose, for instance, that I wanted to express the statement "if a being is human, it is not perfect" in Coq. I will first have to define what the terms 'being', 'human', and 'perfect' are. The natural approach, it seems, is to define the first as a type, and others as unary predicates of that type.</p>
  
  <pre><code>Inductive being : Type :=
  | b : nat -&gt; being. 
  
  Inductive human : being -&gt; Prop :=
  | h : forall ( b : being ), human b.
  
  Inductive perfect : being -&gt; Prop :=
  | p : forall ( b : being ), perfect b.
  </code></pre>
  
  <p>(<code>being</code> is indexed with numbers to ensure there are multiple distinct beings.)</p>
  
  <p>With this definition, the statement can be expressed as</p>
  
  <pre><code>Lemma humans_are_imperfect : 
  forall ( b : being ), human b -&gt; ~ perfect b.
  Admitted. 
  </code></pre>
  
  <p>The problem with this approach is that it allows proofs of nonsense, such as</p>
  
  <pre><code>Lemma humans_are_perfect : 
  forall ( b : being ), human b -&gt; perfect b.
  intros b H. apply ( p b ). Qed.
  </code></pre>
  
  <p>Obviously, there is a problem with the definition of <code>human</code> and <code>perfect</code>, because it indescriminately takes any <code>being</code> and asserts its humanity and perfection. What is needed is a definition of <code>human</code> and <code>perfect</code> that only specifies their <em>types</em>, while remaining ambiguous about which <code>being</code>s they apply to.</p>
  
  <p>This problem could be avoided altogether if the truth condition of <code>perfect</code> was built into its definition, e.g. the constructor only took nonhuman <code>being</code>s as arguments. But supplying all information upfront like that is not always feasible in philosophical arguments. Very often you have to take some type or predicate as a given, and slowly build up its details with further premises.</p>
  
  <p>I have a feeling that what I'm trying to do does not fit very well into the inductive basis of Coq. Maybe I'm better off learning a logic programming language like Prolog, but hopefully I'm wrong.</p>