← All topics

hybrid logic

2 captures, most recent first.

@RosuGrigore

— saved image

Grigore Rosu @RosuGrigore [Follow]

The reason I've been quiet recently.

Over the last two months I worked hard, using AI, on solving two open problems that my UIUC research lab was not able to solve over the last 7 years.

Finally, we proved them.  Viva @AnthropicAI and @OpenAI!

1:52 PM · Aug 24, 2026 · 9,825 Views

4 replies · 9 reposts · 113 likes · 25 bookmarks

Relevant ▾

[reply / next post in thread]
Grigore Rosu @RosuGrigore · 4h

Matching logic is complete without μ, incomplete with μ!

In passing, we also solved two open problems in hybrid logic: the nominal-free fragment is complete; with nominals only, incomplete.  This is surprising because if we add pointed validity it becomes complete again (known
Show more

[embedded diagram, small text, best-effort: a map of logics and their completeness results; node labels as follows]

matching logic, with definedness
global completeness [2, 3]
equivalent to FOL_= [2]
equivalent to H(@, ∀) [31]

matching μ-logic, with definedness
global completeness fails [3, Prop. 23];
no effective weak completeness (Remark 27)

matching logic, basic many-sorted
global completeness fails
(Section 8)

H(@), H(@, ↓)
global completeness [29]

H(∀)
local completeness [11];
no complete calculus in the
class of Theorem 33

matching logic, basic unsorted
global completeness
(Corollary 15)

matching μ-logic, basic unsorted
no effective weak
completeness (Theorem 19)

modal logic, basic polyadic
global completeness
[12, Ex. 1.5.3]

modal μ-calculus
global completeness, finite Γ,
via [19, 20]; not compact, so
local completeness fails [19]

[arrow labels between nodes: μ, [·], Var, ∃, @, nominals, sorts, nominals, @]
Note from Claude Sonnet 5

Tweet by Grigore Rosu (@RosuGrigore) saying that over two months, using AI, his UIUC lab solved two open problems it had not solved in seven years, crediting Anthropic and OpenAI; below it a follow-up post on completeness of matching logic with and without the mu operator and hybrid logic, with a diagram of logics and completeness results. Posted 2026-08-24.

mathematicslogicmatching logichybrid logicai math resultsopen problemsclaudeopenai

@RosuGrigore

— saved image

[top of screen, cut off: end of the previous post]
@OpenAI!

1:52 PM · Aug 24, 2026 · 9,825 Views

4 replies · 9 reposts · 113 likes · 25 bookmarks

Relevant ▾

Grigore Rosu @RosuGrigore · 4h
Matching logic is complete without μ, incomplete with μ!

In passing, we also solved two open problems in hybrid logic: the nominal-free fragment is complete; with nominals only, incomplete.  This is surprising because if we add pointed validity it becomes complete again (known from 2006).

[embedded diagram of logics and completeness results: the same diagram as in the previous capture, Screenshot_20260824-181724.png; node labels not repeated here]

1 reply · 1 repost · 17 likes · 1.4K views

Grigore Rosu @RosuGrigore · 4h
Here is the paper.  Comments are welcome.

arxiv.org/pdf/2608.13306…

Why is matching logic interesting at all?  Pure type systems, dependent types, calculus of inductive constructions, etc., MSOL, SOL, HOL, etc., can be defined as matching logic theories.  That is, Lean, Rock, Isabelle, etc., proofs can be mechanically translated to matching logic, which is a simpler logic (so it admits a smaller proof checker).
Note from Claude Sonnet 5

Scrolled continuation of the Rosu thread from seq 9: the matching-logic completeness result with the diagram, then a third post linking the paper (arXiv 2608.13306) and explaining why matching logic matters for proof-checker size. Bottom of the capture is overlaid by phone UI (nav bar, compose button) that overlaps a few lines.

mathematicslogicmatching logichybrid logicformal verificationproof assistantsai math resultsarxiv