Inversion of an axiom is bad

Using Coq
#1

I stumbled on the following “proof” of False:

Inductive Comb: Set :=
| K : Comb
| App : Comb → Comb → Comb .
Axiom k_eq : forall y z, App (App K y) z = y.
Lemma don’t_invert_axioms: False.
Proof.
assert(k_instance: App (App K K) K = K) by apply k_eq;
inversion k_instance.
Qed.

The problem is that the equation K KK = K follows from the axiom but its inversion has no solutions. Where can I read about this? How can I protect my proofs from this?

#2

It does not have anything to do with inversion. It is just that that your axiom is plain inconsistent. The only sure way to protect your proofs from inconsistent axioms is 1. either do not use axioms 2. exhibit a model of Coq in which your axioms hold. Needless to say, 2 is an incredibly hard task, which makes 1 the only feasible solution in practice.

#3

Thanks, Guillaume, for the prompt reply. I now understand that in the powerful logic of Coq (the Calculus of Inductive Constructions?) my axiom is inconsistent. However, the axiom k_eq is taken from combinatory logic, which is consistent, in the sense that there are equations which cannot be proved; one cannot prove S=K from the equations
Kxy = x
and
Sxyz = (xz)(yz) .
The issue is that Coq introduces stronger logical principles.

Part II of my book is in the style you suggest: all theorems in the book are there proved without any axioms, only rewriting. However, this is heavy for most readers, so Part I is for readers who understand little more than equational reasoning. Indeed, most proofs use a single tactic, that does no more than apply the axioms. At this moment, it seems that all of these proofs written in Coq are “informal” as they use an “inconsistent” axiom even though I am not using the stronger logical principles that expose the inconsistency. Is there a fragment of Coq (or a different proof assistant) in which the existing proofs become formal? In which consistency is restored?

Yours,
Barry

#4

There are lots of ways. It depends what you want to do. Here are a few ways (this is not exhaustive):

  1. Shallow embedding:
Definition K {T} (x y: T) := x.
Definition S {T U V} (x:_->_->V) (y:_->U) (z: T) := (x z) (y z).
  1. Full axiomatic:
Axiom Comb: Set.
Axiom K : Comb.
Axiom S : Comb.
Axiom App : Comb -> Comb -> Comb.
Axiom K_eq : forall x y, App (App K x) y = x.
Axiom S_eq : forall x y z, App (App (App S x) y) z = App (App x z) (App y z).
  1. Equivalence relation:
Inductive Comb: Set :=
| K : Comb
| S : Comb
| App : Comb -> Comb -> Comb.

Inductive eq : Comb -> Comb -> Prop :=
| k_eq: forall x y, eq (App (App K x) y) x
| s_eq: forall x y z, eq (App (App (App S x) y) z) (App (App x z) (App y z)).
1 Like
#5

Thanks, Guillaume. I will explore these in the coming days. Yours, Barry

#6

Let me add to @silene’s answer — what’s inconsistent is not the original axiom, but formalizing it by postulating unprovable equalities between constructors of inductive types — that’s (almost?) always inconsistent.*

*Ignoring advanced tricks such as private inductives, which it doesn’t seem productive to discuss here.

1 Like
#7

Hi Guillaume and Blaisorblade,

I seem to have a solution derived from your comments. No doubt it will be familiar to experts but let me put it on the record.

  1. The inductive type declaration of Comb_Ind supports lightweight function definitions but heavyweight equations.
  2. The fully axiomatic approach introduces a type Comb_Ax that supports lightweight equations but heavyweight function definitions.
  3. So I have built both types, with a function

quotient : Comb_Ind to Comb_Ax
and syntax “x===y” for “quotient x = quotient y”.

It seems that most of my one-line proofs (for tree calculus) are unchanged (I’ve rebuilt a few dozen now), while longer proofs require a little quotient manipulation that seems to be manageable.

Thanks again,
Barry