Terms vs Theorem vs Formula in Coq?

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.

1 Like