  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.

Logic;Logic in Computer Science