From 12276ae68c97287fe7950f439fc1ed4b6f175bbc Mon Sep 17 00:00:00 2001 From: pmbittner Date: Wed, 25 Sep 2024 11:55:01 +0200 Subject: [PATCH] conclude incompleteness/unsoundess from less-expressive --- src/Vatras/Framework/Proof/ForFree.lagda.md | 27 +++++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/src/Vatras/Framework/Proof/ForFree.lagda.md b/src/Vatras/Framework/Proof/ForFree.lagda.md index 46ff90af..2323b53d 100644 --- a/src/Vatras/Framework/Proof/ForFree.lagda.md +++ b/src/Vatras/Framework/Proof/ForFree.lagda.md @@ -139,6 +139,33 @@ less-expressive-from-soundness : ∀ {L M : VariabilityLanguage V} → L ⋡ M less-expressive-from-soundness L-sound M-unsound M≽L = M-unsound (soundness-by-expressiveness L-sound M≽L) + +{-| +A language M that is not at least as expressive as any sound langauge L, +can never be complete. + +Dual theorem to: unsoundness-from-less-expressive +-} +incompleteness-from-less-expressive : ∀ {L M : VariabilityLanguage V} + → Sound L + → M ⋡ L + ------------ + → Incomplete M +incompleteness-from-less-expressive L-sound M⋡L M-comp = M⋡L (expressiveness-by-completeness-and-soundness M-comp L-sound) + +{-| +If there exists a complete language L that is not able to express everything +M can express, then M must be unsound (i.e., there must be meanings in M that +cannot be captured by L but since L is complete, it captures all meanings of interest). + +Dual theorem to: incompleteness-from-less-expressive +-} +unsoundness-from-less-expressive : ∀ {L M : VariabilityLanguage V} + → Complete L + → L ⋡ M + ---------- + → Unsound M +unsoundness-from-less-expressive L-comp L⋡M M-sound = L⋡M (expressiveness-by-completeness-and-soundness L-comp M-sound) ``` Combined with `expressiveness-by-completeness`/`expressiveness-by-soundness` we can even further conclude that L is more expressive than M or vice versa: