How can I proof (or better: convincingly argument) that my COQ theory is consistent?
Let's make the assumption that the COQ system and the standard library is consistent.
I know that a general formal proof of consistency is not possible due to the Gödelian incompleteness theorem.
But, are there some methods or rules of thumb how to argument that the theory is consistent?
To be a bit more concrete: Is it true that my theory is automatically consistent, if I only use inductive data types and no explicit axiomatic propositions?
3
votes
Please stop posting those f***ing "this is a homework" comments. NO, its not. I studied mathematics 20 years ago. And my question surely doesn't sound like homework stuff. If you can answer it then post the answer. If you can't, keep quiet!
– Cryptostasis
Well, I do not know which kind of theory you are thinking of but, at least for logics, one way to show consistency is to use a (structural) proof theoretical argument like cut elimination.
– Rodrigo Ribeiro
Considering the usage of proof assistants, like Coq, to show consistency of a theory, we need to consider: - The theorem prover logic is sound (that is the case for the calculus of (co)inductive constructions). - The theorem prover implementation is correct. That is a hard thing to achieve. I do not know if Coq's type checker is fully verified. Barras have proved a type-checker for Coq in Coq. But, I do not know if this implementation is used in Coq's current version.
– Rodrigo Ribeiro
I am not concerned about the consistency of COQ itself. I assume that it is consistent. I am concerned about the consistency of my theory, which I formulated in COQ. How can I convince someone that I did not introduce contradictory axioms?
– Cryptostasis
Can you formulate your theory in a sequent calculus form? If your answer is "yes", then you just need to prove cut elimination for your calculus. Consistency for logical theories is a corollary of cut elimination.
– Rodrigo Ribeiro
1 Answers
4
votes
The whole point of Coq is that you can trust that your definitions and proofs are logically sound if they are accepted by the system. There are two caveats, however:
You must trust that the system's underlying logic is sound, and that it is implemented correctly.
You must not extend the basic theory with arbitrary axioms, or enable unsafe options (e.g.
-type-in-type).
This last point deserves some explanation. Definitions and proofs that are stated using commands such as Fixpoint, Definition, or Inductive fall within Coq's basic theory, and thus are automatically consistent. This is why Coq places some restrictions these commands, such as only allowing for certain kinds of recursive functions. On the other hand, if you ask Coq to accept arbitrary propositions using the Axiom command or similar ones, then you may end up with an inconsistent development.
Some axioms, such as the excluded middle and functional extensionality, are relatively well-studied and well-understood, and thus not too dangerous if assumed. As a rule of thumb, you can trust axioms that are declared in the standard library. You should nevertheless be careful: for instance, some standard axioms are incompatible with the -impredicative-set option (see here).
If you want to ensure that your development does not rely on special axioms, you can use the Print Assumptions command (see here) to list all axioms that are used in your results.
