 # What axioms are built-in?

Hi, noob’s question: is there a list somewhere of what axioms are built-in into Coq?

Coq is built on type theory and the idea of Curry-Howard’s isomorphism: A proof is a function whose type (assuming it exists) is a valid theorem statement. Since there are no predefined functions, there are no built-in axioms in Coq. For example, modus ponens is just a consequence of function composition; it does not need to be axiomatized in any way.

So, perhaps the question should be: Which of the traditional axioms can be proved in Coq? I don’t know if there exists a comprehensive list.

Oh, interesting. I was actually wondering how exactly Coq was proving any `Prop` from `False`. My first guess was that this was some sort of an axiom.

The logic of Coq allows for inductive types. `False` is defined as an inductive type with zero constructors. So, a pattern-matching construction on a value of that type has no branches and thus has any type.

``````Inductive False := (* nothing *) .
Definition exfalso (P : Prop) (f : False) : P := match f with (* nothing *) end.
About exfalso. (* exfalso : forall P : Prop, False -> P *)
``````

… so would I be right to guess that the difference between `Prop` and `Set` is purely down to how the types in standard library are written? E.g. in that certain constructors take `Prop` as argument(s) but not `Set` or `Type`?

They have entirely different properties. The types of `Prop` do not carry any meaningful information, so they can be self-referential:

``````Inductive foo: Prop := Foo: forall X:Prop, X -> foo.
``````

Types of `Set`, however, are actual datatypes that carry information, so they are much more restricted:

``````Inductive bar: Set := Bar: forall X:Set, X -> bar.
(* Error: Large non-propositional inductive types must be in Type. *)
``````

Conversely, you can compute using types from `Set` but not from `Prop`:

``````Definition bar {A:Prop} (x: A + not A): bool :=
match x with inl _ => true | _ => false end.

Definition foo {A:Prop} (x: A \/ not A): bool :=
match x with or_introl _ => true | _ => false end.
(* Error: Incorrect elimination of "x" in the inductive type "or":
the return type has sort "Set" while it should be "SProp" or "Prop".
Elimination of an inductive object of sort Prop is not allowed on a predicate in sort Set
because proofs can be eliminated only to build proofs. *)
``````

So, as a rule of thumb, types from `Prop` are used to state theorems, while types from `Set` are used to do some actual programming.

2 Likes

Another way to understand your question is “what induction principle is needed to prove Coq consistent?”

Logic of Coq, as presented, has no axioms, it is just a so-called “dependently type lambda calculus” with some extensions such as inductive types: usual name is CIC (Calculus of Inductive Constructions")

Leaving implementation problems aside, soundness of this calculus relies on a “proof of normalization”, basically you want to ensure that “bad” types are not inhabited, and from that you conclude that Coq cannot prove `A /\ not A` [simplifying a lot]

By Gödel we know that Coq cannot prove normalization itself, so we need to use a “stronger” principle at some point; this point gets quite technical quickly, but could informally assume that working in Coq you are assuming axioms similar to the ones in ZF set-theory for example.

A few pointers that you may find helpful: