Negationless intuitionism

The present paper deals with natural intuitionistic semantics for intuitionistic logic within an intuitionistic metamathematics. We show how strong completeness of full first order logic fails. We then consider a negationless semantics à la Henkin for second order intuitionistic logic. By using the theory of lawless sequences we prove that, for such semantics, strong completeness is restorable. We argue that lawless negationless semantics is a suitable framework for a constructive structuralist interpretation of any second order formalizable theory (classical or intuitionistic, contradictory or not).