摘要：We outline here a certain history of ideas concerning the relation between intuitions and their external verification and consider its potential for detrivializing the concept of virtuality. From Descartes and Leibniz onward to 19th-century geometry and the concept of “invariant” that it shares with 19th-century psychology, we follow the thread of what might be informally called an “operational” conception of the virtual, an intuition progressively developed in the 20th century from of group theoretical thinking into “functorial” thinking (in the context of category theory), and eventually intuitions for the concept of “univalence” (homotopy type theory) and its implications for the meaning of equality and identity. At each turn, skeptical arguments haunt this history’s modes of exteriorization, proof, and verification; we consider the later Wittgenstein’s worries concerning rule following and the apparent unbridgeable gap between formal theory and informal practice. We show how the development of mathematical intuitions and formalisms in the last century and the discovery of deep connection between intuitionistic logic and computation have begun to respond to some of these concerns and favour a conception of virtuality that is operational, constructive, pragmatic, and hospitible to scientific detrivialization.
