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. B
    Benjamin Werner <>
  3. H
    Hugo Herbelin <>
  4. T
    Thierry Coquand <>

Maintainers

  1. M
    matej.kosik@inria.fr

Sources

v8.5.0.tar.gz
md5=09cae5a778b3cee470f9dc71b5baface

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: 07 Jun 2016

Dependencies (2)

  1. coq >= "8.5" & < "8.6~"
  2. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None