Formal system

A formal system $(L, I)$ is a collection $I$ of inference rules for manipulating the formulae of a formal language $L$ . #m/def/logic

An $𝑛$ -ary inference rule $𝑅 \in I 𝑛$ is a relation of $L 𝑛$ to $L$ . We write $(H 1, \dots, H 𝑛) \sim 𝑅 C$ as

H 1 \dots H 𝑛 C (𝑅)

where we have $𝑛$ formulae called hypotheses and a single formula called the conclusion. In particular, a nullary inference rule is called an axiom. The collection of $𝑛$ -ary inference rules should be countable, and there should be an effective procedure for deciding whether an inference exists relating a given set of hypotheses to a given conclusion.¹

Syntactic formal theory

Given a formal system $(L, I)$ we form a formal theory $T = T h (L, I)$ by iteratively applying the inference rules: A formula $𝜙 \in L$ is in $T$ iff there exists a tree of inference rules starting from axioms culminating in $𝜙$ . The theory $T$ can be thought of as built up in stages: $T 0$ is the set of axioms, and then $T 𝑖 + 1$ enlarges $T 𝑖$ by applying all inference rules with formulae in $T 𝑖$ as hypotheses.

#state/tidy | #lang/en | #SemBr

2015. Introduction to Mathematical Logic, §1.4, p. 27 gives a definition which is equivalent to ours, except that for $𝑛 \neq 0$ we allow possibly infinite inference rules. ↩

Formal system

Syntactic formal theory

Footnotes