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: