Stream: Coq workshop 2020

Topic: Order of logic

Andreas Röhler (Jul 05 2020 at 10:15):

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

Emilio Jesús Gallego Arias (Jul 06 2020 at 09:05):

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

Karl Palmskog (Jul 06 2020 at 09:07):

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

Hugo Herbelin (Jul 06 2020 at 19:33):

@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.

Andreas Röhler (Jul 07 2020 at 14:47):

Thanks all responding.

Last updated: Apr 20 2024 at 06:02 UTC