section_path: Systems of logic/Extended/Higher order logic
section_name: Higher order logic
paragraph_text: Higher order logic
  
  Higher-order logics extend classical logic not by using modal operators but by introducing new forms of quantification. Quantifiers correspond to terms like "all" or "some". In classical first-order logic, quantifiers are only applied to individuals. The formula " ∃ x (A p p l e (x) ∧ S w e e t (x)) {\displaystyle \exists x(Apple(x)\land Sweet(x))} " (some apples are sweet) is an example of the existential quantifier " ∃ {\displaystyle \exists } " applied to the individual variable " x {\displaystyle x} ". In higher-order logics, quantification is also allowed over predicates. This increases its expressive power. For example, to express the idea that Mary and John share some qualities, one could use the formula " ∃ Q (Q (M a r y) ∧ Q (J o h n)) {\displaystyle \exists Q(Q(Mary)\land Q(John))} ". In this case, the existential quantifier is applied to the predicate variable " Q {\displaystyle Q} ". The added expressive power is especially useful for mathematics since it allows for more succinct formulations of mathematical theories. But it has drawbacks in regard to its meta-logical properties and ontological implications, which is why first-order logic is still more commonly used.