# Why is Coq consistent? What is the intended semantics?

**URL:** <https://discourse.rocq-prover.org/t/why-is-coq-consistent-what-is-the-intended-semantics/347>\
**Category:** Miscellaneous\
**Tags:** faq\
**Created:** [July 3, 2019, 8:07am UTC](https://discourse.rocq-prover.org/t/why-is-coq-consistent-what-is-the-intended-semantics/347 "2019-07-03T08:07:31Z")\
**Posts on this page:** 1\
**Showing post:** 5

<div class="post-metadata">

**Author:** ![palmskog](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/palmskog/32/38_2.png) [@palmskog](https://discourse.rocq-prover.org/u/palmskog)\
**Post date:** [July 8, 2019, 4:09am UTC](https://discourse.rocq-prover.org/t/why-is-coq-consistent-what-is-the-intended-semantics/347/5 "2019-07-08T04:09:06Z")

</div>

I think it’s worth pointing out that while the kernel discussion in [this post](https://discourse.rocq-prover.org/t/understanding-the-coq-kernel/293) is in some sense distinct from the topic here, it also overlaps quite a lot.

---

_[View the full topic](https://discourse.rocq-prover.org/t/why-is-coq-consistent-what-is-the-intended-semantics/347)._