A Foundation for Differentiable Logics using Dependent Type Theory

TL;DR

This work formalizes differentiable and fuzzy logics in a unified framework, encoded using the Mathcomp library in the Rocq proof assistant, and formalises established sequent calculi for fuzzy logics and proposes new sequent calculi for DL2 and STL, and formalises their soundness in this framework.

Abstract

Differentiable logics are a family of quantitative logics originated in the machine learning literature. Because of their origin, differentiable logics often come equipped with analytic properties that guarantee that they are differentiable. However, they usually lack an accompanying theory that describes their algebraic and proof-theoretic properties. Meanwhile, fuzzy logics, seen as substructural logics, have been studied algebraically and proof-theoretically, and some fuzzy logics with desirable analytic properties have also been used in machine learning. Our aim is to systematically compare analytic, algebraic and proof-theoretical properties of both fuzzy and differentiable logics. To this end, we formalize differentiable and fuzzy logics in a unified framework, encoded using the Mathcomp library in the Rocq proof assistant. We propose a single language specification to encompass multiple logics, using intrinsic typing to only allow valid and well-typed formulas for each of the logics that we encode: Yager, Łukasiewicz, Gödel and product fuzzy logics, as well as the differentiable logics DL2 and STL. Algebraically, we show how these logics can be interpreted using residuated lattices, which are prevalent in the theory of substructural logics. Analytically, we formalise the existence of a positive derivative for certain logical connectives, and to this end we formalise L'Hôpital's, contributing it to the Mathcomp library. Proof-theoretically, we formalise established sequent calculi for fuzzy logics, and we propose new sequent calculi for DL2 and STL$_{\infty}$, and formalise their soundness in our framework.

Figures (10)

• Figure 1: Types and expressions of differentiable logics.
• Figure 2: Generic syntax for differentiable logics in Rocq
• Figure 3: Excerpt of the semantics of STL$_\nu$: conjunction, negation, and comparison. (See Fig. \ref{['fig:semantics-lt0-gt0']} for intermediate definitions ssrstl_and_lt0 and ssrstl_and_gt0.)
• Figure 4: Intermediate definitions to define the conjunction of STL$_\nu$. (The right subfigure reproduces part of Table \ref{['tab:semantics-math']} for reading convenience.)
• Figure 5: Hypersequent calculus for Gödel logic where $\mathcal{G}$ and $\mathcal{H}$ are hypersequents, $Q,\ R,\ P,\ S$ are sequents and $p,p_0,p_1$ are formulas.

Theorems & Definitions (29)

• Example 1.1
• Definition 2.1: Fuzzy Differentiable Logics van2022analyzing
• Definition 2.2: DL2 fischer2019dl2
• Definition 2.3: STL varnai
• Definition 3.1
• Example 3.1
• Definition 4.1
• Definition 4.2: Shadow-lifting property varnai
• Theorem 6.1: Differentiable logics as residuated lattices
• proof