Matching logic -- a new axiomatization

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ödel's proof system for first-order intuitionistic logic.

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