Equilibrium Logic

Origin. Pearce (1996). Logic programming semantics. Here-and-there logic. Answer sets as equilibria. Foundation for answer set programming.

Models. HT-models: pairs (H, T) with H ⊆ T. "Here" and "there" worlds. Equilibrium: minimal H for given T. Connection to stable models.

Formalism.

HT-model: (H, T) where H ⊆ T ⊆ At. T: "there" world (classical). H: "here" world (constructive).

Satisfaction: (H,T) ⊨ p iff p ∈ H (H,T) ⊨ ¬φ iff (T,T) ⊭ φ (H,T) ⊨ φ → ψ iff (H,T) ⊭ φ or (H,T) ⊨ ψ, and (T,T) ⊭ φ or (T,T) ⊨ ψ

Total model: (T,T): H = T. Classical model.

Equilibrium model: (T,T) ⊨ φ and no (H,T) ⊨ φ with H ⊂ T. T is minimal model of φ given T-satisfaction.

Stable model connection: T is stable model of program P iff (T,T) is equilibrium model of P. Gelfond-Lifschitz reduct.

Strong equivalence: φ ≡_s ψ iff ∀context C: φ ∧ C ≡ ψ ∧ C Same equilibrium models in all contexts. Characterized by HT-equivalence.

Here-and-there logic: Intermediate logic. Between intuitionistic and classical. Three values: false, here-only, there.

Symbols.

Symbol	Unicode	Name	Meaning
⊨	U+22A8	Double turnstile	Satisfaction in an HT-model
⊭	U+22AD	Negated double turnstile	Failure of satisfaction
⊆	U+2286	Subset	Here-world contained in there-world
⊂	U+2282	Proper subset	Strictly smaller here-world, tested for equilibrium
∈	U+2208	Membership	Atom true at a world
¬	U+00AC	Negation	Intuitionistic negation, evaluated at (T,T)
→	U+2192	Implication	Must hold at both worlds
∧	U+2227	Conjunction	Joins a theory to its context
∨	U+2228	Disjunction	Connective of the axiom separating HT from intuitionistic logic
≡	U+2261	Equivalence	Sameness of equilibrium models
∀	U+2200	Universal quantifier	Ranges over contexts in the definition of ≡_s
φ	U+03C6	Phi	A formula or theory
ψ	U+03C8	Psi	A second formula, compared with φ
H	—	Here	The constructive world of the pair
T	—	There	The classical world of the pair
At	—	Atoms	The propositional signature
C	—	Context	Theory conjoined in the strong-equivalence test
(H,T)	—	HT-model	Here-and-there pair with H ⊆ T
≡_s	—	Strong equivalence	Interchangeable in every context
⊨_HT	—	HT-satisfaction	Satisfaction in the logic of here-and-there

Metatheory. The logic of here-and-there is the logic of the three-element Heyting chain, axiomatized by intuitionistic propositional logic plus the schema φ ∨ (φ → ψ) ∨ ¬ψ; it lies strictly between intuitionistic and classical logic and is the unique maximal intermediate logic below classical. Being three-valued it is decidable, and it has a complete finitary calculus. Pearce (1996) proved the result that gives the framework its point: T is a stable model of a logic program P exactly when (T,T) is an equilibrium model of P read as an HT theory. Since HT is defined for arbitrary formulas rather than for rules, this extends the stable-model semantics to formulas of any shape, and every equilibrium model is a minimal classical model, though the converse fails. Lifschitz, Pearce and Valverde (2001) proved that two theories are strongly equivalent — interchangeable inside any larger theory — exactly when they are HT-equivalent, reducing a non-monotonic question to a monotonic and decidable one; deciding strong equivalence is coNP-complete. Pearce and Valverde carried the framework to first order as quantified equilibrium logic.

Applies to. Answer set programming. Non-monotonic reasoning. Knowledge representation. Planning.

Limitations. Equilibrium models need not exist — the theory corresponding to the program a :- not a has none — and the entailment relation degenerates when they do not. The minimality step that selects them lies outside the logic: here-and-there itself is monotonic and has a complete calculus, but equilibrium consequence is a model-selection relation imposed on top of it, non-monotonic and with no proof system of its own, so nothing is derived in equilibrium logic in the ordinary sense. Ordinary equivalence is not a congruence; only strong equivalence licenses substitution, and uniform equivalence, which permits only facts to be added, is a third and distinct relation, so there is no single notion of two theories being the same. The object language behaves intuitionistically — excluded middle fails and double negation does not cancel — so a classically valid rewriting can change the equilibrium models while preserving the classical ones.