On the dependent conjunction and implication

MaRDI QIDQ6274771zbMATH OpenFDO

Authors Matthieu Herrmann, Alain Prouté

Publication date 20 June 2016

Abstract: We give a theoretical model of conjunctions $EwedgeF$ and implications $EimpliesF$ 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.

This page was built for publication: On the dependent conjunction and implication

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6274771)