McColm's Conjecture

Gregory McColm conjectured that positive elementary inductions are bounded in a class K of nite structures if every (FO + LFP) formula is equivalent to a rst-order formula in K. Here (FO + LFP) is the extension of rst-order logic with the least xed point operator. We disprove the conjecture. Our main results are two model-theoretic constructions, one deterministic and the other randomized, each of which refutes McColm's conjecture.

• Type: Conference
• Year: 1994
• Where: LICS
• Authors: Yuri Gurevich, Neil Immerman, Saharon Shelah
• Keywords: Automated Reasoning, Gregory McColm, LICS 1994, Positive Elementary Inductions, Xed Point Operator