Predicate Logic with Definitions

TL;DR

Predicate Logic with Definitions (PLD) enhances first-order logic by integrating definitions directly into terms and formulas, facilitating practical mathematical formalization and reducing the need for additional quantifiers.

Contribution

It introduces a novel logical framework that incorporates definitions as first-class constructs, enabling more expressive and concise formalizations in mathematics.

Findings

Definitions can be embedded within terms and formulas.

Composite definitions allow building complex definitions from simpler ones.

PLD simplifies formalization by reducing the need for extra quantifiers.

Abstract

Predicate Logic with Definitions (PLD or D-logic) is a modification of first-order logic intended mostly for practical formalization of mathematics. The main syntactic constructs of D-logic are terms, formulas and definitions. A definition is a definition of variables, a definition of constants, or a composite definition (D-logic has also abbreviation definitions called abbreviations). Definitions can be used inside terms and formulas. This possibility alleviates introducing new quantifier-like names. Composite definitions allow constructing new definitions from existing ones.