Project Page Index Table of Contents
  • Axiomatic Assumptions
    • Functional Extensionality
    • Propositional Extensionality
  • Preliminaries
    • Type Theory
    • Synthetic Computability Theory
    • First-Order Logic
      • Full Syntax
      • Full Syntax Operations & Properties
      • Fragment Syntax
      • Fragment Syntax Operations & Properties
      • Formula Enumeration
    • Natural Deduction
    • Constructive Analysis
  • Tarski Semantics
    • Generalized Theory Extension
    • Constructive Analysis of Completeness Theorems
      • Tarki Models
      • Standard Models
      • Exploding Models
      • Minimal Models
    • Extending the Completeness Results
  • Kripke Semantics
    • Kripke Models
    • Normal Sequent Calculus
    • Constructive Analysis of Completeness Theorems
      • Exploding and Minimal Models
      • Standard Models
  • Dialogue Semantics
    • Generalized Intuitionistic E-Completeness
      • Generalized Intuitionistic E-Dialogues
      • Dialogical Sequent Calculus
      • Soundness and Completeness
    • Generalized Intuitionistic D-Completeness
      • Generalized Intuitionistic D-Dialogues
      • Soundness and Completeness
      • Translating LJD into S-Vaidity
    • Full Intuitionistic First-Order Completeness
      • Full Intuitionistic Sequent Calculus
      • Translating between LJT and LJD
      • Translating between LJ and LJD
Generated by coqdoc and improved with CoqdocJS