Proofs of Nonconsequence as Abstract Design in Hyperproof

Design process is a series of activities in which designers try to find or invent entities that satisfy specifications, the specification usually they take as given. The process could be seen as a kind of proof of nonconsequence since the entities must satisfy the specification since they usually invent entities and check if the entities satisfy given specifications, rather than they deduce the entities from the specifications. In this paper, we argue that this similarities between the proof of nonconsequence and the design process are essential, and they makes it possible to formulate the design process in an abstract way. Addition to the above argument, we formulate the logical relation between heterogeneous specifications as heterogeneous logic based on a mathematical theory of design called Abstract Design Theory (ADT), and discuss about such logic in a reasoning system called Hyperproof.