A Note on Relative Efficiency of Axiom Systems

✍ Scribed by Sandra Fontani; Franco Montagna; Andrea Sorbi

• Publisher: John Wiley and Sons
• Year: 1994
• Tongue: English
• Weight: 664 KB
• Volume: 40
• Category: Article
• ISSN: 0044-3050
• DOI: 10.1002/malq.19940400211

✦ Synopsis

Abstract

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.