%PDF-1.4
5 0 obj
<< /S /GoTo /D (chapter*.2) >>
endobj
8 0 obj
(Introduction)
endobj
9 0 obj
<< /S /GoTo /D (section*.3) >>
endobj
12 0 obj
(Motivation)
endobj
13 0 obj
<< /S /GoTo /D (section*.4) >>
endobj
16 0 obj
(Acknowledgements)
endobj
17 0 obj
<< /S /GoTo /D (chapter.1) >>
endobj
20 0 obj
(Arithmetic in all finite types)
endobj
21 0 obj
<< /S /GoTo /D (section.1.1) >>
endobj
24 0 obj
(The theories E-PA and WE-PA)
endobj
25 0 obj
<< /S /GoTo /D (subsection.1.1.1) >>
endobj
28 0 obj
(The language L0)
endobj
29 0 obj
<< /S /GoTo /D (subsection.1.1.2) >>
endobj
32 0 obj
(Deduction framework)
endobj
33 0 obj
<< /S /GoTo /D (subsection.1.1.3) >>
endobj
36 0 obj
(\(Weakly\) extensional interpretation of equality)
endobj
37 0 obj
<< /S /GoTo /D (section.1.2) >>
endobj
40 0 obj
(Restricted theories and first order theories)
endobj
41 0 obj
<< /S /GoTo /D (section.1.3) >>
endobj
44 0 obj
(Intuitionistic variants)
endobj
45 0 obj
<< /S /GoTo /D (subsection.1.3.1) >>
endobj
48 0 obj
(Intuitionistic logic)
endobj
49 0 obj
<< /S /GoTo /D (subsection.1.3.2) >>
endobj
52 0 obj
(Negative translation and application)
endobj
53 0 obj
<< /S /GoTo /D (chapter.2) >>
endobj
56 0 obj
(G\366del's dialectica interpretation)
endobj
57 0 obj
<< /S /GoTo /D (section.2.1) >>
endobj
60 0 obj
(Primitive recursive functions)
endobj
61 0 obj
<< /S /GoTo /D (section.2.2) >>
endobj
64 0 obj
(Quantifier-free part of weakly-extensional arithmetic in all finite types)
endobj
65 0 obj
<< /S /GoTo /D (subsection.2.2.1) >>
endobj
68 0 obj
(G\366del's T)
endobj
69 0 obj
<< /S /GoTo /D (subsection.2.2.2) >>
endobj
72 0 obj
(Translating terms of PRA to terms of T)
endobj
73 0 obj
<< /S /GoTo /D (subsection.2.2.3) >>
endobj
76 0 obj
(Type-1 conservation of T"0362T over PRA)
endobj
77 0 obj
<< /S /GoTo /D (section.2.3) >>
endobj
80 0 obj
(The D-Interpretation)
endobj
81 0 obj
<< /S /GoTo /D (subsection.2.3.1) >>
endobj
84 0 obj
(Definition and justification)
endobj
85 0 obj
<< /S /GoTo /D (subsection.2.3.2) >>
endobj
88 0 obj
(Verifying the axioms of arithmetic)
endobj
89 0 obj
<< /S /GoTo /D (subsection.2.3.3) >>
endobj
92 0 obj
(Extending WE-PAi and WE-PA)
endobj
93 0 obj
<< /S /GoTo /D (chapter.3) >>
endobj
96 0 obj
(Conservation and subtheory results for WKL)
endobj
97 0 obj
<< /S /GoTo /D (section.3.1) >>
endobj
100 0 obj
(Preliminaries)
endobj
101 0 obj
<< /S /GoTo /D (subsection.3.1.1) >>
endobj
104 0 obj
(Subtheories and conservation)
endobj
105 0 obj
<< /S /GoTo /D (subsection.3.1.2) >>
endobj
108 0 obj
(- and -formulas)
endobj
109 0 obj
<< /S /GoTo /D (subsection.3.1.3) >>
endobj
112 0 obj
(WE-PRAQF-AC)
endobj
113 0 obj
<< /S /GoTo /D (subsection.3.1.4) >>
endobj
116 0 obj
(Weak K\366nig's lemma WKL and uniform weak K\366nig's lemma)
endobj
117 0 obj
<< /S /GoTo /D (section.3.2) >>
endobj
120 0 obj
(The theory WE-PRAQF-ACWKL)
endobj
121 0 obj
<< /S /GoTo /D (subsection.3.2.1) >>
endobj
124 0 obj
(Hereditary majorizability)
endobj
125 0 obj
<< /S /GoTo /D (subsection.3.2.2) >>
endobj
128 0 obj
(Conservation result)
endobj
129 0 obj
<< /S /GoTo /D (section.3.3) >>
endobj
132 0 obj
(The theory WE-PRAQF-ACUWKL)
endobj
133 0 obj
<< /S /GoTo /D (section.3.4) >>
endobj
136 0 obj
(The theory E-PRA+QF-AC1,0+QF-AC0,1+WKL)
endobj
137 0 obj
<< /S /GoTo /D (subsection.3.4.1) >>
endobj
140 0 obj
(Non-interpretability of extensionality)
endobj
141 0 obj
<< /S /GoTo /D (subsection.3.4.2) >>
endobj
144 0 obj
(Elimination of extensionality)
endobj
145 0 obj
<< /S /GoTo /D (subsection.3.4.3) >>
endobj
148 0 obj
(Conservation result)
endobj
149 0 obj
<< /S /GoTo /D (section.3.5) >>
endobj
152 0 obj
(The theory E-PRA+QF-AC1,0+QF-AC0,1+UWKL)
endobj
153 0 obj
<< /S /GoTo /D (subsection.3.5.1) >>
endobj
156 0 obj
(Subtheory result)
endobj
157 0 obj
<< /S /GoTo /D (subsection.3.5.2) >>
endobj
160 0 obj
(Conservation result)
endobj
161 0 obj
<< /S /GoTo /D [162 0 R /Fit ] >>
endobj
164 0 obj <<
/Length 544
/Filter /FlateDecode
>>
stream
xڍSMo0
gU?R$AF:%q("z@͛+JÊ^`*]@)kj^SRR3^Ri해D(f+K-Y2I+RԊ@RZM?<H:vo6;Z)5DJVkIJlh/|tE/cx4}B
;2$` uZΤ@>U {#[*?~GF0 ԐХL+f97"Ba1}0Huӄs݆˯gUQ->}x.Ti$k*컟ōSJ}CŌ2Ԇ$|Xkܹ_1P/:ihiC}ؽb &]dX0TiwhShb̀24[QrpqvųhIlV8B-(Pymr"OSrq9e(JX]6WU\~iKendstream
endobj
162 0 obj <<
/Type /Page
/Contents 164 0 R
/Resources 163 0 R
/MediaBox [0 0 612 792]
/Parent 173 0 R
>> endobj
165 0 obj <<
/D [162 0 R /XYZ 72 708.045 null]
>> endobj
166 0 obj <<
/D [162 0 R /XYZ 72 683.138 null]
>> endobj
163 0 obj <<
/Font << /F37 169 0 R /F15 172 0 R >>
/ProcSet [ /PDF /Text ]
>> endobj
176 0 obj <<
/Length 2213
/Filter /FlateDecode
>>
stream
xZKW0'
(GJ$%X&+D\rrmy `K\JJf~͈Ĭk3=[3jS̋QO˯VϾZ3YQ
r6el~B%'xKIOŏ<{8τeB8v& 2
*c=ߢb T2.tVŀ[da豸b+*p!m} ^&N,0Ŏ8NckowhtR52F{Z%+gF&tA:>Ўsʢ
70%JkX Y^
Ǣ`%
«=(9Wm}(L
X,+nch.f%7
^z= Iߜ0|Y ^)*,Qrbn-Y$58E$8n۞
4Ή(8 i]ImbGv
_zDU\otD_
7Lrր>_t-#rGo3d),@Vc)5ŜBǓK(˂~1pG(9?l"DiX?#3LP4<U$Mݎ2q3ˀ.=`ƙ@ J&5%T5/UG!^ :Dk4pO4Kj@I0
nQB[wUzG`n#e{֧u8x.OƞPdu('4*="tsr!d]_*#*5YF
շ6SK+V'`nvD>RLHB"+-Uz7=x(+ǜ",xYWGI.'x >z<4'?)l'$~6k,f'RZfȟf@C+)`%$JDqGynɭov,Aɺ6 ɉ\"r í4)ӋYAD/Q1穊(?@|5D 5Zu)$UE-%@a룟1q7,̹5s
Js(z<hh30/vhƓe^Ҽ1'JE??6?hO{Eƪa[`8aG]6toX{#º;w&%ZMcVUI}>?30ZIu[B}4Nl70}6w
A4;71l?7]|?%J4ǞV6vǩJ4F;cNn-2%rUJ*NE|W
v4ui {|ٞVzwл[]ML ]:S@K;.,ú#q@C;B8`O\
BxJ[euUx$|淅A$"wtVJȫI Je(K4_#?8D`u%&Ec2%
'z^Xh6ME)HF ;谭@>.cl9_C2Um},j=):4v9G#%Z4Z<QFա1aKa¼n=P0$2T(AjҖQr8 vf|
T$pOg3/eFd\|jq2G2e嘓KvMՅ ^Sψ4j|?21^{N=jYe)H<7V4;Bd]3%zB$XKu<};}Y}TVi9cL#Ɯ0Lu m_"ͬkpnuLH4RwMSyK{8!] K&P^bɆ(9-b(s1QPE?3oZ eE 'qWqbp_ EObm(E*Y'C]EY:⃖윟{&M
\,?$xDp*endstream
endobj
175 0 obj <<
/Type /Page
/Contents 176 0 R
/Resources 174 0 R
/MediaBox [0 0 612 792]
/Parent 173 0 R
/Annots [ 179 0 R 180 0 R 181 0 R 182 0 R 183 0 R 190 0 R 197 0 R 198 0 R 199 0 R 200 0 R 201 0 R 202 0 R 203 0 R 204 0 R 205 0 R 206 0 R 207 0 R 208 0 R 212 0 R 213 0 R 214 0 R 215 0 R ]
>> endobj
179 0 obj <<
/Type /Annot
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [71.004 515.119 147.01 525.413]
/Subtype /Link
/A << /S /GoTo /D (chapter*.2) >>
>> endobj
180 0 obj <<
/Type /Annot
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [88.563 495.991 146.48 506.152]
/Subtype /Link
/A << /S /GoTo /D (section*.3) >>
>> endobj
181 0 obj <<
/Type /Annot
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [88.563 474.538 187.19 487.157]
/Subtype /Link
/A << /S /GoTo /D (section*.4) >>
>> endobj
182 0 obj <<
/Type /Annot
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [71.004 443.704 259.372 456.323]
/Subtype /Link
/A << /S /GoTo /D (chapter.1) >>
>> endobj
183 0 obj <<
/Type /Annot
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [88.563 426.9 285.086 437.472]
/Subtype /Link
/A << /S /GoTo /D (section.1.1) >>
>> endobj
190 0 obj <<
/Type /Annot
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [115.486 404.816 242.071 418.067]
/Subtype /Link
/A << /S /GoTo /D (subsection.1.1.1) >>
>> endobj
197 0 obj <<
/Type /Annot
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [115.486 388.644 265.005 398.939]
/Subtype /Link
/A << /S /GoTo /D (subsection.1.1.2) >>
>> endobj
198 0 obj <<
/Type /Annot
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [115.486 366.527 394.972 380.475]
/Subtype /Link
/A << /S /GoTo /D (subsection.1.1.3) >>
>> endobj
199 0 obj <<
/Type /Annot
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [88.563 350.388 334.46 360.682]
/Subtype /Link
/A << /S /GoTo /D (section.1.2) >>
>> endobj
200 0 obj <<
/Type /Annot
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [88.563 331.259 227.511 341.421]
/Subtype /Link
/A << /S /GoTo /D (section.1.3) >>
>> endobj
201 0 obj <<
/Type /Annot
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [115.486 309.807 247.996 322.426]
/Subtype /Link
/A << /S /GoTo /D (subsection.1.3.1) >>
>> endobj
202 0 obj <<
/Type /Annot
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [115.486 290.679 341.97 303.298]
/Subtype /Link
/A << /S /GoTo /D (subsection.1.3.2) >>
>> endobj
203 0 obj <<
/Type /Annot
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [71.004 259.844 280.01 272.464]
/Subtype /Link
/A << /S /GoTo /D (chapter.2) >>
>> endobj
204 0 obj <<
/Type /Annot
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [88.563 243.041 264.42 253.336]
/Subtype /Link
/A << /S /GoTo /D (section.2.1) >>
>> endobj
205 0 obj <<
/Type /Annot
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [88.563 221.588 477.243 234.207]
/Subtype /Link
/A << /S /GoTo /D (section.2.2) >>
>> endobj
206 0 obj <<
/Type /Annot
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [115.486 204.785 204.689 215.079]
/Subtype /Link
/A << /S /GoTo /D (subsection.2.2.1) >>
>> endobj
207 0 obj <<
/Type /Annot
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [115.486 183.332 357.843 195.951]
/Subtype /Link
/A << /S /GoTo /D (subsection.2.2.2) >>
>> endobj
208 0 obj <<
/Type /Annot
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [115.486 164.204 335.277 180.31]
/Subtype /Link
/A << /S /GoTo /D (subsection.2.2.3) >>
>> endobj
212 0 obj <<
/Type /Annot
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [88.563 145.076 225.916 157.695]
/Subtype /Link
/A << /S /GoTo /D (section.2.3) >>
>> endobj
213 0 obj <<
/Type /Annot
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [115.486 125.947 292.384 138.567]
/Subtype /Link
/A << /S /GoTo /D (subsection.2.3.1) >>
>> endobj
214 0 obj <<
/Type /Annot
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [115.486 106.819 330.589 119.439]
/Subtype /Link
/A << /S /GoTo /D (subsection.2.3.2) >>
>> endobj
215 0 obj <<
/Type /Annot
/Border[0 0 0]/H/I/C[1 0 0]
/Rect [115.486 87.06 322.247 100.587]
/Subtype /Link
/A << /S /GoTo /D (subsection.2.3.3) >>
>> endobj
177 0 obj <<
/D [175 0 R /XYZ 72 708.045 null]
>> endobj
178 0 obj <<
/D [175 0 R /XYZ 72 546.949 null]
>> endobj
174 0 obj <<
/Font << /F37 169 0 R /F15 172 0 R /F41 186 0 R /F22 189 0 R /F24 193 0 R /F19 196 0 R /F27 211 0 R >>
/ProcSet [ /PDF /Text ]
>> endobj
218 0 obj <<
/Length 1650
/Filter /FlateDecode
>>
stream
xZMsEW,'v2)(BʁpPX2%sӳ;͎[[J%h_^/(aᕡP7#Zçpurѣ'RVT59K?y0 Iz֔e"jo?_W60+TjGxFl~h
/F˷>~7ZkS׳Յ_xFDWBD^>!0ě^\"wY1Cq[ܜuqVPD9ݘl&ڄA(g|1_NW:,v"%s=bpI!AƵ#O2wjQW*+'5fK2I@ bnH1M-8qܰAQtl(q:z)nv\䆋71\+T;k
X8)!&NLJ[C1S %bAL(յWd9 cyu1U9ś]%znEN+(`KZBRRb'3"(љ(tmyt ԥ<qg=qbiZ6"@CAe`l~zR|t:\*s?ߌKfX.aA|&d)0[nKF%\
$d/m~X:
?@_b~1[,%1C=v|Ɏrݞ
W٥(?, H*5t\WI