Syntax
Generalised Hilbert calculus CK with axioms
- Definition of CK with axioms (and various systems)
- CK with axioms captures a logic
- Properties of CK with axioms
- Enumeration of the language
- Lindenbaum lemma
- Lindenbaum lemma for pairs
- Proof-theoretic results via LEM
- Export file
Kripke semantics
- Definition of the Kripke semantics
- Correspondence results between axioms and frame properties
- Export file
Soundness
- General soundness result
- Soundness of CK
- Soundness of CK + Cd
- Soundness of CK + Idb
- Soundness of WK
- Soundness of CK + Ndb
- Soundness of CK + Cd + Idb
- Soundness of CK + Cd + Nd
- Soundness of CK + Cd + Ndb
- Soundness of CK + Idb + Nd
- Soundness of CK + Idb + Ndb
- Soundness of IK
- Soundness of CK + Cd + Idb + Ndb
Completeness via segments
- General completeness result via segments
- Completeness of CK
- Completeness of WK
- Completeness of CK + Ndb
Completeness via AB-segments
- General completeness result via AB-segments
- Completeness of CK + Cd
- Completeness of CK + Cd + Nd
- Completeness of CK + Cd + Ndb
Completeness via P-segments
- General completeness result via P-segments
- Completeness of CK + Idb
- Completeness of CK + Idb + Nd
- Completeness of CK + Idb + Ndb
Completeness via theories
- General completeness result via theories
- Completeness of CK + Cd + Idb
- Completeness of CK + Cd + Idb + Ndb
- Completeness of IK