Coq 中的逻辑系统。

We have seen many examples of factual claims (_propositions_) and ways of presenting evidence of their truth (_proofs_). In particular, we have worked extensively with _equality propositions_ ([e1 = e2]), implications ([P -> Q]) and quantified propositions ([ forall x, P]). In this chapter, we will see how Coq can be used to carry out other familiar forms of logical reasoning.

Typed language: every sensible expression in Coq’s world has an associated type.

Proposition: All syntactically well-formed propositions have type [Prop] in Coq, regardless of whether they are true.

First-class entities: propositions can be manipulated in all the same ways as any of the other things in Coq’s world.


Definition is_three (n : nat) : Prop :=
n = 3.
Check is_three : nat -> Prop.

Logical Connectives

Conjunction and …

Coq vs. Set Theory

见单独文章 Coq vs. Set Theory