Premium
Provability in Elementary Type Theory
Author(s) -
Andrews Peter B.
Publication year - 1974
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.19740202506
Subject(s) - type (biology) , type theory , consistency (knowledge bases) , mathematics , order (exchange) , citation , computer science , mathematical economics , philosophy , algebra over a field , calculus (dental) , discrete mathematics , library science , pure mathematics , ecology , biology , medicine , dentistry , finance , economics
Results are obtained about special cases of the decision problem for provability in type theory with A-conversion, minus axioms of extensionality, descriptions, choice, and infinity. |&£ . . . ag [A=g] iff there is a substitution 0 such that 9 * A = 0 * B. Hence fA = g iff A conv Jg. This shows the independence of the axioms of extensionality. If £ is quantifier-free, fVjc . . . Vx Q iff r}C is tautologous. Inhere is no decision procedure for the class of wffs of the form 3z [A=B] , or the class of wffs of the form 3g£* where C is quantifier-free. Hence the only solvable classes of wffs in prenex normal form defined solely by the structure of the prefix are those in which no existential quantifiers occur. PROVABILITY IN ELEMENTARY TYPE THEORY by Peter B. Andrews §