230:
173:
62:(Prawitz 1968) and Takahashi (Takahashi 1967) by a similar technique (Takahashi 1967), although Prawitz's and Takahashi's proofs are not limited to second-order logic, but concern
139:
295:
214:
271:
300:
86:
207:
106:
123:
264:
200:
82:
40:
290:
153:, 23:39–96. An errata to this article was published in the same journal, 24:149–156, 1954.
305:
90:
257:
180:
63:
36:
85:
in the sense that each of the statements can be derived from each other in the weak system of
70:
32:
130:
48:
52:
241:
184:
284:
146:
28:
118:
59:
20:
156:
Moto-o
Takahashi, 1967. A proof of cut-elimination in simple type theory. In
51:, using a semantic technique for proving cut-elimination, based on work by
229:
94:
74:
172:
134:
237:
81:
Takeuti's conjecture is equivalent to the 1-consistency of
245:
188:
137:'s Hauptsatz for second order predicate logic. In
73:'s syntactic proof of strong normalization for
149:, 1953. On a generalized logic calculus. In
265:
208:
140:Bulletin of the American Mathematical Society
8:
43:(Takeuti 1953). It was settled positively:
121:, 1968. Hauptsatz for higher order logic.
272:
258:
215:
201:
7:
226:
224:
169:
167:
133:, 1966. A nonconstructive proof of
87:primitive recursive arithmetic (PRA)
14:
296:Conjectures that have been proved
228:
171:
151:Japanese Journal of Mathematics
89:. It is also equivalent to the
1:
158:Japanese Mathematical Society
244:. You can help Knowledge by
187:. You can help Knowledge by
322:
223:
166:
124:Journal of Symbolic Logic
301:Mathematical logic stubs
107:Hilbert's second problem
93:of the Girard/Reynold's
83:second-order arithmetic
16:Theorem in formal logic
240:-related article is a
183:-related article is a
69:It is a corollary of
33:sequent formalisation
27:is the conjecture of
91:strong normalization
25:Takeuti's conjecture
143:, 72:980–983.
127:, 33:452–457, 1968.
64:higher-order logics
181:mathematical logic
37:second-order logic
253:
252:
196:
195:
160:, 10:44–45.
58:Independently by
313:
274:
267:
260:
232:
225:
217:
210:
203:
175:
168:
71:Jean-Yves Girard
321:
320:
316:
315:
314:
312:
311:
310:
281:
280:
279:
278:
222:
221:
164:
131:William W. Tait
115:
103:
41:cut-elimination
17:
12:
11:
5:
319:
317:
309:
308:
303:
298:
293:
283:
282:
277:
276:
269:
262:
254:
251:
250:
233:
220:
219:
212:
205:
197:
194:
193:
176:
162:
161:
154:
144:
128:
114:
111:
110:
109:
102:
99:
79:
78:
67:
56:
15:
13:
10:
9:
6:
4:
3:
2:
318:
307:
304:
302:
299:
297:
294:
292:
289:
288:
286:
275:
270:
268:
263:
261:
256:
255:
249:
247:
243:
239:
234:
231:
227:
218:
213:
211:
206:
204:
199:
198:
192:
190:
186:
182:
177:
174:
170:
165:
159:
155:
152:
148:
147:Gaisi Takeuti
145:
142:
141:
136:
132:
129:
126:
125:
120:
117:
116:
112:
108:
105:
104:
100:
98:
96:
92:
88:
84:
76:
72:
68:
65:
61:
57:
54:
50:
46:
45:
44:
42:
38:
34:
30:
29:Gaisi Takeuti
26:
22:
291:Proof theory
246:expanding it
235:
189:expanding it
178:
163:
157:
150:
138:
122:
80:
55:(Tait 1966);
24:
18:
306:Logic stubs
119:Dag Prawitz
66:in general;
21:mathematics
285:Categories
113:References
101:See also
95:System F
75:System F
135:Gentzen
60:Prawitz
53:Schütte
31:that a
238:logic
236:This
179:This
242:stub
185:stub
49:Tait
39:has
47:By
35:of
19:In
287::
97:.
23:,
273:e
266:t
259:v
248:.
216:e
209:t
202:v
191:.
77:.
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
