we all know what subsets are. note $A \subseteq B \iff x \in A \implies x \in B$ so really subsets are the same thing as logical entailment and we could also write $A \implies B$ (thinking of $A, B$ as [[sigma-algebra|event]]s or as [[predicate]]s.) we say $A$ is [[sufficient]] for $B$ and $B$ is [[necessary]] for $A$. thinking of [[type theory|type]]s as sets we get the same relation. ^boolean **Liskov substitution principle**: $A \subseteq B$ iff we can substitute an $A$ for a $B$ anywhere ie we can say "an A is a B". (even this is a [[metaphor]]; see [[onomasiology]].) more specifically: any [[invariant]]s / [[predicate]]s of $B$ must be [[invariant]]s of $A$. common in [[object oriented language]]s. ^liskov - eg for [[virtual file system]]: which locks are held see [[monotone increasing]] and [[monotone decreasing]] see [[function type]] for detailed example [[quantifier]] [[all men are mortal]] see [[2013SuScalarImplicaturesDownward]] [[2022MerrillEtAlEntailmentSemanticsCan]]