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).
64 of 2004 LIT documents. Back to the full index.
| # | Title | Summary | Status |
|---|---|---|---|
| LIT-032 v2 | A type theory for synthetic ∞-categories | Riehl & Shulman (2017), ARXIV-1705.07442. A three-layer type theory adds a directed interval 2 to HoTT. Its layers are cubes, topes (the coherent theory of a strict interval) and types, and simplices become shapes that can be mapped out of by extension types. One contractibility condition, “Segal” (unique fillers for the 2-1-horn), then yields associativity (Prop. 5.9) and 3-horn fillers (Prop. 5.21). It also makes every function a functor (Prop. 6.1), gives a dependent Yoneda lemma for covariant families (Thm. 9.5), and makes having a left adjoint a proposition when the adjoint’s codomain is Rezk (Thm. 11.23). The bisimplicial-sets semantics is sketched. Segal and Rezk types are shown to match Segal and complete Segal spaces (Props. A.21, A.25), and soundness is not proved in full. | Active — read in full 2026-09-25 (NOTE-069); This is the founding paper of simplicial HoTT, where synthetic (∞,1)-category theory starts. It is worth reading as mathematics by anyone following directed type theory. Its semantics appendix is explicitly a sketch. |
| LIT-054 v2 | A complete graphical calculus for Spekkens’ toy bit theory | Backens & Duman (2014), ARXIV-1411.1618. Take the maximal-knowledge fragment of Spekkens’ toy bit theory with post-selected measurements, viewed as relations over {1,2,3,4}ⁿ. It has a ZX-style red–green graphical calculus that is universal (§4.3), sound (§4.4) and complete (Thm 17). Completeness goes through a proof that the toy theory’s binary “check-matrix” formalism coincides with the qubit stabilizer one (valid states SᵀJS = 0, valid transformations QᵀJQ = J, Lemma 3). With it come graph-state/local-complementation results for toy states (Thms 4–5), map–state duality (§5.2) and an rGS-LO normal form (Thms 10–11). The rewrite rules differ from the stabilizer ZX-calculus only through the phase group: Z₂×Z₂ against Z₄. That difference appears as an “11-commutation” rule in place of π-commutation (§4.5). | Active — read in full 2026-09-25 (NOTE-066); the completeness result is proved and still the diagrammatic reference for the toy bit theory. Read §2.1, §4.2, §4.5 and §5.1 for the stabilizer comparison. The ψ-epistemic framing in the abstract and §1 is motivation only; the paper does no ψ-epistemic analysis. |
| LIT-095 | Two-Level Type Theory and Applications | Annenkov et al. (2017), ARXIV-1705.03307; Mathematical Structures in Computer Science 2023. Two-level type theory (2LTT) pairs a fibrant inner theory (HoTT) with an outer theory with strict equality, so that coherence towers such as semisimplicial types can be stated internally. Basic 2LTT is conservative over HoTT (Props 2.18–2.19): an inner type inhabited in 2LTT is already inhabited in HoTT. A fibrant-replacement type former would force UIP on the inner level (Thm 2.20). | Active — read in part on 2026-09-26, alongside the nLab page it supersedes (LIT-040) — §1–3, §4.7 and §5 in full, §4.3–4.6 at the level of statements; no NOTE yet, so a full reading is still owed |
| LIT-106 v3 | Brandom’s Inferentialist Theory and the Meaning Entitlement Connection | Marabini (2015), DOI-10.12816/0028065. Boghossian’s objection to substantive, entitlement-based theories of meaning (drawn from pejoratives like “Boche”) works against Dummett but not against Brandom. Brandom’s material inferences are non-monotonic and ceteris paribus, so one can grasp a concept while refusing to endorse the inferences it licenses. | Unfetched — seeded from the abstract and a skim on 2026-09-26 (the skim read PhilArchive’s copy through the Wayback Machine); a close reading was attempted the same day and could not fetch it: the Wayback Machine reset its connections, PhilArchive refused the request, and the publisher’s reader (Al-Manhal) needs a sign-in. The article is marked open access, so this is an access failure, not a paywall. It stays Unfetched until it can be fetched. Free copy: philarchive.org/rec/MARBIT-2 (PhilArchive). |
| LIT-107 v3 | Quasi-set theory: a formal approach to a quantum ontology of properties | Holik et al. (2021), DOI-10.1007/s11229-022-03884-8. The paper argues, with no new theorem, that the Lombardi–da Costa ontology of properties for quantum mechanics can be stated in Krause’s quasi-set theory Q. On that ontology a system is a bundle of I-type-properties (instances of universal type-properties, represented by the algebra of observables) with no principle of individuality. For each property instance, the indiscernible instances form a qset U([Π]). An atomic bundle is any qset x with qc(x ∩ U) = 1 for each U; the Axiom of Choice in Q guarantees one exists. The bundle’s kind is Q(B) = {x ∈ P(Q) | R(x)}, whose members are all indiscernible. N particles are a subqset N(B) ⊂ Q(B) with qc = N, a definite number with no labels (§6, pp. 19–22). | Active — read in full 2026-09-26 (NOTE-127); worth reading as a short, clear bridge between the modal-Hamiltonian “ontology of properties” (Lombardi et al.) and quasi-set theory (French & Krause 2006). The new formal content is about two pages (§6). Most of §5 restates Q’s axioms, and the printed proofs contain errors. It is a useful statement of the position, not a result. |
| LIT-145 v2 | Ultrafilters as Propositional Theories | Turner (2025), DOI-10.1111/phc3.70047. An expository piece that redefines a filter over a set W as a “propositional theory” (a set of W-propositions closed under pairwise conjunction and implication, not containing ∅), proves maximal ⇔ prime ⇔ ultra (Thm 2), the ultrafilter extension theorem as a propositional Lindenbaum’s lemma (Thm 3, assuming choice), Łoś’s theorem M_T,[A] ⊨ φ iff ⟦φ⟧_A ∈ T for ultraproducts of “intensional spaces” (Thm 9), and first-order compactness from it (Thm 12); “None of the results are novel” (p. 2). | Active — read in full 2026-09-26 (NOTE-177); worth reading as the most accessible philosopher’s route into ultrafilters and Łoś’s theorem, provided the reader supplies the fixes to a few slips in the proofs (listed under Limitations). |
| LIT-262 v2 | The Geometry of Information Retrieval | van Rijsbergen (2004), DOI-10.1017/CBO9780511543333. The book recasts IR’s vector-space, probabilistic and logical models in one Hilbert-space language. Documents are state vectors. Relevance and aboutness are Hermitian observables that need not commute. Subspaces carry a non-distributive logic whose conditional is shown to be a Stalnaker conditional equal to the Sasaki hook (ch. 5). Gleason’s theorem makes tr(ρP) the probability of a subspace, which ch. 6 uses to rewrite cosine matching, cluster representatives, relevance and pseudo-relevance feedback, dynamic clustering and ostensive retrieval. It is a proposed language, not a tested model: no experiment is reported, and its “content hypothesis” that the probability of a concept is cos²θ is argued, not tested. | Active — read in full 2026-09-27 (NOTE-239); worth reading as the founding statement of the Hilbert-space (quantum-probability) programme in IR. It is short, self-contained and mathematically careful at the level it works at, and its ch. 5 proof that the subspace conditional is a Stalnaker conditional and its ch. 6 trace-formula recastings of standard IR operations are the parts to take away. Read it as a language, not as evidence: it reports no experiment, and every IR payoff it names is a reformulation or a research direction. |
| LIT-267 v3 | The Lattice Representation Hypothesis of Large Language Models | Xiong (2026), ARXIV-2603.01227. Thresholding linear attribute directions (Fisher-LDA probes) gives a crisp object–attribute incidence, and the paper’s Theorem 1 is the standard fact that any such incidence has a complete concept lattice. The geometric meet is half-space intersection; the join is defined as the set union of two cones and “approximated by the conic hull” of their directions, which as written is not a lattice join. On five WordNet domains with GPT-4o-annotated attributes, the probes recover the incidence at F1 69.7–83.2 on three 7–8B models, and profile-based subsumption reaches F1 57.1–77.1. No lattice law is ever tested. | Proposed — read in full 2026-09-27 (NOTE-240); promising as a bridge between probe geometry and formal concept analysis, and unproven as a hypothesis about LLMs. It would be settled by three things. The attributes would have to come from something other than another LLM’s annotations. The region-level join would have to be defined correctly, as the Galois closure of the shared intent. And lattice identities (closure, absorption, meet/join agreement with the recovered context) would have to be tested, not pairwise subsumption and candidate ranking alone. |
| LIT-272 v2 | Reasoning about Meaning in Natural Language with Compact Closed Categories and Frobenius Algebras | Kartsaklis et al. (2014), ARXIV-1401.5980. The paper sets the sentence space equal to the noun space (F(s)=F(n)=W). It then uses the basis-copying map σ: v_i ↦ v_i⊗v_i of the Frobenius algebra fixed by W’s basis to lift corpus-built verb matrices Σ_i sbj_i⊗obj_i into rank-3 tensors. So a transitive sentence becomes sbj⊙(verb·obj) (“copy-subject”) or obj⊙(verbᵀ·sbj) (“copy-object”), a vector in W. On the Grefenstette–Sadrzadeh verb-disambiguation set, copy-object gets Spearman ρ=0.172, against 0.168 (Kron), 0.163 (Multp), 0.143 (copy-subject), 0.050 (additive) and an inter-annotator bound of 0.620. On a 112-term definition-matching task the best F1 is 0.21 (nouns) and 0.27 (verbs). No significance test is reported. The disambiguation numbers are identical to the authors’ COLING 2012 paper, and the definition numbers are the same data re-reported. | Active — read in full 2026-09-27 (NOTE-246); worth reading for the construction, not for its evidence. It is the citable categorical statement of the Frobenius lift of DisCoCat verbs: the functorial recasting, S=N=W, and the copy-subject and copy-object maps. Its experiments are the authors’ COLING 2012 numbers, re-reported without that paper’s caveat that copy-object’s lead is statistically insignificant. The best disambiguation ρ is 0.172, against a human bound of 0.620. The construction depends on a choice of basis, which the paper cites but never draws the consequence of. |
| LIT-273 v2 | Mathematical Foundations for a Compositional Distributional Model of Meaning | Coecke et al. (2010), ARXIV-1003.4394. The paper builds DisCoCat as a product category FVect × P of vector spaces and a free pregroup. A sentence’s meaning is f(w₁⊗…⊗wₙ), where f is the linear map got by putting vector spaces in place of the pregroup types in the reduction p₁…pₙ ≤ s. The ε maps become inner products and the η maps become Σᵢ eᵢ⊗eᵢ. So “John likes Mary” is Σ_ijk c_ijk⟨v|vᵢ⟩⟨w_k|w⟩ sⱼ ∈ S, and “not” is the 2×2 swap matrix placed on the sentence wire. There is no theorem and no experiment. The sentence space S is shown only as 1- or 2-dimensional truth values, over a toy model with one basis vector per individual, and the paper says how neither S nor the verb tensors are to be built from data. Its headline similarity numbers (3/4, 1/4, 3/8) are unnormalised inner products. Under its own Definition 5.1 they are 0.949, 0.316 and 0.6. | Active — read in full 2026-09-27 (NOTE-245); worth reading as the founding statement of DisCoCat, whose ε/η composition, S-for-every-sentence design and “not”-as-swap every later paper in the programme starts from. Read it as a specification, not a result. It proves nothing, runs no experiment, leaves S and the verb tensors unbuilt, and its categorical framing (a product with a posetal pregroup) cannot tell apart the parse ambiguities it says it can reason about. |
| LIT-276 v2 | Measurement as Sheafification: Context, Logic, and Truth after Quantum Mechanics | Ghose (2025), ARXIV-2512.12249. A programmatic essay, with no theorem, model or computation of its own. It restates Abramsky & Brandenburger’s criterion (contextuality and non-locality as the absence of a global section of a presheaf over measurement contexts) and adds three things. It declares measurement to be “sheafification” of that presheaf, without specifying a site, a topology or any sheafified object. It asserts that the Ghose–Patra seven-valued logic is a finite Heyting algebra, without giving an order or operations. It proposes that a quantum potential scaled by 0 ≤ λ ≤ 1 (λ = 1 quantum, λ = 0 classical Hamilton–Jacobi) carries the presheaf continuously to a sheaf, which is asserted, not modelled. Its one worked formula, v2’s Čech “obstruction class” [δs], is a coboundary and so is zero by construction. | Rejected — read in full 2026-09-27 (NOTE-249); not worth a reader’s time for its formal claims. Every correct formal ingredient is Abramsky & Brandenburger’s (LIT-016) or Abramsky, Mansfield & Barbosa’s, and both are better read in the original. What the essay adds is either unconstructed (the sheafification, the site, the seven-element Heyting algebra, the link from λ to cohomology) or wrong as stated: v2’s obstruction class is zero by construction, a sheaf topos is not in general Boolean, and classical distributions do not form a sheaf. Its only value is as a record of a position, the Bohrian reading of contextuality plus the Jaina analogy. |
| LIT-278 v2 | Contextuality, Cohomology and Paradox | Abramsky et al. (2015), ARXIV-1502.03097. For a model whose outcomes live in a commutative ring R, “All-vs-Nothing” (AvN_R) means the R-linear equations satisfied by every support section of every context have no global solution. Theorem 21 proves AvN_R(S) ⇒ SC(Aff S) ⇒ CSC_R(S) ⇒ CSC_ℤ(S) ⇒ SC(S), so every AvN model is strongly contextual with a non-vanishing Čech obstruction on every section. Theorem 4 shows that every state stabilised by an “AvN triple” of n-qubit Pauli operators yields such a model. The “paradox” half proves much less: an informal identification of Liar cycles with strongly contextual support tables, one exact case (the length-4 Liar cycle is the PR box), and the cohomology of paradox deferred to future work. | Active — read in full 2026-09-27 (NOTE-251); worth reading as the place where the cohomological witness is shown complete for a named, large class (every All-vs-Nothing model, over any ring). It is also where the obstruction is defined as a connecting homomorphism. It does not supersede LIT-277. It re-derives none of LIT-277’s computations, and it drops its negative results: the Hardy false positive and the strongly contextual cover with γ = 0. Its “paradox” title-word is supported by about one page of analogy and one worked identification. |
| LIT-281 v2 | Logical and Topological Contextuality in Quantum Mechanics and Beyond | Carù (2019), DOI-10.5287/ora-kznbp4k4y. The thesis’s cohomology chapters republish the 2017 and 2018 papers with the “joint model” renamed the “line model”. The definitions, Thm IV.32 (complete on cyclic scenarios at level |M|−1), Prop IV.34, Thm IV.36 and Conjecture IV.41 carry over unchanged. So does every defect found in the preprint. Under the thesis’s own Def IV.26, the §8 Kochen–Specker cover of Abramsky–Mansfield–Barbosa is still detected on only 6 of 15 sections at levels 0–3 (my recomputation), and a lifted ℤ/2 family shows it is never fully detected at any level. The context-wise reading the worked examples use detects all 15 sections at level 2. The genuinely new material lies outside the cohomology programme: a probabilistic line-model construction (§IV.7), a valuation-algebra “theory of disagreement” with inference algorithms (Ch V, bound O(k^n·l^{k(n−1)+1}) on (n,k,l) scenarios), and the AvN-triple characterisation of stabiliser states (Ch VI). | Active — read in full 2026-09-27 (NOTE-254); worth reading as the consolidated source for Carù’s cohomology programme (Chs III–IV), for the valuation-algebra reformulation of contextuality (Ch V) and for the AvN triple theorem (Ch VI). Chs III–IV repeat, uncorrected, the errors recorded for LIT-279 and LIT-280, so read them with NOTE-252 and NOTE-253 at hand. |
| LIT-298 v2 | The problem of hidden variables in quantum mechanics | Kochen & Specker (1967), DOI-10.1512/iumj.1968.17.17004. Theorem 1 exhibits a finite partial Boolean algebra D, generated by 117 directions in E³, that admits no homomorphism onto Z₂. §4 embeds D in the projections of the spin-1 space of orthohelium’s 2³S₁ state, via α ↦ P J_α². So no assignment of 0/1 values to those quantum propositions respects all the Boolean relations within each commeasurable set. Theorem 0 makes the target precise: a partial Boolean algebra embeds in a Boolean algebra iff its Z₂-homomorphisms separate points. That is, hidden variables in the paper’s sense need enough “global valuations”, and quantum mechanics in dimension 3 has none. The same paper builds a classical hidden-variable model for spin ½ (§6). It argues that von Neumann’s no-go needed additivity on non-commuting observables (Theorem 3). | Active — read in full 2026-09-29 (NOTE-279); worth reading. It is the primary source of the Kochen–Specker theorem and of the partial-algebra formulation that the sheaf and topos programmes generalise. The 117-vector construction is superseded for economy by later small KS sets (e.g. Peres’s 33, Cabello’s 18 in dimension 4); the review LIT-263 covers those. |
| LIT-299 v2 | A topos foundation for theories of physics: III. The representation of physical quantities with arrows δ̆°(A): Σ̲ → ℝ̲≽ | Döring & Isham (2008), DOI-10.1063/1.2883777. Each bounded self-adjoint  becomes an arrow δ̆^o(A) : Σ → ℝ^⪰, where ℝ^⪰ is the presheaf of real-valued order-reversing functions on ↓V. At λ ∈ Σ_V it sends V′ ⊆ V to λ(δ^o(Â)_{V′}), and δ^o(Â)_V is the spectral-order-least operator in V above Â. The map  ↦ δ̆^o(A) is injective, but ℝ^⪰ is only an additive monoid, not the real-number object. Its Grothendieck completion k(ℝ^⪰) is an abelian-group object whose global elements are exactly the functions of bounded variation on V(H). | Active — read in full 2026-09-29 (NOTE-290); worth reading as the source of the quantity-value object ℝ^⪰ and of the explicit statement that Gel’fand points of a context are ultrafilters of its projection lattice. Its results are small, mostly proved or cited from de Groote and Döring. The physically motivated parts (k(ℝ^⪰), “intrinsic dispersion”, unitaries) are definitions with no consequences drawn. |
| LIT-303 v3 | Types and Ontology | Sommers (1963), DOI-10.2307/2183167. Develops a theory of categories via the span of predicates over things, arguing that predicability relations must form a tree (hierarchy) and using category mistakes to diagnose type boundaries (per standard description; abstract not retrieved). | Unavailable — seeded 2026-09-29 from metadata and published descriptions, not read: registered because the owner’s prior-art novelty map cites it. A close reading was attempted on 2026-09-29 and no legitimate full text could be reached; it stays Unavailable until a copy is supplied. |
| LIT-306 v2 | The logic of quantum mechanics | Birkhoff & Neumann (1936), DOI-10.2307/1968621. The paper argues heuristically that the experimental propositions of a quantum system correspond to closed linear subspaces of Hilbert space. Meet is intersection, join is closed linear span, and negation is orthogonal complement. The lattice satisfies L1–L4 and complementation L71–L73 but not the distributive law L6. The paper proposes the modular law L5 as its replacement. Under a finite-dimension assumption, it concludes that the propositional calculus of QM is an abstract projective geometry. The Appendix proves that orthocomplementations on P_{n−1}(F), n ≥ 4, are exactly the polarities of definite diagonal Hermitian forms with respect to an involutory anti-automorphism of F. | Active — read in full 2026-09-29 (NOTE-275); worth reading as the founding text of quantum logic, and for its proposed axiom, which is modularity, not orthomodularity. For the orthomodular Hilbert-lattice machinery that is used today (infinite dimensions, Piron, Solèr), later work supersedes it. The paper itself calls its main conclusions “admittedly heuristic”. |
| LIT-310 v2 | A topos foundation for theories of physics: IV. Categories of systems | Döring & Isham (2008), DOI-10.1063/1.2883826. Proposes axioms for a category Sys of physical systems, symmetric-monoidal under composite ⋄ and under disjoint sum ⊔, whose arrows are translations of local languages. Each arrow j : S₁ → S is realised by a left-exact functor τ(j) between the systems’ topoi, together with arrows φ(j) : Σ_{S₁} → τ(j)Σ_S and β(j) : τ(j)R_S → R_{S₁}. Classical physics satisfies the scheme exactly. In quantum theory the disjoint sum H₁⊕H₂ satisfies it (the pulled-back arrow of Â₁⊕Â₂ is δ̆(A₁)), but the composite H₁⊗H₂ does not: the natural pull-back of δ̆(A₁) differs from δ̆(A₁⊗1̂) off the image of V(H₁), which the authors attribute to “operator entanglement”. | Proposed — read in full 2026-09-29 (NOTE-285); promising and unproven. The rules are explicitly “experimental”, the quantum composite fails the commutativity condition the rules state, and the key negative claims ((4.46), and that no operator B̂ gives the pulled-back arrow) are asserted, not shown. What would settle it is a proof of (4.46) and of the non-existence of B̂, plus a variant of the rules (or of the context category) under which tensor-product composites satisfy (3.18). |
| LIT-318 v3 | The Concept of Mind | Ryle (1949), https://archive.org/details/conceptofmin00ryle. Attacks Cartesian mind-body dualism (‘the ghost in the machine’) as a category mistake — representing facts of mental life as if they belonged to a logical type they do not — and recasts mental concepts dispositionally (per standard description). | Unavailable — seeded 2026-09-29 from metadata and published descriptions, not read: registered because the owner’s prior-art novelty map cites it. A close reading was attempted on 2026-09-29 and no legitimate full text could be reached; it stays Unavailable until a copy is supplied. |
| LIT-325 v3 | A topos perspective on the Kochen–Specker theorem: I. Quantum states as generalized valuations | Isham & Butterfield (1998), DOI-10.1023/A:1026680806775. Isham & Butterfield show that, for bounded self-adjoint operators with discrete spectrum, a global section of the spectral presheaf Σ(Â) = σ(Â) on the category O_d, whose arrows are functional relations B̂ = f(Â), is literally a valuation obeying the value rule and FUNC. A global section of the dual presheaf D(W) = Hom(W, {0,1}) on the poset W of Boolean subalgebras of projectors is literally a Kochen–Specker 0/1 assignment. The Kochen–Specker theorem (cited, not reproved) is therefore equivalent to “no global sections” when dim H > 2 (§§2.2–2.3). In place of the missing global valuations, they construct contextual truth values in the Heyting algebra of sieves: ν^ρ(A ∈ Δ) = {f: B̂ →  | tr(ρ Ê[B ∈ f(Δ)]) = 1}. For every density matrix these satisfy functional composition, null, monotonicity, exclusivity and unit conditions (§4.4, §5.3, Theorem 5.1). | Active — read in full 2026-09-29 (NOTE-271); worth reading as the founding paper of the topos approach to quantum theory and the origin of “Kochen–Specker = no global section of a presheaf over contexts”, credited as such by Abramsky & Brandenburger (LIT-016). The reformulation itself is definitional and its proof is two paragraphs. The paper’s own contribution is the sieve-valued generalized valuation, whose later development (von Neumann algebras as base, daseinisation) lives in Parts III–IV and in Döring–Isham (LIT-343, LIT-335, LIT-299, LIT-310). |
| LIT-335 v2 | A topos foundation for theories of physics: II. Daseinisation and the liberation of quantum theory | Döring & Isham (2008), DOI-10.1063/1.2883742. A projector P̂ is mapped to the clopen sub-object δ(P̂) of the spectral presheaf Σ over the poset V(H) of abelian von Neumann subalgebras, by “daseinisation” (de Groote’s V-support): δ(P̂)V = the least projector in V above P̂. The map is injective and preserves ∨, but only δ(P̂∧Q̂) ⪯ δ(P̂)∧δ(Q̂). This represents the propositional language PL(S) in the Heyting algebra Sub_cl(Σ). A pure state gives the truth object T^ψ, and “A ε Δ” gets the sieve-valued truth value {V′ ⊆ V | ⟨ψ|δ(Ê[A∈Δ]){V′}|ψ⟩ = 1}. | Active — read in full 2026-09-29 (NOTE-292); worth reading as the core reference for “quantum propositions as clopen sub-objects of the spectral presheaf” (daseinisation, Sub_cl(Σ), truth objects). It is a cleaned-up restatement of Isham–Butterfield (LIT-325) plus de Groote’s operation, not a new no-go result. Several proofs are sketched or omitted, and the “no global elements” statement it relies on needs dim H > 2, which it never says. |
| LIT-337 v3 | Boolean Concept Logic | Wille (2000), DOI-10.1007/10722280_22. Extends Formal Concept Analysis with negation by introducing semiconcepts and protoconcepts, which form double Boolean algebras, as a Boolean concept logic (per the standard description of the paper; abstract not retrieved). | Unavailable — seeded 2026-09-29 from metadata and published descriptions, not read: registered because the owner’s prior-art novelty map cites it. A close reading was attempted on 2026-09-29 and no legitimate full text could be reached; it stays Unavailable until a copy is supplied. |
| LIT-340 v2 | A theory of concepts and their combinations I: The structure of the sets of contexts and properties | Aerts & Gabora (2005), DOI-10.1108/03684920510575799. Aerts & Gabora model a concept as an entity with states that change under contexts, a “state context property system” (Σ, M, L, µ, ν). They report an 81-subject e-mail study in which 7 contexts shift the rated frequency of 14 exemplars of “pet” (for example dog 0.50 under “The pet is chewing a bone” against 0.12 in the unit context) and the applicability of 14 properties. They then postulate that contexts and properties each form a complete orthocomplemented lattice, and call the structure quantum-like because a state can be an eigenstate of e ∨ f without being one of e or of f (eq. 19). No theorem is proved, the lattice is not shown to be non-distributive or orthomodular, and the paper contains no Hilbert-space model and no treatment of combination; both are deferred to Part II. | Active — read in full 2026-09-29 (NOTE-294); worth reading as the founding statement of the state-context-property approach to concepts that the prior-art map cites, and for its pet data. Read it as a programme and a data set, not as a result. The lattice structure is assumed (“we suppose”, §3.2), the orthocomplement is illustrated rather than derived, and the “quantum-like” criterion it gives does not by itself make the lattice non-Boolean. |
| LIT-343 v2 | A topos foundation for theories of physics: I. Formal languages for physics | Döring & Isham (2008), DOI-10.1063/1.2883740. The programme paper. Its contention is that a theory of a physical system S is a representation of a typed “local language” L(S) (ground types Σ and R, function symbols A : Σ → R) in a topos. Physical quantities become arrows Σ_φ → R_φ, and propositions become sub-objects of Σ_φ, which form a Heyting algebra. Classical physics is the representation in Sets. The paper proves nothing. Its one argument is that the axiom ¬(A ε Δ) ⇔ A ε ℝ∖Δ is not validated by non-Boolean Heyting representations (§3.2.1). | Active — read in full 2026-09-29 (NOTE-277); worth reading as the statement and vocabulary of the Döring–Isham programme (neo-realism, PL(S) and L(S), state object and quantity-value object, representation in a topos). It is discursive and contains no results, and every piece of quantum mathematics is deferred to papers II–III (LIT-335, LIT-299). |
| LIT-344 v5 | Formal Concept Analysis: Mathematical Foundations | Ganter & Wille (1999), DOI-10.1007/978-3-642-59830-2. The standard mathematical monograph on Formal Concept Analysis: formal contexts, concept lattices and their structure theory (per publisher record). | Unavailable — seeded 2026-09-29 from metadata and published descriptions, not read; a second attempt on 2026-10-09 again reached no lawful full text. Springer sells the 1999 book and the 2024 second edition (OpenAlex: both closed access, no repository copy); HathiTrust holds the 1999 edition search-only; the Internet Archive has no copy. The front matter Springer serves freely (preface and contents) was read; the main text was not. No NOTE is filed. It stays Unavailable until a copy is supplied, not on merit. |
| LIT-350 v3 | Categories and De Interpretatione (Clarendon Aristotle Series, trans. and notes J. L. Ackrill) | Aristotle & (translator) (1963), DOI-10.1093/actrade/9780198720867.book.1. Aristotle’s Categories, whose ch. 10 classifies four kinds of opposites (relatives, contraries, privation/possession, affirmation/negation), and De Interpretatione, whose ch. 7 distinguishes contrary from contradictory statements; here in Ackrill’s standard translation with commentary (per standard description). | Unavailable — seeded 2026-09-29 from metadata and published descriptions, not read: registered because the owner’s prior-art novelty map cites it. A close reading was attempted on 2026-09-29 and no legitimate full text could be reached; it stays Unavailable until a copy is supplied. |
| LIT-353 v3 | The Theory of Representations for Boolean Algebras | Stone (1936), DOI-10.2307/1989664. The paper identifies Boolean algebras with Boolean rings with unit (xx = x), and generalized Boolean algebras with Boolean rings (Thms 1–4). Theorem 67 proves that every Boolean ring A is isomorphic to the algebra B(A) of classes 𝔈(a) = {prime ideals p : a ∉ p}, under symmetric difference and intersection. Its ideal lattice is isomorphic to the system of classes 𝔈(𝔞) under arbitrary unions and finite intersections. The existence of enough prime ideals (Thm 63) is proved by transfinite induction, and Theorem 70 shows that “every Boolean ring has an isomorphic algebra of classes” and “every ideal is the product of its prime divisors” are equivalent without choice. Theorems 68–69 classify all set-representations as restrictions of B(A) to subclasses of prime ideals. The topology, i.e. Stone spaces and duality, is explicitly deferred to “another paper”. | Active — read in full 2026-09-29 (NOTE-272); worth reading as the primary source of the Stone representation theorem, via prime ideals of Boolean rings, and of the Boolean-ring viewpoint. It is long and technical, and for the representation alone Chapter IV plus Theorems 1–2, 33–40 and 49 suffice. For the topological duality (Boolean algebras ↔ totally disconnected compact Hausdorff spaces), the map’s actual need, Stone 1937 (Trans. AMS 41, LIT-358) is the source. |
| LIT-357 v2 | Studies on the Foundation of Quantum Mechanics. I | Husimi (1937), DOI-10.11429/ppmsj1919.19.0_766. Husimi derives Birkhoff and von Neumann’s lattice axioms from statistical premises. Implication is P̄ ≤ Q̄ in every state (and requires compatibility), negation is Q̄ = 1 − P̄, and compatible propositions obey classical logic. Meet is obtained from “Ehrenfest’s principle” (additivity of mean values) via the top eigenvalue of aP + bQ (pp. 778–779), and the modular law, equivalently the parallelogram law |P| + |Q| − |P∩Q| = |P∪Q|, is proved under a finite-chain assumption. The orthomodular identity is used but never named or stated as an axiom. It appears as the step “since we admit traditional logic to any classical part … S + P∩Q = R” for R ⊃ P∩Q (p. 784), and as the case “(Q − P) + P = Q provided Q ⊃ P” of a classical identity (p. 780). | Active — read in full 2026-09-29 (NOTE-312); worth reading as the first derivation of the Birkhoff–von Neumann propositional calculus from operational premises (states, mean values, compatibility), and for its physical account of meet and join. It is not, however, a clean citation for “the orthomodular law”. The law is an unnamed lemma resting on “classical logic within compatible sets”, and the paper’s axiomatic target is modularity under a finite-chain assumption. A text that states orthomodularity as an axiom (e.g. Kalmbach, Orthomodular Lattices, 1983; unverified here) would settle row 1’s citation. |
| LIT-358 v2 | Applications of the theory of Boolean rings to general topology | Stone (1937), DOI-10.1090/S0002-9947-1937-1501905-7. Stone topologises the set 𝔈 of prime ideals of a Boolean ring by taking the sets 𝔈(a) as a basis. 𝔈 is then a totally disconnected, locally bicompact Hausdorff space, bicompact exactly when the ring has a unit (Thm 1), and every such space arises this way (Thm 2). Theorem 4 states that “the algebraic theory of Boolean rings is mathematically equivalent to the topological theory of Boolean spaces”: isomorphism ↔ homeomorphism, ideals ↔ open sets, quotients ↔ closed subsets, unit ↔ bicompactness, and subrings ↔ continuous images (Thm 7). The same paper also contains what are now called the Stone–Čech compactification (Thms 78–79, 88), the Stone–Weierstrass theorem (Thm 82), the Banach–Stone theorem (Thm 83) and closed ideals of C(X) ↔ closed sets (Thm 85). | Active — read in full 2026-09-29 (NOTE-311); worth reading as the primary source of Stone duality and the correct citation for map row 8’s “Stone duality”, replacing LIT-353. For that purpose Chapter I (pp. 378–394) is enough. The rest is a long general-topology memoir whose best-known results (Stone–Čech, Stone–Weierstrass, Banach–Stone) are stated in 1937 vocabulary (bicompact, H-space, analytical isomorphism) and are now better learned from textbooks. |
| LIT-378 | ’What is a Thing?’: Topos Theory in the Foundations of Physics | Döring & Isham (2008), arXiv:0803.0417. A 212-page restatement of the topos programme of papers I–IV. A theory of a system S is a representation of a typed language L(S) in a topos. In quantum theory the topos is presheaves on the poset V(H) of abelian von Neumann subalgebras, propositions are clopen sub-objects of the spectral presheaf Σ via daseinisation, a pure state gives sieve-valued truth values ν(A ε Δ; ψ)V = {V′ ⊆ V | ⟨ψ|δ(Ê[A∈Δ]){V′}|ψ⟩ = 1}, and each bounded self-adjoint  becomes an arrow Σ → ℝ^↔ whose values are monotone intervals over subcontexts. Classical physics fits its axioms for composite systems exactly; quantum theory fits the disjoint sum but not the tensor-product composite. | Active — read in full 2026-10-01 (NOTE-326); worth reading as the one-volume statement of the Döring–Isham topos programme. It is, by the authors’ own account (p. 14), “partly an amalgam” of papers I–IV (LIT-343, LIT-335, LIT-299, LIT-310), with corrections and some new material. The new material is the value of a quantity in a pseudo-state and the inverse-image link between L(S) and PL(S) (§§8.5–8.8, Thm 8.6), the algebra of the candidate quantity-value objects (§9.3), the Boolean-subalgebra base category (§5.5.3), Kochen–Specker as a lifting obstruction (§6.6), and a long speculative §14–15. It adds no new no-go result. Its proofs are as sketchy as the series’ at the same places: Sub_cl(Σ) is Heyting (Thm 16.1) with ⇒ left unwritten, and ι : O → P_clΣ natural and monic is left to the reader. A reader who has read I–IV gains only §§8.5–8.8, 9.3 and 14; a reader new to the programme should start here. |
| LIT-380 v2 | A Topos Perspective on the Kochen-Specker Theorem: III. Von Neumann Algebras as the Base Category | Hamilton et al. (1999), arXiv:quant-ph/9911020. Hamilton, Isham & Butterfield move the series’ base category from operators (O) and Boolean subalgebras (W) to the poset V of commutative von Neumann subalgebras of B(H). There they restate Kochen–Specker as “the spectral presheaf Σ(V) = Gelfand spectrum of V has no global elements” (dim H > 2, cited, §2.2). They identify the coarse-graining presheaf G(V) = L(V), G(i)(P̂) = inf{Q̂ ∈ L(V₂) | P̂ ≤ Q̂} (Def. 3.1), with the presheaf CloΣ of clopen subsets of the spectra; the isomorphism is asserted, and part IV proves it. A state ρ yields the sieve-valued valuation ν^ρ_V(P̂) = {V′ ⊆ V | ρ(G(P̂)) = 1} (Def. 3.4) and the support projectors inf{P̂ ∈ L(V) | ρ(P̂) = 1}. These form a global element of G and hence an “interval valuation”, a subobject of Σ (§§4.2–4.4). The probability-r valuations give subobjects of G but not global elements. | Superseded — by LIT-382; read in full 2026-10-01 (NOTE-327); covered better by part IV (Butterfield & Isham 2002, read alongside), which restates this paper’s V-framework definitions nearly verbatim, proves the G ≅ CloΣ isomorphism that this paper only asserts and develops its interval valuations into theorems, and by Döring–Isham II (LIT-335), whose spectral presheaf over V(H) and clopen propositions are the mature form; it remains the citation for introducing V as the base category (as LIT-335 credits it). |
| LIT-381 v2 | A Topos Perspective on the Kochen-Specker Theorem: II. Conceptual Aspects, and Classical Analogues | Butterfield & Isham (1998), arXiv:quant-ph/9808067. Butterfield & Isham argue that the sieve-valued “generalised valuations” of part I are not a quantum peculiarity but the natural valuations for any presheaf of propositions on any small category. Three supports are offered. (1) Classical physics: the value presheaf Υ(Ā) = Ā(S) on the category M of measurable functions has global sections (one per microstate, eq. 3.7), yet a macrostate R ⊆ S yields a sieve-valued valuation ν^R(A ∈ Δ) = {f_M | B̄(R) ⊆ f(Δ)} (eq. 3.10) with the same FUNC property as the quantum ν^ρ. (2) A proof that a sieve-valued valuation on any presheaf G obeys generalised FUNC, ν(B, G(f)(d)) = f*(ν(A, d)), iff it is a natural transformation G → Ω, i.e. a subobject of G (Theorem 4.1). (3) An informal argument, explicitly “not a genuine deduction” (§5.2), that if partial truth is fixed by which weakenings of a proposition are totally true, the truth value is a sieve. | Active — read in full 2026-10-01 (NOTE-329); worth reading as the series’ conceptual companion and the only place it states the classical analogue and the partial-truth motivation; the mathematics is light (one short theorem), and the sieve semantics it motivates is carried on in part III, part IV and Döring–Isham (LIT-343, LIT-335). |
| LIT-382 v2 | A Topos Perspective on the Kochen-Specker Theorem: IV. Interval Valuations | Butterfield & Isham (2001), arXiv:quant-ph/0107123. Butterfield & Isham show, over the poset V of commutative von Neumann subalgebras, that sieve-valued valuations and “interval valuations” (assignments of support projectors, or of subsets of Gelfand spectra) determine each other under stated conditions. If supports s(α, V) = inf{P̂ | α_V(P̂) = true_V} form a global element of the coarse-graining presheaf G, then α_{V₁}(P̂) = {V₂ ⊆ V₁ | G(s(α, V₁)) ≤ G(P̂)} is a sieve-valued valuation obeying FUNC (Theorem 3.1). There is an analogue for “tight” subobjects of Σ (Theorem 3.2). Both are satisfied by every state’s valuation ν^ρ. The ordering ≤ (or ⊆) is shown to be the natural relation securing sievehood, null, monotonicity, exclusivity and unit (§4). The review §2.4 also supplies the proof, via state extension, that G ≅ CloΣ: restricting the clopen set of P̂ to V₂ gives the clopen set of its coarse-graining. Part III had only asserted this. | Active — read in full 2026-10-01 (NOTE-328); worth reading as the finished statement of the series’ von Neumann-algebra framework. It proves the G ≅ CloΣ isomorphism (coarse-graining = direct image of clopen regions) that Döring–Isham’s daseinisation relies on, and it shows that a state’s sieve-valued truth values are fixed by its support, a global element of G. Its two theorems are correct but close to definitional, so its value lies in the framework rather than in depth. |
| LIT-389 v2 | Some Possible Roles for Topos Theory in Quantum Theory and Quantum Gravity | Isham & Butterfield (1999), arXiv:gr-qc/9910005. Isham & Butterfield argue, without proving anything new, that presheaf toposes over a base of “contexts” suit physics because the subobject classifier Ω is fixed by the base. They say this answers the objection that many-valued logics are arbitrary (§2.2), and that it keeps the logic distributive (§1.1). They then sketch seven applications. Five are speculative one-paragraph proposals (frames, observers, causal sets, TQFT, synthetic-differential-geometry time in continuous histories). One (§3.7) recaps their Kochen–Specker results: KS ⇔ the dual presheaf D(Â) = Hom(W_A, {0,1}) on the operator category O has no global sections (dim H > 2), and every state ψ gives a FUNC-obeying sieve-valued valuation ν^ψ(A ∈ Δ) = {f_O : Â → B̂ | Ê[B ∈ f(Δ)]ψ = ψ}. | Active — read in full 2026-10-01 (NOTE-334); worth reading only as the programme’s short, informal manifesto as of 1999, written before parts III–IV appeared. It joins the Kochen–Specker valuations to the continuum scepticism (real-valued quantities, space and probabilities) that the Döring–Isham programme later develops, and the Literalism/Extra-Values framing appears nowhere else in the record. Its one technical section is a recap of KS I–II, and a reader of LIT-325, LIT-381 and LIT-378 loses little by skipping it. |
| LIT-390 v2 | Topos Theory and Consistent Histories: The Internal Logic of the Set of All Consistent Sets | Isham (1996), arXiv:gr-qc/9607069. Isham takes the poset B of all Boolean subalgebras (“windows”) of the history orthoalgebra UP, ordered by coarse-graining, and shows that the presheaf A_d(W) = {α | some d-consistent W′ ⊇ W contains α} is a subobject of the constant presheaf ΔUP, whereas the naive “realisable in W” assignment is not a presheaf at all (§4.1–4.2). The probability claim ⟨α, p⟩ then gets the sieve-valued semantic value {W ⊆ W₀ | ∃ d-consistent W′ ⊇ W with α ∈ W′} if d(α, α) = p and ∅ otherwise (4.16), a global element 1 → Ω in Set^B, so the logic of “all consistent sets at once” is the distributive but non-Boolean Heyting algebra of sieves on B. | Active — read in full 2026-10-01 (NOTE-333); worth reading as the origin of the Isham school’s sieve-valued, coarse-graining truth values, which the Kochen–Specker series names as its motivation (KS I, ref. [13]); it is the only place the construction is applied to consistent histories, it is short and elementary, and its constructions are correct as stated, but read it knowing that the Heyting values measure only whether α can be embedded in a consistent set (the probability d(α, α) is the same in every window), so it says nothing about the conflicts between consistent sets that motivate it. |
| LIT-408 | Jokes and the Logic of the Cognitive Unconscious | Minsky (1980), MIT AI Memo 603; in Vaina & Hintikka (eds.), Cognitive Constraints on Communication (Reidel, 1984), pp. 175–200. Commonsense logic cannot be made reliable, so each mind accumulates “censors” that learn the precursors of known-bad thought (paradox, circling, false analogy) and suppress it before it occurs. On that view, humour is censor-learning. Its common element is an “unexpected frame-substitution”, and laughter both stops the absurd line of thought and holds it in focus. Logical nonsense is then as “naughty” as Freud’s forbidden wishes, which removes the gap in Freud’s theory. An essay with no data or program. | Active — read in full 2026-10-01 from the MIT AI Memo 603 text (NOTE-361), not the 1984 book chapter, which was not reachable; worth reading as the society-of-mind programme’s account of humour and of “negative meta-knowledge”. Its argument is that commonsense reasoning cannot be made reliable, so minds learn “censors” that suppress known-bad lines of thought, and that humour and laughter are how those censors are taught and engaged, which dissolves Freud’s puzzle about nonsense jokes. It is an essay: no data, no program, and its evolutionary story is offered as “no plea for this particular scenario”. |
| LIT-410 | A Framework for Representing Knowledge | Minsky (1974), MIT AI Memo 306. A self-declared partial theory of thinking: on meeting a situation one retrieves a frame, a stereotyped structure whose terminals carry conditions and weakly bound default assignments, and adapts it by replacing details. Frames that share terminals form frame-systems whose transformations stand for moves, actions or changes of viewpoint, and failed matches are routed through a learned similarity network. The memo applies this to vision, imagery, language, memory and problem solving, and ends by arguing that consistency-seeking logical systems cannot represent commonsense knowledge, because they are monotonic. Nothing is implemented or tested. | Active — read in full 2026-10-01 (NOTE-337); worth reading as the source of the frame idea and of the critique of “logistic” representation that later motivated non-monotonic reasoning. It is a proposal, not a result: no program is described as built, nothing is measured, and the author says so (“Apology!”, p. 2). The parts to take away are the frame with weakly bound default assignments (§1.11), frame-systems sharing terminals across viewpoints (§1), terminals read as questions (§2.8), the similarity network with cluster “capitols” as an account of family resemblance (§§3.4–3.5), and the appendix on monotonicity and consistency (§6). It contains no society-of-agents idea; that arrives in Plain Talk (LIT-399), which calls itself in part a sequel to this memo. |
| LIT-423 v2 | I Am a Strange Loop | Hofstadter (2007), Basic Books. Per its publisher, an “I” is “a strange loop where the brain’s symbolic and physical levels feed back into each other and flip causality upside down”, and the book asks whether that “I” is real or “merely a convenient fiction”, and how selves “can exist in the minds of others”. Its 26 contents entries run from souls and the causal potency of patterns, through Gödel’s “quintessential strange loop” and downward causality, to “How we live in each other”, “Consciousness = thinking” and zombies and dualism. Unread: registered from the description and the catalogue’s contents note. | Unavailable — registered 2026-10-01 from the publisher’s description and the Library of Congress catalogue record with its contents note, not read: no lawful full text could be reached. The Internet Archive scans are lending-only, and no publisher or author copy is posted. It stays Unavailable until a copy is supplied. |
| LIT-437 v2 | Gödel, Escher, Bach: an Eternal Golden Braid | Hofstadter (1979), Basic Books. The book that introduced the “strange loop”: per its publisher, an account of the “I”, self and consciousness built on the self-referential construction Gödel used to make a sentence assert its own unprovability. Chapters alternate with contrapuntal dialogues, chiefly between Achilles and the Tortoise, each built to exhibit the idea it discusses. Unread: no lawful full text was reachable, so it is registered from the publisher’s description and the catalogue record, and its year is the only date a source gives. | Unavailable — registered 2026-10-01 from the publisher’s description and the Library of Congress catalogue record, not read: no lawful full text could be reached. The Internet Archive scans of the 1979 Basic Books printing are lending-only, HathiTrust is search-only, and no publisher or author copy is posted. It stays Unavailable until a copy is supplied. |
| LIT-794 v2 | Making It Explicit: Reasoning, Representing, and Discursive Commitment | Brandom (1994), Harvard University Press. Explains meaning by use in normative terms. Asserting is undertaking a commitment, licensing others’ reassertion and taking on responsibility to show entitlement; interlocutors keep score of one another’s commitments and entitlements; a claim’s content is its inferential role (what it follows from, what follows from it, what it rules out). Logical vocabulary makes these implicit proprieties explicit. Skimmed: the Preface and the core of chapter 3 only. | Active — skimmed 2026-10-09 (NOTE-622); the Preface and the core of chapter 3 (pp. 141–157 and 172–193) were read, the rest of the 741 pages not. Worth reading as the source of the deontic scorekeeping model of assertion. Asserting undertakes a commitment, authorizes others to reassert it, and takes on a responsibility to show entitlement if challenged. Every interlocutor keeps a score of everyone’s commitments and entitlements, so the score is doubly perspectival, and an assertion’s significance is the change it makes to each score, fixed by the content’s inferential role. Read it with the caveat that the reading covers the model, not the book’s arguments for it (chapters 1–2, 4–9). |
| LIT-818 | Defaults in Update Semantics | Veltman (1996), J. Philos. Logic 25(3):221–261. Defines an update system (a sentence’s meaning is an operation on information states), proves it reduces to static propositions exactly when it is additive, and shows epistemic “might” and “presumably” are non-persistent tests. Builds a decidable non-monotonic logic of default rules (“if φ, normally ψ”) in which specificity and other priorities between conflicting defaults follow from coherence and applicability conditions on expectation frames. | Active — read 2026-10-09 (NOTE-617); worth reading as the programmatic statement of update semantics: the meaning of a sentence is the change it makes to an information state, and an update system is “additive”, so reducible to static propositions, exactly when updates are total, idempotent, persistent, monotone and strengthening. “Might” and “presumably” fail persistence: they are tests on a state, not information about the world. Its second half is a theory of defaults in which priority between conflicting rules (“more specific wins”, the Nixon diamond left open) follows from a coherence and an applicability criterion rather than being stipulated. Read the default theory as one formalisation the author himself hopes will be bettered; the framework is the lasting part. |
| LIT-838 | The Semantics of Definite and Indefinite Noun Phrases | Heim (1982), Ph.D. dissertation, University of Massachusetts Amherst (Garland, 1988). Indefinites and definites are variables with no quantificational force; indefinites are bound by the nearest operator, which explains donkey anaphora. Meaning is recast as file change potential on a common ground of numbered cards, and the definite/indefinite contrast becomes one felicity condition (new card versus familiar card), from which binding, existential readings, presupposition projection and narrow-scope definites follow. | Active — read 2026-10-09 (NOTE-608); worth reading as the founding statement of file change semantics and of the variable analysis of indefinites: an indefinite has no quantificational force of its own and is bound by whatever operator is nearest (an adverb of quantification, a determiner, the unpronounced necessity operator of a bare conditional), which is what makes donkey sentences come out right. Its third chapter replaces truth conditions by file change potentials, operations on a structured common ground of numbered cards, and derives the definite/indefinite contrast from one felicity condition: an indefinite opens a new card, a definite must update a familiar one. Read it as an argued theory with worked examples and stated open problems (specific indefinites, weak crossover, accommodation), not as a closed system. |
| LIT-841 | Semantic Unification: A Sheaf Theoretic Approach to Natural Language | Abramsky & Sadrzadeh (2014), ARXIV-1403.3351, in the Lambek Festschrift (LNCS 8222, pp. 1–13). Models basic Discourse Representation Structures as sections of a presheaf of consistent literals over (vocabulary, variables), an anaphoric resolution as a cover by variable maps, and the meaning of a discourse as the gluing of its sentences’ sections, unique when it exists. Failure to glue is inconsistency, not contextuality in the Abramsky–Brandenburger sense; competing resolutions are competing covers, ranked in the probabilistic section by corpus counts. | Active — read in full 2026-10-09 (NOTE-644); worth reading as the first paper to model discourse meaning as sheaf-theoretic gluing, and as the record’s earliest bridge between the Abramsky–Brandenburger framework and natural-language semantics. A basic Discourse Representation Structure is a section of a presheaf of consistent literals; a choice of anaphoric resolution is a cover, a jointly surjective family of variable maps; and the meaning of the discourse is the gluing, which is unique when it exists (Proposition 1, its only result). Its “contextuality” is context dependence, not the failure of a compatible family to glue: the only obstruction it exhibits is inconsistency of literals. Its probabilistic section ranks candidate covers by summed corpus counts rather than gluing distributions. Short and preliminary by its own account. |
| LIT-843 | Combining contextuality and causality: a game semantics approach | Abramsky, Barbosa & Searle (2024), ARXIV-2307.04786, Phil. Trans. R. Soc. A 382:20230002. Adds an enabling relation to a measurement scenario and reads contextuality as a game: the Experimenter chooses measurements, Nature chooses outcomes, and Nature’s deterministic strategies replace the event sheaf. Recovers flat contextuality and Gogioso–Pinzani causal Bell scenarios, and expresses adaptive MBQC by Experimenter strategies. The strategy presheaf is not a sheaf: compatible deterministic strategies can fail to glue or glue non-uniquely. | Active — read in full 2026-10-09 (NOTE-646); worth reading as the version of sheaf-theoretic contextuality in which measurements are performed in a causal order and the choice of the next one may depend on earlier outcomes. A causal measurement scenario adds an enabling relation (Kahn and Plotkin’s information matrices renamed); Nature’s deterministic strategies over it replace the event sheaf, and the Abramsky–Brandenburger definitions of empirical model and contextuality then go through unchanged. Flat scenarios and Gogioso and Pinzani’s Bell scenarios with a causal order come out as special cases, and Experimenter strategies express adaptive measurement, as in the Anders–Browne GHZ OR-gate. Its sharpest point is that the strategy presheaf is not a sheaf: deterministic, compatible local strategies can fail to glue (Example 7.2) or glue non-uniquely (Example 7.3). A short paper; several results are deferred to an extended version. |
| LIT-845 | Closing Bell: Boxing black box simulations in the resource theory of contextuality | Barbosa, Karvonen & Mansfield (2021), ARXIV-2104.11241, in Samson Abramsky on Logic and Structure in Computer Science and Beyond (Springer, 2023). Characterises which convex maps between the empirical models of two scenarios are induced by classical (non-adaptive) procedures: exactly those given by a non-contextual model of a “hom” scenario [S, T] whose outcomes are procedures. Non-local games are procedures into a one-bit scenario, and the hom construction makes scenarios with predicates a closed category. | Active — read in full 2026-10-09 (NOTE-650); worth reading as the result that says which transformations between the empirical models of two different scenarios are classical. A probabilistic procedure S → T (a mixture of deterministic procedures, each answering every measurement of T by a context of S and a post-processing of outcomes) induces a convex map EMP(S) → EMP(T). A convex map is so induced exactly when it comes from a non-contextual model, satisfying a simpliciality predicate, on a new “hom” scenario [S, T] whose outcomes are procedures. Compatible local procedures that do not glue into one global procedure are contextual models of [S, T]: “contextual simulations”. The construction makes scenarios with predicates a closed category. Non-adaptive only; the arXiv v2 corrects Theorem 44 of the published chapter. |
| LIT-934 v2 | Quantum structure in cognition | Aerts (2009), Journal of Mathematical Psychology 53(5):314–348. Membership weights for pairs of concepts and their conjunctions and disjunctions (Hampton 1988) have a Kolmogorovian model iff they are neither over- nor underextended and a Kolmogorovian factor is non-negative; many items fail. A subspace lattice with meet and join fits the second kind of failure but provably not the first, which the paper models with an emergent-concept sector in Fock space. Negation appears only as an orthocomplement used to derive conjunction from disjunction. | Active — read 2026-10-14 (NOTE-808) in full; worth reading as the paper that sorts Hampton’s concept-combination data into two kinds of non-classicality and proves that the main kind, over- and underextension, cannot come from a subspace lattice’s meet and join. Read it knowing that its fitting model has a free parameter per item and stipulated conditions, that its two-layer account of thought is interpretation, and that negation enters only as the orthocomplement used to derive the conjunction model, never measured. Registered for QUESTION-055; THEORY-255 is filed from it. |
| LIT-956 v2 | Back and forth between algebraic geometry, algebraic logic, sheaves and forcing | Sayed Ahmed (2018). Distributive lattices with join-preserving idempotent operators are represented, after Comer, as continuous sections of a sheaf of quotient algebras over the Priestley space of their fixed-point part; a small site is said to give a notion of forcing, with a Łukasiewicz conjunction forced through a tensor product, and many-valued theories are interpreted in a quasi-topos. Most theorems are stated with sketched proofs or none, and negation is never written out. | Active — read 2026-10-14 (NOTE-817) in full; worth reading only as a pointer to Comer’s sheaf duality for algebras of formulas, extended here to distributive lattices with operators, and to presheaf forcing with an added Łukasiewicz clause. Read it knowing that its main theorems are stated with sketched proofs or none, that it never writes negation or a pseudo-complement, and that it concerns distributive lattices and forcing posets, not contexts. It does not supply the Heyting-over-contexts machinery QUESTION-055 was filed for; no THEORY is filed from it. |
| LIT-1019 | Information Flow: The Logic of Distributed Systems | Barwise & Seligman (1997), Cambridge University Press. Channel theory: a classification is a set of tokens, a set of types and a relation saying which token is of which type; infomorphisms are maps between classifications, channels are families of infomorphisms into a core, and information flows along a channel by the regularities of its core, captured by local logics. Not read. | Unavailable — filed 2026-10-13 from its Crossref record, not read. Registered at the owner’s request from the survey of the Mathematics of Meaning corpus, for CLAIM-098, CLAIM-011 and QUESTION-005. No NOTE is filed, and it stays Unavailable until it is read, not on merit. Looked for on 2026-10-13, none found: OpenAlex reports it closed, with no open-access or repository location; Semantic Scholar has no record of the DOI; Crossref gives only Cambridge Core’s terms licence; Cambridge Core sells the chapters behind ‘Get access’; a web search found no author-posted chapter or draft, and no personal page for Jerry (Jeremy) Seligman listing one; the PhilArchive record (BARIFT) could not be opened from here (bot challenge). Seligman’s later chapter on channels in Sommaruga (ed.), Formal Theories of Information (Springer 2009; Auckland ResearchSpace 2292/13632) is a separate work, not a chapter of this book, and was not read. |
| LIT-1050 | On the logic of theory change: Partial meet contraction and revision functions | Alchourrón, Gärdenfors and Makinson (1985), JSL 50(2). The AGM theory: postulates for contracting and revising a logically closed belief set, and their characterization by partial meet contraction. | Active — read in full 2026-10-15 from a scan of the published article (JSL 50(2), pp. 510–530) that David Makinson posts on his own site (sites.google.com/site/davidcmakinson/, a Google Drive file linked from his publication list as item 23); Unpaywall, OpenAlex and Semantic Scholar report it closed, Cambridge Core and JSTOR are subscription, and Project Euclid refused this environment. Worth reading as the source of the AGM postulates for contracting and revising a logically closed theory, of the Levi identity as the definition of revision, and of the two representation theorems: the six basic postulates characterize exactly the partial meet contractions (Observation 2.5), and with the two supplementary postulates exactly those generated by a transitive relation over the maximal non-implying subsets (Corollary 4.5). For CLAIM-294 it shows that in AGM the closed theory alone does not fix a revision, since a selection function or ordering must be added and different ones disagree on the same theory, but the added state is a preference over remainders, not a record of what a belief depended on; the paper does not discuss why beliefs are held or the belief-base point, which belongs to Hansson (LIT-1072). For QUESTION-105 it answers only a one-step version: a theory plus a transitive ordering suffices, with no redundancy in the finite case (Observation 4.6), and it says nothing about iterated revision. |
| LIT-1072 | Logic of Belief Revision | Hansson’s Stanford Encyclopedia survey of the logic of belief revision: AGM and its alternatives, and the contrast between revising logically closed belief sets and revising belief bases, which keep the beliefs held in their own right apart from their consequences. | Active — read in full 2026-10-15 from the Stanford Encyclopedia’s own page (plato.stanford.edu/entries/logic-belief-revision/), the revision it dates “substantive revision Wed Jul 29, 2026”, also served as the Fall 2026 archive edition. Worth reading as a compact, current survey of AGM belief revision and its rivals, and as the standard statement of why a belief base is not its closure: two bases with the same consequences are “statically equivalent” but not “dynamically equivalent”, bases escape the Recovery postulate, and they keep inconsistent states apart where every closed set collapses to one. For QUESTION-105 and CLAIM-294 it shows the full-belief form of the claim that current conclusions are not a sufficient state for revision (the Abe and Bob example), and also that belief-set models carry the missing difference in a selection mechanism or entrenchment ordering instead of a base; for CLAIM-295 its bases widen the operations that stay well defined but record only which beliefs are basic, not reasons, sources or defeated alternatives. Truth maintenance appears once, as history. The phrases “between belief states represented as closed sets” and “belief bases retaining additional structure” that the filing attributes via A10 are not in this revision. |
| LIT-1087 | Negation as Failure | Clark gives a query evaluator for a data base of clauses (a Horn clause prover in which a ground negated literal ~P is taken as a lemma when the recursive evaluation of P fails on every branch) and proves it sound with respect to the completed data base: the clauses read as the if-halves of if-and-only-if definitions, plus equality axioms saying distinct names denote distinct objects. Theorem 2: if for some selection rule every branch of the evaluation tree of Q terminates with failure, then not-(exists x)Q is a theorem of the completed data base. A branch that does not terminate licenses nothing; the rule requires the search to be exhausted, which the paper calls “the exhaustive but unsuccessful search for a proof of P”. The evaluator is in general incomplete (non-ground negation, a single evaluation tree, no case analysis); it is complete for allowed queries on hierarchical data bases (Theorem 4). | Active — read in full 2026-10-15 (NOTE for L39) from the author’s own copy, a scan linked from Keith Clark’s Imperial College page for the paper (www.doc.ic.ac.uk/~klc/NegAsFailure.pdf, via www.doc.ic.ac.uk/~klc/neg.html); the scan’s printed pages run 113–141, not the 293–322 Crossref gives for the Plenum chapter, and which printing it is was not identified. Unpaywall, OpenAlex and Semantic Scholar report the chapter closed. Worth reading as the source of negation as failure and of the completed data base: a Horn clause evaluator that takes ~P as a lemma when every branch of the evaluation tree for P terminates in failure is sound for the clauses read as if-and-only-if definitions plus axioms that distinct names denote distinct objects (Theorem 2); a non-terminating search licenses nothing, the evaluator is in general incomplete, and it is complete for allowed queries on hierarchical data bases (Theorem 4). Clark identifies the assumption with Reiter’s closed world assumption in one paragraph and makes no formal comparison. For CLAIM-306 it confirms the record’s gloss (“a finitely failed attempt … sound with respect to the completion”), and it shows that a search cut off by a deadline is not a failure in Clark’s sense: the rule needs the search exhausted, so the medic’s rule in CASE-085 is a stronger default than negation as failure, not negation as failure on a time bound; and since the EMT’s own knowledge implied the item was stocked, negation as failure would have refused the conclusion. |
| LIT-1088 | On Closed World Data Bases | Reiter defines the closed-world assumption (CWA) for a function-free first-order database as reasoning from DB together with the negation of every ground atom that DB does not entail, and contrasts it with the open-world assumption (OWA), under which only what DB entails is an answer. He shows that, when DB with these added negations is consistent, closed-world evaluation of any existential query reduces to ordinary (open-world) evaluation of atomic queries combined by union, intersection, difference and projection, so the negations never need to be listed. The CWA can make a consistent database inconsistent (Pa ∨ Pb yields ¬Pa and ¬Pb); consistent Horn databases, and all definite databases, stay consistent. Nothing in the paper concerns how long a search takes: non-entailment is a fixed logical relation, and the CWA’s justification is stated as an assumption of total knowledge of the domain, not proved as a soundness condition. | Active — read in full 2026-10-15 from the author’s preprint as presented at the 1977 Toulouse workshop, University of British Columbia Department of Computer Science Technical Report 77-16 (October 1977), served by UBC’s technical-report archive (www.cs.ubc.ca/sites/default/files/tr/1977/TR-77-16.pdf); the published Plenum chapter (pp. 55–76) is closed (Unpaywall and OpenAlex: closed; Semantic Scholar: no open PDF) and was not seen. Worth reading as the source of the open/closed-world distinction and of the closed-world assumption as a formal object: add the negation of every ground atom the database does not entail, a convention Reiter says “presumes total knowledge about the domain”. It shows that closed-world evaluation of any existential query reduces to open-world evaluation of atomic queries when the database stays consistent under the assumption, that consistent Horn and all definite databases do, and that a disjunctive database such as Pa ∨ Pb does not. For CLAIM-306 it supplies the definition and the completeness assumption (stated, not proved as a soundness condition; a formal soundness result would be Clark’s), and nothing about search time: non-entailment is a fixed relation, so “a closed-world assumption taken on a time bound” is the record’s extension. It also cuts against reading CASE-085 as a closed-world inference: a medic who knows the item is stocked holds a disjunction over compartments, Reiter’s Example 5.1, where the assumption is inconsistent. |
| LIT-1100 | Answering Queries Using Views | Levy et al. (1995), PODS 1995. For conjunctive queries and views, a view can be used in an equivalent rewriting of a query exactly when there is a containment mapping (a homomorphism of bodies) from the view into the query, so every possible use of a stored view is found among those mappings. Without comparison predicates, a minimal rewriting needs no more literals than the query and no new variables, which puts the search in NP; deciding whether some rewriting uses a given set of views (with comparisons only in the query), whether a rewriting with fewer than k literals exists, and whether a rewriting using only the views exists are each NP-complete, and with comparisons in both query and views existence is Π2p-complete. The hardness has two independent sources, the number of mappings and the choice of which query literals to drop, and a polynomial algorithm removes the redundant literals for a given mapping, exactly under stated conditions. Only equivalent rewritings are studied; contained rewritings, the cost of the resulting plan and the size of view collections are outside it. | Active — read in full 2026-10-15 from the authors’ camera-ready of the PODS 1995 extended abstract (pp. 95–104), linked from Alberto Mendelzon’s University of Toronto publications page and fetched from www.cs.toronto.edu/pub/papers/pods95LMSS.ps.Z, because ACM’s open-access PDF refused requests from this environment. Worth reading as the paper that reduces reuse of stored views to query containment: a view can be used in an equivalent rewriting exactly when its body maps homomorphically into the query’s, a minimal rewriting is no longer than the query, and finding a rewriting, a shorter one or one using only the views is NP-complete for conjunctive queries without comparisons (Π2p-complete for existence with comparisons in both), with two independent sources of hardness (THEORY-389). For CLAIM-303 and CLAIM-308 it shows that recognizing that stored answers cover a new question is a worst-case NP-complete search in the size of the question and the stored items’ definitions, not in the stored data, so the per-use cost c_a has a recognition term that varies with the question and the store; it says nothing about prose arguments, contained (partial) reuse, or whether recognized reuse pays. |
| LIT-1104 | Why and Where: A Characterization of Data Provenance | Buneman et al. (2001), ICDT 2001. The paper separates two meanings of the provenance of a piece of output data. Why-provenance is the witness basis: for each valuation of the query that produces the value, the part of the source the query’s patterns matched, one witness per derivation. Where-provenance is the location in the source a value was copied from. For a hierarchical data model and a query language that covers positive (SPJU) relational queries, the witness basis is preserved by the paper’s query rewriting, and the minimal witness basis is the same for equivalent queries with equality conditions, while where-provenance is not invariant over equivalent queries in general and is preserved by rewriting only for a restricted class it calls traceable. Proofs are omitted, and nothing covers negation, aggregation, updates or additions to the source. | Active — read in full 2026-10-15 (NOTE-920) from the authors’ postprint in the University of Pennsylvania’s ScholarlyCommons repository (repository.upenn.edu/handle/20.500.14332/6246, file k50.pdf, 15 pp., camera-ready text of October 2000 without LNCS page numbers), found through Unpaywall and OpenAlex (green, submittedVersion) and fetched through the repository’s API because the landing page is script-only; the Edinburgh repository handle (hdl.handle.net/20.500.11820/46e660d2-8247-4d26-ae49-65fd1bf8364b) returned an error. Worth reading as the source of the distinction between why-provenance, a set of witnesses with one per derivation, and where-provenance, the location a value was copied from, and of the result that only the first can be made independent of how a positive query is written (minimal witness basis, for queries with equality conditions; where-provenance only for “traceable” queries; proofs omitted) (THEORY-367). For QUESTION-105 it shows that a minimal witness basis is a retained state that decides survival under deletion of source facts in set semantics, and that “provenance” names two structures of which only one is invariant; it covers no additions, no negation or aggregation, no strengths of support and no measure of how much is retained. For CLAIM-303 it shows that why-provenance can be recomputed on demand from the query and the source rather than filed; for CLAIM-306 it has nothing for absence, since both notions are defined only for what is in the output. |
| LIT-1110 | Provenance Semirings | Green et al. (2007), PODS 2007. Annotating each input tuple with an element of a commutative semiring, and computing union and projection with + and join with ·, gives one positive relational algebra (RA+) that is set semantics over the Booleans, bag semantics over the naturals, c-tables over positive Boolean expressions, event tables over sets of outcomes, and lineage over sets of tuple ids. The polynomials N[X] in the tuple ids are the most general such annotation: for any RA+ query and any commutative semiring K, the K-annotated answer is the provenance polynomial evaluated at the input’s K-annotations (Theorem 4.3). For datalog the paper needs ω-continuous semirings and formal power series N∞⟦X⟧, with the analogous factorization (Theorem 6.4) and a criterion for infinite coefficients (Theorem 6.5). Everything is positive: no negation, difference or aggregation, and revaluing inputs can only remove output tuples, never add them; trust and deletion propagation are not treated. | Active — read in full 2026-10-15 (NOTE-913) from the authors’ postprint in the University of Pennsylvania’s ScholarlyCommons repository (repository.upenn.edu/handle/20.500.14332/8764, file pods07.pdf, 10 pp., posted by permission of ACM), found through Unpaywall and OpenAlex (green, submittedVersion) and fetched through the repository’s API because the landing page is script-only. Worth reading as the source of semiring provenance: for positive relational algebra over any commutative semiring the annotated answer is the provenance polynomial in N[X] evaluated at the input annotations, and for datalog over ω-continuous semirings the same holds with formal power series in N∞⟦X⟧ (THEORY-373, THEORY-380). For QUESTION-105 it shows that retaining one polynomial per output suffices for every revision that re-annotates input facts in a commutative semiring, deletion included, without rerunning the query; it proves no minimality, and it excludes added facts, negation and contraction. Its “why-provenance” is one set of contributing tuples per output, coarser than the witness basis of LIT-1104 that it cites as the same notion, and its structure for it fails its own semiring axioms. Deletion propagation and trust are not in the paper; deletion follows from Theorem 4.3 as the record’s application. For CLAIM-293 the polynomial separates joint from alternative support but, like topology, leaves the strengths to the valuation; for CLAIM-306 it has no account of absence. |
| LIT-1111 | Optimal Implementation of Conjunctive Queries in Relational Data Bases | Chandra and Merlin (1977), STOC 1977. Defines conjunctive queries (existentially quantified conjunctions of atoms, no equality, constants naming distinct elements) and proves that two are equivalent exactly when there are homomorphisms each way between their natural models (Lemma 13). Every conjunctive query has a minimal equivalent query, unique up to isomorphism, reached by folding (Theorem 12), and that minimal query yields an evaluation program within a constant factor of optimal in the paper’s cost model (Theorem 16). The hardness results are that evaluating a boolean conjunctive query on a database is NP-complete when the query is part of the input (Theorem 7), and that deciding whether one query is a folding of another is NP-complete (Theorem 11). The paper does not state a containment theorem or the NP-completeness of containment or equivalence as such; both are standard corollaries of Lemma 13’s proof and Theorem 11’s construction, and later papers cite them to it. | Active — read in full 2026-10-15 from a scan of the published STOC 1977 paper (pp. 77–90) hosted in the directory of UBC’s course CPSC 504 (www.cs.ubc.ca/~laks/cpsc504/chandra-merlin-1977.pdf), because ACM’s open-access PDF refused requests from this environment; key statements checked against page images, the OCR layer being poor. Worth reading as the source of the homomorphism criterion for conjunctive queries: two are equivalent iff homomorphisms run both ways between the queries read as small databases (Lemma 13), every one has a minimal equivalent unique up to isomorphism (Theorem 12), and evaluating a conjunctive query with the query as input is NP-complete (Theorem 7), as is recognizing a folding (Theorem 11) (THEORY-371). It states equivalence, not containment, and does not state that containment is NP-complete; both are corollaries later work attributes to it. For CLAIM-303 it gives the base procedure, and the worst-case cost, of deciding that a stored answer covers a new question, in the size of the two descriptions; it says nothing about prose arguments or typical cost. |
| LIT-1114 | Maintaining Views Incrementally | Gupta et al. (1993), SIGMOD 1993. Two algorithms compute the changes to a stored derived relation (a view) from changes to the base relations, without recomputing it. Counting stores, for each derived tuple, the number of its derivations and propagates signed counts through delta rules stratum by stratum; it is stated correct for nonrecursive Datalog or SQL views with stratified negation and aggregation, under set or duplicate semantics, and is argued to cost little beyond evaluating the view. DRed (delete and rederive), for recursive views under set semantics only, deletes an overestimate of what a deletion invalidates, puts back those tuples that still have a derivation from what remains, then adds what insertions derive; it is stated to yield exactly the tuples derivable from the new base. The paper is an extended abstract: the theorems are stated without proof (proofs are referred to a 1992 AT&T report), cost claims are argued, not measured, and there are no experiments. | Active — read in full 2026-10-15 from the ACM’s typeset PDF of the SIGMOD ‘93 extended abstract (pp. 157–166), as posted on Columbia University’s Ph.D. candidacy exam reading list in database systems (www.cs.columbia.edu/~gravano/Qual/Papers/13%20-%20Maintaining%20Views%20Incrementally.pdf); a scan with an OCR layer, so definitions and theorems were read from page images. The full version with the proofs (AT&T Bell Labs TR 921214-19-TM, 1992) was not found. Worth reading as the source of the two standard incremental view maintenance algorithms: counting, which stores one derivation count per derived tuple and is stated correct for nonrecursive views with stratified negation and aggregation under set or duplicate semantics (THEORY-362), and DRed, which for recursive views under set semantics overdeletes, rederives what still has a derivation and then inserts, and is stated to give exactly what the new base derives (THEORY-387). The theorems are stated without proof here, and cost claims are argued, not measured. For QUESTION-105 it shows that, for revisions given as changes to base facts under a fixed program, the retained state can be a count per conclusion when support is acyclic and nothing beyond the materialization when it is not, with support rechecked at revision time; neither is provenance or a record of defeated alternatives. For CLAIM-303 it shows the dependency-tracking cost can sit at derivation time (counting) or at revision time (DRed), without measuring either, and that a view kept this way never goes stale. |
| LIT-1116 | Answering Queries Using Views: A Survey | Halevy (2001), VLDB Journal 2001. A survey that separates two problems of answering queries from stored views: finding an equivalent rewriting, which query optimization needs, and finding a maximally-contained rewriting or all certain answers, which data integration needs when sources are incomplete. Its theoretical findings, mostly reported from other papers: an equivalent conjunctive rewriting exists only if one exists no longer than the query, so finding one is NP-complete in the size of the query and view definitions, and checking a candidate is itself NP-complete; the inverse-rules algorithm builds the maximally-contained rewriting, as a possibly recursive datalog program, in time polynomial in the query and views; and finding all certain answers is polynomial in the size of the stored data in many open-world cases, but co-NP-hard in that size under the closed-world assumption even for conjunctive views and queries, or open-world with union in the views or ≠ in the query. Choosing which views to store is left as the next problem; cost-based choice among rewritings is described for practical optimizers, without guarantees. | Active — read in full 2026-10-15 from the publisher’s PDF (VLDB Journal 10: 270–294) hosted on Columbia’s database Ph.D. candidacy-exam reading list (www.cs.columbia.edu/~gravano/Qual/Papers/halevy01.pdf); reference list scanned, not read. Worth reading as the map of answering queries from stored views: equivalent rewritings for optimization against maximally-contained rewritings and certain answers for incomplete sources, with the complexity results of the field as it reports them (THEORY-374). For CLAIM-303 and CLAIM-308 it shows that recognizing reuse is graded: certifying that stored answers settle a question exactly is NP-complete in the size of the question and definitions, extracting what they do give is polynomial (inverse rules) without saying whether it is all, and finding all certain answers from the stored contents is co-NP-hard in their size under the closed-world assumption. For QUESTION-114 it puts this recognition step upstream of view selection, which it names as the open problem. Its results on certain answers and inverse rules are reported from papers the record has not read. |
| LIT-1213 v2 | Knowledge and common knowledge in a distributed environment | Halpern & Moses (1990; first at PODC 1984). With knowledge defined as truth at every point a processor cannot distinguish from the present one, a guaranteed simultaneous coordinated attack makes the attack common knowledge; over a channel that can lose any message nothing becomes common knowledge that would not with no messages delivered, so no correct protocol ever attacks, and not even eventual coordination can be guaranteed. Uncertain start and delivery times alone make common knowledge unattainable; ε-, eventual and timestamped common knowledge are attainable in many systems. | Active — read 2026-10-29 (NOTE-1381) in full, from the authors’ arXiv deposit of the JACM version; worth reading as the paper that makes “knowing” precise for processors in a system of runs and proves that guaranteed coordinated action needs common knowledge, that a channel which can lose any message cannot create it, and that any uncertainty in timing already rules it out, with weaker ε-, eventual and timestamped variants that are attainable. Read it knowing that the protocols are deterministic, that several results (the S5 properties, Theorems 11–12) are proved elsewhere or left to the reader, and that it credits the coordinated attack problem to Gray (1978) without citing Akkoyunlu et al. (1975). |
| LIT-1633 v2 | Mr. Russell’s “Causal Theory of Perception” | Newman (1928). Against Russell’s claim that we know only the structure of the external world: any collection of the right cardinality can be given relations with any structure we please, so knowing only structure is knowing only cardinality, unless the relations are specified as more than abstract relations. | Unavailable — filed 2026-10-27, not read. A close reading was attempted on 2026-10-27 and no lawful full text was reached: the article is closed on Unpaywall and OpenAlex (Mind, Oxford University Press), with no repository copy. It stays Unavailable until a copy is supplied. |
| LIT-1643 v2 | Belief, awareness, and limited reasoning | Fagin & Halpern (1987). Logics of explicit and implicit belief that avoid logical omniscience by adding an awareness operator: an agent explicitly believes only what it implicitly believes and is aware of, so a proposition built from concepts the agent lacks cannot be explicitly entertained. | Unavailable — filed 2026-10-27, not read. A reading was attempted on 2026-10-27 and no lawful full text was reached: Unpaywall and OpenAlex both give the article as closed, and the only other location OpenAlex lists is a CiteSeerX cache, which is not the authors’ or the publisher’s copy, so it was not used. It stays Unavailable until a copy is supplied. |
| LIT-1645 v2 | Logic: The Theory of Inquiry | Dewey (1938). Inquiry is “the controlled or directed transformation of an indeterminate situation into one that is so determinate in its constituent distinctions and relations as to convert the elements of the original situation into a unified whole”; recognizing that a situation is problematic and formulating the problem are themselves stages of inquiry, and hypotheses are operational proposals tested by the changes they make. | Unavailable — filed 2026-10-27, not read. A reading was attempted on 2026-10-27 and no lawful full text was reached: the book has no DOI to look up on Unpaywall, and the Internet Archive records found are controlled-lending copies or a Digital Library of India scan whose copyright status was not established, so none was used. It stays Unavailable until a copy is supplied. |
| LIT-1652 v2 | Counterexample-Guided Abstraction Refinement | Clarke et al. (2000), CAV 2000. Model checking runs on an existential abstraction that merges states, built from the atomic formulas of the program’s conditions and of the property, so a property true of the abstraction is true of the program. An abstract counterexample is checked against the concrete system by forward image computation. If it is spurious, the abstract state where it first has no concrete continuation is split, to separate the states reachable along it from those with the transition onward, and checking runs again. The coarsest split is stated to be NP-hard (proof omitted), so a polynomial non-optimal one is used. For finite-state programs and ACTL* properties whose counterexamples are paths or loops, the loop ends in a real counterexample or a proof. The property is never revised. | Active — read in full 2026-10-27 (NOTE-1231), from the authors’ manuscript of the CAV paper in CMU’s repository; worth reading as the founding paper of counterexample-guided abstraction refinement and as an exact case of a failure under a fixed specification read as a missing distinction, located and repaired by a split. The specification itself is never revised. Two of its four theorems have no proof in this text. |
| LIT-1661 v3 | Institutions: abstract model theory for specification and programming | Goguen & Burstall (1992). An institution is a category of signatures with sentences, models and satisfaction, subject to the Satisfaction Condition: a translated sentence holds in a model exactly when the original holds in the model’s reduct. From it, theories and model classes form a Galois connection; theories have colimits whenever signatures do, so specifications can be glued; constraints forcing free or initial interpretation can be added as sentences without losing this; and institution morphisms translate between logics, letting one logic’s prover be used on another’s theories when every model is reached. | Active — read in full 2026-10-29 (NOTE-1348) from a copy of the published article supplied by the owner; worth reading as the source of the Satisfaction Condition, the one axiom that makes truth invariant under change of notation, and of what follows from it for every logic at once: theories glue wherever signatures do (Theorem 11), constraints for abstract data types glue too, and a translation between logics that meets the condition and reaches every model lets one logic’s prover decide another’s entailments (Proposition 35). For this record it gives a precise standard of correct translation, relative to a translation of models, distinct from structural resemblance and from route agreement. Proofs are omitted for the Satisfaction Condition of its own examples; natural language is named as an application and not developed. Source of THEORY-1150 and THEORY-1142. |