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 systems

• Definition of wBIH and sBIH
• Enumeration of the language
• wBIH and sBIH capture finitary logics
• Extensional interactions between WBIH and sBIH
• Proof-theoretic properties of wBIH
• Proof-theoretic properties of sBIH
• Preliminaries to the Lindenbaum lemma
• Lindenbaum lemma
• Export file

Kripke semantics

• Definition of the Kripke semantics
• Bisimulation
• Soundness results
• Completeness of wBIH
• Completeness of sBIH
• Consequences of soundness and completeness results
• Export file

Abstract algebraic logic

• Definition of bi-Heyting algebras
• Definitions of algebraic semantics
• Soundness results
• Implicativity of sBIL
• Algebraic completeness for sBIL
• Algebraizability of sBIL with respect to bi-Heyting algebras
• wBIL is not algebraizable
• wBIL is finitely equivalential
• wBIL has no algebraic semantics with respect to bi-Heyting algebras
• wBIL is the truth degree preserving logic of bi-Heyting algebras