Lecture Notes in Computer Science, 2002, Volume 2420/2002, 581-592, DOI: 10.1007/3-540-45687-2_48

On the Structure of the Simulation Order of Proof Systems
Extended Abstract

Jochen Messner

View Related Documents

Abstract

We examine the degree structure of the simulation relation on the proof systems for a set L. As observed, this partial order forms a distributive lattice. A greatest element exists iff L has an optimal proof system. In case L is infinite there is no least element, and the class of proof systems for L is not presentable. As we further show the simulation order is dense. In fact any partial order can be embedded into the interval determined by two proof systems f and g such that f simulates g but g does not simulate f. Finally we obtain that for any non-optimal proof system h an infinite set of proof systems that are pairwise incomparable with respect simulation and that are also incomparable to h.

Fulltext Preview

Image of the first page of the fulltext document