First-Order Logic

In set theory (and mathematics in general), there is a language ("formal system") used to formalize statements and axioms known as first-order logic. Alternatively known as predicate logic, this allows for general statements to be made about sets and their elements, among other things. There is a traditional collection of symbols used in first-order logic, including equality (`=`), conjunction / intersection (`\land`), disjunction / union (`\lor`), implication (`\to`), biconditional (`\leftrightarrow`), negation (`\neg`), "for all" (`\forall`), and "exists" (`\exists`). These are also used with arbitrary variables and conventional punctuation.

Contrast this with propositional logic, which uses only implication and negation to describe cause-and-effect relationships. Both propositional and predicate logic use collections of symbols, operators, axioms, and inference rules (such as modus ponens) in order to establish the respective systems.
Modus Ponens: `P \land (P\to Q)\to Q`

In second-order logic, predicates and subsets can be described and quantified, unlike in first-order logic, which deals only in individual elements and relations. Another limitation is that first-order logic cannot uniquely describe infinite structures like the `\mathbb N` or `\mathbb R`, while second-order logic can. For instance, second-order logic can express the property that every subset of the naturals has a lowest element, but, by definition, first-order logic cannot.

Higher-order logic is an extension of this concept. First-order logic quantifies over individuals, second-order logic quantifies over sets, third-order logic quantifies over sets of sets, and so on. As part of this naming scheme, propositional logic is sometimes labelled "zeroth-order logic", as each higher order logic system is a superset of the constructions of those below it.

It is a famous result as part of Gödel's incompleteness theorem that no formal system which models Peano arithmetic can be simultaneously...

• Sound: Everything valid in the system is true
• Complete: Everything true is valid in the system
• Effective: There exists a terminating proof-checking decision algorithm

In other words, no system can assert its own consistency, nor can it prove / disprove every possible statement made.