System lock (Girard's epidictic/systems)

[engboris]

Transcendental syntax sees the ability to do quantification (for all, there exists, but also dependent typing) as possible because we have guarantees on the shape of objects within a system we are in.

With the "bare" Stellogen, we have no such garantees of systemic regularities. We need way to enforce such regularities. My idea is to be able to define "systems" (using blocks system ... end) with :

• a set of allowed macros/identifiers;
• a plugin-galaxy which acts like a sort of ID card attached of galaxies of a same system to produce an artificial regularity. Tests can then those plugins (called mould by Girard) into account.

We can also imagine arbitrary typeless labels/tags to categorize the entities of a system. This would allow us to reproduce the distinction between individuals and properties in predicate calculus (first-order logic) for instance.

We can then imagine to open and close scopes for systems with begin some_system and end some_system. Doing so guarantees that everything is done w.r.t the system and it should also allows quantification since there is now enforced regularities.

I'm not sure about the actual design of those things. It's left for discussions. But the point is that we want the behaviour and guarantees of logical systems (Peano arithmetic, natural deduction, intuitionistic logic, classical logic, propositional calculus etc) without being closed to them.