General

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

Generalised Hilbert Calculus BIH

• Definition of BIH
• Lists of formulae
• BIH captures a logic
• Properties of BIH (1)
• Properties of BIH (2)
• Enumeration of the language and proofs

Lindenbaum lemma

• Preliminaries
• Constructive Lindenbaum lemma

Alternative Kripke semantics

Soundness

Quasi-completeness

Model existence

Completeness

Results for semi-decidable contexts