Qiana: A First-Order Formalism to Quantify over Contexts and Formulas

What if Juliet had checked Romeo’s pulse before drinking the potion?
What if your database insists Elvis is both alive and dead, but you still want to reason about it without everything collapsing?
What if we could treat contexts — like beliefs, stories, or data sources — as first-class citizens in logic, and even quantify over them?

That’s exactly what Qiana (Quantifying over Agents and Assertions) sets out to do.

The Problem

Traditional logic is powerful, but struggles when statements are only true in certain contexts. Modal logics let us say things like “Alice believes φ”, but they don’t let us quantify over formulas or contexts. Higher-order logics can, but they’re undecidable or unusable in practice.

So how can we express rules like:

• “Everyone believes everything Alice says.”
• “In context C, contradictions exist but don’t explode into nonsense.”
• “If in story A Juliet dies, and in story B she lives, then we can compare the outcomes.”

The Qiana Trick

Qiana borrows McCarthy’s idea of ist(c, φ) (“formula φ is true in context c”) and combines it with a system for quoting formulas — turning formulas into objects we can quantify over.

Key features:

• Quantify over formulas: e.g., ∀φ. ist(says(FriarLaurence), φ) → φ.
• Quantify over contexts: e.g., ∀c. ist(c, dead(Juliet)) → sad(c).
• Paraconsistency inside contexts: contradictions don’t make the system explode.
• First-order logic compatibility: it’s finitely axiomatizable, so we can run it in existing theorem provers like Vampire.

What Can It Do?

The paper demonstrates three fun scenarios:

1. Reasoning in Epistemic Contexts Model beliefs and knowledge (Romeo thinks Juliet is dead → tragedy ensues).

2. Paraconsistency Keep reasoning even if a context holds contradictions (Romeo both believes Juliet has a pulse and that she’s dead).

3. Mixing Stories Compare alternative narratives, like Shakespeare’s original ending vs. a happy fanfiction rewrite.

Why It Matters

Qiana isn’t just about Shakespearean tragedy. It opens up applications wherever contextual reasoning is key:

• Knowledge graphs & data integration: keep contradictory facts from different sources in separate contexts, and still reason safely.
• Modeling beliefs & misinformation: represent what each agent thinks, even when wrong.
• Legal or ethical reasoning: compare alternative interpretations of laws or norms.
• Multi-context AI systems: give LLM agents or autonomous systems “context-aware” reasoning.
• Story engines & simulation: manage branching narratives or “what-if” scenarios in games or literature.

The Bottom Line

Qiana is a new logical framework that makes contexts and formulas first-class, lets us quantify over them, and stays usable with real theorem provers. It’s a rare combination of expressivity + practicality.

Or, to put it in Shakespearean terms:

“All the world’s a stage… and with Qiana, each context its own play.”

The Team

• Simon Coumes
• Myself
• François Schwarzentruber
• Fabian Suchanek