First-order logic

First-order logic is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. It is also known as first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic. First-order logic uses quantified variables over (non-logical) objects. It allows the use of sentences that contain variables, so that rather than propositions such as Socrates is a man one can have expressions in the form X is a man where X is a variable. This distinguishes it from propositional logic, which does not use quantifiers.