Part of modern symbolic logic which systematically exhibits the logical relations between propositions involving quantifiers such as "all" and "some.
" The predicate calculus usually builds on some form of the propositional calculus and introduces quantifiers, individual variables, and predicate letters. A sentence of the form "All F's are either G's or H's" is symbolically rendered as (∀x)[Fx ⊃ (Gx ∨ Hx)], and "Some F's are both G's and H's" is symbolically rendered as (∃x)[Fx ∧ (Gx ∧ Hx)]. Once conditions of truth and falsity for the basic types of propositions have been determined, the propositions formulable within the calculus are grouped into three mutually exclusive classes: (1) those that are true on every possible specification of the meaning of their predicate signs, such as "Everything is F or is not F"; (2) those false on every such specification, such as "Something is F and not F"; and (3) those true on some specifications and false on others, such as "Something is F and is G." These are called, respectively, the valid, inconsistent, and contingent propositions. Certain valid proposition types may be selected as axioms or as the basis for rules of inference. There exist multiple complete axiomatizations of first-order (or lower) predicate calculus ("first-order" meaning that quantifiers bind individual variables but not variables ranging over predicates of individuals). See also logic .