Construction of a theory using natural deduction

Question

Suppose I want to construct some first-order formal language $\mathcal{L}$ from signature $\sigma$ using natural deduction. That is, we have basic judgments like "$\phi$ is a term" or "P is a formula" etc , and correspondent rules, e.g. : $$\frac{\begin{array}{@{}c@{}} f\in F \quad t_1 \, term \dots t_n \, term \end{array}}{f(t_1,\dots,t_n) \, term}$$

By this means we can construct appropriate formal language $\mathcal{L}$ with some set of terms and formulas of this language using these rules and judgements.

However, now I want to turn my language into a theory, i.e. define some certain set of sentences to be axioms (I suppose they are called non-logical axioms) from which by the means of some rules other sentences can be derived. And here comes my confusion, since natural deduction system is supposed to have empty set of axioms.

Question: How do we do this sort of definition of a theory in terms of natural deduction? Should we introduce some new judgements like "A is an axiom" and "B is a theorem" to our deductive system, or it can be done using some of the rules?

P.S. I know that there exists Hilbert-system of deduction that has non-empty set of axioms. However, as our language was initially constructed by natural deduction, I suppose that the definition of a theory over that language should also be in that same deductive system.

Answer 1

Tipically, they are written as rules.

You can see the natural deduction version of the equality axioms:

$$\dfrac {}{x=x} (= \text{I})$$

$$\dfrac {s=t \ \ \ \ \ \ \phi[s/x]}{\phi[t/x]} (= \text{E})$$

In the same way, we can manage e.g. the transitivity axiom: $(a<b∧b<c)→(a<c)$ for $<$:

$$\dfrac {a<b \ \ \ b<c}{a<c}(< \text{trans})$$