Document [original]

Consistency Decision I

Self-Inconsistency

Michael Pfender∗

July 14, 2016

Abstract

The consistency formula for g¨odelian Arithmetics Tcan

be stated as free-variable predicate in terms of the categorical

theory PR of primitive recursive functions/maps/predicates.

Free-variable p. r. predicates are decidable by g¨odelian the-

ory T,key result, built on recursive evaluation of p. r. map

codes and soundness of that evaluation into theories T: inter-

nal, arithmetised p. r. map code equality is evaluated into map

equality of T.In particular the free-variable p. r. consistency

predicate of Tis decided by T.Therefore, by G¨odel’s second in-

completeness theorem, g¨odelian quantified Arithmetics Tturn

out to be self-inconsistent.

∗michael.pfende[email protected]erlin.de

Contents
Cartesian language CA 4
1 Fundamental object language symbols . . . . . 4
2 Cartesian category axioms . . . . . . . . . . . . 5
Primitive Recursion PR 14
1 Iteration axioms added . . . . . . . . . . . . . . 14
2 Full schema of primitive recursion . . . . . . . 16
3 Predicate abstraction PRa ........... 18
Numerals and universal set 20
Evaluation 24
1 Evaluation of PR into “set” theory T..... 25
2 Evaluation Theorem . . . . . . . . . . . . . . . 28
PR Stimmigkeit with T 30
1 Internal notion of equality . . . . . . . . . . . . 30
2 PR evaluation Stimmigkeits Theorem . . . . . 31
Decision of PR predicates 37
G¨odel’s incompleteness theorems 39
Inconsistency provability 40
1 Proof R´esum´e: . . . . . . . . . . . . . . . . . . 41
2 Discussion..................... 42
Appendix: Iterative evaluation 44
2

Introduction

The formula which expresses in a g¨odelian (quantified) arith-

metical theory Tthe consistency of Tcan be stated as free-

variable primitive recursive predicate in terms of the categorical

theory PR of primitive recursive (“p. r.”) maps/predicates.

Free-variable p. r. predicates are decided by a quantified

arithmetical theory Tsatisfying an axiom of finite descent –

of chains in linearily ordered semiring [ω] of polynomials in

one indeterminate ω(thought “big”), coeﬃcients in .1

This Decision Theorem is our key result. It builds on re-

cursive, Complexity Controlled Iterative evaluation of primi-

tive recursive map codes and Stimmigkeit/soundness of that

evaluation into T: Internal, arithmetised primitive map code

equality is evaluated into map equality of theory T.

In particular the free-variable primitive recursive consis-

tency predicate ConTof theory Tis decided by T.This de-

cision gives, by G¨odel’s second incompleteness theorem, self-

inconsistency of theory Tas final result.

The Appendix is to give a detailed construction and proof

for resolution of double recursive PR map code evaluation into

a CCI: Complexity Controlled Iteration with complexity val-

ues in [ω] which has only finite descending chains: is an or-

dinal in terms of first order set theory, subsystem of Principia

Mathematica PM “und verwandte Systeme” as in particular

Zermelo-Fraenkel set theory ZF.

Theory basis both for present negative approach to classical

foundations as well as for self-consistency of (recursive) itera-

1set theories satisfy finite descent since ωωthere is an ordinal

tive descent theory πRstrengthening PR (within the monog-

raphy Arithmetical Foundations2) is exposition of fully for-

malised free-variables cartesian categorical theory PR of prim-

itive recursion.3

It comes in two levels: First Categorical cartesian lan-

guage CA generated over a (proto) natural numbers object

−→ s

−→ – zero and successor functions – and second, built

on this, axioms and fundamental theorems making into an

NNO (Natural Numbers Object) in the sense of availability of

endo map iteration and the schemata of primitive recursion

proper: Theory PR of primitive recursion.

These explicit axioms, lemmata and theorem are stated for

reference in later sections of present paper as well as for the

corresponding sections of positive second paper.

1 Cartesian language CA

1.1 Fundamental object language symbols

{, , ×,0,s,id,◦,Π,�,r}

2Pfender 2016c

3Manin 2010 “treats, among other things, a categorical approach to the theory

of computation, quantum computation, and the P/NP problem.” In Foundations

let us use here categorical language with its absence of formal variables for in-

dividuals: categories have only objects and maps as fundamental notions. This

circumstance makes coding – g¨odelisation – of categorical theories comparably

simple. In cartesian categories, free variables (re)enter as names for identic maps

and projections out of (cartesian) products. So Free-Variables primitive recursive

Arithmetic comes back in a conveniently codable way.

is the one-element object, the natural numbers object

of theories CA and PR to come, ×the cartesian product of

objects and of maps.

0isthezero constant 0: →,s is the “fundamental”

successor function s:→

Identity id is the family of identity maps to all objects

obained out of and by cartesian product ×,◦is map com-

position occasionally replaced by concatenation, Πsymbolises

the family of terminal maps into object ,�and r are left resp.

right projections out of cartesian product(s) A×B

Theory PR of primitive recursion below will come with an

additional symbol §for endomap iteration.

1.2 Cartesian category axioms

•Ax [ ]

{Obj ,}

one-element object and natural numbers object

map 0: →zero constant

map s: →successor function

Obj A

Ax [id]

map idA=id:A→Aidentity map

map f

Ax [ reflexivity ]

f=f

map f,g;

f=g

Ax [ symmetry ]

g=f

map f,g,h;

f=g;g=h

Ax [ transitivity ]

f=h

f:A→B;g:B→C

Ax [ ◦]

map (gf)=(g◦f)=g(f):A→C

(g◦f):A→B→Ccomposition

outmost brackets may be omitted

f, ˜

f:A→B;g:B→C;f=˜

Ax [ ◦sub ]

g◦f=g◦˜

fLeibniz’ substitutivity

f:A→B;g, ˜g:B→C;g=˜g

Ax [sub◦]

g◦f=˜g◦fsecond Leibniz substitutivity

f:A→B

Ax [ ◦id ]

f◦id = f◦idA=f

id ◦f=id

B◦f=f

neutrality of identities to composition

f:A→B;

var a∈A, a := idA

Lem [ ◦var ]

f(a)=f(idA)=f◦idA=f

free variable as identity

f(a)∈B“dependent variable”

f:A→B;g:B→C;h:C→D

var a∈A

•Ax [ ass ◦]

(h◦g)◦f=h◦(g◦f):A→D

=h◦g◦f=hgf =h(g(f(a))))

associativity of composition

Numerals:

0: →numeral.

n:→numeral

n+1=sn=(s◦n): →numeral

Cartesian structure:

Obj A

Ax [Π]

map Π=Π

A:A→terminal map

f:A→

Ax [!Π]

f=Π

uniqueness, naturality of family Π

diagram: Af��

��

id ��

Remark: This naturality axiom for family Πwill not hold

in half-terminal monoidal categories introduced in Budach &

Hoehncke 1975, and to be considered “marginally”: Theory

P�

Ra of partially defined recursive maps.

Obj A, B

•Ax [Obj×]

Obj (A×B)

cartesian product of objects

[ Outmost brackets may be omitted ]

Obj A, B

var a∈A, var b∈B

•Ax [ �,r]

map a=�=�A,B :A×B→A

map b=r=r

A,B :A×B→B

left resp. right projection,

variables as projections

map f:C→A, g :C→B

•Ax [indu]

map (f,g):C→A×B

induced map into product

�◦(f,g)=f, r◦(f,g)=g

diagram

f��

(f,g)��

��

A×B

�

��

f, ˜

f:C→A;g, ˜g:C→B;

f=˜

f;g=˜g

Ax [ sub( ,)]

(f,g)=(˜

f,˜g)

compatibility of inducing with ‘=’

h:D→C, f :C→A, g :C→B

Ax [ distr ]

(f,g)◦h=(f◦h, g ◦h):D→(A×B)

distributivity of ◦over forming

induced map into product

var c∈C, c := idC

[ Lem ]

�◦(f,g)(c)=�◦(f(c),g(c)) = f(c)

r◦(f,g)(c)=r◦(f(c),g(c)) = g(c)

q. e. d.

h:C→(A×B)

Ax [ retr.pairing ]

(�A,B ◦h, rA,B h)=h

pairing is retractive

even isomorphic

f:C→A;g:C→B;h:C→(A×B);

�A,B ◦h=f;r

A,B ◦h=g

Lem [!( ,)]

h=(f,g)

uniqueness of induced map

Proof:

h=id

A×B◦h

=(�A,B ◦idA,B,rA,B ◦idA,B)◦h[retr.pairing]

=(�A,B,rA,B)◦h

=(�A,B ◦h, rA,B ◦h) [distr]

=(f,g):C→A×B[sub( ,)]

Obj A, B

Lem [(�,r) ]

(�A,B,rA,B)=id

A×B

Proof: uniqueness of induced into product A×B

f:A→A�,g:B→B�

var a:= �A,B,b:= rA,B

Def [×maps ]

(f×g)=(f◦�, g ◦r) : (A×B)→(A�×B�)

f×g=(f×g)(a, b)=(f(a),g(b))

cartesian map product

f:A→A�,g:B→B�

[ unary ×]

(A×g)=

def (idA×g):A×B→A×B�

(f×B)=

def (f×idB):A×B→A�×B

map f:A→A�,g:B→B�

Thm [ nat�,r ]

�◦(f×g)=f◦�;r◦(f×g)=g◦r

naturality of projection families �and r

Proof: uniqueness of induced map into product A�×B�

Diagram:

Af��

A�

A×B

�

��

f×g��

��

A�×B�

�

��

Bg��B�

f:A→A�,f

�:A�→A��;

g:B→B�,g

�:B�→B��

Thm [×◦]

idA×idB=id

A×B:A×B→A×B

(f�◦f)×(g�◦g)=(f�×g�)◦(f×g):

(A×B)→(A�� ×B��)

bifunctoriality of cartesian product

Proof: uniqueness of induced maps into products

commuting diagram:

Af��A�f�

��A��

(A×B)

�

��

(f×g)��

((f�f)×(g�g))

��

(A�×B�)

�

��

(f�×g�)��(A�� ×B��)

�

��

Bg��B�g�

��B��

2 Primitive Recursion PR

2.1 Iteration axioms added

f:A→A, var a∈A, var n∈

Ax [ §]

f§=f§(a, n):A× → A

f§(a, 0) := f§(idA,0Π

A)=a=id

f§◦(A×s) = f§(a, sn)

=f◦f§=f(f§(a, n)) : A× → A→A

fn(a):=f§(a, n)

apply iteratively ntimes endomap f

to initial argument a

diagram:

A×A×s��

f§

��

A×

f§

��

(id,0) ��

�

id ��

�

�=(§)

Af��A

f:A→B;g:B→B;h:A× → B;

var a∈A, var n∈;

h(a, 0) = f(a);

h(a, sn)=gh(a, n)

Ax [FR!]

h=g§(f×id )i.e.

h(a, n)=gn(f(a)) :

Freyd’s uniqueness of iterated endomap g

initialised by a map f

[g§(f×id ) does the job ]

diagram4

A×A×s��

��

�

g§◦(f×)

��

A×

��

�

g§◦(f×)

��

(idA,0)

��

�

��

�

�== = =

Bg��B

f, ˜

f:A→A;f=˜

Lem [§]

f§=˜

f§:A× → A

uniqueness of “simple” iterated endo f

4Freyd 1972

Proof:

f=f

entails ˜

f§(a, 0) = idA

and ˜

f§(a, s n)= ˜

f◦˜

f§(a, n)=f◦˜

f§(a, n); [sub ◦]

entails

f§=f§◦(idA×)by[FR!]

=f§◦(idA×)=f§

2.2 Full schema of primitive recursion

g=g(a):A→B

h=h((a, n),b):(A×)×B→B

Def Thm [pr]

f=f(a, n):A× → Bs. t.

(anchor) f(a, 0) = g(a) and

(step) f(a, sn)=h((a, n),f(a, n))

f=: pr[g,h]

(pr!) uniqueness of fto satisfy

these (anchor) and (step) equations.

Interpretation:

general primitive recursive map f=f(a, b)initialised by a

map g=g(a)and iteratively extended using a step map h=

h((a, n),b)which depends on previous value bbut (possibly)

also from initial argument aas well as from running recursion

parameter n

Schema (pr) without use of free variables:

g:A→B,

h:(A×)×B→B

(pr)

pr[g,h]:=f:A× → B

f(idA,0) = g:A→B

f(idA×s) = h(idA×,f):

(A×)→(A×)×B→B

(pr!) : funique

Schema (pr) is a consequence of iteration schema (§) and

uniqueness of the initialised iterated h, this taken above as

axiom (FR!)

Remark: Full schema (pr) of primitive recursion is an ax-

iom in the classical theory of primitive recursion, subsystem

of any arithmetical theory T.

Free-Variables Arithmetics of the natural numbers ,the

integers ,and the rationals can be based on the axioms of

the cartesian theory PR of primitive recursion as defined by

the axioms introduced in the above. Goodstein’s5uniqueness

axioms U1to U4basic for his Free-Variables Arithmetics are

theorems of PR.

5Goodstein 1971

2.3 Predicate abstraction PRa

We discuss a p. r. abstraction scheme as a definitional en-

richment of PR into theory PRa of PR decidable objects and

PR maps in between, decidable subobjects of the objects of

PR.

The extension PRa is given by adding schemes (ExtObj),

(ExtMap),and (Ext=) below. Together they correspond to the

scheme of abstraction in set theory, and they are referred as

schemes of PR abstraction.

Our first predicate-into-object abstraction scheme is

χ:A→aPR-predicate:

sign ◦χ=¬¬χ=χ:A→ →

(ExtObj)

{A:χ}object (of emerging theory PRa)

Subobject {A:χ}⊆Amay be written alternatively with

bound variable aas {A:χ}={a∈A:χ(a)}

Example: The subdiagonal grid

{×:≤}={(a, b)∈ × :a≤b}⊂×

The maps of PRa =PR + (abstr) come in by

{A:χ},{B:ϕ}PRa-objects

f:A→BaPR-map

PR �χ(a)=⇒ϕf(a)i.e.

[χ=⇒ϕ◦f]=

PR trueA:AΠ

−→ 1

−→

(ExtMap)

fis a PRa-map f:{A:χ}→{B:ϕ}

A posteriori we introduce, following Reiter 1982, the for-

mal truth Algebra as

=def {n∈:n≤s0}

with proto Boolean operations on restricting – in codomain

and domain – to boolean operations on resp.

×={(m, n)∈ × :m, n ≤s0}

Definition of cartesian product of objects within PRa.

PRa-maps with common PRa domain and codomain are

considered equal, if their values are equal on their defining

domain predicate. This is expressed by the scheme

f, g :{A:χ}→{B:ϕ}PRa-maps

PR �χ(a)=⇒f(a).

=Bg(a)

(Ext=)

f=g:{A:χ}→{B:ϕ}

explicitly:

f=PRa g:{A:χ}→{B:ϕ},also noted

PRa �f=g:{A:χ}→{B:ϕ}

Structure Theorem for the theory PRa of primitive re-

cursion with predicate abstraction: 6

•PRa is a cartesian p. r. theory

•Theory PR is cartesian p. r. embedded

•Theory PRa has (universal) extensions of all of its pred-

icates and boolean truth object noted as codomain of

these predicates, with truth values false ≡0,true ≡1≡

s0: →as well as predicative equalities m.

=n:

× → ,a .

=˜a:A×A→and map definition by

case distinction

•PRa has all finite (projective) limits, in particular equalis-

ers, pullbacks and kernel pairs

•PRa has (binary) sums (coproducts) and coequalisers of

kernel pairs, of equivalence predicates.

3 Numerals and universal set

Objective numerals revisited

num(0) ≡0: →

num(1) = s(0) = s◦0: → →

num(n+ 1) ≡n+1=s◦n=s(n): →

n∈Nmeta-variable over “naive” natural numbers

6see Pfender,Kr¨

oplin,Pape 1994

Internal numerals

Numeralisation ν=ν(n): →is p. r. defined by

ν(0) = �0�:→

g¨odel number, utf8 code of 0

ν(1) = �s�∗�◦�∗�0�:→

string concatenation of symbol codes,

ν(sn)= �s�⊙ν(n)∈,⊙≡ �◦�

This internal numeralisation distributes the “elements” (num-

bers) of the NNO over ,with suitable gaps to receive in

particular any other symbols of object language PR.

Predicate Lemma: Enumeration ν:→defines a

characteristic p. r. image predicate im[ν]: →and by this

PRa object

˙=ν={:im[ν]}∼

of (enumerated) internal numerals

Proof of Lemma: Use iterative ‘or’ for definition of im[ν]:

im[ν](c)=∨n≤c[c.

=ν(n)]

ν:→has codomain restriction ν:→˙={:im[ν]}

and is then an iso with p. r. inverse

ν−1=ν−1(c)=min{n≤c:ν(n).

=c}:˙∼

−→ q. e. d.

Extend numeralisation to object by

ν=ν(0) = �0�∈˙=ν={�0�}∼

and definition of (nested) numpairs and predicative numpair

sets by

A, B PR objects, νA:→A, νB:→B

A={A:im[νA]},˙

B={B:im[νB]}⊂given

�A˙

×B�={:im[νA×B]}⊂constructed by

νA×B(a, b)=�ν(a); νB(b)�:A×B→

im[νA×B](c)=∨n≤c[c=νA×B(n)] : →

Abbreviations:

•�...�=�(�... �)�

•⊙=�◦�

•˙

×=�×�

•;=�,�

Universal set

Define universal set ={:}⊂of all numerals ν(n)

and (possibly nested) numpairs first by p. r. enumeration

�0�∈

n∈=⇒�s�⊙ν(n)∈

x∈ ∧ y∈=⇒�x;y�∈

This enumeration has characteristic p. r. image predicate

= (c): →defined as follows:

(c)=





true if ∨n≤cct (n)=c

false otherwise, i. e. if ∧n≤cct (n)�=c

ct :→is the p. r. enumeration/counting process given

by cyclic application of the rules above generating as a “set”,

analogon to Cantor count

ct ×:∼

−→ ×∼

−→ � ˙

×�⊂

Variable c∈works in fact as an upper bound, since obviously

ct (n)>n, n∈free.

Numeral Theorem

•ν:→has a retraction ν−:�˙∼

−→

•analogously for all objects Aof theory PR :

νA:A→has a retraction ν−:�˙

A∼

−→ A

•these make up a natural equivalence ν=[νA]A(out of

PRa iso maps), see commutative diagram below, where

f=νB◦f◦ν−1

A:˙

A→˙

B, and

f=˚

f(x)=











f(x)∈˙

B⊂ ⊂ ⊥

=∪{�⊥�}for x∈˙

xfor x∈⊥�˙

(undefined argument)

diagram:

Af��

∼

��

∼

��

f��

⊂

��

⊂

��

⊥

f��

�

��

⊥

�

��

4 Evaluation

From now on we place ourselves in a “g¨odelian” quantified

arithmetical frame theory Tstrengthened by the following axiom

schema (fin desc) of finite descent of chains in linear order

of semiring [ω] of polynomials in indeterminate ω(thought

“big”), coeﬃcients in :

qn=qn(ω): →[ω]

descending chain above 0 in [ω]

(fin desc)

∃m∈qm(ω)≡0

Such frame theory Tis a subsystem of Principia Math-

ematica PM,of Zermelo-Fraenkel set theory ZF,and of von

Neumann-G¨odel-Bernays set theory NGB.First-order subsys-

tems of these theories suﬃce. Cf. the classical arithmetical

theories Tas considered in Smorynski 1977, part D.1 in the

Handbook of Mathematical Logic, here strengthened by schema

(fin desc).

These “set” theories Tare considered as extensions (in lan-

guage and theorems) of cartesian p. r. theory PRa with pred-

icate abstracction. Such classical extension Tis to have in

particular p. r. enumerated subsets of NNO and p. r. count-

able unions of such subsets as subsets of .Schema (fin desc)

is to guarantee termination of evaluation of PR map codes.

4.1 Evaluation of PR into “set” theory T

We define T-recursively an evaluation

eva :PR×⊥−→ ⊥

of PR map code set

PR = ∪A,B[A, B]PR ⊂

on numerals and (nested) numpairs out of

=∪A˙

A⊂of forgoing section,

universal set for theories CA as well as PR (and PRa) within

theory T,augmented by symbol ⊥=�⊥�∈for trash

element – into ⊥=∪{⊥}⊂

With objects , , A, B, C, A�,B�considered as PR objects

as well as Tsets, with coding – g¨odelisation –�f�of (CA and)

PR, and with

‘;’ = �,��...�=�(�... �)�,⊙=�◦�,˙

×=�×�,˙

§=�§�

we define

Basic map/function code evaluation eva :

eva(�0�,�0�)= �0�∈˙⊂

Obj(A),a∈˙

A⊂ ⊂

⇓

eva(�id�,a)=a

n∈

⇓

eva(�s�,ν(n)) = ν(s n)∈˙⊂

Obj(A),a∈˙

⇓

eva(�Π�,a)= �0�∈˙⊂

Obj(A),Obj(B),a∈˙

A, b∈˙

⇓

eva(��,�a;b�)=a

eva(�r�,�a;b�)=b

Put together:

ba ∈bas = {id,0,s,Π,�,r}

={idA,0,s,ΠA,�

A,B,rA,B :ObjA, B}⊂PR

A= Dom[ba],B= Codom[ba],a∈˙

⇓

eva(�ba�,a)=νB(ba(ν−1

A(a))) ∈˙

B⊂

eva(ba,x)=⊥for x∈(⊥�˙

Evaluation of composed map codes:

f∈[A, B],g∈[B,C],a∈˙

(compos) ⇓

eva(g⊙f,a)=eva(g,eva(f,a)) ∈˙

C⊂

formally (and for PR instead of CA in fact)

double recursive

f∈[C, A]⊂PR ⊂,g∈[C, B]⊂PR

c∈˙

C⊂

(indu) ⇓

eva(�f;g�,c)=�eva(f,c); eva(g,c)�

∈�A˙

×B�=ν(A×B)⊂

primitive recursive

f∈[A, A�]⊂PR,g∈[B,B�]⊂PR

a∈˙

A, b∈˙

(×)⇓

eva(�f˙

×g�,�a;b�)=�eva(f,a); eva(g,b)�

∈�A�˙

×B��⊂

(redundant)

f∈[A, A],a∈˙

(anchor it) ⇓

eva(f˙

§,(a,�0�)) = a

f∈[A, A],a∈˙

A, n ∈

(step it) ⇓

eva(f˙

§,(a,�s�⊙νn)

=eva(f,eva(f˙

§,(a,νn)) ∈˙

double recursive

inner recursion on n

f∈[A, B],x∈⊥�A

(trash) ⇓

eva(f,x)=⊥ ∈ ⊥

in particular:

f∈[A, A],x∈⊥��A˙

× �

(trash it) ⇓

eva(f˙

§,x)=⊥

4.2 Evaluation Theorem

(i) Double recursion above defines a total T-map

eva =eva(f,x):PR×⊥→⊥

(ii) eva is characterised within g¨odelian Arithmetics Tby

eva(�ba�,x) = ba(x)

for ba ∈bas (basic map constants)

eva(g⊙f,a)=eva(g,eva(f,a))

eva(�f;g�,c)=�eva(f,c); eva(g,c)�

eva(�f˙

×g�,�a;b�)=�eva(f,a); eva(g,b)�

as well as

eva(f˙

§,�a;�0��)=aand

eva(f˙

§,�a;ν(s n�)=eva(f,eva(f˙

§,�a,νn�)

a∈˙

A, b∈˙

B, c∈˙

C, n ∈all free

eva(f,x)=⊥for x∈(⊥�Dom[f])

(iii) eva defines within theory Ta (natural) family

ev =evA,B =evA,B(f,a):[A, B]×A→B

A, B PR objects by

evA,B(f,a)=ν−1

B◦eva(f,ν

A(a)) :

[A, B]×A∼

−→ [A, B]×˙

Aeva

−−→ ˙

B∼

−→ B

(iv) This family ev =evA,B is (jointly) objective:

f:A→BPR map, a∈Afree

ev(�f�,a)=evA,B(�f�,a)=f(a)∈B

Totality of this map – this map family – defined by an Ack-

ermann type double recursion is certainly believed in set the-

ory, but bears a problem constructively. In the Appendix we

resolve this map into a CCI,aComplexity Controlled Iteration

which always terminates, at least within quantified arithmeti-

cal theories T– with finite descent (fin desc) – as frame. The

corresponding Evaluation Resolution Theorem of the Appendix

then infers present Evaluation Theorem.

5 PR Stimmigkeit with T

5.1 Internal notion of equality

For cartesian p. r. theory PR we have the objective notion of

map equality

=k:N→PR ×PR

(k:→)�→ �f=kg�

externally p. r. enumerated. Numeral

k:0

−→ s

−→ ... s

−→ “in N”isametafree external

counting index.

PR map equality pairs �f=kg�=�f,g�kcome in se-

quentially by (external) p. r. enumeration of (binary) deduction

trees.

This enumeration has an internal p. r. equality enumeration

analogon

ˇ= k:→PR ×PR ⊂ ×

k�→ (fˇ= kg),k∈free

where we write fˇ= kgfor

ˇ= k.

=(f,g)∈PR ×PR

given by p. r. count of internal deduction trees, example: For

k∈suitable a transitivity-of-equality deduction tree has

form

fˇ= kh

dtreek=⇑

fˇ= ig

⇑

dtreeii dtreeji

gˇ= jh

⇑

dtreeij dtreejj

i, j < k, ii, ji < i, ij, jj < j

5.2 PR evaluation Stimmigkeits Theorem

framed by quantified arithmetical theory Twith finite descent

in [ω]:

For p. r. theory PR with its internal notion of equality ‘ ˇ=’

we have for evaluation family

ev =[evA,B :[A, B]×A→B]A,B :

(i) PR to Tevaluation Stimmigkeit:

T�fˇ= kg=⇒ev(f,x)=ev(g,x)(•)

k∈,f,g∈PR,x∈all free

Substituting “concrete” PR codes into fresp. gwe get

by objectivity of evaluation ev :

(ii) T-framed objective soundness of PR to T:

For p. r. maps f,g :A→B

T��f�ˇ= k�g�=⇒f(a)=g(a)

k∈,a∈Aboth free

(iii) Specialising to case f:= χ:A→={0,1}ap.r.

predicate and to g: = true we get

T-framed logical Stimmigkeit of PR :

T�∃kProvPR(k, �χ�)=⇒∀aχ(a)

If ap.r.predicateis–withinT–PR-internally prov-

able by say kth proof, then it holds in Tfor all of its

arguments.

(iv) what we will need for decidability and consistency con-

siderations is equivalent subcase (equivalent via Cantor

count ctA:∼

−→ A)

T�∃kProvPR(k, �χ�)=⇒∀nχ(n)

χ=χ(n): →a numerical PR predicate

Proof of assertion (•) by primitive recursion on k, dtreek

the kth deduction tree of the theory proving its root equation

fˇ= kgThese (argument-free) deduction trees are counted in

lexicographical order.

Super Case of equational internal axioms, in particular

•associativity of (internal) composition:

�h⊙g�⊙fˇ= h⊙�g⊙f�=⇒

ev(�h⊙g�⊙f,a)=ev(�h⊙g�,ev(f,a))

=ev(h,ev(g,ev(f,a)))

=ev(h,ev(�g⊙f�,a)) = ev(h⊙�g⊙f�,a)

This proves assertion (•) in present associativity-of-com-

position case.

•Analogous proof for the other flat – equational – cases,

namely reflexivity of equality, left and right neutrality of

identities, Godement’s equations for the induced map:

��⊙�f;g�ˇ= f,�r�⊙�f;g�ˇ= g

and definition of cartesian product of maps via induced

map, as well as retractive pairing

��⊙h;�r�⊙h�ˇ= h

and distributivity equation

�f;g�⊙hˇ= �f⊙h;g⊙h�

for composition with an induced.

•proof of (•) for the last equational cases, iteration equa-

tions:

–iteration anchoring, equation

f˙

§⊙��id�;�0�⊙�Π��ˇ= �id�:

T�ev(f˙

§⊙��id�;�0�⊙�Π��,a)

=ev(f˙

§,(ev(�id�,a),ev(�0�,ev(�Π�,a)))

=ev(f˙

§,(a, ev(�0�,0))

=ev(f˙

§,(a, 0)) = a=ev(�id�,a)

–iteration step, case of genuine iteration equation

f˙

§⊙��id�˙

×�s��ˇ= (f⊙f˙

§)

where ˙

×is the internal cartesian product of map

codes:

T�ev(f˙

§⊙��id�˙

×�s��,(a, n))

=ev(f˙

§,ev(�id�˙

×�s�,(a, n)))

=ev(f˙

§,(a, sn))

=ev(f,ev(f˙

§,(a, n)))

=ev(f⊙f˙

§,(a, n))

[ Internal cartesian map product is defined as an internal

induced ]

Proof of PR to Tevaluation Stimmigkeit for the genuine

Horn case axioms, of form

fˇ= ig∧˜

fˇ= j˜

g=⇒hˇ= k˜

h,i,j<k

Transitivity-of-equality case

fˇ= ig∧gˇ= jh=⇒fˇ= kh

Evaluate here at argument a∈Aand get in fact

T�fˇ= kh

=⇒ev(f,a)=ev(g,a)∧ev(g,a)=ev(h,a)

by hypothesis fˇ= ig,gˇ= jh

=⇒ev(f,a)=ev(h,a):

transitivity export q. e. d. in this case

Compatibility case of composition with equality

gˇ= ig,fˇ= j˜

f=⇒g⊙fˇ= kg⊙˜

ev(g⊙f,a)=ev(g,ev(f,a)) = ev(g,ev(˜

f,a))

=ev(g⊙˜

f,a)

by hypothesis on fˇ= ˜

fand by Leibniz’ substitutivity in T

q. e. d. in this first compatibility case.

Case of compatibility of composition with equality in second

factor:

gˇ= i˜

g=⇒g⊙fˇ= k˜

g⊙f:

ev(g⊙f,a)=ev(g,ev(f,a)) = ev(˜

g,ev(f,a)) (∗)

=ev(˜

g⊙f,a)

(∗) holds by gˇ= i˜

gand induction hypothesis on i: arbitrary

argument, here ev(f,a)

This proves Stimmigkeits assertion (•) in this 2nd compat-

ibility case.

Compatibility case of internal formation of the induced

map with internal equality:

fˇ= i˜

f,gˇ= j˜

g=⇒�f;g�ˇ= k�˜

g;˜

f�:

ev(�f;g�,c)=(ev(f,c),ev(g,c)) = (ev(˜

f,c),ev(˜

g,c))

by hypothesis fˇ= i˜

f,gˇ= j˜

=ev(�˜

f;˜

g�,c)

Same for compatibility of internal cartesian map product with

equality (redundant).

(Final) case of Freyd’s (internal) uniqueness of the ini-

tialised iterated is case

h⊙��id�;�0�⊙�Π��ˇ= if

∧h⊙��id�˙

×�s��ˇ= jg⊙h

=⇒hˇ= kg˙

§⊙�f˙

×�id��(∗∗)

internal version of hunique, h=PR g§◦(f×id) in

A×A×s��

��

�

A×

��

�

(id,0Π)��

�

f��

�

Bg��B

Comment: his an internal comparison candidate fullfill-

ing the same internal p. r. equations as the initialised iterated

g˙

§⊙�f˙

×�id��It should be – is:Stimmigkeit – evaluated

equal to the latter on A×;hcorresponds to h, fto f, gto

g, and g˙

§⊙�f˙

×�id��to g§◦(f×id )

Stimmigkeits proof in this case

h⊙��id�,0�ˇ= if∧h⊙��id�˙

×s�ˇ= jg⊙h

=⇒hˇ= kg˙

§⊙��id�˙

×f�

is the following, by (structural) recursion on k:

ev(h,(a, 0)) = ev(f,a) (hypothesis on i<k)

=ev(g˙

§⊙�f˙

×�id��,(a, 0))

as well as – induction on n–

ev(h,(a, sn))

=ev(h⊙��id�˙

×�s��,(a, n))

=ev(g⊙h,(a, n)) (hypothesis on j<k)

=ev(g,ev(h,(a, n)))

=ev(g,ev(g˙

§⊙�f˙

×�id��,(a, n)))

by induction hypothesis on n

=ev(g⊙�g˙

§⊙�f˙

×�id��,(a, n))

=ev(g˙

§⊙�f˙

×�id��,(a, sn))

q. e. d.

6 Decision of PR predicates

We consider PR predicates χfor decision by quantified arith-

metical theorie(s) T(with finite descent in [ω]), without re-

striction of generality just predicates χ=χ(n): →

Basic tool for decision is T-framed evaluation-Stimmigkeit

of PR above, namely

χ=χ(n): →PR predicate

T�∃kProvPR(k, �χ�)=⇒∀nev(�χ�,n)=true

T�∃kProvPR(k, �χ�)=⇒∀nχ(n)

Within Tdefinefor χ:→a predicate out of PR a

partially defined predicate decision

∇χ=











false if ∃k¬χ(k)

true if ∃kProvPR(k, �χ�)

⊥otherwise i. e.

if ∀kχ(k)∧∀k¬ProvPR(k, �χ�)

(derivable but not provable)

:→ ∪ {⊥}={0,1,⊥}

well defined by Stimmigkeit/soundness

−−−−−−−−−−−−−−−−−

T�∃kProvPR(k, �χ�)=⇒∀nχ(n)

−−−−−−−−−−−−−−−−−

and same as

∇χ=











false if ∃k¬χ(k)

true if ∀kχ(k)∧∃kProvPR(k, �χ�)

⊥if ∀kχ(k)∧∀k¬ProvPR(k, �χ�)

Union of latter two cases gives

Decidability Theorem:

Complete T-alternative for PR predicates χ=χ(n): →:

•counterexample T�∃n¬χ(n)

or else

•theorem T�∀nχ(n)

Decision Remark: this does not mean a priori that de-

cision algorithm ∇χterminates for all such predicates χ.The

theorem says only that χis decidable “by”, within theory T,

that it is not independent of T.

7 G¨odel’s incompleteness theorems

We visit §2. G¨odel’s theorems, in Smorynski 1977, Handbook

of Mathematical Logic.

First Incompleteness Theorem. Let Tbe a formal

theory containing arithmetic. Then there is a sentence ϕwhich

asserts its own unprovability and such that:

(i) If Tis consistent, T�� ϕ

(ii) If Tis ω-consistent, T�� ¬ϕ

In §3.2.6 Smorynski discusses possible choices of arithmetic

theory, namely

(a) PRA = classical primitive recursive arithmetic.

(b) PA = Peano Arithmetic.

Conjecture: PA ∼

=PR +∃

and a bad example. It is bad because the whole encod-

ing problem is more easily solved in a set theory than in

an arithmetical theory. By the same token, it is a good

example.”

We take for formal extension Tof PR one of the categorical

pendants to g¨odelian quantified arithmetical theories – with

finite descent – (subsystems of ZF,see Osius 1974).

A minimal choice for our purposes – conjecture – is quan-

tified arithmetical theory T=PA +ωω:

PA + the lexicographic order on ωω⊃[ω] a well-order.

Smorynski’s proof gives the First G¨odel’s incompleteness

theorem for T,and from that the following

Second incompleteness theorem: Let Tbe one of the

quantified arithmetical theory extensions above of PR and T

consistent. Then

T�� ConT

where here ConT=¬∃kProvT(k, �false�) is the sentence

asserting the consistency of T.

The consistency formula ConTof Tis not derivable in

Metamathematics, even if theory Titself is taken as meta-

mathematical frame, provided that Tis consistent.

8 Inconsistency provability

Predicate ProvT(x, y) corresponds to G¨odel formula

45.xBy, x ist Beweis von y.

G¨odel proves that this formula is rekursiv, primitive recursive

in contemporary terms.

[ Later Ackermann found “Ackermann recursive” functions

growing faster than any “primitive recursive” function, evalu-

ation eva above is of this type ]

Formula 46.∃xxBy ‘yist beweisbar’ is a priori, formally

not primitive recursive, same as for “undecidable” formula 17 Gen r

But ConT=¬∃kProvT(k, �false�)=∀k¬ProvT(k, �false�)

corresponds to the free-variable PR predicate ¬ProvT(k, �false�):

→,decidable by Decision Theorem above.

From the above G¨odel’s 2nd theorem and PR decision

theorem for quantified arithmetical theories we conclude

Inconsistency provability theorem for quantified arith-

metical theories T(with finite descent): Such theory Tderives

its own inconsistency formula:

T�¬ConTi. e. T�∃kProvT(k, �false�)

8.1 Proof R´esum´e:

•The consistency formula for “any” theory, in particular

for an arithmetical theory, can be stated in terms of a free

variable PR predicate: For any number k(k∈free),

kis not the enumeration index of a proof code for (code

of) false.

•Quantified arithmetics Twith finite descent admit (cor-

rectly terminating) evaluations of their PR map code sets.

•Such theory Tis able to decide any PR predicate on

counterexample vs. PR provability: Decision Theorem.

•In particular the consistency formula of such theory T

is decided by theory Ttaken as “metamathematical”

frame.

•This result leads to self-inconsistency of quantified arith-

metical theory (with finite descent) by the second G¨odel’s

Incompleteness Theorem on non-derivability of theorie’s

Tconsistency formula, theory Tassumed consistent.

[If Tis inconsistent, it derives everything, in particular

its own inconsistency formula ]

Note: Observe that G¨odel’s undecidable formula 17 Gen r

is not primitive recursive.

Remark: A way out will be given in part II on Iterative

Self-Consistency. Choose as “metamathematical” frame itera-

tive descent theory πR: p. r. theory PR with extension objects

of predicates – among these universal object of all (inter-

nal) numerals and nested numpairs –, and additional axiom

schema of non-infinite descent of all complexity controlled it-

erations.

8.2 Discussion

Background for the discussion are the books of Yu. I. Manin

2010 and K. Sigmund 2015.

“Vorbilder des Wiener Kreises sind der Physiker Albert

Einstein, der Mathematiker David Hilbert und der Philosoph

Bertrand Russell.” 7

Russell had discovered a first contradiction in Frege-Cantor’s

set theory, namely availability of “set” R={x:x�∈ x}with

paradoxical property R∈R⇐⇒ R�∈ R, and authored with

Whitehead 1900 the (typified) Principia Mathematica PM in

order to exclude this paradoxon from set theory.

The first two of Hilbert’s famous 10 (later 23) problems8

ask for a provably consistent foundation of Mathematics (and

decision of the Continuum Hypothesis CH). Hilbert: “Wir

7Sigmund 2015

8talk at ICM conference Paris 1900, Gesammelte Abhandlungen. Springer 1970

wollen wissen, wir werden wissen. ... Niemand wird uns aus

dem Paradies vertreiben, in das Cantor uns gef¨uhrt hat.” Hilbert

devoted himself to a solution of these first (and second) prob-

lems.

In the opinion of the majority of Mathematicians, G¨odel

has “erledigt” Hilbert’s formalistisches Programm with the

publication of his two incompleteness theorems for Principia

Mathematica PM und verwandte Systeme, such as in particu-

lar Zermelo-Fraenkel set theory ZF.

The anti-idealistic anti-metaphysical Wiener Kreis, G¨odel’s

intellectual home, celebrated G¨odel for his [vermeintliche] Rel-

ativierung of the GREEK identity of truth with provability in

axiomatic Mathematics.9

G¨odel himself was said to have doubts on his assump-

tion of ω-consistency, of non-ω-inconsistency. Did he even

have doubts on consistency of PM? As K. Sigmund reports,

G¨odel became deeply depressive, after his death answers to

letters (not given to mail) were found in his desk revealing his

platonic convictions.

A. Grothendieck told us after his “green” talk in the 1980ties

in Berlin, that S. Eilenberg had proposed to N. BOURBAKI a

categorical approach to Foundations “but A. Weyl n’en voulait

pas.”

9cf. Manin 2010, II 11.7. G¨odel’s Incompleteness Theorem for Arith-

metic. ... {true formulas}�={deducible formulas}

Appendix: Iterative evaluation

We resolve uniform evaluation eva into a CCI (Complexity

Controlled Iteration) and show within framework of quantified

arithmetical theory Twith finite descent of chains of polyno-

mials in [ω] the following

Evaluation Resolution:

Evaluation eva =eva(f,x):PR×⊥�⊥can be re-

solved into a Complexity Controlled Iteration (CCI):

while cx f>0do(f,x):=e(f,x)od

where cx =cx f:PR→[ω] is a suitable map code complex-

ity within the linearily ordered semiring of polynomials with

coeﬃcients in .This complexity descends, eventually down

to 0,with each application of evaluation step e=e(f,x):

PR×⊥→PR×⊥and is to give evaluation result as value

in right component upon reaching complexity 0 = cx �id�

in left component PR.

Iterative evaluation of cartesian theory CA

evaluation step

e=e(f,a)=(emap(f,a),earg(f,a)) :

CA ×⊥−→ CA ×⊥

⊥=∪{⊥}⊂,⊥=�⊥�(trash)

=∪A˙

A={:−→ }universal set

of internal numerals and (nested) numpairs

earg(f,a)is the intermediate argument obtained by one eval-

uation step applied to the pair (f,a),and emap(f,a)is the

remaining map code still to be evaluated on intermediate argu-

ment earg(f,a),same then iteratively applied to pair (emap,earg)

This evaluation step eis defined by recursive case distinc-

tion below, controlled by -valued descending complexity

cx =cx f∈

in turn p. r. defined by

cx �id�:= 0

cx �ba�:= 1,ba ∈bas �{id}={0,s,Π,�,r}

cx �g⊙f�:= cx f+cx g+1

cx �f;g�:= cx f+cx g+1

cx �f˙

×g�:= cx f+cx g+1

evaluation step e=e(f,a) is p. r. defined (and is itera-

tion complexity-controlled) as follows:

•basic map cases:

e(�id�,a):=(�id�,a),cx �id�=0,stationary;

e(�ba�,a):=(�id�,eva(�ba�,a))

with eva(�ba�,a)=νBba ν−1

A= Dom ba,B= Codom ba

ba ∈bas�={0,s,ΠA,�

A,B,rA,B :A, B PR objects}

ν=νA:A∼

−→ ˙

A(internal) numeralisation;

cx(�id�)=0<cx(�ba�)=1,ba ∈bas�

•composition cases:

–identity subcase:

e(g⊙�idA�,a):=(g,a)

cx g<cx g+0+1=cx �g⊙�idA��

–For f∈[A, B],g∈[B,C],a∈A, cx f>0:

e(g⊙f,a)=(emap(g⊙f,a),earg(g⊙f,a))

:= (g⊙emap(f,a),earg(f,a))

Complexity descent:

cx emap(g⊙f,a)

=cx (g⊙emap(f,a),a)

=cx emap(f,a)+cx g+1

<cx f+cx g+1

=cx �g⊙f�

•cases of an induced:

–identities case:

e(��idC�;�idC��,c):=(�idC×C�,�c;c�)

cx �idC×C�=c(�id�)=0

<1=cx(��idC�;�idC��)

–case f∈[C, A],g∈[C, B],not both equal to �idC�:

e(�f;g�,c)

:= (�emap(f,c); emap(g,c)�,�earg(f,c); earg(g),c�)

cx emap(�f;g�,c)

=cx emap(f,c)+cx emap(g,c)+1

<cx f+cx g+1=cx �f;g�

since in this case cx f>0and/or cx g>0,

and therefore cx emap (f,c)<cx f

and/or cx emap(g,c)<cx g

cartesian cases:

e(�idA�˙

×�idB�,�a;b�):=(�idA×B�,�a;b�)

cx �idA×B�=0

<1=cx �idA�+�idB�+1=cx ��idA�˙

×�idB��

For f∈[A, A�],g∈[B,B] not both identity codes:

e(f˙

×g,�a;b�)

:= (emap(f,a)˙

×emap(g,a),�earg(f,a); earg(g,b)�)

one-step-evaluate both components fand gin parallel.

Complexity descent:

cx �emap(f,a)˙

×emap(g,b)�

=cx emap(f,a)+cx emap(g,b)+1

<cx f+cx g+1=cx �f˙

×g�.

Evaluation of theory PR

Let ˙

§=�§�code the iteration symbol of PR

CA evaluation step eis extended by clause:

For endomap code f∈[A, A]=[A, A]PR and a∈˙

e(f˙

§,�a;�0��):=(f0,a)

e(f˙

§,�a,ν(s n)�):=(�f⊙fn�,a)

where f0:= �id�

fsn:= �f⊙fn�recursively:

code expansion

Complexity extension:

cx f˙

§:= (cx f+ 1) ·ω∈[ω]

[ω] the well-ordered semiring of polynomials in one indeter-

minate over ,pendant to set theoretic ordinal ωω: Within

set theory T,[ω] has only finite descending chains.

In this “acute” iteration case we have

complexity descent

cx f0=cx �id�=0<(cx f+ 1) ·ω=cx f˙

and further inductively

cx fsn=cx �f⊙�f... f�...�

=cx f·sn+n

<(cx f+ 1) ·(n+ 1)

<(cx f+ 1) ·ω=cx f˙

Explication: cx now takes values within the linearily or-

dered semiring [ω]⊃of polynomials in one indeterminate

ω,ωthought to represent (arbitrarily) big natural numbers.

So in fact cx(fsn)<cx(f˙

§) since the former polynomial has

lower degree than the latter.

Linear order of polynomials p, q ∈[ω] is defined hierar-

chically by first comparison of the degrees of pand q, second

in case of equal degrees by comparison of the pivot coeﬃcients,

and third, if the pivot monomials are equal, recursively by com-

parison of the polynomials pand qwith the two pivot mono-

mials deleted.

Note: A first approach to evaluate arbitrary constants c:

→Aof PR into numerals/nested numpairs has been given

in Lassmann 1981.

Evaluation Resolution Theorem:

•Evaluation eva of PR map code variable f∈[A, B]=

[A, B]PR ⊂PR on (fitting) arguments a∈˙

A⊂is to-

tally defined by the complexity controlled iteration

(CCI)

eva =eva(f,a):=











init �(h,x):=(f,a)

∗

while [cx h>0]

do (h,x):=e(h,x)od

∗

result := x

which always terminates, (at least) within quantified

arithmetical theories Twith finite descent since there

complexity (co)domain [ω] has only finite descending

chains whence

f∈[A, A] (endo)map code variable

(term)

(∃m∈)em(f,a)=(�id�,eva (f,a))

[m=m(f,a)=µ{˜m:cx e˜m(f,a)=0}]

so eva (f,a)=rem(f,a)

•eva is characterised by the double recursion

(“Ackermann”)

eva(ba,a)=νB(ba(ν−1

A(a)))

for ba ∈bas,A= Dom[ba],B= Codom[ba]

eva(g⊙f,a)=eva(g,ev(f,a))

eva�f;g�,c)=�eva(f,c); eva(g,c)�

eva(f˙

×g,�a;b�)=�eva(f,a); eva(g,b)�

as well as

eva(f˙

§,�a;�0��)=aand

eva(f˙

§,�a;ν(s n)�)=eva(f,ev(f˙

§,�a;νn�)

•define (natural) evaluation family

ev =evA,B =evA,B(f,a):[A, B]×A→Bby

evA,B(f,a)=ν−1

B(eva(f,ν

A(a))

This family ev is objective:

f:A→BPR map

ev (�f�,a)=f(a):A→B

“evaluation is application.”

Proof of evaluation resolution theorem

by (external) Peano induction on iteration-index-until-termi-

nation m=m(h,x)∈,via case distinction on PR map

hand (fitting) x∈appearing in the diﬀerent cases of the

asserted conjunction.

•anchor m=0,1:h=�ba�,ba ∈bas = {id,0,s,Π,�,r}

see evaluation definition above.

cases µ=µ{˜m:e˜m(h,x)=(�id�,ev (h,x))}=m+1:

•case (h,x)=(g⊙f,a) of an (internally) composed,

subcase f=�id�: obvious.

•non-trivial subcase (h,x)=(g⊙f,a),f�=�id�:

eva(g⊙f,a)=rem(g⊙emap(f,a),earg(f,a))

by iterative definition of eva in this case,

mfold iteration

=eva(g,eva(emap(f,a),earg(f,a)))

=eva(g,rem(f,a))

=eva(g,eva(f,a))

The latter three equations hold (backwards) by induction

hypothesis on m

Objectivity in this case, substitute �f:A→B�into

f∈[A, B],�g:B→C�into g∈[B,C]:

ev(�g◦f�,a)=ev(�g�⊙�f�,a)

=ev(�g�,ev(�f�,a)) see eva just above

=ev(�g�,f(a)) = g(f(a))

both by hypothesis on m

=(g◦f)(a) q. e. d. in this case

•case (h,x)=(�f;g�,c) of an (internal) induced: Obvious

by definition of eva and then of ev on an induced into a

product.

•case (h,x)=(f˙

×g,�a;b�) of an (internal) cartesian prod-

uct: Obvious by definition of eva and then of ev on a

cartesian product of maps.

•anchor case (h,x)=(f˙

§,�a;�0��) of an iterated:

eva(f˙

§,(a,�0�)) = a=eva(�id�,a)

•step case (h,x)=(f˙

§,�a;ν(s n)�) of a genuine (inter-

nally) iterated:

eva(f˙

§,�a;ν(s n)�)

=eva(e(f˙

§,�a;ν(s n)�)

=eva(fsn,a)(definition of evaluation step e)

=eva(f⊙fn,a)(recursive definition of fsn)

=eva(f,eva(fn,a)) by induction hypothesis on m

case of a composed map

=eva(f,eva(f˙

§,�a;νn�)

Proof of objectivity in this last case: substitute �f�

into f∈[A, A] and get from the above

ev(�f§�,(a, sn))

ev(�f�˙

§,(a, sn))

=ν−1

A(eva(�f�˙

§,�νA(a); ν(s n)�))

=ν−1

A(eva(�f�⊙�f�˙

§,�νA(a); νn�))) by the above

=ν−1

A(eva(�f◦f§�,�νA(a); νn�)))

=(f◦f§)(a, n)=f§(a, sn)bynaturality of ν

This shows the theorem in the remaining iteration case q. e. d.

Thanks to S. MING and J. Sablatnig for valuable com-

ments and suggestions.

References

[1] Barwise ed. 1977: Handbook of Mathematical Logic.

North Holland.

[2] N. BOURBAKI 1966: ´

El´ements de math´ematique,

th´

eorie des ensembles, chapitres 1 et 2, Descrip-

tion de la math´ematique formelle, Th´eorie des ensembles,

troisi`

eme edition revue et corrig´

ee, hermann.

[3] S. Eilenberg, C. C. Elgot 1970: Recursiveness. Aca-

demic Press.

[4] G. Frege 1879: Begriﬀsschrift. Reprint in “Begriﬀss-

chrift und andere Aufs¨atze”, 2te Auflage 1971, I. Angelelli

editor. Georg Olms Verlag Hildesheim, New York.

[5] P. J. Freyd 1972: Aspects of Topoi. Bull. Australian

Math. Soc. 7, 1-76.

[6] K. G¨

odel 1931: ¨

Uber formal unentscheidbare S¨atze

der Principia Mathematica und verwandter Systeme I.

Monatsh. der Mathematik und Physik 38, 173-198.

[7] R. L. Goodstein 1971: Development of Mathematical

Logic, ch. 7: Free-Variable Arithmetics. Logos Press.

[8] D. R. Hofstadter 1979/1999: G¨

ODEL, ESCHER,

BACH: an Eternal Golden Braid. BASIC BOOKS.

[9] A. Joyal 1973: Arithmetical Universes. Talk at Oberwol-

fach.

[10] J. Lambek, P. J. Scott 1986: Introduction to higher

order categorical logic. Cambridge University Press.

[11] F. W. Lawvere 1964: An Elementary Theory of the

category of Sets. Proc. Nat. Acad. Sc. USA 51, 1506-1510.

[12] F. W. Lawvere 1970: Quantifiers and Sheaves. Actes du

Congr`es International des Math´ematiciens, Nice, Tome I,

329-334.

[13] Yu. I. Manin 2010: A Course in Mathematical Logic for

Mathematicians. Second Edition. With collaboration by

B. Zilber. Graduate Texts in Mathematics, Springer.

[14] G. Osius 1974: Categorical set theory: a characterisation

of the category of sets. J. Pure and Appl. Alg. 4, 79-119.

[15] M. Pfender 1974: Universal Algebra in S-Monoidal Cat-

egories. Algebra-Berichte Nr. 20, Mathematisches Institut

der Universit¨at M¨unchen. Verlag Uni-Druck M¨unchen.

[16] M. Pfender 2008: RCF 2: Evaluation and Consistency.

arXiv:0809.3881v2 [math.CT]. Has a gap.

[17] M. Pfender 2012: Arithmetical Foundations, αversion.

http://www3.math.tu-berlin.de/preprints/files/Preprint-

38-2012.pdf

[18] M. Pfender 2014: Consistency Decision. arXiv:

1405.3944v1 [math.GM] 9 May 2014.

[19] M. Pfender 2015: Arithmetical Foundations: Re-

cursion.Evaluation.Consistency. arXiv 1312.7275v2

[math.LO].

[20] M. Pfender 2016b: Consistency Decision II: Iterative

Self-Consistency. Preprint in preparation.

[21] M. Pfender 2016c: Arithmetical Foundations:

Recursion.Evaluation.Consistency. KIEPERT Berlin.

To appear.

[22] M. Pfender, M. Kr¨

oplin, D. Pape 1994: Primitive

Recursion, Equality, and a Universal Set. Math. Struct. in

Comp. Sc. 4, 295-313.

[23] L. Rom`

an 1989: Cartesian categories with natural num-

bers object. J. Pure and Appl. Alg. 58, 267-278.

[24] K. Sigmund 2015: Sie nannten sich Der Wiener Kreis.

Exaktes Denken am Rand des Untergangs. Springer Spek-

trum.

[25] C. Smorynski 1977: The Incompleteness Theorems. Part

D.1 in Barwise ed. 1977.