The property of a deductive system with a conditional connective $\to$ such that

is a theorem only if $\phi$ itself contains an instance of $\to$. The property is named after logician Wilhelm Ackermann (1896–1962), who proved that the property holds of his system $\text{Π}$. Because intuitionistic negation is frequently defined by the scheme $\neg \phi {=}_{df}\phi \to \perp$ (where $\perp$ is the falsum constant), the Ackermann property is sometimes revised so that the condition is that $\phi$ must contain an instance of $\to$ or an instance of a negation $\neg$. A converse Ackermann property has also been studied in which $\left(\phi \to \psi \right)\to \xi$ is a theorem of some deductive system only if $\xi$ contains an instance of the $\to$ connective.