nLab
higher-order logic

Contents

Idea

A higher-order logic is any logic which features higher-order predicates, which are predicates of predicates or of operations. If we think of a predicate as a function to truth values, then a higher-order predicate is a function on a power set or a function set.

Typed higher-order logic may be called higher-order type theory. Typed higher-order intuitionistic logic is often identified with the internal logic of a topos.

Last revised on November 1, 2014 at 16:39:27. See the history of this page for a list of all contributions to it.