A New Kind of Science
I can imagine a process where one could use a metalanguage to derive syntactic structures with certain formal properties induced by formal maps between them. This is how I imagine Grothendieck toposes are used in Lawvere's categorical semantics. The way this would work would be like the module system in a high-level functional programming language where one could instantiate syntactic structures at any level by concrete syntactic objects, which might be derivations in some formal deduction system, or they might be programs-cum-proofs in some type theory, or a construction in some algebraic language like a diagram algebra. However what I imagine is not a single formal system one could download and compile. Rather it would be a network of interconnected systems where syntactic structures defined in one place can be instantiated in many others. So it would not grow monolithically like a proof library, but organically like an ecosystem. Subscribe to Thomas Kern . For more...