Premium
A Note on Relative Efficiency of Axiom Systems
Author(s) -
Fontani Sandra,
Montagna Franco,
Sorbi Andrea
Publication year - 1994
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.19940400211
Subject(s) - axiom , mathematics , mathematical proof , extension (predicate logic) , axiom of choice , urelement , zermelo–fraenkel set theory , conservative extension , function (biology) , constructive set theory , choice function , discrete mathematics , set theory , computer science , set (abstract data type) , geometry , evolutionary biology , biology , programming language
We introduce a notion of relative efficiency for axiom systems. Given an axiom system A β for a theory T consistent with S 1 2 , we show that the problem of deciding whether an axiom system A α for the same theory is more efficient than A β is II 2 ‐hard. Several possibilities of speed‐up of proofs are examined in relation to pairs of axiom systems A α , A β , with A α ⊇ A β , both in the case of A α , A β having the same language, and in the case of the language of A α extending that of A β : in the latter case, letting Pr α , Pr β denote the theories axiomatized by A α , A β , respectively, and assuming Pr α to be a conservative extension of Pr β , we show that if A α — A β contains no nonlogical axioms, then A α can only be a linear speed‐up of A β ; otherwise, given any recursive function g and any A β , there exists a finite extension A α of A β such that A α is a speed‐up of A β with respect to g . Mathematics Subject Classification: 03F20, 03F30.