Project Page Index Table of Contents
  • Preliminaries
    • Lists
    • Tactics
    • Boolean propositions and decisions
    • Discrete types
    • Lists
  • Decidability and Enumerability
    • Closure of enumerable types
    • Enumerability of pairs of natural numbers
    • Discrete types are closed under ...
    • Enumerable types are closed under ...
    • Enumerable predicates are closed under ...
  • Many-One Reductions
  • Post's Theorem and Markov's Principle
  • Post Correspondence Problem
    • Traditional Definition
    • Inductive Definition
    • Binary PCP
    • Enumerability
  • Infinite Data Types
    • Definition of infinite and generating types
    • Infinite data types are generating
    • Generating data types are infinite
    • Generating data types are in bijection to nat
    • Example
  • First-Order Logic
    • Syntax
    • Enumerability
  • Tarski Semantics
    • Variables and Substitutions
    • Interpretations
  • Natural Deduction
    • Definition
    • Soundness
    • Generalised Induction
    • Enumerability
  • Kripke Semantics
    • Kripke Models
    • Connection to Tarski Semantics
    • Soundness
  • FOL Reductions
    • Encodings
    • Standard Model
    • Stability
    • Validity
    • Provability
    • Satisfiability
    • Corollaries
    • Non-Standard Model
  • Intuitionistic FOL
    • Reductions
    • Corollaries
  • Classical Natural Deduction
    • Double Negation Translation
    • Reduction
    • Corollaries
  • Weakening
Generated by coqdoc and improved with CoqdocJS