A Foundation for Differentiable Logics using Dependent Type Theory

TL;DR

This paper develops a unified formal framework for differentiable and fuzzy logics using dependent type theory, enabling systematic comparison of their algebraic, analytic, and proof-theoretic properties within a proof assistant.

Contribution

It introduces a formalized, unified language for multiple fuzzy and differentiable logics in a proof assistant, including new sequent calculi and algebraic interpretations.

Findings

Formalization of fuzzy and differentiable logics in a proof assistant

Unified language specification for multiple logics

New sequent calculi for DL2 and STL$_{ ext{infinity}}$

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, {\L}ukasiewicz, G\"{o}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\^opital'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.