Reading Coq is built on Constructive Logic, which is assumed to differ from classical logic. If yes, may you comment on the differences?

@Andreas Röhler that's a very general question, there's a myriad of resources to look into, depending on your background

for example, this might be one starting point: https://coq.discourse.group/t/why-is-coq-consistent-what-is-the-intended-semantics/347

@Andreas Röhler

Shortly:

- The logic of Coq is computational: if you have a close proof of the existence of a number which satisfies some property, you can "evaluate" the proof and it'll give you the witness of the existence.
- The logic of Coq does not assume excluded-middle (classical reasoning) by default. But you can postulate excluded-middle (by requiring some special file of the library,
`Classical.v`

) and Coq shall become a classical logic. - The (only) drawback is that classical logic breaks the property that a close proof of the existence of a number which satisfies some property provides the witness by evaluation. This is limitation from the computational point of view but this remains perfectly ok from the logical point of view.

Thanks all responding.

Last updated: Jun 17 2024 at 22:01 UTC