11 Quantifiers

We have been using for-all since 842Induction, so here we mostly see how this quantifier interacts with the other logical connectives. It’s important to realize that implication (non-dependent function) is just a special case of for-all (dependent function), which is a primitive feature provided by Agda.

There is some potentially confusing prose at the start of this PLFA chapter, regarding bound and free variables. Given an expression of the form ∀ (x : A) → C, where C can be a complex subexpression, we say that an occurrence of the variable x in C is a bound occurrence. It is bound by the enclosing quantifier ∀ x. Occurrences of variables that are not bound are free.

Another way to look at it is to think of an expression as having a tree structure. An occurrence of x will be at a leaf of that tree. If, when tracing up towards the root, we encounter a ∀ x internal node, then the occurrence is bound; otherwise, it is free. We will need to precisely formalize these ideas shortly, when dealing with material from the second volume of PLFA.

Interestingly, when for-all is built in, existential quantification can be derived like the other logical connectives we have seen. Evidence that an existential statement holds is a pair consisting of a witness and a proof that the witness has the desired property. A bit of special syntax helps make it more readable, but unfortunately that syntax doesn’t always get used during interaction. (You don’t have to know how to write or even read this kind of Agda syntax declaration.) There’s nothing new here as far as Agda features or interaction is concerned. The proofs in 747Quantifiers that use co-patterns resemble the ones we’ve seen earlier.

What we studied in the Connectives and Negation chapters was propositional logic (for-all is used only to quantify variables at the top level of a formula). Adding quantifiers that can be used at any level gives us predicate logic. There is no difference between intuitionistic and classical logic on the quantifier level; the only difference lies in the absence or presence of something like LEM. If we view for-all as generalized conjunction, and there-exists as generalized disjunction, then we can see why some logical statements involving quantifiers might not be provable in intuitionistic logic (for example, the generalization of the unprovable propositional version of one of deMorgan’s laws).

PLFA finishes off the Bin-isomorphism exercise here, by asking you to show an isomorphism between ℕ and ∃[ x ](Can x). But this is essentially what you already did in the final exercises for the Isomorphism chapter.