lacunary - Mathnotes

A formal system $\mathcal{F}$ is an ordered quadruple

$$\mathcal{F}=(\mathrm{\Sigma },W,A,R)$$

where:

1. $\mathrm{\Sigma }$ is a finite, nonempty alphabet (a set of symbols);
2. $W\subseteq {\mathrm{\Sigma }}^{\ast }$ is the set of well-formed-formulas (wffs), defined inductively by formation rules specifying which finite strings over $\mathrm{\Sigma }$ belong to $W$
3. $A\subseteq W$ is a distinguished subset of $W$, whose members are called axioms.
4. $R$ is a finite set of rules of inference, each of which is a relation on $W$ determining from which formulas other formulas may be derived.

A derivation (or proof) in $\mathcal{F}$ is a finite sequence of formulas

$${\phi }_1,{\phi }_2,\dots ,{\phi }_n$$

such that for each $i\le n$,

1. Either ${\phi }_i\in A$, or
2. ${\phi }_i$ follows from earlier formulas in the sequence by an inference rule in $R$.

A formula $\psi \in W$ is a theorem (or provable formula) of $\mathcal{F}$ if there exists such a derivation ending with $\psi$. We then write

$${⊢}_{\mathcal{F}}\psi .$$

The system $\mathcal{F}$ is said to be recursive (or effectively generated) if $W$, $A$, and $R$ are all @recursively-enumerable sets, so that derivations can be verified by a finite mechanical procedure.