Matching logic -- a new axiomatization

TL;DR

This paper introduces a simplified axiomatization and proof system for first-order matching logic, inspired by classical logic axiomatizations, eliminating the need for free variables and substitution notions.

Contribution

It presents a new, simpler proof system for matching logic, adapting classical axiomatizations to improve clarity and foundational understanding.

Findings

A new proof system for matching logic is proposed.

The proof system simplifies existing frameworks by removing free variable notions.

Applications to first-order matching logic with definedness are demonstrated.

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.