— 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