NECESSARILY NON-ANALYTIC INDUCTION——SUMMARY OF SOME RESULTS
───────────────────────────────────────────────────────────
version: 2019–05–14
Eric Johannesson and Anders Lundstedt
eric.johannesson@philosophy.su.se
anders.lundstedt@philosophy.su.se
§1 Introduction
───────────────
Sometimes when trying to prove a fact F by induction one gets "stuck" when
trying to prove the induction step. A solution is sometimes to instead prove a
"stronger" fact S by induction. This proof method is usually called something
like "strengthening of the induction hypothesis". However, there need not always
be a precise sense in which the fact S is "stronger". Thus, following Hetzl and
Wong (2018), we use the more general terminology "non-analytic induction proofs"
for such proofs. A natural question for such proofs is whether the
non-analyticity is necessary——that is, whether one could prove F without a
"detour" proving some other fact. Hetzl and Wong have made precise sense of this
question for first-order theories and sentences of arithmetic.
∗∗
In §2 we give two examples of non-analytic induction proofs, proving the two
facts:
(F1) For all natural numbers n: 1+3+5+⋅⋅⋅+(2n-1) = k² for some natural number
k.
(F2) For all natural numbers n: 1+1/2²+1/3²+⋅⋅⋅+1/(n+1)² < 2.
∗∗
In §3 we present a slight generalization and reformulation of some of the
notions introduced by Hetzl and Wong.
∗∗
In §4 we show, using the notions introduced in §3, that there is a precise sense
in which (F1) must be proved by non-analytic induction.
∗∗
In §5 we present some preliminary results towards settling whether (F2) must be
proved by non-analytic induction in any precise sense afforded by the notions
introduced in §3.
∗∗
In §6 we present some ideas for future work.
∗∗
§2 Two results proved by non-analytic induction
───────────────────────────────────────────────
For our first case, we have that the sum of any initial segment of the odd
natural numbers is a perfect square, that is,
for all natural numbers n: 1+3+5+⋅⋅⋅+(2n-1) = k² for some natural number
k,
or, avoiding ellipsis notation, the following.
∗∗
DEFINITION. f₁ : ℕ → ℕ is recursively defined by
f₁(0) := 0,
f₁(n+1) := f₁(n)+2n+1.
∗∗
FACT 1. For all natural numbers n: f₁(n) = k² for some natural number k.
PROOF ATTEMPT. "Straightforward induction":
– Base case: f₁(0) = 0 = 0² (by definitions) so f₁(0) = k² for k = 0.
– Induction step:
f₁(n+1) = f₁(n)+2n+1 (by definition)
= k²+2n+1 (for some k, by induction hypothesis).
But k²+2n+1 is not a perfect square for all natural numbers k and n so how
do we proceed from here?
ACTUAL PROOF. It suffices to prove the following "stronger" fact, of which
Fact 1 is a logical consequence.
f₁(n) = n² for all natural numbers n.
(This fact is not a logical consequence of Fact 1, so it is stronger than Fact 1
in at least that sense.)
We prove this fact by induction.
– Base case: f₁(0) = 0² ≡ 0 = 0 (by definitions).
– Induction step:
f₁(n+1) = f₁(n)+2n+1 (by definition)
= n²+2n+1 (by induction hypothesis)
= (n+1)² (by elementary arithmetic). □
∗∗
For our second case, we have
1+1/2²+1/3²+⋅⋅⋅+1/(n+1)² < 2 for all natural numbers n,
or, avoiding ellipsis notation, the following.
∗∗
DEFINITION. f₂ : ℕ → ℚ is recursively defined by
f₂(0) := 1,
f₂(n+1) := f₂(n)+1/(n+2)².
∗∗
FACT 2. f₂(n) < 2 for all natural numbers n.
PROOF ATTEMPT. "Straightforward" induction:
– Base case: f₂(0) < 2 ≡ 1 < 2 (by definition).
– Induction step:
f₂(n+1) = f₂(n)+1/(n+2)² (by definition)
< 2+1/(n+2)² (by induction hypothesis).
But 2+1/(n+2)² ≮ 2 for any natural number n so how do we proceed from
here?
ACTUAL PROOF. It clearly suffices to prove the "stronger" fact
f₂(n) ≤ 2-1/(n+1) for all natural numbers n.
(In what sense is this fact stronger than Fact 2? It is at least stronger in the
sense that for all f : ℕ → ℚ,
f(n) ≤ 2-1/(n+1) for all n
implies
f(n) < 2 for all n,
while the converse implication does not hold for all f : ℕ → ℚ.)
We prove this fact by induction.
– Base case: f₂(0) ≤ 2-1/(0+1) ≡ 1 ≤ 1 (by definitions).
– Induction step:
f₂(n+1) = f₂(n)+1/(n+2)² (by definition)
≤ 2-1/(n+1)+1/(n+2)² (by induction hypothesis)
= 2-1/(n+2)-1/(n+1)(n+2)² (by lots of elementary arithmetic)
≤ 2-1/(n+2) (by more or less obvious facts). □
∗∗
§3 Definitions
──────────────
What follows in this section is a reformulation and slight generalization of
some of the notions introduced by Hetzl and Wong (2017).
∗∗
DEFINITIONS.
– The ∗full (first-order) language of arithmetic∗, notation ℒ[full], is the
first-order language that for each natural number n has
– a constant symbol n,
– a function symbol f of arity n+1 for each function f : ℕⁿ⁺¹ → ℕ,
– a relation symbol P of arity n for each relation P ⊆ ℕⁿ.
– The ∗minimal (first-order) language of arithmetic∗, notation ℒ[min], is
the ℒ[full]-reduct with signature ⟨0,1,+,⋅,<⟩.
– A first-order language L is a ∗(first-order) language of arithmetic∗ if
and only if L is an ℒ[min]-expansion and an ℒ[full]-reduct.
∗∗
Thus a first-order language of arithmetic has as symbols natural numbers and
operations and relations on natural numbers. This is just a convenient "trick"
which allows us to easily define the standard model.
∗∗
DEFINITIONS. Let L be a language of arithmetic.
– The ∗standard L-model∗ has domain ℕ and each symbol interpreted as itself.
– An L-model not isomorphic to the standard L-model is a ∗non-standard
L-model∗.
– The L-theory ∗true L-arithmetic∗ is the theory of the standard L-model.
– Any subset of true L-arithmetic is a ∗theory of L-arithmetic∗.
∗∗
DEFINITION. Let L be a language of arithmetic and let φ(x) be an L-formula in
the free variable x. The ∗induction instance∗ for φ(x) is the L-sentence
IND(φ) :≡ φ(0)∧∀x(φ(x)→φ(x+1))→∀x.φ(x).
∗∗
DEFINITION. Let L be a language of arithmetic and let T be an L-theory. Let φ(x)
be an L-formula in the free variable x. Say that ∗T proves ∀x.φ(x) by
necessarily non-analytic induction∗ if and only if there is an L-formula ψ(x) in
the free variable x such that
(1) T,IND(φ) ⊬ ∀x.φ(x),
(2) T ⊢ φ(0),
(3) T ⊢ ψ(0),
(4) T ⊢ ∀x: ψ(x)→ψ(x+1),
(5) T ⊢ ∀x.ψ(x)→∀x.φ(x).
∗∗
REMARK. The above definition does not require T to be a theory of arithmetic
(that is, T could contain sentences false in the standard model). We will of
course require T to be a theory of arithmetic when using this definition to make
precise sense of the necessary non-analyticity of non-analytic induction proofs
(of arithmetic) found in the wild. But we do not rule out that there might be
interesting uses of the above definition with T not a theory of arithmetic.
∗∗
When trying to prove that typical T and φ(x) satisfy the above definition, the
hardest part will be——as far as we can tell at least——to show condition (1).
Therefore it makes sense to break out a lemma that captures the idea of using
non-standard models to establish (1).
∗∗
LEMMA. Let L be a language of arithmetic. Let φ(x) be an L-formula in the free
variable x such that ∀x.φ(x) is true in the standard L-model. Let T be an
L-theory such that T ⊢ φ(0). The following are then equivalent.
– T,IND(φ) ⊬ ∀x.φ(x).
– There is a non-standard L-model M ⊨ T and a non-standard number c in M
such that M ⊨ φ(c) and M ⊭ φ(c+1).
PROOF. By soundness and completeness,
T,IND(φ) ⊬ ∀x.φ(x)
is equivalent to
there is M ⊨ T,IND(φ) such that M ⊭ ∀x.φ(x)
which, since the conclusion of IND(φ) then is false in M, is equivalent to
there is M ⊨ T such that M ⊭ φ(0)∧∀x(φ(x)→φ(x+1)) and M ⊭ ∀x.φ(x)
which, since M ⊨ T ⊢ φ(0), is equivalent to
there is M ⊨ T such that M ⊭ ∀x(φ(x)→φ(x+1)) and M ⊭ ∀x.φ(x)
which is equivalent to
there is M ⊨ T and c in M such that M ⊭ φ(c)→φ(c+1) and M ⊭ ∀x.φ(x)
which is equivalent to
there is M ⊨ T and c in M such that M ⊨ φ(c) and M ⊭ φ(c+1) and
M ⊭ ∀x.φ(x)
which, dropping the now redundant M ⊭ ∀x.φ(x), is equivalent to
there is M ⊨ T and c in M such that M ⊨ φ(c) and M ⊭ φ(c+1)
which, since ∀x.φ(x) holds in the standard model, is equivalent to
there is nonstandard M ⊨ T and a non-standard number c in M such that
M ⊨ φ(c) and M ⊭ φ(c+1). □
∗∗
DEFINITION. The ℒ[min]-theory PA⁻ is axiomatized by the following.
– 0 and 1 are distinct:
0 ≠ 1.
– Associativity of addition and multiplication:
(x+y)+z = x+(y+z),
(x⋅y)⋅z = x⋅(y⋅z).
– Commutativity of addition and multiplication:
x+y = y+x,
x⋅y = y⋅x.
– Distributivity of addition over multiplication:
x⋅(y+z) = x⋅y+x⋅z.
– 0 is an additive identity and a multiplicative zero:
x⋅0 = 0.
– The order is irreflexive:
x ≮ x.
– The order is transitive:
x < y ∧ y < z → x < z.
– The order is total:
x < y ∨ x = y ∨ y < x.
– The order is discrete:
x = 0 ∨ x = 1 ∨ 1 < x.
– Addition and multiplication respect the order:
x < y → x+z < y+z,
x < y ∧ 0 ≠ z → x⋅z < y⋅z.
– Smaller elements can be subtracted from larger:
x < y → ∃z. x+z = y.
∗∗
FACTS.
– For all ℒ[min]-structures M: M ⊨ PA⁻ if and only if M is the non-negative
part of a nontrivial discretely ordered commutative ring.
– PA⁻ is a theory of ℒ[min]-arithmetic.
– PA ≡ PA⁻∪{IND(φ) : φ an ℒ[min]-formula in one free variable}.
∗∗
§4 Fact 1 must be proved by non-analytic induction
──────────────────────────────────────────────────
DEFINITION. ℤ[X] := ⟨ℤ[X],0,1,+,⋅,<⟩ is the ordered ring of polynomials in the
indeterminate X with coefficients in ℤ.
∗∗
Elements of ℤ[X] are polynomials
z₀+z₁X+z₂X²+⋅⋅⋅+zₙXⁿ
with z₀,z₁,...,zₙ in ℤ and if n ≠ 0 then zₙ ≠ 0. These can be divided into the
∗constants∗ polynomials
z (z in ℤ)
and the ∗non-constant∗ polynomials
z+pX (p in ℤ[X], z in ℤ).
∗∗
Addition, multiplication and subtraction in ℤ[X] are as expected. The order is
given by
z₀+z₁X+z₂X²+⋅⋅⋅+zₙXⁿ > 0 if and only if zₙ > 0,
p > q if and only if p-q > 0.
∗∗
DEFINITION. ℤ[X]⁺ = ⟨ℤ[X]⁺,0,1,+,⋅,<⟩ is the non-negative part of ℤ[X], that is,
a polynomial p from ℤ[X] is in ℤ[X]⁺ if and only if p ≥ 0.
∗∗
Elements of ℤ[X]⁺ are polynomials
z₀+z₁X+z₂X²+⋅⋅⋅+zₙXⁿ
with z₀,z₁,...,zₙ in ℤ and zₙ ≥ 0 and if n ≠ 0 then zₙ ≠ 0. The constant
polynomials are
n (n in ℕ)
and the non-constant polynomials are
z+pX (p in ℤ[X], z in ℤ, p > 0).
∗∗
FACT. ℤ[X]⁺ ⊨ PA⁻.
PROOF. ℤ[X]⁺ is the non-negative part of the nontrivial discretely ordered
commutative ring ℤ[X]. □
∗∗
DEFINITION. The language of arithmetic L₁ is ℒ[min] expanded with the function
symbol f₁.
∗∗
DEFINITION.
– The theory T₁ of L₁-arithmetic is defined by
T₁ := PA⁻, f₁(0) = 0, ∀x. f₁(x+1) = f₁(x)+2x+1.
– The L₁-formulas φ₁(x) and ψ₁(x) are defined by
φ₁(x) :≡ ∃y. f₁(x) = y⋅y,
ψ₁(x) :≡ f₁(x) = x⋅x.
∗∗
FACT. T₁ proves ∀x.φ₁(x) by necessarily non-analytic induction.
PROOF. We verify conditions (1)–(5) with ψ = ψ₁.
(2) Trivial.
(3) Trivial.
(4) The proof of Fact 1 given earlier can be straightforwardly formalized
in PA⁻.
(5) Trivial.
(1) We appeal to the lemma in §3 and exhibit a non-standard L₁-model M ⊨ T₁
and an element c in M such that M ⊨ φ(c) and M ⊭ φ(c+1). Let M be the
L₁-expansion of ℤ[X]⁺ with f₁ interpreted as follows.
f₁ᴹ(0) := 0,
f₁ᴹ(n+1) := f₁ᴹ(n)+2n+1,
f₁ᴹ(pX-1) := pX²
f₁ᴹ(pX-1+(n+1)) := f₁ᴹ(pX-1+n)+2(pX-1+n)+1,
f₁ᴹ(pX-1-(n+1)) := f₁ᴹ(pX-1-n)-2(pX-1-n)+1.
The right hand side of the last equation does indeed define a polynomial
of ℤ[X]⁺ since by construction the degree of f₁ᴹ(z+pX) is greater than the
degree of pX for all integers z and all p in ℤ[X]⁺. (We get the last
equation by solving
f₁ᴹ(pX-1-n) = f₁ᴹ(pX-1-(n+1)+1) = f₁ᴹ(pX-1-(n+1))+2(pX-1-(n+1))+1
for f₁ᴹ(pX-1-(n+1)).)
We then have
f₁ᴹ(X-1) = X²
which is a perfect square in M and we have
f₁ᴹ(X) = f₁ᴹ(X-1)+2(X-1)+1
= X²+2X-1
which is not a perfect square in M. Thus we have M ⊨ φ₁(X) and
M ⊭ φ₁(X+1). By construction we also have M ⊨ T₁ so we are done. □
∗∗
§5 Must Fact 2 be proved by non-analytic induction?
───────────────────────────────────────────────────
Since Fact 2 is a statement involving rationals, a little work is needed to
phrase it as a natural statement in first-order arithmetic (that is, without
involving any coding).
∗∗
DEFINITION. g : ℕ → ℕ and h : ℕ → ℕ are recursively defined by
g(0) := 1,
g(n+1) := (n+2)²g(n)+h(n),
h(0) := 1,
h(n+1) := (n+2)²h(n).
∗∗
We have
f₂(n) = g(n)/h(n)
so the inequality f₂(n) < 2 can be rewritten as
g(n) < 2h(n).
Similarly the inequality f₂(n) ≤ 2-1/(n+1) becomes
(n+1)g(n) ≤ (2n+1)h(n).
∗∗
All in all, we have the following rephrasings of Fact 2 and its proof attempt
and proof.
∗∗
LEMMA. For all natural numbers n, if (n+1)g(n) ≤ (2n+1)h(n) then g(n) < 2h(n).
PROOF. Suppose (n+1)g(n) ≤ (2n+1)h(n). Since (2n+1)h(n) < 2(n+1)h(n) we then
have (n+1)g(n) < 2(n+1)h(n) so we must have g(n) < 2h(n). □
∗∗
FACT 2'. g(n) < 2h(n) for all n.
PROOF ATTEMPT. Induction on n.
– Base case:
g(0) < 2h(0) ≡ 1 < 2⋅1 (by definition)
≡ 1 < 2.
– Induction step:
g(n+1) = (n+2)²g(n)+h(n) (by definition)
< (n+2)²⋅2h(n)+h(n) (by induction hypothesis)
But for any n we have (n+2)²⋅2h(n)+h(n) ≮ 2h(n). Thus we are "stuck".
ACTUAL PROOF. By the lemma, it suffices to prove
(n+1)g(n) ≤ (2n+1)h(n) for all n.
We prove this by induction on n.
– Base case:
(0+1)g(0) ≤ (2⋅0+1)h(0) (by definition)
≡ 1⋅1 ≤ 1⋅1
≡ 1 ≤ 1.
– Induction step: Our induction hypothesis is
(IH) (n+1)g(n) ≤ (2n+1)h(n)
and we must show
(GOAL) (n+2)g(n+1) ≤ (2n+3)h(n+1).
We have
(n+2)g(n+1) = (n+2)((n+2)²g(n)+h(n))
= (n+2)³g(n)+(n+2)h(n)
and
(2n+3)h(n+1) = (2n+3)(n+2)²h(n)
= (2n+3)(n+2)(n+2)h(n)
= (2n²+7n+6)(n+2)h(n)
= (2n²+7n+5)(n+2)h(n)+(n+2)h(n)
so (GOAL) is equivalent to
(n+2)³g(n) ≤ (2n²+7n+5)(n+2)h(n),
which is equivalent to
(n+2)²g(n) ≤ (2n²+7n+5)h(n),
which we have by
(n+2)²g(n) = ((n+1)+1)²g(n)
= ((n+1)²+2(n+1)+1)g(n)
= ((n+1)²+2(n+1))g(n)+g(n)
= (n+3)(n+1)g(n)+g(n)
≤ (n+3)(2n+1)h(n)+g(n) (by (IH))
≤ (n+3)(2n+1)h(n)+2h(n) (by Lemma and (IH))
= (2n²+7n+5)h(n). □
∗∗
REMARK. We find it a bit curious that the proof we gave of Fact 2 uses only one
application of the induction hypothesis, while the above proof of Fact 2' uses
two applications. Is there a proof of Fact 2' which, in some precise sense, uses
only one application of the induction hypothesis?
∗∗
DEFINITION.
– The language of arithmetic L₂ is ℒ[min] expanded with the function symbols
g and h.
– The L₂-sentences DEF(g) and DEF(h) and the L₂-formulas φ₂(x) and ψ₂(x) are
defined by
DEF(g) :≡ g(0) = 1 ∧ ∀x. g(x+1) = (x+2)⋅(x+2)⋅g(x)+h(x)
DEF(h) :≡ h(0) = 1 ∧ ∀x. h(x+1) = (x+2)⋅(x+2)⋅h(x),
φ₂(x) :≡ g(x) < 2⋅h(x),
ψ₂(x) :≡ (x+1)⋅g(x)+h(x) ≤ 2⋅(x+1)⋅h(x).
∗∗
CONJECTURE. There is an L₂-theory T ⊇ PA⁻ of arithmetic such that
(1) T ⊢ DEF(g),
(2) T ⊢ DEF(h),
(3) T proves ∀x.φ₂(x) by necessarily non-analytic induction.
∗∗
Adapting the proof of the previous section——cleverly interpreting function
symbols on ℤ[X]⁺——will not work to settle the above conjecture, as the unique
L₂-expansion M of ℤ[X]⁺ that satisfies DEF(g) and DEF(h) has gᴹ(p) = hᴹ(p) = 0
for all non-constant polynomials p. In fact, if M ⊨ DEF(h) is the non-negative
part of a discretely ordered commutative polynomial ring R[X] then hᴹ(p) = 0 for
all non-constant polynomials——for if hᴹ(p) ≠ 0 for some non-constant polynomial
p then the degrees of hᴹ(p), hᴹ(p-1), hᴹ(p-2), ... would form an infinitely
descending chain of natural numbers. It does not help if M instead is the
non-negative part of a discretely ordered commutative ring R[X,X⁻¹] of Laurent
polynomials——in that case if hᴹ(p) ≠ 0 for some non-constant polynomial p then
there is a natural number n such that the degree of hᴹ(p-n) is less than its
order. For more details see §A.
∗∗
§6 Future work
──────────────
One line of future work would of course be to settle the conjecture in §5.
∗∗
In §4 we expanded ℤ[X]⁺ to an L₁-model M in order to show that T₁ proves
∀x.φ₁(x) by necessarily non-analytic induction. For each sentence σ of true
L₁-arithmetic false in M it is natural to ask whether adding σ to T₁ lets us
prove ∀x.φ₁(x) with an analytic induction proof. One simple sentence of true
L₁-arithmetic that is false in M is "all numbers are odd or even", that is
σ₁ :≡ ∀x∃y: x = y+y ∨ x = y+y+1.
∗∗
CONJECTURE. T₁∪{σ₁} proves ∀x.φ₁(x) by necessarily non-analytic induction.
∗∗
To more systematically settle conjectures like the one above one could attempt
to establish more general results——instead of hand-crafting countermodels for
each particular case. We hope that the literature on first-order arithmetic
already contains lots of applicable results.
∗∗
Veryfing provability in weak fragments of arithmetic is hard. It is easy to
rely on something true that is not provable in the fragment one works with. Thus
it would be worthwhile to verify the provability statements in §4 with a theorem
prover.
∗∗
An interesting future line of work would be to consider other settings than
arithmetic. For example, in computer science, many basic facts of functions on
inductive structures seem to require non-analytic induction proofs.
∗∗
One might also approach the problem of non-analytic induction proofs from the
more proof-theoretical side, for example by studying derivations in natural
deduction. Dag Prawitz's (2018) recent work may be useful.
∗∗
§A Some results
───────────────
DEFINITIONS. Let p be a polynomial in the inderminate X or let p be a Laurent
polynomial in the indeterminates X and X⁻¹.
– The ∗degree∗ of p, notation deg(p), is the largest n such that the
coefficient of Xⁿ is non-zero.
– The ∗order∗ of p, notation ord(p), is the smallest n such that the
coefficient of Xⁿ is non-zero.
∗∗
Examples.
– deg(X³+4) = 3.
– ord(X³+4) = 0.
– deg(X²+20X⁻⁵) = 2.
– ord(X²+20X⁻⁵) = -5.
∗∗
LEMMA. Let R[X]⁺ be the non-negative part of a discretely ordered commutative
ring of polynomials. If f : R[X]⁺ → R[X]⁺ satisfies
f(p+1) = (p+2)²f(p)
for all non-constant polynomials p then f(p) = 0 for all non-constant
polynomials p.
∗∗
PROOF. Let p be a non-constant polynomial. Note that if f(p) ≠ 0 then f(p-1) ≠ 0
and deg(f(p)) > deg(f(p-1)). Thus if f(p) ≠ 0 for some non-constant polynomial p
we have the contradiction that we have an infinitely descending chain of natural
numbers:
deg(f(p)) > deg(f(p-1)) > deg(f(p-2)) > ⋅⋅⋅ □
∗∗
LEMMA. Let R[X,X⁻¹]⁺ be the non-negative part of a discretely ordered
commutative ring of Laurent polynomials. If f : R[X,X⁻¹]⁺ → R[X,X⁻¹]⁺ satisfies
f(p+1) = (p+2)²f(p)
then f(p) = 0 for all non-constant polynomials p.
∗∗
PROOF. Let p be a non-constant polynomial. As in the previous proof, note that
if f(p) ≠ 0 then deg(f(p)) > deg(f(p-1)). Also note that that
ord(f(p)) = ord(f(p-1)). Thus if f(p) ≠ 0 for some non-constant polynomial p
we have the contradiction that for some natural number n we have
deg(f(p-n)) < ord(f(p-n)). □
∗∗
REMARK. We could have used the above proof for the previous lemma too.
∗∗
FACT. Let M be an L₂-structure that is the non-negative part of a discretely
ordered commutative ring of polynomials, or of Laurent polynomials.
(1) If M ⊨ DEF(h) then hᴹ(p) = 0 for all non-constant polynomials p.
(2) If M ⊨ DEF(h)∧DEF(g) then gᴹ(p) = 0 for all non-constant polynomials p.
PROOF.
(1) The appropriate lemma is immediately applicable.
(2) Suppose M ⊨ DEF(h)∧DEF(g). Let p be a non-constant polynomial. We have
gᴹ(p+1) = (p+2)²gᴹ(p)+hᴹ(p) (by M ⊨ DEF(g))
= (p+2)²gᴹ(p) (by (1) and M ⊨ DEF(h)).
Thus the appropriate lemma gives gᴹ(p) = 0 for all non-constant
polynomials p. □
∗∗
REFERENCES
──────────
Hetzl, Stefan and Tin Lok Wong (2017): "Some observations on the logical
foundations of inductive theorem proving", Logical Methods in Computer Science
13(4).
Prawitz, Dag (2018): "The concepts of proof and ground", preprint.