A collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over non-logical objects and 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 ‘there exists X such that X is Socrates and X is a man’ and there exists is a quantifier while X is a variable. This distinguishes it from propositional logic, which does not use quantifiers or relations.