Topics — What a work is about. Nucleation holds whatever reading the owner files here, whether or not an Anthology of the SOTA topic could also hold it; instruction for ML practice belongs to the anthology (ADR-048). The words are seeded from the clusters the reading-time triage of 2026-09-25 found, and grow by decision.
Logic — valid inference and its formal theories — propositional and model-theoretic structures, proof and consequence, and inferentialist accounts of meaning (group: philosophy).
38 of 1352 THEORY documents. Back to the full index.
| # | Title | Summary | Status |
|---|---|---|---|
| THEORY-020 | Every Boolean algebra is the clopen algebra of its Stone space of prime ideals, and a finite one is the power set of its atoms, so a single Boolean context always has two-valued valuations and the Kochen–Specker obstruction lies in how contexts overlap | Stone (1936, 1937), LIT-353 and LIT-358: every Boolean ring is isomorphic to the compact open sets of its prime-ideal space, a totally disconnected, locally compact Hausdorff space that is compact exactly when there is a unit, and every such space arises this way. Kochen & Specker (LIT-298, Thm 0) turn this into the criterion that a partial Boolean algebra embeds in a Boolean one iff its two-valued homomorphisms separate points. The joining of the two, that non-classicality needs more than one context, is the record’s. Neither Stone paper uses “ultrafilter” or states a duality of categories. | Active |
| THEORY-024 v2 | Classical Boolean logic is restored when a presheaf of contextual data acquires a global section or is sheafified | Ghose (2025), LIT-276 — asserts that the Heyting algebra of truth values “becomes Boolean” when the presheaf data collapse to a global section, and that sheaves encode Boolean reasoning. Both claims are asserted, not proved. The record’s readings refute them. The internal logic of a topos is fixed by the base category and its topology, not by whether one presheaf has a section (Isham–Butterfield, LIT-325, §6). Sheaf toposes such as Sh(ℝ) are not Boolean (NOTE-249). The contextuality criterion itself is untouched. | Rejected |
| THEORY-037 v3 | In the topos programme quantum propositions form a distributive Heyting algebra, not an orthocomplemented lattice, and its negation is a pseudo-complement under which excluded middle can fail | Döring & Isham (2007, II), LIT-335 — daseinisation maps each projector injectively to a clopen sub-object of the spectral presheaf, with δ(P∨Q) = δ(P)∨δ(Q) but only δ(P∧Q) ⪯ δ(P)∧δ(Q). The orthocomplement is carried to inner daseinisation, not to ¬δ(P). That Sub_cl(Σ) is Heyting (Thm 2.5) is sketched in the source, and the record re-derives it: each Σ_V is extremally disconnected, so Sub_cl(Σ) is a frame. Paper I (LIT-343) chooses intuitionistic deduction. Isham–Butterfield (LIT-325) state that the Heyting algebra is fixed by the base category. | Active |
| THEORY-041 | Birkhoff and von Neumann proposed the modular law, not orthomodularity, and proved it fails for closed subspaces in infinite dimension; Husimi used the orthomodular identity only as an unnamed proof step | Birkhoff & von Neumann (1936), LIT-306 — the lattice of closed subspaces is orthocomplemented and not distributive. They propose modularity (L5), motivated by a dimension function, and give an explicit infinite-dimensional pentagon that breaks it. The word “orthomodular” does not occur. Husimi (1937), LIT-357, derives modularity as the parallelogram law under a finite-chain assumption and uses the orthomodular identity as a step without naming it. Citing either paper for “the orthomodular lattice of quantum logic” misattributes it. | Active |
| THEORY-042 | Under a superselection rule a coherent superposition across sectors is operationally a mixture, because no observable connects the sectors; Wick, Wightman and Wigner proved such a rule for integer versus half-integer spin and only postulated it for charge | Wick, Wightman & Wigner (1952), LIT-339 — they define a superselection rule and show that a superposition across sectors “is not a pure state, but a statistical mixture”. They prove the rule from time reversal for integer versus half-integer angular momentum, and postulate it for charge with “no conclusive evidence”. What follows for Birkhoff–von Neumann’s lattice (LIT-306), a product of sector lattices with central sector projections, is the record’s inference. The centre-of-the-algebra formulation belongs to Haag, who is not read. | Active |
| THEORY-127 v4 | On the court agenda, and on any agenda in which every proposition reaches every other by conditional entailment and some minimally inconsistent triple stays consistent with two of its members negated, a group whose judgments are robustly rational under universal domain and respect unanimity cannot form its judgment on each proposition from its members’ judgments on that proposition alone unless one member dictates; its judgments must supervene on the members’ whole sets of judgments, and so can depart from what the members judge on the same proposition while being wholly fixed by them | List & Pettit (2006), LIT-705: under universal domain, robust group rationality (complete, consistent, deductively closed group judgments for every profile of rational member judgments) is inconsistent with majoritarian, uniform proposition-wise and proposition-wise supervenience (Propositions 1–3; the last two proved elsewhere and cited), and consistent with set-wise supervenience, which the premise-based and distributed premise-based procedures achieve (Propositions 4–5). Members’ judgments on a conclusion can then be insufficient, or even unnecessary, to fix the group’s judgment on it. List (2014), LIT-700, makes this the mark of a third kind of collective attitude: corporate attitudes, a group agent’s, supervene “holistically”, while aggregate and common attitudes supervene proposition by proposition. Active since 2026-10-19 for categorical judgments on the court agenda and on agendas with two stated connectedness conditions: the record re-derived Proposition 3 (and Proposition 2 as a corollary) itself. The extension to corporate attitudes in general is QUESTION-152. | Active |
| THEORY-162 | What an utterance does to the context it is used in is part of its meaning, and its truth conditions do not fix it: sentences with the same truth conditions can differ in what they make available to later discourse, in whether they inform or only test, and in whether they describe a state of affairs or bring one about | Heim (1982), LIT-838; Veltman (1996), LIT-818; Krifka (2024), LIT-835. Three readings find, each in its own domain, sentences that agree in truth conditions or in the proposition they carry but differ in their effect on a conversational state. The effects are anaphoric potential (Heim), tests rather than information (Veltman), and changing indices rather than eliminating them (Krifka). This is the dynamic view: meaning as context-change potential. It does not say that truth conditions are irrelevant, since each framework recovers them, or that the three formalisms agree with each other. | Proposed |
| THEORY-255 v3 | In Aerts’s subspace model of Hampton’s membership data, and in any lattice whose membership weight is order-preserving, whatever its negation, taking concept conjunction and disjunction as meet and join cannot produce overextension or underextension, so a model of the guppy-type deviations must take conjunction as some operation other than the meet or drop the monotone weight, while the Kolmogorov-type deviations can be had from the meet of a non-Boolean subspace lattice | Aerts (2009), LIT-934, Theorem 9 and §§2.2–3.3, read in full in NOTE-808. The impossibility is a proof, and it needs only that membership is monotone in the subspace. The fits that place the k-type deviations in a tilted subspace lattice and the ∆-type ones in an emergent sector are models with free parameters, not tests. Negation appears only as the orthocomplement used to derive the conjunction model from the disjunction model; no negated concept is measured. | Active |
| THEORY-341 | Inferring not-P from failure to prove P is a deduction only under two separate conditions: Clark shows that when every branch of the search for a proof of P ends in failure, not-P is a theorem of the completed database, and a search that does not finish licenses nothing; Reiter’s closed-world assumption, adding the negation of every ground atom the database does not entail, keeps a consistent Horn database consistent and can make a disjunctive one inconsistent | Clark (1978), LIT-1087, read in NOTE-894, and Reiter (1978), LIT-1088, read in NOTE-899 from his 1977 workshop report. Clark proves negation as failure sound with respect to the completed database (the clauses read as if-and-only-if definitions, plus axioms that distinct names denote distinct things), given a finite failure tree for some selection rule; it is incomplete in general. Reiter defines the closed-world assumption by entailment, reduces closed-world query evaluation to open-world atomic queries when the assumption is consistent, and shows it consistent for Horn and definite databases but not for Pa ∨ Pb. Soundness here is relative to the completion, not to the world, and neither paper says anything about a search cut short by time. | Active |
| THEORY-347 | Belief bases with the same logical closure can revise to opposite conclusions on the same input, so a closed belief set does not fix its own revision; partial meet contraction of a base need not satisfy Recovery, and bases keep distinct inconsistent states apart, while a belief-set model reproduces the base difference only by attaching a different selection mechanism to the same set | Hansson’s Stanford Encyclopedia survey (2006, revised 2026), LIT-1072, read in NOTE-866, with Alchourrón, Gärdenfors and Makinson (1985), LIT-1050, read in NOTE-874. Bases {p, q} and {p, p ↔ q} have one closure, yet revised by ¬p one yields q and the other ¬q: statically but not dynamically equivalent. Base contraction escapes the Recovery that AGM proves for closed theories, and many inconsistent bases exist where there is one inconsistent closed set. A base marks which beliefs are held in their own right and recomputes the rest; it is not a record of reasons, sources or defeated alternatives, and the survey gives no result that bases handle iterated revision better. | Active |
| THEORY-353 | For a logically closed theory, the contractions satisfying the six basic AGM postulates are exactly the partial meet contractions, and those satisfying the two supplementary postulates as well are exactly the ones whose selection of remainders is generated by a transitive relation; the theory alone does not fix the contraction, and the results concern one change of one fixed theory | Alchourrón, Gärdenfors and Makinson (1985), LIT-1050, read in NOTE-874, with Hansson’s survey, LIT-1072, read in NOTE-866. Contracting a closed theory A by x keeps what a selected set of maximal x-free subsets of A share; the six basic postulates characterize exactly these partial meet contractions (Observation 2.5), and with the two supplementary postulates exactly those selected by a transitive relation (Corollary 4.5). Revision follows by the Levi identity. A selection function or ordering must be added to A, and in the finite case distinct ones give distinct contractions. Nothing here concerns iterated change, where the selection comes from, or why a belief is held. | Active |
| THEORY-362 v2 | For nonrecursive Datalog or SQL views with safe stratified negation and stratified aggregation, under set or duplicate semantics, storing with each derived tuple only the number of its derivations suffices to maintain the view under insertions and deletions of base tuples: signed counts propagated through delta rules stratum by stratum give each tuple’s change as its new count minus its old, a tuple leaves when its count reaches zero, and a MIN or MAX group whose extreme is deleted is recomputed from the stored lower stratum | Gupta, Mumick and Subrahmanian (1993), LIT-1114, read in NOTE-915. Algorithm 4.1 evaluates delta rules in order of rule stratum and combines signed counts; Theorem 4.1 states it derives count(t^ν) − count(t) for every tuple, and Theorems 6.1 and 6.2 extend this to negated and aggregate subgoals. Its cost is argued to be close to evaluating the view and is not measured. All three theorems are stated without proof in this extended abstract. It does not say that a count suffices when support is cyclic: the paper keeps counting to nonrecursive views. | Active |
| THEORY-367 v2 | For SPJU relational queries, which Buneman, Khanna and Tan’s tree model encodes, the minimal witnesses of an output tuple, the inclusion-minimal sets of source facts from which the query still derives it, are the minimal sets matched by single derivations and so are the same for every equivalent query, while where-provenance, the source location a value was copied from, can differ between equivalent queries | Buneman, Khanna and Tan (2001), LIT-1104, read in NOTE-920. Two meanings of the provenance of output data: why it is there (the witness basis, the source structures matched by each valuation that produces it) and where a value came from (the source paths bound to the output variable). The first is preserved by the paper’s rewrite system and, cut down to minimal witnesses, agrees across equivalent queries with equality conditions; the second is shown by example to depend on how the query is written. Proofs are omitted. It is not a theory of revision: additions to the source, negation, aggregation and strengths of support are all outside it. | Active |
| THEORY-371 | For conjunctive queries without equality or comparisons, two queries are equivalent exactly when homomorphisms run both ways between the queries read as small databases, every such query has a minimal equivalent query unique up to isomorphism obtained by deleting atoms, and evaluating one against a database is NP-complete when the query is part of the input | Chandra and Merlin (1977), LIT-1111, read in NOTE-907. Reading a conjunctive query as its natural model, equivalence becomes a pair of homomorphisms (Lemma 13), the minimal equivalent query is unique up to isomorphism (Theorem 12), and evaluation with the query as input is NP-complete (Theorem 7), as is deciding whether one query is a folding of another (Theorem 11). The paper states equivalence, not containment, and does not state that containment or equivalence is NP-complete; those are corollaries later work attributes to it. Nothing here reaches queries with equality, comparisons, negation or union. | Active |
| THEORY-373 | For positive relational algebra on relations whose tuples are annotated from a commutative semiring, every query’s annotated answer equals its answer over provenance polynomials N[X] in the input tuple ids, evaluated at the input annotations, so set, bag, c-table and event-table semantics all factor through the polynomials; revaluing inputs can remove output tuples but never add them, and nothing is shown for negation, difference or aggregation | Green, Karvounarakis and Tannen (2007), LIT-1110, read in NOTE-913. Union and projection add tags, join multiplies them; the usual RA identities hold exactly when the tags form a commutative semiring, and a map of tags commutes with every query exactly when it is a semiring homomorphism. The polynomials N[X] are the free commutative semiring, so the annotated answer in any semiring is the polynomial answer evaluated at the input annotations (Theorem 4.3). It is a sufficiency result for revisions that re-annotate existing inputs, not a minimality result, and it excludes added facts and every nonmonotone operation. | Active |
| THEORY-374 v2 | Given views with conjunctive definitions, deciding that they answer a conjunctive query exactly is NP-complete in the size of the query and definitions, while a maximally-contained rewriting can be built in time polynomial in that size without saying whether it is exact; and finding all certain answers from the stored contents is polynomial in their size under the open-world assumption when the views are conjunctive and the query conjunctive or datalog, but co-NP-hard in that size under the closed-world assumption even for conjunctive views and queries | Halevy (2001), LIT-1116, read in NOTE-921, reporting Levy et al. 1995 (LIT-1100, read), Duschka, Genesereth and Levy, and Abiteboul and Duschka 1998 (not read). Reuse of stored views is graded: certifying an exact rewriting is NP-complete in the size of the definitions, building everything the views give (maximally contained) is polynomial, and the certain answers can cost a co-NP-hard search in the size of the stored data. Promoted 2026-10-21 on a re-derivation of the last two parts (ADR-047 v2); the primary papers they come from are unread. None of it prices recognition for definitions outside conjunctive queries and datalog, or says how costly recognition is on typical queries. | Active |
| THEORY-380 v2 | For datalog over a finite input instance annotated from a commutative ω-continuous semiring, with an answer’s tag defined as the sum over its derivation trees of the product of its leaves’ tags, the tags are the least fixed point of a finite polynomial system and factor through formal power series N∞⟦X⟧ in the input tuple ids; an answer tuple’s series has an infinite coefficient exactly when one of its derivation trees contains a tuple lying on a cycle of unit rules | Green, Karvounarakis and Tannen (2007), LIT-1110, read in NOTE-913. A recursive query can derive a tuple in infinitely many ways, so polynomials do not suffice and the semiring needs infinite sums. With ω-continuous semirings and the provenance semiring N∞⟦X⟧ the paper states the analogues of the relational results: a fixed-point characterization (Theorem 5.6), factorization (Theorem 6.4), and a test for infinite coefficients (Theorem 6.5), with algorithms that decide finiteness and compute coefficients. Proofs are not given. Plain N and N[X] are excluded, the provenance can be an infinite object held only as equations, and negation remains outside. | Active |
| THEORY-387 v2 | For positive recursive Datalog views under set semantics, deleting every derived tuple that has any derivation through a deleted base fact, then restoring each deleted tuple that still has a derivation from what remains, then adding what insertions derive, leaves exactly the tuples derivable from the new base (E − Δ⁻) ∪ Δ⁺, with no derivation counts stored; the extension to stratified negation and aggregation is asserted, not shown, and the size of the overestimate is not measured | Gupta, Mumick and Subrahmanian (1993), LIT-1114, read in NOTE-915. DRed runs stratum by stratum: semi-naive Δ⁻-rules compute an overestimate of deletions, δ⁺-rules put back those with a derivation in the reduced database, and Δ⁺-rules add insertions. Theorem 7.1 states the result contains t if and only if t has a derivation in (E − Δ⁻) ∪ Δ⁺; the proof is in a 1992 AT&T report the record has not seen. The paper asserts, and does not show, that DRed handles stratified negation, aggregation and rule changes, that it beats the PF algorithm by up to an order of magnitude, and that it is slower than counting on nonrecursive views. | Active |
| THEORY-389 | For conjunctive queries and views without comparison predicates, a stored view can be used in an equivalent rewriting of a query exactly when the view’s body maps homomorphically into the query’s, a minimal rewriting needs no more literals than the query, and deciding whether a rewriting shorter than the query or one using only the views exists is NP-complete in the size of the query and view definitions; with comparisons in both, deciding whether any rewriting uses the views is Π2p-complete | Levy, Mendelzon, Sagiv and Srivastava (1995), LIT-1100, read in NOTE-909. Every use of a view in an equivalent rewriting comes from a containment mapping from the view into the query (Proposition 3.1); without comparisons a locally minimal complete rewriting has at most as many literals as the query (Lemma 3.5), which puts the problems in NP, and they are NP-complete (Theorems 3.7, 3.9, 3.10), with two independent sources of hardness. The results are worst case, in the size of the definitions rather than the stored data, for equivalent rewritings under set semantics only; they do not say recognizing reuse is costly in practice, and they do not cover contained (partial) rewritings. | Active |
| THEORY-462 v2 | If commonsense knowledge includes defaults that later evidence displaces, a monotonic logic, in which an added axiom can never remove a theorem, cannot represent that displacement as it stands; Minsky’s further claim, that no logistic system, one that separates propositions from general laws of inference, can carry commonsense knowledge even once repaired, is asserted, not shown | Minsky (1974), the frames memo, LIT-410, read in NOTE-337. Its appendix argues that “logistic” systems fail for commonsense on five counts, of which monotonicity is a correct observation about classical logic. That no repair is possible is asserted (“I think such attempts will continue to fail”), and consistency being undesirable is argued by analogy. The reading says the memo is a source of hypotheses, not evidence; this account takes from it only the half that holds by definition and marks the rest as the memo’s claim. Active as the definitional half and a report of how the memo supports the rest; the further claim is THEORY-1239, Proposed. | Active |
| THEORY-493 | From core mereology, classical extensional mereology (GEM) is reached by exactly three pairings of a decomposition principle with an unrestricted-sum principle: Supplementation with Sum2, Strong Supplementation with Sum3, and Complementation with Sum1; Supplementation with Sum3, the pairing given by Simons (1987), does not yield it, because which definition of ‘sum’ is used decides which decomposition axiom is needed | Varzi, SEP “Mereology” (2003, revised June 2026), LIT-124, read in full in NOTE-163. A result the entry reports with citations (Hovda 2009; Cotnoir and Varzi 2019) and a countermodel (its Fig. 4; Pietruszczak 2000a, Pontow 2004), and which corrects Simons (1987), Casati and Varzi (1999) and the entry’s own 2003 edition. The record has not checked the proofs. It is stated for first-order theories with a single primitive P and infinitary principles as axiom schemas, and it is a fact about axiom systems: it does not say classical mereology is true of anything. | Active |
| THEORY-516 | For any presheaf of propositions over a small category of contexts, a sieve-valued valuation satisfies the generalized functional-composition condition exactly when it is a subobject of that presheaf, and the construction runs unchanged in classical physics, where every microstate gives a global section yet truth values are still non-Boolean sieves; so the logic of the truth values is fixed by the base category, not by whether a presheaf has global sections | Butterfield & Isham (1998), LIT-381, read in full in NOTE-329: Theorem 4.1 proves that generalized FUNC is exactly naturality of ν : G → Ω, for any presheaf G of posets on any small category. In classical physics the value presheaf has a global section per microstate (3.6–3.7), yet the macrostate and microstate valuations are sieve-valued, and NOTE-329 shows excluded middle failing at a microstate. Isham & Butterfield (1999), LIT-389 (NOTE-334), adds that Ω is unique for a given topos and that a base with one arrow between any two objects gives two-valued logic. The choice of base, and so of the logic, remains free. | Active |
| THEORY-535 | Quantum systems read as bundles of property-instances with no principle of individuality can have their kinds and their number stated in quasi-set theory, so that N indistinguishable particles get a definite quasi-cardinal without labels; the construction covers kinds and counting only, not states, actualization or dynamics | Holik, Jorge, Krause & Lombardi (2021), LIT-107, read in full from the preprint in NOTE-127. The Lombardi–da Costa ontology of properties makes a quantum system a bundle of instances of universal type-properties, with no principle of individuality. Krause’s quasi-set theory Q, reinterpreted over property-instances, represents an atomic bundle as a qset taking one instance from each qset of indiscernibles, guaranteed by Q’s Axiom of Choice, and N particles as a subqset of quasi-cardinal N. The new formal content is about two pages (§6), the printed proofs contain errors, and states, actualization and dynamics are not formalized. The claims about Kochen–Specker and non-separability are recharacterizations by definition, not results. | Proposed |
| THEORY-544 | In homotopy type theory extended with a strict directed interval and a layer of shapes, one contractibility condition, the Segal condition, gives a type identities, associativity and three-dimensional coherence, makes every function between Segal types a functor, and yields a dependent Yoneda lemma for covariant families; that such types are (∞,1)-categories rests on a semantics only sketched | Riehl & Shulman (2017), LIT-032, read in full in NOTE-069. The internal results of §§5–11 are proved: associativity from the Segal condition applied to A^2 (Prop. 5.9), inner 3-horns (Prop. 5.21), functoriality of every function (Prop. 6.1), the dependent Yoneda lemma (Thm 9.5), and uniqueness of left adjoints into a Segal type from a Rezk type (Thm 11.23). Segal and Rezk types match Segal and complete Segal spaces (Props A.21, A.25), but soundness of the type theory in bisimplicial sets is sketched and depends on an unproved initiality theorem. Coherence in all dimensions is conjectured, not proved. | Active |
| THEORY-595 | A filter over a set of worlds is a finitely consistent propositional theory and an ultrafilter a negation-complete one; read so, the ultrafilter extension theorem is Lindenbaum’s lemma for propositions, and Łoś’s theorem builds a model that makes true exactly what an ultrafilter says, which proves first-order compactness without proof theory, given the axiom of choice | Turner (preprint 2021, published 2025), LIT-145, read in NOTE-177. An expository paper: “None of the results are novel” (p. 2). Maximal, prime and ultra filters coincide (Thm 2); every filter extends to an ultrafilter (Thm 3); Łoś’s theorem (Thm 9); compactness (Thm 12). The results are standard and correct, though the write-up has slips. A filter is only finitely consistent, and that is the point. The pairings with Lindenbaum and Henkin are analogies, not reductions. | Active |
| THEORY-619 | Over the poset of commutative von Neumann subalgebras, coarse-graining a projector to a smaller subalgebra is exactly the direct image of its clopen region of the Gelfand spectrum under restriction, so the coarse-graining presheaf is the presheaf of clopen spectral regions; and a quantum state’s sieve-valued truth values are fixed by one coherent family of regions, its supports: a proposition is true at a subcontext exactly when the support there lies under the coarse-grained proposition | Butterfield & Isham (2001), “Topos Perspective on the Kochen-Specker Theorem: IV”, LIT-382, read in full in NOTE-328. §2.4 proves G ≅ CloΣ: restricting the characters of V₁ that make P̂ true gives exactly the characters of V₂ that make its coarse-graining true, via a cited state-extension theorem. Theorem 3.1 shows that any assignment defined by “support ≤ coarse-grained proposition”, with supports forming a global element of G, is a sieve-valued valuation obeying FUNC; a state’s supports qualify. Both theorems are close to definitional. Nothing here builds Heyting operations on clopen sub-objects. | Active |
| THEORY-642 | Basic two-level type theory, an inner homotopy type theory with an outer level of strict equality, is conservative over homotopy type theory, so an inner type it proves inhabited is already inhabited in HoTT, but a fibrant-replacement type former would force uniqueness of identity proofs on the inner level | Annenkov, Capriotti, Kraus & Sattler (2017; MSCS 2023), LIT-095, whose §§1–3 were read in full in NOTE-047, the reading of the nLab page it supersedes (LIT-040). Props 2.18–2.19 prove that inhabitation of inner types is reflected, through a presheaf model over any model of HoTT. Thm 2.20 proves that a fibrant-replacement former implies UIP for inner types. The conservativity is the weak, inhabitation-reflecting kind. Results that use the axioms relating the two levels’ natural numbers, which untruncated semisimplicial types need, are not known to transfer. | Active |
| THEORY-647 v2 | If outright belief is credence ultraclose to 1 relative to a context level, conjunction holds for any standard (‘few’) number of believed propositions and fails for an ultralarge number, which dissolves the Lottery Paradox as an accumulation of negligible rounding errors | Wenmackers (2011), LIT-163, chapter 3, read in NOTE-139. Stratified Belief, B(x) iff P(x) ≃_V 1 in Hrbacek’s relative analysis, satisfies a Stratified Conjunction Principle for a standard number of conjuncts (proved) and fails for an ultralarge number. The proofs hold inside the framework. That belief works this way is argued: any explicit threshold collapses the model back to the Lockean one, the author calls it “crude”, and knowledge is set aside. | Proposed |
| THEORY-649 | When agents holding uniformly random consistent theories over two or three atomic sentences each average their theories once, bit by bit, with all peers within a Hamming bound of confidence, an individual agent ends up with the inconsistent theory at most 1.81% of the time, but the chance that some agent in the group does reaches 6.4% for two sentences and 16.9% for three | Wenmackers (2011), LIT-163, chapter 5, read in NOTE-139. An exact count, extended by sampling, of how often one round of bounded-confidence averaging over theories yields the inconsistent theory. The per-agent fraction F_AG peaks at 1.8112% (M = 2) and 0.3215% (M = 3); the per-profile fraction F_OP reaches 6.4298% and 16.867%. The thesis’s headline, that the risk “can be made arbitrarily small” by adding sentences, rests on two values of M and is contradicted for F_OP. | Active |
| THEORY-665 v2 | Asserting is undertaking a commitment that entitles others to reassert it and carries a responsibility to show entitlement if challenged; every interlocutor keeps score of everyone’s commitments and entitlements, so the score is doubly perspectival, and a speech act’s significance is the change it makes to the scores, fixed by its content’s inferential role | Brandom (1994), LIT-794, skimmed in NOTE-622: the Preface and the core of chapter 3 only. This states the deontic scorekeeping model of assertion, not the book’s arguments for it, and rests on a skim. By the author’s account the model is an idealization limited to semantic inference, with implicature left to an outer shell. It gives no single objective score, only scores kept from each perspective. | Proposed |
| THEORY-698 | Thresholding linear attribute probes on a language model’s embeddings yields a complete concept lattice for any incidence whatever, so the lattice is guaranteed by construction; what the Lattice Representation Hypothesis measured is per-attribute agreement with GPT-4o annotations at F1 70–83, and no lattice law | Xiong (2026), LIT-267, read in NOTE-240. Theorem 1 is the basic theorem of formal concept analysis applied to the crisp relation got by thresholding Fisher-LDA probes, and it holds for every binary relation; the paper’s own proof plan says so. The empirical content is that the thresholded probes on three 7–8B models agree with a GPT-4o-annotated incidence at macro F1 69.7–83.2 and predict WordNet subsumption at F1 57.1–77.1. No closure, absorption or recovered-lattice comparison is tested, and the paper’s join is not a lattice join as written. It is not evidence that language models encode a lattice beyond the incidence. | Active |
| THEORY-725 | On the court agenda {P, Q, R, R iff (P and Q)} under universal domain, proposition-wise majority voting is not robustly rational, while the premise-based procedure is, and it makes the group’s judgments a function of the members’ whole judgment sets that the members’ judgments on the conclusion neither fix nor need to enter | List & Pettit (2006), LIT-705, read in full in NOTE-550, for the court agenda only. Proposition 1: majority voting on each proposition is not robustly rational, by the discursive dilemma. Proposition 4: the premise-based procedure, majorities on P, Q and the biconditional with R derived, is robustly rational and makes the group’s set a function of the members’ sets. Under it the members’ judgments on R do not fix the group’s (weak discontinuity), and under the distributed procedure they need not enter (strong discontinuity, Proposition 5). The general impossibility for proposition-wise rules is THEORY-127, still Proposed. | Active |
| THEORY-807 | The guppy-type overextension in Hampton’s membership data arises because a combined concept is in part a new, emergent concept and not only a logical combination of its parts, so human concept combination runs in two superposed layers, one classical and logical and one quantum and conceptual | Aerts’s reading, which THEORY-255’s title carried before the promotion audit narrowed it (batch 018) to the impossibility Theorem 9 proves. Aerts (2009), LIT-934, read in NOTE-808, fits the ∆-type deviations with one emergent subspace per pair and reads thought as two superposed layers. The narrowing was right that the theorem does not force an emergent concept, only dropping the meet or the monotone weight; this entry is the emergence reading as Aerts’s thesis. Filed under ADR-047 v4 so the wide form stays a thesis evidence can confirm or reject. | Proposed |
| THEORY-1064 | In counterexample-guided abstraction refinement, a spurious counterexample locates the distinction its abstraction lacked: walking it forward through the concrete system, the first abstract state where no concrete continuation exists merges the states the trace can reach with the states that have the transition onward, and splitting them removes the counterexample; for finite-state programs and ACTL* properties whose counterexamples are paths or loops, repeating check and split ends in a real counterexample or a proof | Clarke, Grumberg, Jha, Lu and Veith (2000), LIT-1652, read in NOTE-1231 from the authors’ manuscript of the CAV paper. Active: the test for spuriousness (Lemma 1), the three-way cut at the failing state and the termination argument are given in full. The NP-hardness of the coarsest split is stated with its proof omitted, and the loop case rests on a theorem proved elsewhere. It does not say that the split found is the smallest, or how many rounds are needed. | Active |
| THEORY-1094 | In counterexample-guided abstraction refinement the property and the concrete system are fixed inputs: the property’s atomic formulas help build the first abstraction and no abstraction may merge states that disagree on them, every refinement only splits classes toward the concrete state space, and a real counterexample ends the procedure; so the loop revises which of the concrete system’s distinctions the model draws, never the property or the space of possible answers | Clarke, Grumberg, Jha, Lu and Veith (2000), LIT-1652, read in NOTE-1231. A textual fact about the algorithm as specified in §§3–4, and the exact form of the limit the exchange of 2026-10-27 (A16 §6) gave for CEGAR as the formal neighbour of inquiry as specification (CLAIM-470). It does not say that a property cannot be revised by anyone, only that no step of this procedure does it. | Active |
| THEORY-1142 | A translation between two logics presented as institutions is correct, in the Satisfaction Condition’s sense, when a translated sentence holds in a model exactly when the original holds in the model’s translation; given the model translation this fixes the sentence translation up to semantic equivalence, and when every model of the target is reached it preserves and reflects entailment, so one logic’s prover can decide the other’s; but the condition alone admits collapsing translations and is relative to a model translation it does not supply | Goguen and Burstall (1992), LIT-1661, read in NOTE-1348 from the published JACM article: Definition 32 (p. 125), Proposition 33 and Proposition 35 (p. 126), Theorem 39 (pp. 127–129). Active: proved, and checked on toy morphisms between propositional institutions. The collapsing morphism and the atom-negating morphism are my constructions, not the paper’s. It is a criterion relative to a chosen model translation, and says nothing about translation beyond truth conditions. | Active |
| THEORY-1150 | In any logical system presented as an institution, theories can be glued wherever their vocabularies can: if the category of signatures has colimits, so does the category of theories, the glued theory being the semantic closure of the union of the parts’ translated sentences; and because constraints requiring free or initial interpretation also obey the Satisfaction Condition, theories carrying them glue the same way | Goguen and Burstall (1992), LIT-1661, read in NOTE-1348 from the published JACM article. Theorem 11 (p. 108) proves that the forgetful functor from theories to signatures reflects colimits, using only the Satisfaction Condition and the Closure Lemma; Proposition 23 and Theorem 24 (p. 119) extend it to theories with data constraints. Active: proved, and checked on a toy propositional institution. It does not say that signatures have colimits in a given logic, that the glued theory is consistent, or anything about proofs: closure is semantic. | Active |
| THEORY-1239 | No logistic system, one that separates propositions from general laws of inference, can carry commonsense knowledge, whose defaults later evidence displaces: attempts to repair its monotonicity will continue to fail | Minsky’s (1974) further claim against logic, from the frames memo’s appendix (LIT-410, read in NOTE-337, C7). It was kept here when the twenty-fourth status review promoted THEORY-462 (ADR-065 §3; ADR-047, kind 1). Monotonicity is a correct observation about classical logic. The memo asserts that no repair can succeed: “I think such attempts will continue to fail”. The record holds no reading of the non-monotonic logics that were built to repair it. The condition is carried over word for word, so “the account” in it now means this entry, and “its first half” means THEORY-462. | Proposed |