Matching logic -- a new axiomatization
Logic in Computer Science
2025-06-26 v3 Logic
Abstract
In these notes we propose a new, simpler proof system for first-order matching logic with application and definedness. The new proof system is inspired by Tarski's axiomatization for first order-logic with equality (simplified by Kalish and Montague), that does not involve the notions of a free variable and free substitution. We give also a proof system for first-order matching logic with application, obtained by adapting to matching logic G\"{o}del's proof system for first-order intuitionistic logic.
Cite
@article{arxiv.2506.13801,
title = {Matching logic -- a new axiomatization},
author = {Laurenţiu Leuştean and Dafina Trufaş},
journal= {arXiv preprint arXiv:2506.13801},
year = {2025}
}
Comments
This version is a a vast extension of the previous version arXiv:2506.13801v2. We changed the title and the abstract of the preprint to reflect this fact