Predicate calculus (also called first-order logic, functional calculus, or quantification theory) is a theory in symbolic logic that uses statements such as “there exists an object such that…” or “for all objects, it is the case that…”. It is a much more solid theory than propositional calculus, taking the interrelationship between sentences much further, but it is weaker than certain branches of mathematics, such as arithmetic and set theory.