todo: better exposition of the concepts I mention in this first paragraph..
We presuppose knowledge of the weaker theories. Informally, a formula is any logical expression (e.g. propositions or predicates with or without free variables) which can denote a truth value, while terms or variables themselves do not. On the meta-level, one must understand typing (terms vs. predicates) and “arity-function” for predicates. We also consider propositions from before as zero-arity predicates.The quantifiers $\forall, \exists$ range over the whole domain of discourse. The quantifier bind variables like in an integral '$\int_{-2}^7t^n\,\mathrm dt$', which is $\alpha$-equivalent to, e.g., '$\int_{-2}^7r^n\,\mathrm dr$'.
There are two derivation rules
| ${\large\frac{\forall x.\,\phi(x)}{\phi(y)}}(\forall E)$ |
|---|
| ${\large\frac{\phi(y)}{\exists x.\,\phi(x)}}(\exists I)$ |
|---|
Notably, there is no $\forall I$ or $\exists E$.
We will also extend the language by introducing equality '$=$' with the usual replacement rules. (On a completely formal level, one can get a lot of structure out of different usage of equality, see Intuitionistic type theory and Identity type). One thing we want from equality is a term substituion rule along those lines:
$\large\frac{a=b\hspace{1cm}P(a)}{P(b)}$
This is then always true for logical equality. Conversely, the axioms for equality in mathematical theory (Peano axioms for natural numbers or set theory axioms like in the theory of ZFC) are rules that tell you when you can follow that $a=b$. For example, the almost always adopted extensionality axioms for sets says that if two sets have the same members, then they are equal.
In the following, we introduce some predicates which are used to formulate logical sentences more concisely. To make reading easier, I've split this predicate defintion in three conceptual parts. The first couple of definitions are really just common abbreviations in logic. After that follow some set theoretical notions, which are used in formulations of the axioms, set specifications, theorems and so on.
We write
| predicate | $(\alpha\neq\beta) \equiv \neg(\alpha = \beta) $ |
| predicate | $(\alpha=\beta=\gamma) \equiv (\alpha = \beta \land \beta = \gamma) $ |
and
| predicate | $\nexists x.\,\phi(x) \equiv \neg(\exists x.\ \phi(x)) $ |
| predicate | $\exists! x.\,\phi(x) \equiv \exists x.\,\left(\forall y.\,(\phi(y) \Leftrightarrow x=y)\right) $ |
where the brackets for the variable $x$ of the predicate $\phi(x)$ are used in the obvious way, although only writing $\phi$ would not imply that it doesn't contain $x$. Above we have also written the (meta-)symbol
$\equiv$
the first time, which we use to introduce new notation.
I came up with
$\phi(!a) \equiv \phi(a) \land \forall x.\left(\phi(x)\implies x=a\right)$
for a predicate $P$, expressing that $P$ only holds for the term $a$. Then
$\exists! x.\,\phi(x) \equiv \exists x.\,\phi(!x)$
We also use the abbreviation
| predicate | $\forall x,y.\,\psi(x,y) \equiv \forall x.\left(\forall y.\,\psi(x,y)\right) $ |
and the same goes for existential quantification as well as the restricted quantifiers above. We also use the obvious extension of this for longer sequences of quantifications with the same quantifier, e.g. $\forall x_1\dots x_n\ \phi$.
The expression $\phi(x)$ itself is sometimes called the “matrix” of the sentence, specifically if it contains several free variables.
An important classical rule is that if something doesn't hold for all things, then there exists a thing for which it doesn't hold.
$\large\frac{\neg\forall x.\,\psi(x)}{\exists x.\,\neg\psi(x)}$
The rule is then also adopted read from bottom to top, and that's also true for the following analog
$\large\frac{\neg\exists x.\,\psi(x)}{\forall x.\,\neg\psi(x)}$
Wikipedia: First order logic, List of first order theories, Intuitionistic type theory (wikipedia)
nLab: Identity type