1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Empty set of logical axioms. $\endgroup$ – Mauro ALLEGRANZA Jul 1 '17 at 15:53
  • $\begingroup$ See e.g. Sara Negri & Jan von Plato, Proof Analysis: A Contribution to Hilbert’s Last Problem, Cambridge (2011), page 50 for examples. $\endgroup$ – Mauro ALLEGRANZA Jul 1 '17 at 15:56
  • $\begingroup$ @MauroALLEGRANZA So, can we say that a theory over $\mathcal{L}$ is defined by natural deduction with empty set of logical axioms, some non-empty set of sentences called non-logical axioms and a set of rules? Or it would be better to define it with no axioms at al, just with rules? $\endgroup$ – Sergey Dylda Jul 1 '17 at 17:48
  • 1
    $\begingroup$ Rules; the transitivity axiom: $(a < b \land b < c ) \to (a < c)$ can be rewritten as: $\dfrac {a < b \ \ \ \ b < c} {a < c}$. $\endgroup$ – Mauro ALLEGRANZA Jul 1 '17 at 18:16
2
$\begingroup$

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})$$

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.