General

• Existential quantifiers in Type
• General tools
• General purpose tools in Type

Syntax

• Definition of the syntax
• Technical results on lists of formulas

Generalised Hilbert system FOBIH

• Definition of FOBIH
• FOBIH captures a logic
• Proof-theoretic properties of FOBIH
• Standard Lindenbaum lemma
• Constant domain Lindenbaum lemma
• Dual constant domain Lindenbaum lemma

Kripke semantics

Soundness

Completeness

First-order constant domain intuitionistic logic

• Syntax
• Technical results on lists of formulas
• Definition of FOCDIH
• FOCDIH captures a logic
• Proof-theoretic properties of FOCDIH
• Standard Lindenbaum lemma
• Constant domain Lindenbaum lemma
• Kripke semantics
• Soundness
• Completeness
• Conservativity of FOBIL over FOCDIL