package coq-paradoxes

  1. Overview
  2. No Docs
Paradoxes in Set Theory and Type Theory

Install

Dune Dependency

github.com Edit opam file Versions (6)

Authors

  1. B
    Bruno Barras
  2. T
    Thierry Coquand
  3. H
    Hugo Herbelin
  4. B
    Benjamin Werner

Maintainers

  1. H
    Hugo.Herbelin@inria.fr

Sources

v8.9.0.tar.gz
md5=d60308dcf8e2dfe8e8880b454203e9f3

Description

A formalisation of Burali-Forti paradox in system U (the existence of an ordinal of ordinals is inconsistent), of Diaconescu paradox (axiom of choice implies excluded-middle), of Reynolds paradox (there is no set-theoretic model of system F) and Hurkens paradox in system U (adapted by H. Geuvers to show the inconsistency of Excluded-Middle in impredicative-Set Calculus of Inductive Constructions).

Tags

keyword: Reynolds paradox keyword: Burali-Forti paradox keyword: Diaconescu paradox keyword: set theory keyword: system U keyword: inconsistency keyword: Hurkens paradox category: Mathematics/Logic/Foundations

Published: 08 Dec 2019

Dependencies (2)

  1. coq >= "8.9" & < "8.10~"
  2. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None