Abstract
This paper investigates the conditions under which diagonal sentences can be taken to constitute paradigmatic cases of self-reference. We put forward well-motivated constraints on the diagonal operator and the coding apparatus which separate paradigmatic self-referential sentences, for instance obtained via Gödel’s diagonalization method, from accidental diagonal sentences. In particular, we show that these constraints successfully exclude refutable Henkin sentences, as constructed by Kreisel.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
Notes
See [14, p. 34] or [19, pp. 91]. It is crucial that we only assign indices to p.r. functions via their p.r. constructions. Note that there are functions which are defined by μ-recursion, but “happen” to be p.r. The set of indices of p.r. functions which are constructed primitive recursively is p.r., while the set of (partial) recursive functions which are p.r. is undecidable by Rice’s theorem.
A proof of this theorem can be found in [14, p. 41].
This construction is inspired by Picollo’s [20] method of obtaining ω-chains of sentences, each referring to its subsequent expression.
References
Boolos, G. (1995). Quotational ambiguity. In P. Leonardi M. Santambrogio (Eds.) On Quine: New Essays, pp. 283–296. Cambridge University Press.
Cain, J., & Damnjanovic, Z. (1991). On the weak Kleene scheme in Kripke’s theory of truth. The Journal of Symbolic Logic, 56, 1452–1468.
Carnap, R. (1934). Logische Syntax der Sprache. Springer. Translated and reprinted in [4].
Carnap, R. (2001). Logical syntax of language. Routledge.
Feferman, S. (1960). Arithmetization of metamathematics in a general setting. Fundamenta Mathematicae, 49, 35–92.
Fraassen, B. C. (1970). Inference and self-reference. Synthese, 21 (3-4), 425–438.
Grabmayr, B. (2021). On the invariance of Gödel’s second theorem with regard to numberings. Review of Symbolic Logic, 14(1), 51–84.
Grabmayr, B., & Visser, A. (2021). Self-reference upfront: a study of self-referential Gödel numberings. Review of Symbolic Logic, pp. 1–40. https://doi.org/10.1017/S1755020321000393.
Halbach, V., & Leigh, G. (2021). The road to paradox: a guide to syntax, truth, and modality. Cambridge University Press. To be published.
Halbach, V., & Visser, A. (2014a). Self-reference in arithmetic I. Review of Symbolic Logic, 7(4), 671–691.
Halbach, V., & Visser, A. (2014b). Self-reference in arithmetic II. Review of Symbolic Logic, 7(4), 671–691.
Heck, R.K. (2007). Self-reference and the languages of arithmetic. Philosophia Mathematica, 15(1), 1–29. (originally published under the name “Richard G. Heck, Jr”).
Henkin, L. (1952). A problem concerning provability. Journal of Symbolic Logic, 15, 160.
Hinman, P. G. (1978). Recursion-theoretic hierarchies. Berlin: Springer.
Jeroslow, R. G. (1973). Redundancies in the Hilbert-Bernays derivability conditions for Gödel’s second incompleteness theorem. Journal of Symbolic Logic, 38(3), 359–367.
Kreisel, G. (1953). On a problem of Henkin’s. Indagationes Mathematicae, 15, 405–406.
Kripke, S. A. (1975). Outline of a theory of truth. Journal of Philosophy, 72(19), 690–716.
Löb, M. H. (1955). Solution of a problem of Leon Henkin. Journal of Symbolic Logic, 20(2), 115–118.
Odifreddi, P. (1989). Classical recursion theory. Amsterdam: North-Holland.
Picollo, L. (2018). Reference in arithmetic. Review of Symbolic Logic, 11(3), 573–603.
Quine, W. V. (1940). Mathematical Logic. W. W. Norton, New York, 1 edition.
Schindler, T. (2015). Type-free truth. Ludwig Maximilians Universität München: PhD thesis.
Smoryński, C. (1985). Self-reference and modal logic. Springer.
Tarski, A. (1936). Der Wahrheitsbegriff in den formalisierten Sprachen. Studia Philosophica, 1, 261–405. Reprinted as ‘The Concept of Truth in Formalized Languages’ in [25] pp. 152–278. Page references are given for the translation.
Tarski, A. (1956). Logic, Semantics, Metamathematics. Oxford: Clarendon Press.
Visser, A. (1989). Semantics and the liar paradox. In D. Gabbay F. Guenthner (Eds.) Handbook of Philosophical Logic, vol. IV, pp. 617–706. Reidel, Dordrecht.
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher’s Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
We thank Albert Visser and two referees for valuable comments and suggestions. Volker Halbach gratefully acknowledges the support of his work on this paper by the Leverhulme Trust. Balthasar Grabmayr thanks the Azrieli Foundation for their generous support. The order of the authors is alphabetical. The authors contributed equally to this work.
Appendices
Appendix: A. Proof of Lemma 5.11
We first prove the more general result that for any non-constant uniform function u: Fmlx →Termx the claim holds. Let \(r\in \mathcal {R}\) be a reduced representation of u. By Lemma 5.9, it contains bn as a subterm, where \(\mathsf {ev}(b_{n})=\ulcorner -\urcorner _{f}\). We prove by induction over the complexity of r that \(\varphi (s) \vartriangleleft _{*} \mathsf {ev}(r)(\varphi )\), for some term s. For the base case it is sufficent to check the claim for r = bn, since no other C-basic function represents a function of the right type. Clearly, we have \(\varphi (x)\vartriangleleft \ulcorner {\varphi (x)}\urcorner \). For the induction step, again by Fact 5.8 and the fact that ev(r) is not constant, r must be of the form r = ⊙(bm,q), where ev(bm) is one of the basic functions \(\text {Sub}_{t},\ulcorner -\urcorner _{f},\ulcorner -\urcorner _{t}\) or \(\overline {f}\) with ar(f) ≥ 1. We now show by the following case distinction that \(\varphi (s)\vartriangleleft _{*}\mathsf {ev}(r)(\varphi )\), for some term s.
-
(1)
If ev(bm) = Subt, then by Fact 5.5 q is of the form , where ev(qi) : Fmlx →Termx for i = 1, 2. Both q1 and q2 are reduced, and at least one of ev(q1) and ev(q2) is not a constant function. If ev(q1) is not constant, then by the induction hypothesis we have \(\varphi (s)\vartriangleleft _{*}\mathsf {ev}(q_{1})(\varphi )\) for some term s. By Fact 5.3 there is a closed term t ≼ev(q1)(φ) such that \(\varphi (s)\vartriangleleft _{*}t\); and since t ≼ev(r)(φ), this shows \(\varphi (s)\vartriangleleft _{*}\mathsf {ev}(r)(\varphi )\). Now suppose ev(q1) is a constant function. Then ev(q2) must not be constant, and thus by the induction hypothesis \(\varphi (s)\vartriangleleft _{*}\mathsf {ev}(q_{2})(\varphi )\) for some term s. Also, ev(q1) cannot be closed, otherwise ev(r) would be a constant function. Hence, by Lemma 5.10, ev(q1)(φ) contains a free variable x. This means that ev(q2)(φ) ≼ev(r)(φ), and we conclude that \(\varphi (s)\vartriangleleft _{*}\mathsf {ev}(r)(\varphi )\) by Fact 5.2.
-
(2)
If \(\mathsf {ev}(b_{m})=\ulcorner -\urcorner _{t}\), then ev(q): Fmlx →Termx is a non-constant function. By induction hypothesis there is a term s such that \(\varphi (s)\vartriangleleft _{*}\mathsf {ev}(q)(\varphi )\). We also have \(\mathsf {ev}(q)(\varphi )\vartriangleleft \ulcorner {\mathsf {ev}(q)(\varphi )}\urcorner \), hence \(\varphi (s) \vartriangleleft _{*} \mathsf {ev}(r)(\varphi )\).
-
(3)
If \(\mathsf {ev}(b_{m})=\overline {f} \colon {\text {Term}_{x}^{n}} \to \text {Term}_{x}\), then by Fact 5.5, q must be of the form (if n = 1 we simply have q), with each qi of type Fmlx →Termx. There is i ≤ n such that qi is not a constant function. By induction hypothesis, \(\varphi (s) \vartriangleleft _{*} \mathsf {ev}(q_{i})(\varphi )\), for some term s. Since ev(qi)(φ) ≼ev(r)(φ), we obtain \(\varphi (s) \vartriangleleft _{*} \mathsf {ev}(r)(\varphi )\) by Fact 5.2.
-
(4)
Finally, if \(\mathsf {ev}(b_{m}) = \ulcorner -\urcorner _{f}\), then ev(q): Fmlx →Fmlx is a non-constant function. We now show that φ(s) ≼ev(q)(φ) or \(\varphi (s)\vartriangleleft _{*}\mathsf {ev}(q)(\varphi )\), for some term s. In either case, we obtain the desired result, i.e., \(\varphi (s) \vartriangleleft _{*} \mathsf {ev}(r)(\varphi )\). We prove this disjunction by a further local induction over the complexity of q. If q is bl, for some l ∈ ω, then we have φ(x) ≼ev(bl)(φ). This is because the only C-basic function of the right type is \(\text {id}_{\text {Fml}_{x}}\). For the inductive step, it is sufficient to assume by Fact 5.8 and the fact that ev(q) is not a constant function, that q is of the form \(\odot (b_{k},q^{\prime })\) where ev(bk) is \(\text {Sub}_{f},\overline {\star }\) or \(\overline {R}\) with ar(R) ≥ 1. We proceed by considering each of these cases:
-
(a)
If ev(bk) = Subf, then \(q^{\prime }\) must be with \(\mathsf {ev}(q_{1}^{\prime })\colon \text {Fml}_{x}\to \text {Fml}_{x}\) and \(\mathsf {ev}(q_{2}^{\prime })\colon \text {Fml}_{x}\to \text {Term}_{x}\). At least one of \(\mathsf {ev}(q_{1}^{\prime })\), \(\mathsf {ev}(q_{2}^{\prime })\) is not a constant function. If \(\mathsf {ev}(q_{1}^{\prime })\) is not constant, then by the induction hypothesis, we have \(\varphi (s)\preceq \mathsf {ev}(q_{1}^{\prime })(\varphi )\) or \(\varphi (s)\vartriangleleft _{*}\mathsf {ev}(q_{1}^{\prime })(\varphi )\) for some term s. In the former case, we have \(\varphi (s[x/\mathsf {ev}(q_{2}^{\prime })(\varphi )]) \preceq \mathsf {ev}(r)(\varphi )\). In the latter case we conclude \(\varphi (s)\vartriangleleft _{*}\mathsf {ev}(r)(\varphi )\) by a similar argument as in (1). Now if \(\mathsf {ev}(q_{1}^{\prime })\) is a constant function, then \(\mathsf {ev}(q_{2}^{\prime })\) is not constant and hence \(\mathsf {ev}(q_{1}^{\prime })\) cannot be closed. Then \(\mathsf {ev}(q_{1}^{\prime })(\varphi )\) contains a free variable by Lemma 5.10, and we obtain \(\mathsf {ev}(q_{2}^{\prime })(\varphi )\preceq \mathsf {ev}(r)(\varphi )\). By the outer induction hypothesis, \(\varphi (s)\vartriangleleft _{*}\mathsf {ev}(q_{2}^{\prime })(\varphi )\) for some term s. We then conclude \(\varphi (s)\vartriangleleft _{*}\mathsf {ev}(r)(\varphi )\) by another use of Fact 5.2.
-
(b)
If \(\mathsf {ev}(b_{k})=\overline {\star }\), then \(q^{\prime }\) must be (if n = 1 we simply have \(q^{\prime }\)), with each \(q_{i}^{\prime }\), \(\mathsf {ev}(q_{i}^{\prime })\colon \text {Fml}_{x}\to \text {Fml}_{x}\). At least one \(q_{i}^{\prime }\) is not a constant function. Hence by induction hypothesis \(\varphi (s)\preceq \mathsf {ev}(q_{i}^{\prime })(\varphi )\) or \(\varphi (s)\vartriangleleft _{*}\mathsf {ev}(q_{i}^{\prime })(\varphi )\). Since \(\mathsf {ev}(q_{i}^{\prime })(\varphi )\preceq \mathsf {ev}(q^{\prime })(\varphi )\), we are done.
-
(c)
The case for \(\mathsf {ev}(b_{k})=\overline {R}\), where ar(R) ≥ 1, proceeds similarly to (4.b).
-
(a)
The proof is complete since diagonal operators cannot be constant functions.
Appendix : B. Uniform Constructions of Deviant Henkin Sentences
This part of the appendix contains several explicit constructions of deviant provability predicates which yield refutable Henkin sentences. Since all of these constructions will rely on the recursion theorem, we start by briefly introducing this important recursion theoretic result.
We start by assigning indices to p.r. functions.Footnote 1 We write Fa for the p.r. function with index a. Note that each p.r. function has infinitely many indices. Moreover, the set of indices is p.r. The following recursion theorem for p.r. functions shows that we can construct p.r. functions in a self-referential way, by using their indices in their own definitions.Footnote 2
Theorem B.1 (Primitive Recursion Theorem)
For every k+ 1-ary p.r. function \(G(\vec x,y)\), there is an index a such that \(F_{a}(\vec x) = G(\vec x,a)\), where \(\vec x\) is a k-tuple of variables.
In this paper we only consider standard interpretations which are intuitively “effective” (for a definition of a standard interpretation see Section 4). More precisely, we require that for every standard interpretation \(\mathcal {I}\) there is a recursive function which maps each pair (n,k) of numbers to an index a such that \(\mathcal {I}({f_{n}^{k}}) = F_{a}\).
Before we provide our constructions we fix some more notation. Let \({\mathscr{L}}\) be given as in Section 4 and let # be some standard elementary numbering of \({\mathscr{L}}\) such that #e > 0, for all well-formed expressions e in \({\mathscr{L}}\). Let \({P_{i}^{k}}\) be the projection function which maps a k + 1-tuple to its i + 1-th component (where i ≤ k).
Let the function \(\mathcal {I}^{\prime } \colon \{{f_{n}^{k}} \mid n \neq 0, k \neq 0 \} \to \mathfrak {Pr}\) be given by
Clearly, \(\mathcal {I}^{\prime }\) is surjective. For each index a of a unary function, let \(\mathcal {I}^{a}\) be the extension of \(\mathcal {I}^{\prime }\) by map** the function symbol \({f_{0}^{0}}\) to Fa. Each such \(\mathcal {I}^{a}\) is a standard interpretation function of \({\mathscr{L}}\). We observe:
Fact B.2
For each index a of a unary function, there is an \({\mathscr{L}}_{0}\)-formula Bewa(x) which weakly represents \(\mathsf {Basic}(\mathcal {I}^{a})\) relative to #. Moreover, there is a p.r. function H which maps each such a to the #-code of Bewa(x).
We now prove Lemma 4.2 by providing two examples of uniform diagonal operators which satisfy the fixed-point property of Lemma 4.2. The first example employs a canonical numeral function, namely, standard numerals, but is based on a contrived numbering. The second example uses a standard numbering, but relies on an artificial numeral function. These examples can be developed for all uniform diagonal operators introduced in this paper. For the sake of simplicity, however, we will base the exposition on diagonal operators which are particularly suitable.
1.1 B.1 First Proof of Lemma 4.2
We base the first construction on the diagonal operator dB introduced in Example 3.5. Similar but slightly more complicated constructions can be given for dG and dJ.
Let J be a unary p.r. function which maps the #-code of ϕ to the #-code of \({f_{0}^{0}}(\ulcorner {\phi }\urcorner ^{\text{\texttt {\#}}})\). Let ∧# denote the #-tracking function of \(\overline {\wedge }\), i.e., ∧#(#ϕ,#ψ) = #ϕ ∧ ψ. Similarly, let Sub# denote the #-tracking function of Subf : Fmlx ×Termx →Fmlx, defined in Section 3. Let z be the #-code of the formula
We now define a function G: ω2 → ω by setting
Clearly, G is p.r. Using Theorem B.1, we find an index a such that
We now set
Using the fixed-point property of a, we get
We now define a numbering α as follows:
The numbering α is injective and elementary. Moreover, Bewa(x) also weakly represents \(\mathsf {Basic}(\mathcal {I}^{a})\) relative to α. We set . By Eq. 2 and the fact that , we have for each ϕ(x) ∈Fmlx that
Hence, dB given by is a uniform diagonal operator with respect to α, standard numerals and \(\mathcal {I}^{a}\) (see also Definition 4.1 and Example 3.5). Moreover, Bew∗(x) is a fixed-point of \(k_{d_{B}}\), i.e.,
This completes our first proof of Lemma 4.2. Note that while our construction employs the standard numeral function, the numbering α is contrived. We now show that if we leave the numeral function unconstrained, we can construct a deviant provability predicate satisfying Lemma 4.2 for any given standard numbering.
1.2 B.2 Second Proof of Lemma 4.2
We base the second construction on Jeroslow’s operator dJ introduced in Section 3.2. Once again, similar but slightly more complicated constructions can be given for dB and dG.
Let subJ be \({f_{n}^{1}}\) for some n such that Fn maps the #-codes of ϕ(x) and t(x) to the #-code of \(\phi (t(\ulcorner {t(x)}\urcorner ^{\text{\texttt {\#}}})\). Let z be the #-code of the formula
We now define a function G: ω2 → ω by setting G(p,q) := ∧#(z,H(q)). By Theorem B.1, there is an index a such that Fa(p) = G(p,a), for all p ∈ ω. We now define the formula
Given the fixed-point property of a, we have
Hence, the map** ν : ω →ClTerm given by
is a numeral function (for \(\mathcal {I}^{a}\)). We moreover have that
Hence, for each ϕ ∈Fmlx
In other words, dJ given by \(\phi (x) \mapsto \mathsf {sub}_{J}(\ulcorner {\varphi (x)}\urcorner ^{\text {\texttt {\#}}, \nu },\ulcorner {\mathsf {sub}_{J}(\ulcorner {\varphi (x)}\urcorner ^{\text {\texttt {\#}}, \nu },x)}\urcorner )\) is a uniform diagonal operator with respect to #, ν and \(\mathcal {I}^{a}\).
Moreover, Bew‡(x) is a fixed-point of \(k_{d_{J}}\), i.e., we have
This completes our second proof of Lemma 4.2. As opposed to the contrived numbering α used in B.1, our second proof works for any given standard numbering. However, the uniform diagonal operator dJ is based on the contrived numeral function ν.
1.3 B.3 Proof of Lemma 7.1
Let sub be \({f_{n}^{1}}\) for some n such that Fn is the #-tracking function of the substitution function for formulas. Moreover, let num be \({f_{n}^{0}}\) for some n such that Fn maps every number to the #-code of its standard numeral. Finally, let be \({f_{n}^{0}}\) for some n such that Fn maps the #-code of ϕ(x,y) to the #-code of (here we assume that our indexing of p.r. functions permits this construction). For each index a, consider the formulaFootnote 3
Theorem B.1 yields an index a of a unary p.r. function map** the #-code of to the #-code of , for each n ∈ ω. We now set . Hence, we have
Therefore,
We now set \(t_{n} :\equiv \mathsf {sub}(t, \mathsf {num}(\overline {n}) )\), for each n ∈ ω. Note that tn is not contained in tm, for n≠m. We can then show in \(\mathsf {Basic}(\mathcal {I}^{a})\) that
For each n ∈ ω, we define
We observe:
Fact B.3
For each n ∈ ω,
-
(1)
Bewn(x) weakly represents provability in \(\mathsf {Basic}(\mathcal {I}^{a})\);
-
(2)
\(\mathsf {Basic}(\mathcal {I}^{a}) \vdash t_{n} = \ulcorner {\mathsf {Bew}_{n}(t_{n})}\urcorner ^{\text {\texttt {\#}}}\);
-
(3)
\(\mathsf {Basic}(\mathcal {I}^{a}) \vdash \neg \mathsf {Bew}_{n}(t_{n})\).
Finally, Bewn(x) does not contain tn (at least for sensible choices of Bewa(x)). This completes our proof of Lemma 7.1.
1.4 B.4 Proof of Lemma 7.3
Let subJ be given as in Section B.2. Let jump be \({f_{n}^{0}}\) for some n such that Fn maps the #-code of \(\mathsf {sub}_{J}({f^{0}_{0}}(\overline {m}),\ulcorner {\mathsf {sub}_{J}({f^{0}_{0}}(\overline {m}),x)}\urcorner ^{\text {\texttt {\#}}})\) to the #-code of \(\mathsf {sub}_{J}({f^{0}_{0}}(\overline {m+1}),\ulcorner {\mathsf {sub}_{J}({f^{0}_{0}}(\overline {m+1}),x)}\urcorner ^{\text {\texttt {\#}}})\), for m ∈ ω. By Theorem B.1, there is an index a of a unary p.r. function which maps n to the #-code of
For each n ∈ ω, we define the formula
Given the fixed-point property of a, we have
Hence, the map** ν : ω →ClTerm given by
is a numeral function (for \(\mathcal {I}^{a}\)). We moreover have that
For each n ∈ ω we set \(t_{n} :\equiv \mathsf {sub}_{J}({f^{0}_{0}}(\overline {n}),\ulcorner {\mathsf {sub}_{J}({f^{0}_{0}}(\overline {n}),x)}\urcorner ^{\text {\texttt {\#}}, \nu })\). Recall that dJ is the uniform diagonal operator which maps any formula ϕ(x) to the term
Fact B.4
We have tn ≡ dJ(Bewn(x)), for each n ∈ ω.
Proof
We have
□
We observe:
Fact B.5
For each n ∈ ω,
-
(1)
Bewn(x) weakly represents provability in \(\mathsf {Basic}(\mathcal {I}^{a})\);
-
(2)
\(\mathsf {Basic}(\mathcal {I}^{a}) \vdash t_{n} = \ulcorner {\mathsf {Bew}_{n}(t_{n})}\urcorner ^{\text {\texttt {\#}}}\);
-
(3)
\(\mathsf {Basic}(\mathcal {I}^{a}) \vdash \neg \mathsf {Bew}_{n}(t_{n})\).
Finally, we observe that
Thus, \(\vartriangleleft _{\ast }^{\text {\texttt {\#}},\nu }\) is ill-founded but irreflexive.
1.5 B.5 A Henkin Sentence Without an Additional Conjunct
We now construct a Henkin sentence which is not of the form χ(x) ∧Bew(x). Let subJ be given as in Section B.2. We assume that for each index a of a unary function, Bewa(x) also satisfies \(\mathsf {Basic}(\mathcal {I}^{a}) \vdash \neg \mathsf {Bew}^{a}(\ulcorner {\phi }\urcorner ^{\text {\texttt {\#}}})\), for all non-formulas ϕ. Let H be a p.r. function which maps each such a to the #-code of Bewa(x) (see Fact B.2). Let K be a p.r. function which maps each #-code of ϕ to the #-code of \(\ulcorner {\phi }\urcorner ^{\text {\texttt {\#}}}\). Let Sub# denote the #-tracking function of the substitution function Subf defined in Section 3. Let \(\overline {\mathsf {sub}_{J}}_{\text {\texttt {\#}}}\) denote the #-tracking function of the binary function \(\overline {\mathsf {sub}_{J}}\) introduced in Section 3. Let the function L: ω → ω be given by
We define G: ω2 → ω by setting
Using Theorem B.1, there is an index a such that Fa(p) = G(p,a), for all p ∈ ω. We now define the formula
Given the fixed-point property of a, we have
We observe that application of Jeroslow’s diagonal operator to the provability predicate Bew◇(x) yields a refutable Henkin sentence:
Fact B.6
-
(1)
Bew◇(x) weakly represents provability in \(\mathsf {Basic}(\mathcal {I}^{a})\);
-
(2)
\(\mathsf {Basic}(\mathcal {I}^{a}) \vdash \neg \mathsf {Bew}^{\diamond }(d_{J}(\mathsf {Bew}^{\diamond }(x)))\).
To sum up, \(d_{J}(\mathsf {Bew}^{\diamond }(x))\) is a refutable Henkin sentence, where dJ is a uniform diagonal operator and the underlying naming relation is given by a standard numbering and numeral function. Hence, in particular, the corresponding naming relation is well-founded.
Rights and permissions
Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article's Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article's Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
About this article
Cite this article
Grabmayr, B., Halbach, V. & Ye, L. Varieties of Self-Reference in Metamathematics. J Philos Logic 52, 1005–1052 (2023). https://doi.org/10.1007/s10992-022-09696-y
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10992-022-09696-y