Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Lecture

Coq: Introduction

Description

This lecture introduces Coq, a formal proof management system. The lecture covers the basics of Coq, including defining propositions, proving theorems, and using tactics. It also explores concepts like disjunction, conjunction, and star in Coq.

Official source

Ontological neighbourhood

Logic

Classical logic: First-order logic

Related concepts (32)

Theorem

In mathematics, a theorem is a statement that has been proved, or can be proved. The proof of a theorem is a logical argument that uses the inference rules of a deductive system to establish that the theorem is a logical consequence of the axioms and previously proved theorems. In mainstream mathematics, the axioms and the inference rules are commonly left implicit, and, in this case, they are almost always those of Zermelo–Fraenkel set theory with the axiom of choice (ZFC), or of a less powerful theory, such as Peano arithmetic.

Mathematical proof

A mathematical proof is a deductive argument for a mathematical statement, showing that the stated assumptions logically guarantee the conclusion. The argument may use other previously established statements, such as theorems; but every proof can, in principle, be constructed using only certain basic or original assumptions known as axioms, along with the accepted rules of inference. Proofs are examples of exhaustive deductive reasoning which establish logical certainty, to be distinguished from empirical arguments or non-exhaustive inductive reasoning which establish "reasonable expectation".

Gödel's incompleteness theorems

Gödel's incompleteness theorems are two theorems of mathematical logic that are concerned with the limits of in formal axiomatic theories. These results, published by Kurt Gödel in 1931, are important both in mathematical logic and in the philosophy of mathematics. The theorems are widely, but not universally, interpreted as showing that Hilbert's program to find a complete and consistent set of axioms for all mathematics is impossible. The first incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an effective procedure (i.

Logical disjunction

In logic, disjunction, also known as logical disjunction or logical or or logical addition or inclusive disjunction , is a logical connective typically notated as and read aloud as "or". For instance, the English language sentence "it is sunny or it is warm" can be represented in logic using the disjunctive formula , assuming that abbreviates "it is sunny" and abbreviates "it is warm". In classical logic, disjunction is given a truth functional semantics according to which a formula is true unless both and are false.

Universal quantification

In mathematical logic, a universal quantification is a type of quantifier, a logical constant which is interpreted as "given any", "for all", or "for any". It expresses that a predicate can be satisfied by every member of a domain of discourse. In other words, it is the predication of a property or relation to every member of the domain. It asserts that a predicate within the scope of a universal quantifier is true of every value of a predicate variable.

Related lectures (35)

Concept of Proof in Mathematics

Delves into the concept of proof in mathematics, emphasizing the importance of evidence and logical reasoning.

Proofs: Logic, Mathematics & Algorithms

Explores proof concepts, techniques, and applications in logic, mathematics, and algorithms.

Coq Workshop: Introduction to Interactive Theorem Proving

Introduces Coq, an interactive theorem assistant based on the Curry-Howard isomorphism.

Coq: Overview

Introduces Coq and focuses on proving the theorem and_comm step by step.

Propositional Logic: Translations and Equivalences