Is an empty conjunction in propositional logic true? Consider an illustratory formula
$\psi \equiv \bigwedge_{i \in \emptyset} false$, does $\psi$ valuate to $true$?
Is such a formula ill-formed?
If not, is there a symbol for an empty formula?
The reason why I ask is that I have a definition where I can have a conjunction over a set of constraints, and it would be really helpful if I could interpret an empty set of constraints as true.
 A: With Stefan, I think empty conjunction is equivalent to $\top$ for the following reason within classical propositional logic:
$\Gamma\vDash\Delta\qquad$ iff $\qquad\vDash\bigwedge\Gamma\supset\bigvee\Delta$
Now for the special case $\Delta = \emptyset$,
$\Gamma\vDash\emptyset\qquad$ iff $\qquad\Gamma\vDash\bot\qquad$ iff $\qquad\vDash\bigwedge\Gamma\supset\bot$
and similarly, for the special case $\Gamma = \emptyset$,
$\emptyset\vDash\Delta\qquad$ iff $\qquad\top\vDash\Delta\qquad$ iff $\qquad\vDash\top\supset\bigvee\Delta$
A: It makes a lot of sense anyway. Truth is usually denoted by $\top$. Consider, that $a\wedge \top \equiv \top \wedge a \equiv a$, so $\top$ acts like an identity of $\wedge$. We define empty sums to be $0$, because then certain recursive formulas still work in some "borderline cases". Similarly we should define empty conjunctions to be $\top$. 
Another reason, why that makes sense, is the universal property of a product with some index set $I$ known from category theory . If $I$ is empty, then the product turns out to be a terminal object. The terminal object of a category of propositions, where an arrow $a \to b$ exists, if and only if $a \vdash b$, is $\top$. In lattice theory terminal objects are known as "maximal elements" and products as "infima".
