Individual km#HOL__higher-order_logic  based on a hierarchy of types
  >part of:  predicate_logic__predicatelogic__predicate_calculus  permits the formulation of quantified statements such as "there is at least one X such that..." or "for any X, it is the case that...", where X is an element of a set called the domain of discourse
     >part of:  mathematical_logic__symbolic_logic__metamathematics__metamathematic
        >part of:  formal_logic
           >part of:  logic.philosophy  the branch of philosophy that analyzes inference
              >part of:  philosophy  the rational investigation of questions about existence and knowledge and ethics
        >part of:  abstract_algebra

No statement uses or specializes HOL; click here to add one.