2 Logic Types: Pluralistic Reasoning Framework
2.1 Logic Type Hierarchy
An inductive type enumerating 13 reasoning paradigms.
Each handles specific classes of paradoxes as boundary conditions rather than errors.
Classification of logic types as Substructural, Extension, Alternative, Generalization, or Classical.
A type family assigning EML trees to each logic type. Currently uniform; extensible to logic-specific tree types.
A type family of contraction relations indexed by LogicType. For Classical logic this is the Tamari contraction from EMLRegistry.
A structure specifying forward and backward maps between logic types with soundness and completeness proofs.
Cross-logic contraction allowing reasoning that spans multiple logic types via intra-logic contraction, inter-logic translation, and transitivity.
2.2 Cayley-Dickson Connection
Maps logic types to Cayley-Dickson construction steps.
Divides logic types into associative and non-associative sectors of the split-octonion algebra.
2.3 Normal Forms and Contraction Theorem
The normal form for each logic type. For Classical logic this is rightComb.
For any logic type \(lt\) and tree \(t\), \(\mathsf{LogicContraction}\ lt\ t\ (\mathsf{LogicNormalForm}\ lt\ t.\mathsf{size})\). Proven for all 13 logic types via \(\mathsf{contracts\_ to\_ rightComb}\).
2.4 Logic Monad: Self-Contained Self-Reference
The free monad over binary trees: \(\mathsf{LogicM}\ \alpha \) is a tree whose leaves carry values of type \(\alpha \) and whose internal nodes represent non-associative composition of computations.
\(\mathsf{pure}\ a\) = a leaf containing \(a\) (a completed computation)
\(\mathsf{node}\ l\ r\) = deferred composition of two sub-computations
\(\mathsf{bind}\) = substitution: replace every leaf with a new tree
This is self-contained by definition (recursive structure IS self-reference) and extensible (interpreters fold over \(\mathsf{LogicM}\ \alpha \) to produce any target monad).
The free monad \(\mathsf{LogicM}\) satisfies the three monad laws:
\(\mathsf{pure}\ a \gg \! \! = f = f a\) (left identity)
\(m \gg \! \! = \mathsf{pure} = m\) (right identity)
\((m \gg \! \! = f) \gg \! \! = g = m \gg \! \! = (\lambda x.\ f x \gg \! \! = g)\) (associativity)
Proof by structural induction on the tree.
For each logic type \(\mathsf{lt}\), the \(\mathsf{LogicMonad}\ \mathsf{lt}\ \alpha \) structure wraps a \(\mathsf{LogicM}\ \alpha \) and normalizes it via \(\mathsf{LogicContraction}\ \mathsf{lt}\). The normalization cost is \(\mathsf{cdStep}\ \mathsf{lt}\).
This is the minimal monad for each logic: it does the least work (pure substitution) and then normalizes using that logic’s contraction dynamics. The self-reference property of the free monad (bind = substitution) means every logic monad shares the same core recursion — they differ only in how they normalize.
The pluralistic logic monad transcends identity: the monad structure (pure, bind, the laws) is invariant under change of logic. Only the normalization differs. This means the “eternal” layer (pure functional composition) is common to all logics; the “endless” layer (iteration, normalization cost) is what distinguishes them.
The forgetful functor from \(\mathsf{LogicMonad}\ \mathsf{lt}\) to \(\mathsf{LogicM}\) is an isomorphism of monads for any \(\mathsf{lt}\). Only the normalization (LogicContraction) changes between logics.
2.5 Institutional Closure: Interacting Logic Monads
The institutional closure pipeline composes four layers:
Temporal normalization — linearize the event timeline via \(\mathsf{LogicContraction\ Temporal\ =\ contracts\_ to}\).
Fuzzy grading — evaluate each event’s impact through graded membership (Sorites-like gradation).
Deontic update — revise norms from accumulated blame, using \(\mathsf{LogicContraction\ Deontic}\).
Self-recognition — the monadic bind that identifies the output norm as the institution’s own (fixed point).
The pipeline is a monadic computation \(\mathsf{LogicM\ Event \to LogicM\ Norm}\) using the shared \(\mathsf{LogicM}\) backbone, with logic-specific normalization at each layer.
\(\mathsf{selfRecognize} \circ \mathsf{closure} = \mathsf{closure}\): self-recognition is a fixed point. Once the pipeline has produced a norm, further recognition does not change it.
\(\mathsf{closure} \circ \mathsf{temporalNormalize} = \mathsf{closure}\): the normalization pipeline is a projection. Re-processing an already- normalized history yields the same norm.
2.6 Decision Composition API
A Gate is a binary decision predicate indexed by a logic modality: \(\mathsf{Gate} = (\mathsf{name} : \mathsf{String}) \times (\mathsf{modality} : \mathsf{LogicType}) \times (\mathsf{check} : \mathsf{EMLTree} \to \mathsf{Prop})\). Every logic type gives rise to a Gate via \(\mathsf{ofLogicType}\), and every tree passes any such gate (by 26).
A Decision is the refinement type from the specification: \(\mathsf{Decision\ gates} = \{ d : \mathsf{EMLTree} \mid \forall g \in \mathsf{gates},\ g.\mathsf{check}\ d \} \). The type parameter \(\mathsf{gates}\) IS the channel: downstream functions know statically which gates the datum has passed.
\(\mathsf{compose} : \mathsf{Decision\ gates} \to \mathsf{Gate} \to \mathsf{Decision\ (g :: gates)}\). The return type is strictly richer than the input type: a gate is added to the type-level history.
The mirror image of \(\mathsf{rightComb}\): \(\mathsf{leftComb}(0) = \mathsf{Leaf}\) and \(\mathsf{leftComb}(n+1) = \mathsf{Node}(\mathsf{leftComb}(n),\ \mathsf{Leaf})\). Unlike \(\mathsf{rightComb}\), this is not the equilibrium attractor — it represents a fully left-associative configuration.
A LogicPipeline is a sequence of logic types to run as gates. Running it on a tree produces a Decision tagged with all of them. The institutional closure is a pipeline with gates Temporal, Fuzzy, Deontic.
For any tree and any gate in the closure pipeline, \(\mathsf{soundness}\) guarantees the gate check holds. This is the compile-time contract: the type signature IS the channel.
\(\mathsf{decide}\) runs the institutional closure on \(\mathsf{LogicM\ Event}\) and produces a Decision whose datum passes all closure gates. The channel is the type: \(\mathsf{Decision\ (closurePipeline.gates)}\).
2.7 Paradox Taxonomy
An inductive type enumerating 12 paradox classes, each with a native logic type: self-reference (ManyValued), vagueness (Fuzzy), inconsistent definition (Paraconsistent), temporal decision (Temporal), deontic (Deontic), epistemic (Epistemic), quantum superposition (Quantum), constructive (Intuitionistic), relevance (Relevance), empty reference (Free), infinity (Infinitary), modality (Modal).
A structure parameterized by a problem class, a name, a list of suitable logics, a tree family \(\mathsf{LogicType} \to \mathsf{EMLTree}\) (the paradox as encoded in each logic), and a normal form family \(\mathsf{LogicType} \to \mathsf{EMLTree}\) (the resolution target for each logic).
The WfCA collapse rule: pairs a Problem with a LogicType. Records the tree (problem as interpreted in this logic), target (normal form), cost (pentagonator distance \(\Phi \)), and proof (contraction path). A problem’s superposition of possible resolutions collapses to the definite outcome given by the logic type’s contraction rule.
2.8 The Liar as a Problem Instance
The Liar Paradox stated as a Problem of class \(\mathsf{selfReference}\). Its tree is the size-3 symmetric tree \(\mathsf{Node}(\mathsf{Node}(\mathsf{Leaf},\ \mathsf{Leaf}),\ \mathsf{Node}(\mathsf{Leaf},\ \mathsf{Leaf}))\) for most logics, except ManyValued which uses a size-2 left-comb encoding the three-valued disjunction \(\mathsf{True} \lor \mathsf{False} \lor \mathsf{Undefined}\). All logics target \(\mathsf{rightComb}(3)\) as the normal form.
2.9 Liar Wrappers
The Liar wrapped in Fuzzy logic. The fixed point \(\neg 0.5 = 0.5\) gives pentagonator distance \(\Phi = 1\) (CD step 1). Proven via the generic liarWrapper.
A Problem of class \(\mathsf{metaParadox}\) constructed from any existing Problem and LogicType whose proof is missing.
The Liar wrapped in Classical logic. Cost \(\Phi = 0\) (at equilibrium). Proven using \(\mathsf{contracts\_ to\_ rightComb}\): the symmetric tree contracts to \(\mathsf{rightComb}(3)\) in finitely many steps.
2.10 Nested Wrappers (Stacked Collapse)
A sequence of logic-wrapped problems, each collapsing the previous layer’s output. Implements the nested wrapper pattern from Lumo section B:
Each layer’s logic type is tracked via a dependent pair \(\Sigma lt,\ \mathsf{WrappedProblem}\ p\ lt\). The total cost is the sum of per-layer costs.
A four-layer prototype tower alternating Classical and Fuzzy wrappers. Demonstrates the stacked collapse pattern; the full tower with Quantum, Intuitionistic, Fuzzy, and Classical layers is not yet populated because non-Classical LogicContractions are missing.
2.11 Temporal Paradox Problem
The Grandfather Paradox stated as a Problem of class \(\mathsf{temporalDecision}\). Its tree is a left-comb chain of size 4, encoding the 4-step time-travel causal loop: traveler exists \(\to \) travels back \(\to \) grandfather killed \(\to \) traveler never born (contradiction). The normal form is \(\mathsf{rightComb}(4)\).
For any logic lt, constructs the WrappedProblem with \(\textsf{cost} = \textsf{cdStep}(\textsf{lt})\). Resolves the temporal causal loop via \(\mathsf{contracts\_ to\_ rightComb}\).
The Grandfather tower: one layer per suitable logic.
The cost \(\Phi (\text{Grandfather}, \text{lt})\), equal to \(\textsf{cdStep}(\text{lt})\).
\(\textsf{grandfatherCost}(\text{lt}) \le \textsf{cdStep}(\text{lt})\) for every logic type.
2.12 Russell’s Paradox Problem
Russell’s Paradox stated as a Problem of class \(\mathsf{inconsistentDef}\). Its tree is a left-comb chain of size 3, encoding the three levels of set-theoretic diagonalization: elements \(\to \) self-membership predicate \(\to \) the set of all sets not containing themselves. The normal form is \(\mathsf{rightComb}(3)\).
Disclaimer: This formalization is deliberately incomplete with respect to the infinity/eternity axis. The “cheat” of setting cost \(= \textsf{cdStep}\) captures only the Cayley–Dickson property-loss dimension, not the regularization dimension (endless \(\to \) eternity \(\to \) actual \(\infty \to \) boundlessness). Future work must pin this axis down properly; here we procrastinate it using the same wrapper pattern as Liar/Sorites/Grandfather.
For any logic lt, constructs the WrappedProblem with \(\textsf{cost} = \textsf{cdStep}(\textsf{lt})\). Resolves set-theoretic diagonalization via \(\mathsf{contracts\_ to\_ rightComb}\).
The Russell tower: one layer per suitable logic.
The cost \(\Phi (\text{Russell}, \text{lt})\), equal to \(\textsf{cdStep}(\text{lt})\).
\(\textsf{russellsCost}(\text{lt}) \le \textsf{cdStep}(\text{lt})\) for every logic type.
2.13 The Very Big Box
The Very Big Box is the product space
where each coordinate is a problem in a specific logic and the Tower construction provides the nesting structure. Currently four problem classes are populated: \(\mathsf{selfReference}\) (Liar), \(\mathsf{vagueness}\) (Sorites), \(\mathsf{temporalDecision}\) (Grandfather), and \(\mathsf{inconsistentDef}\) (Russell’s). The remaining 9 classes represent the real friction: every cell in this product that lacks a proof is a concrete blocker.
2.14 Sorites as a Problem Instance
The Sorites (Heap) Paradox stated as a Problem of class \(\mathsf{vagueness}\). Its tree is a left-comb chain of size 5, encoding the inductive threshold: “If \(n\) grains form a heap, then \(n-1\) grains form a heap.” The normal form is \(\mathsf{rightComb}(5)\).
For any logic lt, constructs the WrappedProblem with \(\textsf{cost} = \textsf{cdStep}(\textsf{lt})\). Follows the same pattern as the generic Liar wrapper, using \(\mathsf{contracts\_ to\_ rightComb}\).
The Sorites tower: one layer per suitable logic, analogous to the Liar tower.
The cost \(\Phi (\text{Sorites}, \text{lt})\), equal to \(\textsf{cdStep}(\text{lt})\).
\(\textsf{soritesCost}(\text{lt}) \le \textsf{cdStep}(\text{lt})\) for every logic type.
2.15 Decomposition: Ontological Underdetermination
A witness of a contraction path through the Tamari lattice: \(\mathsf{Path}\ s\ t\) is an inductive sequence of \(\mathsf{contracts\_ one}\) steps from \(s\) to \(t\).
\(\mathsf{nil}\) — the trivial path (reflexivity).
\(\mathsf{cons}\ h\_ one\ p\) — prepend a single contraction step to an existing path.
For any path \(p : \mathsf{Path}\ s\ t\), we have \(\mathsf{contracts\_ to}\ s\ t\). The path provides constructive evidence for the existence of a contraction sequence.
The number of contraction steps in a path: \(\mathsf{length}(\mathsf{nil}) = 0\), \(\mathsf{length}(\mathsf{cons}\ h\_ one\ p) = 1 + \mathsf{length}(p)\).
Concatenates two compatible paths: \(\mathsf{append} : \mathsf{Path}\ s\ t \to \mathsf{Path}\ t\ u \to \mathsf{Path}\ s\ u\).
2.16 Reverse Contraction: Generating Predecessors
Generates all immediate predecessors of a tree under \(\mathsf{contracts\_ one}\). For a target tree \(t\), \(\mathsf{reverse\_ one}(t)\) is a list of all \(s\) such that \(s \to t\) in one step. Three structural cases:
\(\mathsf{Leaf}\) has no predecessors.
\(\mathsf{Node}\ l\ (\mathsf{Node}\ r_1\ r_2)\): the rotation target plus predecessors from reversing the left and right subtrees.
\(\mathsf{Node}\ l\ r\) (right child not a Node): predecessors from reversing the left and right subtrees only.
This is the core de-composition primitive: given an outcome, what could have immediately preceded it?
If \(s \in \mathsf{reverse\_ one}(t)\) then \(\mathsf{contracts\_ one}\ s\ t\). Every generated predecessor is a valid immediate prior configuration.
If \(\mathsf{contracts\_ one}\ s\ t\) then \(s \in \mathsf{reverse\_ one}(t)\). Every valid immediate predecessor is generated.
2.17 Decomposition Structure
For a target tree \(\mathsf{target}\), a \(\mathsf{Decomposition}\) pairs a \(\mathsf{source}\) with a proof \(\mathsf{contracts\_ to}\ \mathsf{source}\ \mathsf{target}\). This is the ontological unit of de-composition: an outcome together with a specific prior configuration that could have produced it.
\(\mathsf{size}(\mathsf{leftComb}\ n) = n\).
\(\mathsf{size}(\mathsf{rightComb}\ n) = n\).
For \(n \ge 2\), \(\mathsf{rightComb}\ n \neq \mathsf{leftComb}\ n\). The two canonical trees of size \(n\) are distinct in the Tamari lattice.
For \(n \ge 2\), the target \(\mathsf{rightComb}\ n\) has at least two distinct Decompositions with different sources:
This is the core ontological result: the past is underdetermined by the present. The same outcome (rightComb \(n\)) admits multiple evidential histories (rightComb \(n\) itself and leftComb \(n\), among others).
There exist two distinct paths between the same source-target pair in \(T_3\):
Explicitly, \(\mathsf{leftComb}\ 3 \to \mathsf{rightComb}\ 3\) has two distinct maximal chains in the Tamari lattice:
\(((ab)c)d \to (a(bc))d \to a((bc)d) \to a(b(cd))\) (3 steps)
\(((ab)c)d \to (ab)(cd) \to a(b(cd))\) (2 steps)
This proves that intent is not uniquely determined by outcome — multiple reasoning chains can connect the same evidence to the same verdict.
2.18 The Hypercomputer: Infinite Ancestor Enumeration
The immediate predecessor sources of a target tree \(\mathsf{predecessors}(t) = \mathsf{reverse\_ one}(t)\). Soundness is maintained as a separate theorem \(\mathsf{predecessors\_ sound}\): if \(s \in \mathsf{predecessors}(t)\) then \(\mathsf{contracts\_ one}\ s\ t\).
A finite chain of contraction steps from an ancestor to a target. \(\mathsf{Chain.tip}\ t\) is the empty chain (the present moment without a reconstructed past). \(\mathsf{Chain.link}\ h\ r\) prepends a contraction step.
Enumerate all ancestor sources up to depth \(n\) via DFS, returning a flat list. This is the hypercomputer in function form: the infinite tree of all possible pasts is present as the limit of \(\mathsf{ancestorsUpTo}\ t\ n\) as \(n \to \infty \). No single data structure holds the whole tree; instead the recursion is explicit in the partial function, and every finite approximation is immediately available. “Instant lookup” = calling this function with any depth \(n\).
A \(\mathsf{viewDFS}\) is a single lineage (DFS) extracted from the ancestor space by always following the first predecessor. Returns a \(\mathsf{Chain}\) that may end at any depth. This is the narrative self in formal type: committed to a single thread, but honest about termination.
Lean 4 Coinductive Limitation
The infinite ancestor tree cannot be represented as a closed coinductive data type in Lean 4 because coinductive is restricted to Prop-valued predicates, and nested inductives with Prop fields through List and Sigma are rejected by the kernel positivity checker. The workaround (partial functions) is not a limitation of the framework but a design choice: the hypercomputer exists as the limit of finite approximations, not as a closed value. This matches the ontology: the infinite crystal seed is not a thing we hold, but a thing we approach.
2.19 Boundlessness: The Terminal Regularization
The regularization ladder (endless \(\to \) eternal \(\to \) actual \(\infty \to \) boundlessness) is capped by the idempotent resolution framework: a boundary-response operation that is already idempotent is already at its own limit.
An idempotent resolution for a type \(\alpha \) consists of:
\(\mathsf{step} : \alpha \to \alpha \), a regularization step that is idempotent (\(\mathsf{step} \circ \mathsf{step} = \mathsf{step}\)).
\(\mathsf{limit} : \alpha \to \alpha \), the limiting configuration reachable in one step from any image of \(\mathsf{step}\) (\(\mathsf{limit} = \mathsf{step} \circ \mathsf{limit}\)).
The canonical example is rightCombResolution, where \(\mathsf{step}(t) = \mathsf{rightComb}(t.\mathsf{size})\): every tree is mapped to its right-comb normal form in one step, and applying the step again does nothing because a right-comb is already in normal form.
\(\mathsf{size}(\mathsf{rightComb}\ n) = n\) for all \(n : \mathbb {N}\).
The Very Big Box is the product of idempotent resolutions over all populated problem classes:
The canonical veryBigBox assigns rightCombResolution to each coordinate.
The step function of rightCombResolution is already its own fixed point:
This is the terminal regularization: applying boundary-response again changes nothing. Not because there is nothing more to say, but because saying more is already captured by the first application.
Applying rightComb normal form to a tree that is already a rightComb is the identity:
Boundlessness is not a structure we build, but a property we recognize.
Relation to the Hypercomputer.
The idempotent resolution caps the hypercomputer: where \(\mathsf{ancestorsUpTo}\) approaches the infinite ancestor tree by finite approximation, the idempotent resolution declares that the limit has been reached. The Very Big Box is the product closure of all problem classes, and boundlessness is the fixed point that requires no further iteration. This is the formal declaration that the framework is closed under its own boundary-response operation.
2.20 Completed Work
All LogicContraction, LogicNormalForm, and logic_contracts_to_normal_form definitions are filled and proven for all 13 logic types. The Liar problem has a complete WrappedProblem for each suitable logic via liarWrapper. The Sorites and Grandfather problems follow the same pattern with soritesWrapper and grandfatherWrapper.
The Decomposition infrastructure (Path, reverse_one, Decomposition, predecessors, ancestorsUpTo, Chain, viewDFS) is complete with soundness, completeness, non-unique-decomposition, and path-diversity theorems proven for all \(n \ge 2\) in \(T_n\) — zero sorries.
The Friction Lagrangian \(\mathcal{L}_{\text{friction}}\) is computed from the full Liar tower. The blocking chain for the Liar is fully resolved.
2.20.1 Remaining Work
Other problem classes — \(\mathsf{selfReference}\) (Liar), \(\mathsf{vagueness}\) (Sorites), \(\mathsf{temporalDecision}\) (Grandfather), and \(\mathsf{inconsistentDef}\) (Russell’s) are instantiated. The other 9 classes (deontic, epistemic, quantum, etc.) need Problem definitions with their own tree families.
Tower composition — the current towers are flat (all logics stacked). The institutional closure pipeline demonstrates a first step toward nested composition (temporal \(\to \) fuzzy \(\to \) deontic \(\to \) self-recognition). Full LogicTranslation instances between adjacent logics remain.
Shortest-path cost — the \(\Phi \) cost currently equals \(\textsf{cdStep}\) by definition; a BFS algorithm over \(\textsf{reverse\_ one}\) would compute the actual PentagonatorDistance.
Ancestor enumeration — \(\mathsf{reverse\_ one}\) can be iterated to produce \(\mathsf{ancestorsBounded}\), a bounded BFS generating all distinct sources for a given target with \(\mathsf{Path}\) witnesses.
Path cost — a \(\mathsf{pathCost}\ lt\ p\) function summing \(\mathsf{cdStep}\) per logic type along a path, enabling cross-logic cost comparison for the same reasoning chain.
Decision decomposition — extend the DecisionComposition API with \(\mathsf{decisionDecompositions}\) that enumerates all prior decisions that could compose to a given decision.
Regularization axis — the institutional closure sketch uses placeholder normalization; the full endless/eternal/infinite/boundless hierarchy must be formalized to compute real costs.
2.20.2 Liar Cost: Hardness Measure
The Liar as perfect anti-coherence (\(X = \neg X\)) gives a hardness measure for each logic: how many contraction steps are required to resolve it.
The cost \(\Phi (\text{Liar}, \text{lt})\) to resolve the Liar under logic lt. Conjectured to equal the Cayley–Dickson step.
\(\textsf{liarCost}(\text{lt}) \le \textsf{cdStep}(\text{lt})\) for every logic type. For Classical and Fuzzy the bound is tight (equality).
For any logic lt, constructs the WrappedProblem with \(\textsf{cost} = \textsf{liarCost}(\text{lt})\). Fills all 12 mail slots.
\(\textsf{liarCost}(\text{Classical}) = 0 = \textsf{classicalLiar.cost}\).
\(\textsf{liarCost}(\text{Fuzzy}) = 1 = \textsf{fuzzyLiar.cost}\).
2.20.3 Friction Lagrangian
The tower sums costs across all logic layers. The total Friction Lagrangian \(\mathcal{L}_{\text{friction}} = \sum _{\text{lt}} \Phi (\text{Liar}, \text{lt})\) is the total resistance of the logical ecosystem to self-negation.
The sum of \(\Phi \) costs across all layers of the Liar tower.
With all 12 suitable logics, the Friction Lagrangian converges to a stable value:
This is the “curvature of mind” — the total structural work the system must do to resolve perfect anti-coherence across the full space of logics.
The blocking chain is now fully resolved for the Liar problem. Previously the sorries in LogicTypes.lean were abstract goals; now every definition and theorem is filled, and the Very Big Box has its first complete product cell: the Liar across all 12 logics.