Source-linked AI summary
Positive Topology and Feasible Refinement: Forcing Matrices, Positivity, and Information
Mirco A. Mannucci, Giovanni Sambin
TL;DR
The paper asks how a relation between points and observables can support both universal refinement and witnessed feasibility. It induces cover and positivity from that relation and shows that the forcing relation can be recovered from either residual; resource-enriched semantics remains an open program.
Problem
Method
Results
The forcing relation is recoverable from either left adjoint, while a point forcing a generator makes that generator positive.
Source: §5.1 · p. 8, §8 · p. 10Takeaways & Limitations
Compatibility makes refinement sound by requiring that refining a hypothesis does not lose its witnesses.
Source: §5.3 · p. 8The resource-enriched framework remains a bridge to future work, with its value structure, truth-relation recovery, thresholds, and logical interactions not fixed here.
Source: §9.3 · p. 12
Abstract
from arXiv · showhide
We develop a conceptual and operational account of Positive Topology starting from a basic relation between points or models and observable properties. From this relation, two complementary structures emerge. The first captures universal refinement and cover: what must hold across all relevant cases and how information can be systematically refined. The second captures positivity and witnessed existence: what can be positively realized and sustained without relying on classical complements. A central result shows that the underlying relation between points and observables can be reconstructed from either of these induced structures. We also clarify the distinction between point-based and pointfree formulations: when points are available, positivity can be derived from the underlying forcing relation, while in the formal pointfree setting positivity is taken as primitive and its compatibility with cover is imposed axiomatically. We develop two complementary interpretations of the framework. The first is information-theoretic, viewing cover as refinement of partial information and positivity as witnessed feasibility. The second is game-theoretic, viewing positivity as the ability of a witness or hypothesis to survive successive legitimate refinements. The final part of the paper is deliberately programmatic. We outline how resource constraints, verification costs, and finite budgets can be incorporated into the framework. This leads to resource-sensitive notions of forcing, cover, positivity, and refinement, and raises new questions about how these structures behave as available resources change. Examples from medical diagnosis, legal reasoning, and AI systems illustrate the potential relevance of the approach to grounded, explainable, and resource-aware inference.
1 Introduction: Why Positive Topology?
Positive Topology pairs universal cover, which tracks semantic implications, with positivity, which tests for witnessed realizability. The paper motivates this pairing through diagnosis and extends it to other domains, while identifying witness preservation under refinement as a compatibility condition.
1.1 A motivating example: Medical diagnosis
- A cover records that whenever a condition holds, some observable in the covering set holds; positivity asks whether a profile is realizable by a witness.The medical example contrasts a realizable symptom cluster with an inconsistent combination.Source: §1.1 · p. 3
The compatibility axiom.
- Compatibility requires diagnostic refinement to preserve witnesses, making witness preservation the framework's soundness condition.For example, a pneumonia witness confined to a profile yields a fever, cough, or infiltrates witness confined to that profile.Source: The compatibility axiom · p. 3
1.2 The general pattern
- Across domains, points represent states or models and observables represent properties; cover expresses entailment, positivity witnessed consistency, and forcing connects the two.Examples include medicine, law, programming, finance, science, and AI; the resource-aware extension is left as a programmatic direction for a subsequent article.Source: §1.2 · p. 4
2 The starting datum: a forcing/incidence relation
The paper starts from an incidence relation between points and observables, then induces universal cover and an extensional topology on points. The resulting structures encode observable behavior while identifying points that share the same neighborhood profile.
2 The starting datum: a forcing/incidence relation
- A forcing table is a relation between points or models and basic opens or observables, interpreted as which observables each point satisfies.The relation can be viewed as a Boolean-valued matrix.Source: §2 · p. 4
3.1 Direct image and the universal residual
- The direct image and its universal residual form an adjunction, with the residual selecting observables whose forced points all lie in a given set.The maps are ext and 2, with ext U ⊆ E iff U ⊆ 2E.Source: §3.1 · p. 5
3.2 Cover and the pointfree (formal-cover) side
- Cover means every point forcing a is also forced by some member of U, so it captures universal semantic entailment.In the medical example, a disease condition covers a set of symptoms when every patient with that condition exhibits at least one of them.Source: §3.2 · p. 5
3.3 Extensional topology on points
- The operator int = ext ◦ 2 extracts the largest extensional open contained in a set, and its fixed points are precisely the extensional opens.Pointfree semantics identifies points with the same observable neighborhood behavior rather than preserving their multiplicity.Source: §3.3 · p. 6
4 The second adjunction: positivity via 3 ⊣rest
The positivity construction pairs a constraint-selected set of points with an existential map that records which observables they witness. These maps form an adjunction, giving positivity a witnessed, complement-free interpretation.
4.1 Neighborhood sets and constraint-selected points
- The neighborhood set of a point records its observable profile, while rest U selects points whose entire neighborhood behavior lies in U.In the medical example, this selects patients with no symptoms outside the specified cluster.Source: §4.1 · p. 6
4.2 The existential “hit” map
- The hit map 3D collects observables witnessed by at least one point in D, and 3 ⊣ rest expresses the resulting adjunction.Equivalently, 3D ⊆ U exactly when D ⊆ rest U; this treats U as a closed-like constraint without using negation.Source: §4.2 · p. 7
5 Positivity and closed sets without complements
Positivity is defined through witnessed existence: a basic observable is positive when a point realizes it while its full neighborhood stays within a specified code. The resulting operator is idempotent, and its compatibility with cover preserves witnesses under refinement.
5.1 The positivity operator J = 3 ◦rest
- a ⋉U means a point realizes a while all its basic neighborhoods lie in U, so positivity detects symptom combinations that actually occur.A point forces positivity for any generator it satisfies and any U containing its neighborhood behavior.Source: §5.1 · pp. 7–8
5.2 Elementary properties
- J is contractive, monotone, and idempotent; its fixed points are formal closed codes in which each admitted observable has a witness whose profile stays inside the code.This gives closedness a positive, constructive interpretation rather than one based on complements.Source: §5.2 · p. 8
5.3 The compatibility axiom
- Compatibility is provable when cover and positivity come from points, but is assumed axiomatically in the formal setting to ensure refinement does not lose witnesses.It is the soundness condition connecting cover-based refinement with positive witnesses.Source: §5.3 · p. 8
6 Information content and refinement games
Cover treats a generator as partial information that can be refined into feasible subcases; positivity means a witnessed possibility of continuing rather than classical negation of emptiness. In the refinement game, positivity gives the witness a strategy that survives successive challenges.
6 Information content and refinement games
- A cover refines partial information into feasible subcases, while positivity marks a witnessed possibility of continuing the refinement process.The account treats existence as more than classical negation of emptiness.Source: §6 · p. 9
6.1 The refinement game G(a, U)
- If a ⋉U, Witness can answer every cover challenge with a position in U; a point witnessing positivity supplies this winning strategy.Refiner chooses a cover and Witness chooses a subcase, keeping each position inside U.Source: §6.1 · p. 9
- In the legal-reasoning analogy, opposing counsel demands finer distinctions and the advocate must find a precedent at each challenge.Positivity corresponds to having a real case to cite throughout the exchange.Source: §6.1 · p. 10
7 Two adjunctions and four operators
The forcing relation induces two adjunctions and four operators, assigning distinct roles to points, observables, and subsets of each. Their composites yield saturation and interior on opens, and reduction and closure on positive codes and points.
7 Two adjunctions and four operators
- The two adjunctions arising from the forcing relation provide four maps between point sets and observable sets.These are ext, 2, 3, and rest.Source: §7 · p. 10
- ext sends observable sets to points satisfying some observable, while 2 returns observables universally valid on a set of points.Source: §7 · p. 10
- 3 records observables witnessed in a point set, and rest selects points confined to an observable profile; their composites yield reduction and closure, alongside saturation and interior from ext and 2.The composites are J = 3 ◦rest, cl = rest ◦3, A = 2 ◦ext, and int = ext ◦2.Source: §7 · p. 10
8 Reconstruction of forcing from residuals
The forcing relation can be recovered from its induced residual structure through singleton reconstruction. However, either composite alone generally loses witness-level information.
8 Reconstruction of forcing from residuals
- The reconstruction principle relies on left adjoints preserving joins and being determined by their action on singletons.Source: §8 · p. 10
- The forcing relation is uniquely determined by the extensional map arising from it, using singleton reconstruction.For ext, membership of a point in ext U is equivalent to satisfying some observable in U.Source: §8 · p. 10
- The composites j = 2 ◦ext and J = 3 ◦rest generally lose witness-level information, so a single composite does not determine forcing.The residual pair, rather than either composite alone, determines forcing.Source: §8 · p. 10
9 Feasible refinement and resources: a programmatic sketch
This section sketches a resource-bounded extension as a programmatic direction, not part of the survey’s mathematically established core.
9.1 Truth first, cost second: a minimal baseline
- Budgeted forcing requires both truth at a point and verification cost within the budget, so increasing budgets yields a monotone filtration of forcing relations.The proposed baseline assigns costs to true incidences; it does not treat affordability as truth.Source: §9.1 · p. 11
9.2 Budget-indexed covers and positivity: the next problem
- At each fixed budget, cover and positivity can be induced from budget-restricted forcing, but their variation across budgets has no automatic monotonicity law.The section defers conditions for useful coherence among the budget-indexed families.Source: §9.2 · p. 12
9.3 Enriched values: an outlook, not a final semantics
- An enriched value structure could recover ordinary and budget-indexed forcing and suggest an enriched positivity operator, but its semantics and interaction with logical rules remain unsettled.The proposal assumes a sufficiently complete residuated monoidal order; the precise value object and threshold role are left for later work.Source: §9.3 · p. 12
10 Conceptual summary and outlook
The survey distinguishes its developed formal layers from its announced resource programme. It then sketches a possible budget-indexed logical semantics and points to AI engineering as an application context.
10 Conceptual summary and outlook
- Forcing and the two adjunctions, along with cover, positivity, and closedness without complements, are developed here; the resource layer remains a research programme.The survey explicitly distinguishes the status of these three layers.Source: §10 · p. 12
10.1 Outlook: toward budget-indexed truth
- A future resource logic would define satisfaction over semantic states, syntax, and budgets, while its syntax, budget algebra, structural rules, and link to positivity remain open.The proposed semantics is distinct from the budgeted incidence relation of Section 9.Source: §10.1 · p. 13
A Application to AI engineering
- The appendix presents forcing, positivity, and cost as providing concrete engineering value for AI systems.Source: A Application to AI engineering · p. 13
A.1 The AI analogue of forcing
The appendix maps Positive Topology’s formal structures to AI-system evaluation and sketches how they might inform safety and LLM workflows. It presents that workflow as illustrative, with important typing and formalization boundaries.
A.1 The AI analogue of forcing
- The Boolean forcing table can serve as an AI evaluation matrix whose observables are system constraints, with resource-sensitive constructions as possible refinements.Example constraints include successful tool calls, disallowed-content checks, and latency limits.Source: §A.1 · p. 13
A.2 Two adjunctions = two engineering operations
- The two adjunctions correspond to specification refinement and witness finding, supporting specification management, counterexample search, and safe operating-region identification.The appendix characterizes these as engineering operations over traces and checks.Source: §A.2 · p. 13
A.3 Positivity = safety envelopes
- Positivity offers a constructive safety alternative: a closed code U with JU = U is a safety envelope, understood as a robust region rather than a complement.The motivation is that complements may be unobservable and violations sparse and adversarial.Source: §A.3 · p. 14
A.4 LLM + PosTop: an illustrative architecture
- The proposed LLM workflow is an architectural schema, not a theorem; it requires encoding hypotheses into the formal structure and representing the observation state.Its cover-check direction depends on representation, and a fully typed account of hypotheses, observations, resource choice, and agent traces is deferred.Source: §A.4 · p. 14
B Software and Reproducibility
The appendix describes the software accompanying the survey and gives instructions for setting up the environment, running examples, and executing notebooks and tests.
B Software and Reproducibility
- The repository implements forcing, adjunction, cost-aware, and explainability components, with examples and tests organized alongside the paper and code.The sources are snapshot together with the paper under version tags, and the environment is pure Python with pytest.Source: B Software and Reproducibility · p. 15
B.1 Environment setup
- The environment setup uses a virtual environment and installs the package with its development dependencies.The stated commands create and activate .venv, then run pip install -e .[dev].Source: §B.1 · p. 15
B.2 Running the examples
- The medical and guardrail scripts print operator results, compatibility witnesses, and guardrail counterexamples corresponding to formal statements.Source: §B.2 · p. 15
B.3 Notebooks and tests
- The appendix describes headless notebook execution and tests for adjunction and proof obligations, including mathematical invariants and explainability helpers.The tests cover idempotence and contractivity.Source: §B.3 · p. 16