Skip to main content
Mathematics LibreTexts

5.11: The Collection of Axioms Is Representable

  • Page ID
    10071
  • \( \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \) \( \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} \)\(\newcommand{\id}{\mathrm{id}}\) \( \newcommand{\Span}{\mathrm{span}}\) \( \newcommand{\kernel}{\mathrm{null}\,}\) \( \newcommand{\range}{\mathrm{range}\,}\) \( \newcommand{\RealPart}{\mathrm{Re}}\) \( \newcommand{\ImaginaryPart}{\mathrm{Im}}\) \( \newcommand{\Argument}{\mathrm{Arg}}\) \( \newcommand{\norm}[1]{\| #1 \|}\) \( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\) \( \newcommand{\Span}{\mathrm{span}}\) \(\newcommand{\id}{\mathrm{id}}\) \( \newcommand{\Span}{\mathrm{span}}\) \( \newcommand{\kernel}{\mathrm{null}\,}\) \( \newcommand{\range}{\mathrm{range}\,}\) \( \newcommand{\RealPart}{\mathrm{Re}}\) \( \newcommand{\ImaginaryPart}{\mathrm{Im}}\) \( \newcommand{\Argument}{\mathrm{Arg}}\) \( \newcommand{\norm}[1]{\| #1 \|}\) \( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\) \( \newcommand{\Span}{\mathrm{span}}\)\(\newcommand{\AA}{\unicode[.8,0]{x212B}}\)

    In this section we will exhibit two \(\Delta\)-formulas that are designed to pick out the axioms of our deductive system.

    proposition 5.11.1.

    The collection of Gödel numbers of the axioms of \(N\) is representable.

    proof

    The formula \(AxiomOfN\) is easy to describe. As there are only a finite number of \(N\)-axioms, a natural number \(a\) is in the set \(AXIOMOFN\) if and only if it is one of a finite number of Gödel numbers. Thus

    \(AxiomOfN \left( a \right) =\)

    \[a = \overline{\ulcorner \left( \forall x \right) \neg Sx = 0 \urcorner} \lor \\ a = \overline{\ulcorner \left( \forall x \right) \left( \forall y \right) \left[ Sx = Sy \rightarrow x = y \right] \urcorner} \lor \\ \vdots \\ \lor a = \overline{ \ulcorner \left( \forall x \right) \left( \forall y \right) \left[ \left( x < y \right) \lor \left( x = y \right) \lor \left( y < x \right) \right] \urcorner}.\]

    (To be more-than-usually picky, we need to change the \(x\)'s and \(y\)'s to \(v_1\)'s and \(v_2\)'s, but you can do that.)

    proposition 5.11.2.

    The collection of Gödel numbers of the logical axioms is representable.

    proof

    The formula that recognizes the logical axioms is more complicated than the formula \(AxiomOfN\) for two reasons. The first is that there are infinitely many logical axioms, so we cannot just list them all. The second reason that this group of axioms is more complicated is that the quantifier axioms depend on the notion of substitutability, so we will have to use our results from Section 5.10.

    Quite probably you are at a point where you could turn to Section 2.3.3 and write down a \(\Delta\)-definition of the set \(LOGICALAXIOM\). To do so would be a worthwhile exercise. But if you are feeling lazy, here is an attempt:

    \(LogicalAxiom \left( a \right) =\)

    \[\left( \exists x < a \right) \left( Variable \left( x \right) \land a = \bar{2}^\bar{8} \bar{3}^{Sx} \bar{5}^{Sx} \right) \lor \\ \left( \exists x, y < a \right) \left( Variable \left( x \right) \land Variable \left( y \right) \land \\ a = \bar{2}^\bar{4} \bar{3}^{\left( \bar{2}^\bar{2} \bar{3}^{\left( \bar{2}^\bar{8} \bar{3}^{Sx} \bar{5}^{Sy} + 1 \right)} + 1 \right)} \bar{5}^{\left( \bar{2}^\bar{8} \bar{3}^{\bar{2}^\bar{12} \bar{3}^{Sx} + 1} \bar{5}^{\bar{2}^\bar{12} \bar{3}^{Sy} + 1} + 1 \right)} \right) \lor \\ \left( \left( \exists x_1, x_2, y_1, y_2 < a \right) \left( Variable \left( x_1 \right) \land \cdots \land Variable \left( y_2 \right) \land \\ a = \: \text{Ugly Mess saying} \: \left[ \left( x_1 = y_1 \right) \land \left( x_2 = y_2 \right) \right] \rightarrow \\ \left( x_1 + x_2 = y_1 + y_2 \right) \right) \right) \lor \\ \vdots \\ \text{(Similar clauses coding up (E2) and (E3) for} \: \cdot, E, =, \: \text{and} \: < \text{)} \\ \vdots \\ \lor \left( \exists f , x, t, y < a \right) \left( Formula \left( f \right) \land Variable \left( x \right) \land Term \left( t \right) \land \\ Substitutable \left( t, x, f \right) \land Sub \left( f, x, t, y \right) \land \\ a = \bar{2}^\bar{4} \bar{3}^{\left( \bar{2}^\bar{2} \bar{3}^{\left( \bar{2}^\bar{6} \bar{3}^{Sx} \bar{5}^{Sf} + 1 \right)} + 1 \right)} \bar{5}^{Sy} \right) \lor \\ \text{(Similar clause for Axiom (Q2))}.\]

    To look at this in a little more detail, the first clause of the formula is supposed to correspond to axiom (E1): \(x = x\) for each variable \(x\). So \(a\) is the Gödel number of an axiom of this form if there is some \(x\) that is the Gödel number of a variable [which is what \(Variable \left( x \right)\) says] such that \(a\) is the Gödel number of a formula that looks like

    variable with Gödel number \(x =\) variable with Gödel number \(x\).

    But the Gödel number for this formula is just \(2^8 3^{Sx} 5^{Sx}\), so that is what we demand that \(a\) equal.

    The second clause covers axioms of the form (E2), when the function \(f\) is the function \(S\). We demand that \(a\) be the code for the formula

    \[\left( v_i = v_j \right) \rightarrow Sv_i = Sv_j,\]

    where \(x = \ulcorner v_i \urcorner\) and \(y = \ulcorner v_j \urcorner\). After you fuss with the coding, you come out with the expression shown. The other clauses of type (E2) and (E3) are similar.

    The last clause that is written out is for the quantifier axioms (Q1). After demanding that the term coded by \(t\) be substitutable for the variable coded by \(x\) in the formula coded by \(f\) and that \(y\) be the code for the result of substituting in that way, the equation for \(a\) is nothing more than the analog of \(\left( \forall x \phi \right) \rightarrow \phi_t^x\).

    Exercises

    1. Complete the definition of the formula \(LogicalAxiom\).

    This page titled 5.11: The Collection of Axioms Is Representable is shared under a CC BY-NC-SA 4.0 license and was authored, remixed, and/or curated by Christopher Leary and Lars Kristiansen (OpenSUNY) via source content that was edited to the style and standards of the LibreTexts platform; a detailed edit history is available upon request.