On the dependent conjunction and implication

TL;DR

This paper develops a theoretical model for conjunctions and implications where the second component depends on the truth of the first, reflecting common mathematical reasoning and connecting to type theory and the language of mathematics.

Contribution

It introduces an accessible extension of Lawvere's quantifiers to model dependent conjunctions and implications, linking formal logic with mathematical language and intuition.

Findings

Models the dependency of F on E in conjunctions and implications

Connects the concept with Lawvere's quantifiers and type theory

Explains the linguistic and philosophical significance of dependency in mathematics

Abstract

We give a theoretical model of conjunctions $E\wedge F$ and implications $E\implies F$ where $F$ is meaningful only when $E$ is true, a situation which is very often encountered in everyday mathematics, and which was already formalized by several type theorists. We present a version of these concepts which should be more attractive for mathematicians and in particular for non logicians, by using an extension of Lawvere's definition of the quantifiers. We explain the link of this phenomenon with the principle of description, why this dependency is obtained through the use of a "hidden" variable, and more generally the link of these concepts with the vernacular language of mathematics, which is actually our main motivation. Despite its links with topos theory, this article is readable by non specialists.