17. Beyond First-Order Logic

17.1. Sorts

17.2. Function types

17.3. Higher-order logic

17.4. Inductive Types

17.5. Dependent Types