 Constructive mathematicians, following Bishop, traditionally assume intuitionistic logic and work with strong definitions of concepts. For example, they equate “there is at most one number \(n\) such that \(P(n)\)” with “if \(n\) and \(m\) are distinct numbers then not \(P(n)\) or not \(P(m),\)” rather than the more natural “if \(n\) and \(m\) are numbers such that \(P(n)\) and \(P(m)\) then \(n = m\)”. Shulman [2022] suggests that an “affine” logic of proof and refutation, with additional connectives and an antithesis translation into intuitionistic logic, would be more useful for constructive mathematics.