Project Page Index Table of Contents
  • Preliminaries by Autosubst
    • Axiomatic Assumptions
    • Basic definitions for substiutions
  • Preliminaries FOL*
    • Syntax of FOL*
    • Operations & Properties of FOL*
    • Natural Deduction for FOL*
  • Tarski Semantics
    • Generalized Theory Extension
    • Enumeration of formulas and ND
    • Definition of Tarski Semantics
    • Soundness
    • Consistency
    • Completeness
    • Constructive Analysis
  • Kripke Semantics
    • Kripke Models
    • Soundness
    • Normal Sequent Calculus
    • Constructive Analysis of Completeness Theorems
      • Exploding and Minimal Models
      • Standard Models
      • MP is required
  • On Markov's Principle
    • BPCP reduces to ND
    • BPCP reduces to classical ND
    • Signature Extension
    • ND is L-enumerable
    • Connections to MPL
  • Preliminaries FOL
    • Syntax of FOL
    • Operations & Properties of FOL
    • Natural Deduction for FOL
    • Intuitionistic Sequent Calculus
  • Algebraic Semantics
    • Heyting Algebras
    • MacNeille Completion
    • Soundness
    • Lindenbaum Algebra
    • Completeness
    • Boolean algebras
  • Dialogue Semantics
    • Soundness and completeness for E-Dialoagues
    • Translating between LJT and LJD
    • Translating between LJ and LJD
Generated by coqdoc and improved with CoqdocJS