# Open Problems

Here are some interesting open problems about matching logic, listed in no particular order. Recall that we use ML for the fragment of matching logic without fixpoints, MmL for the full matching μ-logic, and AML for applicative matching logic.

**OP1. Global completeness of ML**

Recall that the formulas of ML, called *patterns*, evaluate to the sets of elements that match them. This is different from first-order logic (FOL), where formulas evaluate to only two possible values: true or false. It is more similar to modal logic, where formulas evaluate to the sets of worlds in which they hold.
The distinction between *global* and *local*, deduction/entailment/completeness etc, is known in modal logic and also exists in ML.
Roughly speaking, *local deduction* uses only the (logical) axioms and proof rules in the proof system of ML to prove patterns, while *global deduction* allows to prove patterns in *theories*, i.e., any sets of patterns that are taken as additional axioms, which can be used in the same way as the logical axioms.
Similarly, *local (semantic) entailment* considers all models, while *global entailment* considers only models satisfying the given theory.
In other words, local X is the special case of global X, where the underlying theory is the empty theory.

The two different completeness results are then stated as the following:

- Global completeness: global entailment implies global deduction, for all theories.
- Local completeness: local entailment implies local deduction.

Local completeness has been solved positively in the MmL paper, by a hard proof, inspired from local completeness proof of modal logic.
Global completeness has been solved positively, for the case when the underlying theory contains the special *definedness symbols*, from which equality and membership can be defined as derived constructs.

The open problem is the the global completeness in its full generalarity, where the underlying theories may not contain definedness symbols.

**OP2. Completeness and decidability of the quantifier-free fragment of MmL**

Modal μ-logic is often called the "queen logic" for fixpoint reasoning,
because of its rich expressiveness and good meta-properties.
It has a (locally) complete proof system that can prove all valid formulas of the empty theory.
Also, its SATISFIABILITY problem is decidable in the complexity class of EXPTIME-complete.
Note that modal μ-logic is an extension of the basic modal logic with a binder μ that constructs least fixpoints,
while MmL, excluding its FOL quantifiers, is an extension of the many-sorted polyadic modal logic with the binder μ.
Therefore, we conjecture that the completeness and decidability of modal μ-logic can be generalized to the completeness and decidability of the *quantifier-free fragment* of MmL (QF-MmL), without FOL ∀/∃ quantifiers or element variables.
Specifically, we conjecture that:

- QF-MmL has a (locally) complete proof system, given as the proof system of MmL, from which all axioms/rules about quantifiers are removed;
- The SATISFIABILITY of QF-MmL is decidable in EXPTIME.

Note that both the completeness and decidability of modal μ-logic are proved for the local case, as we discussed in OP1. We in further conjecture that the above two statements about QF-MmL also hold in the global sense for all theories.

**OP3. Henkin semantics of MmL and its completeness**

In the MmL paper, we capture precisely natural numbers with addition and multiplication in MmL, which shows that MmL cannot have a proof system that is both sound and complete.
This drives us to look for an *alternative semantics* of MmL, where the least fixpoint patterns are not interpreted as the true least fixpoints in the models, but only the least fixpoints that are *expressible* in the logic.
Such an alternative semantics is called Henkin Semantics, or General Semantics, in second-order logic or FOL with least fixpoints.
Here, the open problem is to propose a similar Henkin semantics for MmL, and prove that the proof system we gave in the MmL paper is *complete* w.r.t. to the Henkin semantics.