## Transfinite Type Theory with Type Variables |

### What people are saying - Write a review

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

### Contents

The System Q | 1 |

Basic Logic in Q | 28 |

The Theorem of Infinity and Related Results | 67 |

2 other sections not shown

### Common terms and phrases

A0 are free Aa in C0 Aa or Ba agrees with 9 assignment which agrees Axiom of Choice axiom of infinity Axiom Schema axioms of Q B0 Rule consistency proof contains Deduction Theorem define definition EE-Rules Exist finite type theory formalized formation rules free in Aa free occurrences free variables functions h A0 h Aa h Assign]g22 h F0 h r0 h T0 h TS]t2 Hence inductive hypothesis instance of Axiom interpretation of Q Lemma natural numbers Note occurrence of Aa Premiss primitive recursive functions proof is left proof is similar reader result of replacing RuleP rules of inference schemata Simultaneous Substitution system Q Theorem and Rule theorem of Q transfinite type theory type symbols type variables VaA0 Variable]w2t2 variables of Aa wff Aa wff of Q0 wff of type wflF x-variable occurs free x2 h xa occurs free