The formulation of a higher-order logic allows some freedom—there are certain places where choices can be made. Several of these choices produce equivalent results. Before getting to the formal machinery, I informally set out my decisions on these matters. Other treatments may make different choices, but ultimately it is largely a matter of convenience that is involved.
Unable to display preview. Download preview PDF.