Skip to content

Miniscoping Rules

CPC has mini scoping rules, we should add those too.

image

However, there are also dual rules for \exists. For completeness sake, it might make sense to cover those too.

To discuss: maybe instead of and and or ours should be strong and weak version? e.g. the strong one would be either \forall x. (F1 \land F2) = \forall x. F1 \land \forall x. F2 or \exists x. (F1 \lor F2) = \exists x. F1 \lor \exists x .F2

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information