I want to triple check, but those 3 are the same in Coq, right?
Somehow I had the impression that is not true in HOL Light and wanted to double-check if at least in Coq that was not true.
I am also curious to know in what other Interactive Theorem Provers (ITPs) is there a distinction between terms/formulas vs Theorems. e.g. in Lean.
Indeed, a single syntax plays many roles in Coq: types and propositions, programs and proofs.
But be careful with words. “They are the same” is a vague statement: the same language can be used to say different things. Proving a proposition and implementing a program are still conceptually different activities (though the line between them can blur or even disappear at times). To make an analogy, we can give orders or recite poetry in English, but are orders and poems the same thing because they’re in the same language?
More technically, the words “term”, “theorem”, “formula” don’t have absolute meanings, and in fact even in Coq, they can reasonably be given quite different meanings. One should be precise about what they mean, especially when comparing concepts across languages.
In logic, a conventional definition might be as follows: a term is a bunch of symbols (most likely following some syntax), a formula is a term to which we can assign a truth value, and a theorem is a true formula. (There may be variations depending on technical details.)
In Coq, one could similarly say that a term is a bunch of symbols that follows the syntax of Gallina, a formula (or proposition, or type) is a term of type Prop (or sometimes Type), so a formula could be inhabited or not, and a theorem is an inhabited formula.
But in other theorem provers like, HOL Light, the distinction between a theorem and a term is rigorous. As I understand it, a term can only be of type theorem if it has actually been the output of a set of inference rules or tactics, but what I thought was weird is that Coq does not actually make this distinction explicit for some reason. Do you know why?
Wrote a related question: Why doesn't Coq have a theorem Type like HOL Light?
In Coq too; very little is non-rigorous about theorem provers. It’s just a different rigorous distinction.
That’s a completely formal fact. T is a theorem if there is a closed term t such that t : T.
As was already answered in the question you linked to, HOL Light has a theorem type because it follows the LCF approach where you only build correct theorems by using safe primitives. The approach followed by Coq is that the kernel will type check any term you give it, and will reject any ill-typed term. Thus, you can have unsafe procedures generating proof terms, and soundness is ensured by the kernel being called to close a proof.