A formal system is a collection of inference rules for manipulating the formulae of a formal language. #m/def/logic
An -ary inference rule is a relation of to .
We write as
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.1
Syntactic formal theory
Given a formal system
we form a formal theory by iteratively applying the inference rules:
A formula is in iff there exists a tree of inference rules starting from axioms culminating in .
The theory can be thought of as built up in stages:
is the set of axioms, and then enlarges by applying all inference rules with formulae in as hypotheses.
#state/tidy | #lang/en | #SemBr
Footnotes
2015. Introduction to Mathematical Logic, §1.4, p. 27 gives a definition which is equivalent to ours, except that for we allow possibly infinite inference rules. ↩