Project Page
Index
Table of Contents
Preliminaries by Autosubst
Axiomatic Assumptions
Basic definitions for substiutions
Preliminaries FOL*
Syntax of FOL*
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
De Morgan Translation
Constructive Analysis
Compactness and Weak König's Lemma
Theorems 15 and 42
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
Definition of Tarski Semantics
Algebraic Semantics
Heyting Algebras
MacNeille Completion
Soundness
Lindenbaum Algebra
Completeness
Boolean algebras
Generalised Lindenbaum Algebras
Completeness
Completeness for Boolean algebras
Dialogue Semantics
Soundness and completeness for E-Dialoagues
Translating between LJT and LJD
Translating between LJ and LJD
The well-foundedness of the induction relation
Translating LJD into S-Validity