Papers · Foundations
Six Birds Foundations VII: Lawful Theory Interaction
When two theories combine into something genuinely new, and when the order of combining stops mattering.
In plain words
Two theories, each lawful on its own, are put together. When do they really interact, and when is the result a new theory rather than the two old ones restated? It is easy to answer carelessly. A shared vocabulary gets called interaction. Any new quantity gets called a genuine joint theory. This paper gives a typed certificate language for such claims. Each record keeps apart things that are easily confused: content that is expressible, present, reachable or occurrent; theories that touch versus theories that join; one theory enabling another versus determining it; order mattering versus time having an arrow.
Most of the catalog's 36 entries are definitions, and the paper says so. The mathematics sits in two places. First, an observable of a joint theory is strict, meaning it is not a function of either parent or of the two together, exactly when each of those three views has a pair of states it cannot tell apart but the observable can. Second, if admitting a new item can only ever enable further admissions, every admission order ends in the same final state, by Newman's lemma. A single guard that lets one admission block another is enough to produce two different endings.
A small finite world of two theories anchors the catalog. It is small enough to enumerate and rich enough that every certificate has an instance in it. Twenty seven named countermodels there each show one property without the other. A soundness check links the two levels: a semantic strict join earns the language's strictness certificate, but only once two further facts are also proved. The results are formalized in Lean 4, with the exceptions stated.
What it shows
- A typed certificate language for claims about how theories interact, organized in 36 entries.
- A joint observable is strict exactly when it has a split pair against each parent and against their pairing.
- Admission order does not matter when admission only enables; one disabling guard breaks this.
- Twenty seven countermodels in a finite reference world, with Lean 4 proofs.
What it does not claim
Most catalog entries are definitions or recorded refusals, not theorems. Strictness is tested only against the two parents and their pairing, not against every description of the join. No real scientific theories are instantiated.
Cite
Tsiokos, I. (2026). Six Birds Foundations VII: Lawful Theory Interaction. Zenodo. https://doi.org/10.5281/zenodo.23187549