In formal logic, variables are symbols that represent elements in a domain of discourse. They serve as placeholders that can take on different values or objects, allowing for generalization and the formulation of statements that can be universally or existentially quantified. The use of variables is essential for constructing formal proofs, as they help express relationships and properties in a structured manner.