Defining a predicate without specifying its truth condition in Coq

Question

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.

Inductive being : Type :=
| b : nat -> being. 

Inductive human : being -> Prop :=
| h : forall ( b : being ), human b.

Inductive perfect : being -> Prop :=
| p : forall ( b : being ), perfect b.

(being is indexed with numbers to ensure there are multiple distinct beings.)

With this definition, the statement can be expressed as

Lemma humans_are_imperfect : 
forall ( b : being ), human b -> ~ perfect b.
Admitted.

The problem with this approach is that it allows proofs of nonsense, such as

Lemma humans_are_perfect : 
forall ( b : being ), human b -> perfect b.
intros b H. apply ( p b ). Qed.

Obviously, there is a problem with the definition of human and perfect, because it indescriminately takes any being and asserts its humanity and perfection. What is needed is a definition of human and perfect that only specifies their types, while remaining ambiguous about which beings they apply to.

This problem could be avoided altogether if the truth condition of perfect was built into its definition, e.g. the constructor only took nonhuman beings 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.

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.

Arthur Azevedo De Amorim Arthur Azevedo De Amorim · Accepted Answer · 2014-10-25T22:44:19

What you want to do can be perfectly expressed in Coq using just higher-order predicate logic, without the need for inductive definitions. You can work with your theorems just by postulating the existence of a type being, predicates human and perfect, and inference rules relating those.

Section SomePhilosophy.

Variable being : Type.
Variable human perfect : being -> Prop.

Hypothesis human_not_perfect : forall b, human b -> ~ perfect b.

(* ... some theorems about the above notions ... *)

End SomePhilosophy.

After closing the section, all of your definitions will become parametric with respect to choices of being, human and perfect that satisfy your hypothesis. In your original approach, you constrained your theory by fixing upfront what being is, since you gave its definition. Here, being can by anything.

Defining a predicate without specifying its truth condition in Coq

1 Answers