Dirk Gently’s principle

Content created by Fredrik Bakke.

Created on 2025-08-14.
Last modified on 2025-08-14.

module logic.dirk-gentlys-principle where
Imports 
open import foundation.coproduct-types
open import foundation.decidable-types
open import foundation.disjunction
open import foundation.empty-types
open import foundation.function-types
open import foundation.law-of-excluded-middle
open import foundation.propositions
open import foundation.universe-levels

Idea

Dirk Gently’s principle is the logical axiom that the type of propositions is linearly ordered. In other words, for every pair of propositions P and Q, either P implies Q or Q implies P:

The proof strength of this principle lies strictly between the law of excluded middle and De Morgan’s law, Section 8.5 [Die18].

The name is based on the guiding principle of the protagonist of Douglas Adam’s novel Dirk Gently’s Holistic Detective Agency who believes in the “fundamental interconnectedness of all things.” [Die18]

Statement

instance-prop-Dirk-Gently-Principle :
  {l1 l2 : Level} → Prop l1 → Prop l2 → Prop (l1 ⊔ l2)
instance-prop-Dirk-Gently-Principle P Q = (P ⇒ Q) ∨ (Q ⇒ P)

instance-Dirk-Gently-Principle :
  {l1 l2 : Level} → Prop l1 → Prop l2 → UU (l1 ⊔ l2)
instance-Dirk-Gently-Principle P Q =
  type-Prop (instance-prop-Dirk-Gently-Principle P Q)

level-Dirk-Gently-Principle : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
level-Dirk-Gently-Principle l1 l2 =
  (P : Prop l1) (Q : Prop l2) → instance-Dirk-Gently-Principle P Q

Dirk-Gently-Principle : UUω
Dirk-Gently-Principle =
  {l1 l2 : Level} → level-Dirk-Gently-Principle l1 l2

Properties

The law of excluded middle implies Dirk Gently’s principle

instance-Dirk-Gently-Principle-LEM' :
  {l1 l2 : Level} (P : Prop l1) (Q : Prop l2) →
  is-decidable (type-Prop P) →
  instance-Dirk-Gently-Principle P Q
instance-Dirk-Gently-Principle-LEM' P Q (inl p) =
  inr-disjunction (λ _ → p)
instance-Dirk-Gently-Principle-LEM' P Q (inr np) =
  inl-disjunction (ex-falso ∘ np)

level-Dirk-Gently-Principle-LEM :
  (l1 l2 : Level) → LEM l1 → level-Dirk-Gently-Principle l1 l2
level-Dirk-Gently-Principle-LEM l1 l2 lem P Q =
  instance-Dirk-Gently-Principle-LEM' P Q (lem P)

level-Dirk-Gently-Principle-LEM' :
  (l1 l2 : Level) → LEM l2 → level-Dirk-Gently-Principle l1 l2
level-Dirk-Gently-Principle-LEM' l1 l2 lem P Q =
  swap-disjunction (level-Dirk-Gently-Principle-LEM l2 l1 lem Q P)

References

[Die18]
Hannes Diener. Constructive reverse mathematics. 2018. arXiv:1804.05495.

Recent changes