## Proof theory of impredicative subsystems of analysis |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

Introduction | 9 |

SUBSYSTEMS OF ANALYSIS WITH INCOM | 29 |

Axioms and Basic Inferences of the Formal System Aj 33 IIjComprehen | 54 |

Copyright | |

3 other sections not shown

### Common terms and phrases

28.6 we obtain a e C0 additional axiom schema arithmetical formula assertion follows assertion holds assumption axiom of PB basic inference rule Cantor normal form complete induction complex predicate quantifier constant prime formula Corollary 28.6 Ct(P Cut Elimination Theorem cut of grade dg(c e-number Ej-formula F holds Fbe derived follows from Lemma formal system A2 formula F formula of stage formula V X free number variable free predicate variable fundamental function gr(F Hence we obtain I.H. we obtain induction on dg Inductive Definition inference of PB KScb Lemmata limit ordinal mula n-place recursive n2-formula natural numbers numerical substitute obtain D[U Ordering Proof ordinal notation P-form predicate quantifier V X principal inference Proof by induction proof of Lemma proof theoretical ordinal prove Qt+1 Replacement rules result of replacing set theory strong formula structural rule subsystems of analysis Takeuti weak formula Yasugi zero-interpretation