Proof Theory of Impredicative Subsystems of Analysis |
Contents
Introduction | 9 |
SUBSYSTEMS OF ANALYSIS WITH IICOM | 29 |
Axioms and Basic Inferences of the Formal System A2 33 IIComprehen | 54 |
Copyright | |
3 other sections not shown
Common terms and phrases
additional axiom schema arithmetical formula assertion follows basic inference rule C₂ complex predicate quantifier constant prime Corollary Cut Elimination cut of grade e-number F be derived F holds formal system formula F formula V XF free number variable free predicate variable fundamental function Hence we obtain II-CA II-formula impredicative induction on dg INDUCTIVE DEFINITION inference rule inference S 2.0 Lemma Lemmata Let F Let PBF lv F mula n-place natural numbers numerical substitute obtain D[U occur in F Ordering Proof ordinal notation P-form predicate quantifier VX premise F principal inference Proof by induction proof of Lemma PV F Q₁ Qa+¹ Replacement rules result of replacing SRF holds st F structural rule subsystems of analysis V X F weak formula Y₁ YASUGI zero-interpretation ψσα