diff --git a/CLAIMS.md b/CLAIMS.md index 42354c01..d180c1d3 100644 --- a/CLAIMS.md +++ b/CLAIMS.md @@ -43,7 +43,7 @@ is a CI failure (`.github/workflows/lane-shas.yml`). | ADR-0104 | `curriculum_loop_closure` | Curriculum-sourced proposals route through single reviewed teaching path | `evals/curriculum_loop_closure/results/v1_dev.json` | `cb94ca0042d78ec2624129ff6493d52e767b69feea32d2997b85d88f1c0883af` | | ADR-0131 | `math_teaching_corpus_v1` | Math teaching corpus replays deterministically; all chains pass exit criterion (correct_rate=1.0, wrong=0) | `evals/math_teaching_corpus/v1/report.json` | `eaf160d145da29f9050ede8d58bf111b0f651dd40aeae9201857d0b97e014dd4` | | ADR-0206 | `deductive_logic_v1` | Propositional entailment scored against an independent truth-table oracle; dev+holdout+external 716/716 correct, wrong=0, refused=0 | `evals/deductive_logic/report.json` | `97a230949016e38d5e3f37a69e4245b320575ee70e5af92ff7607f7b05f74b5f` | -| ADR-0256 | `deduction_serve_v1` | Flag-gated deduction serving decides real English/member/fused arguments end-to-end under earned SERVE licenses; wrong=0 across all splits | `evals/deduction_serve/report.json` | `f4fa7331bbee40c898be9ea2a8cabf36f28c8a19a7500433e0fa966c05905a8a` | +| ADR-0256 | `deduction_serve_v1` | Flag-gated deduction serving decides real English/member/fused/verb/existential arguments end-to-end under earned SERVE licenses; wrong=0 across all splits | `evals/deduction_serve/report.json` | `0b461a5a49c8f8260ca87d0c9c9f9a17232bd1fdedd982e34649eedf9cca30b5` | ## Verification diff --git a/chat/data/deduction_serve_ledger.json b/chat/data/deduction_serve_ledger.json index 017d644e..43a9e5a1 100644 --- a/chat/data/deduction_serve_ledger.json +++ b/chat/data/deduction_serve_ledger.json @@ -91,6 +91,34 @@ "t2_verified": 0, "wrong": 0 }, + "en_exist_chain": { + "correct": 720, + "refused": 0, + "t2_agrees_gold": 0, + "t2_verified": 0, + "wrong": 0 + }, + "en_exist_negative": { + "correct": 720, + "refused": 0, + "t2_agrees_gold": 0, + "t2_verified": 0, + "wrong": 0 + }, + "en_exist_universal": { + "correct": 720, + "refused": 0, + "t2_agrees_gold": 0, + "t2_verified": 0, + "wrong": 0 + }, + "en_exist_witness": { + "correct": 720, + "refused": 0, + "t2_agrees_gold": 0, + "t2_verified": 0, + "wrong": 0 + }, "en_member_atomic": { "correct": 720, "refused": 0, @@ -148,7 +176,7 @@ "wrong": 0 } }, - "content_sha256": "b5dd8db3ac4770f229269c16d388325a0763237ff84c21618309468eabf46a77", + "content_sha256": "a056f899a47bbd4536e3141f47a9131c9058ab55f2e9567fdcb254145e2dc252", "note": "Sealed-practice committed ledger for deduction serving (ADR-0256). Engine reads, never writes. Ceilings stay at safe defaults (theta_SERVE=0.99). A band earns SERVE by demonstrated pipeline reliability (reader+projector+engine) at volume >= 657 committed.", "provenance": "evals.deduction_serve.practice.runner.seal_ledger", "schema": "deduction_serve_ledger_v1" diff --git a/chat/deduction_surface.py b/chat/deduction_surface.py index 1e1e7304..3ee45b3f 100644 --- a/chat/deduction_surface.py +++ b/chat/deduction_surface.py @@ -41,6 +41,15 @@ Bands (docs/research/deduction-serve-arc-phase0-baseline-2026-07-23.md): atoms, decided by the same engine. Tried strictly AFTER v4-CM (the earlier bands refuse quantifier-led verb universals, is-a + verb mixes, and ``does not`` negation) — again a pure widening tier. +- Band v6-EX (ADR-0261) — existential arguments ("All wolves are mammals. Some + wolves are tame. Therefore some mammals are tame."), read by + ``generate.proof_chain.exist``: v5-VP's lowering over a domain widened with + one Skolem witness per existential premise and one ARBITRARY element per + existential conclusion (what keeps the domain open, so an existential is + refuted only by a genuine universal). Tried LAST, strictly after v5-VP — the + earlier fallback bands refuse every ``some``-led sentence, and the + categorical band v1b, which reads some-syllogisms in its own synthetic + regime, is tried well before this one and keeps them. A pure widening tier. Fail-closed (INV-34): once ``looks_like_deductive_argument`` fires, every path below returns a committed, honest surface — reader refusal, out-of-band shape, @@ -61,10 +70,12 @@ from generate.proof_chain.categorical import CategoricalError, decide_syllogism from generate.proof_chain.cond_member import CondMemberArgument, read_cond_member_argument from generate.proof_chain.english import EnglishArgument, read_english_argument from generate.proof_chain.entail import evaluate_entailment_with_trace +from generate.proof_chain.exist import ExistArgument, read_exist_argument from generate.proof_chain.member import MemberArgument, read_member_argument from generate.proof_chain.render import ( render_entailment, render_entailment_english, + render_entailment_exist, render_entailment_member, render_entailment_verb, render_syllogism, @@ -155,6 +166,9 @@ def deduction_grounded_surface( verb = _verb_band_surface(text, license_lookup) if verb is not None: return verb + exist = _exist_band_surface(text, license_lookup) + if exist is not None: + return exist return _READER_REFUSAL_SURFACE.format(reason=comp.reason) # Band v1 — propositional argument. projected = to_deductive_logic(comp) @@ -191,6 +205,10 @@ def deduction_grounded_surface( verb = _verb_band_surface(text, license_lookup) if verb is not None: return verb + # Band v6-EX fallback — the existential shapes every earlier band guards out. + exist = _exist_band_surface(text, license_lookup) + if exist is not None: + return exist return _OUT_OF_BAND_SURFACE @@ -251,6 +269,21 @@ def _verb_band_surface(text: str, license_lookup: _LicenseLookup) -> str | None: return _license_gate(surface, arg.band, license_lookup) +def _exist_band_surface(text: str, license_lookup: _LicenseLookup) -> str | None: + """Band v6-EX (ADR-0261): read *text* as an existential argument (witness + and arbitrary-element domain widening over v5-VP's two atom families), and + decide with the same verified ROBDD engine; ``None`` when the reader + refuses (the caller keeps its pre-existing honest surface — this band only + ever widens what is decided). Rendered by ``render_entailment_exist``, + whose UNKNOWN scoping discloses the no-existential-import reading.""" + arg = read_exist_argument(text) + if not isinstance(arg, ExistArgument): + return None + trace = evaluate_entailment_with_trace(arg.premise_formulas, arg.query_formula) + surface = render_entailment_exist(trace, arg.premise_texts, arg.query_text) + return _license_gate(surface, arg.band, license_lookup) + + def _license_gate(surface: str, band: str, license_lookup: _LicenseLookup) -> str: """Serve *surface* authoritatively iff *band* holds a SERVE license; else serve the same sound answer DISCLOSED (hedged). The one place the earned- diff --git a/core/cli_test.py b/core/cli_test.py index 0f94f2bf..e66a95ab 100644 --- a/core/cli_test.py +++ b/core/cli_test.py @@ -181,6 +181,7 @@ TEST_SUITES: dict[str, tuple[str, ...]] = { "tests/test_member_argument_reader.py", "tests/test_cond_member_argument_reader.py", "tests/test_verb_argument_reader.py", + "tests/test_exist_argument_reader.py", "tests/test_deduction_serve_e2e.py", ), "full": ("tests/",), diff --git a/docs/adr/ADR-0261-existential-witness-band.md b/docs/adr/ADR-0261-existential-witness-band.md new file mode 100644 index 00000000..b7352aac --- /dev/null +++ b/docs/adr/ADR-0261-existential-witness-band.md @@ -0,0 +1,195 @@ +# ADR-0261 — Band v6-EX: existential arguments, decided + +- **Status:** Proposed +- **Date:** 2026-07-24 +- **Arc:** deduction-serve (ADR-0256 → 0257 → 0258 → 0259 → 0260 → this) +- **Governs:** `generate/proof_chain/exist.py`, the `en_exist_*` shape-bands, + their arena templates, the `v2_exist` lane split, the `_exist_band_surface` + serving tier, and the refuse-don't-drop contract of + `generate.meaning_graph.projectors.to_syllogism`. + +## 1. Context + +The band cascade reads `all` and `no`; `some` refuses +(`quantifier_out_of_band`) in every fallback tier — ADR-0258 §6 listed +existentials as a deliberate scope-out, and the generalization arc +(docs/plans/generalization-arc-2026-07-24.md Phase 1.2) schedules them as the +move that completes the square of opposition. + +Band v1b already decides categorical some-syllogisms — but only inside the +shared reader's morphology lexicon, and only for arguments that are purely +categorical. Real subject matter is neither: it mixes singular facts, verb +predicates, and vocabulary the lexicon has never seen. Everything outside that +narrow window refused. + +Existentials are also the first construct in this arc whose lowering is not a +straightforward instantiation. A universal instantiates at things the argument +already names; an existential asserts a thing the argument does NOT name, and +an existential conclusion asks about things that may not be named at all. Get +that wrong in the obvious way — lower `some` over just the named individuals — +and the reader will report REFUTED for arguments that are merely unproven, +which is precisely the wrong-answer class this arc exists to prevent. + +## 2. Decision + +Add `generate.proof_chain.exist.read_exist_argument` as the LAST fallback tier +(after v1 / v1b / v2-EN / v3-MEM / v4-CM / v5-VP), extending v5-VP's +per-individual lowering — both atom families unchanged — with two new kinds of +domain element: + +- **A witness per existential PREMISE** (a Skolem constant nothing else + names): "some C1 are C2" ⇒ `mem(w,C1) & mem(w,C2)`; the O-form negates the + second conjunct; the verb forms mint a verb atom instead. +- **One arbitrary element per existential CONCLUSION**: a domain element about + which no premise asserts anything and at which every universal is still + instantiated. + +An existential conclusion lowers to the disjunction of its conjunction over +the WHOLE domain — named individuals, witnesses, and the arbitrary element. + +New sentence shapes, all `some`-led: +`some are|is [not] [a|an] ` (I-form and O-form) and +`some [do not] []`. Every other shape delegates verbatim to +v3-MEM's and v5-VP's parsers, refusals included. + +Bands (priority order): `en_exist_negative` (any negative universal) > +`en_exist_chain` (≥2 universals) > `en_exist_universal` (exactly 1) > +`en_exist_witness` (no universals). Rendered by `render_entailment_exist` — +the verb surface with the no-existential-import reading disclosed in the +UNKNOWN template. Rides `deduction_serving_enabled` (default off); no new flag. + +**Second decision, forced by the first (§5.1):** `to_syllogism` now REFUSES +when the comprehension carries a relation it cannot express, instead of +filtering that relation out and projecting the remainder. + +## 3. Why this is sound + +1. **ENTAILED.** Let *M* be any first-order model of the premises. Each + witness is interpretable in *M* (its existential premise asserts a + satisfier); universal instantiation is truth-preserving at every element; + the arbitrary element may be interpreted as ANY element, domains being + non-empty. So every lowered premise holds in *M*. If the lowered premises + propositionally entail the query disjunction, some element of *M* + satisfies the conjunction — which is ∃. Skolem constants occur nowhere in + the original argument, so this is entailment-preserving Skolemization, not + merely satisfiability-preserving. +2. **REFUTED — the arbitrary element is load-bearing.** Refuting ∃x φ(x) + means deriving ∀x ¬φ(x). The lowered conjunction dual is entailed only if + it is entailed at the arbitrary element, and that element is arbitrary (no + premise mentions it), so what holds of it holds of every element — the + universal is genuinely derived, never assumed by domain closure. Without + it, "Rex is a wolf. Rex is not tame. Therefore some wolves are tame." + would come back REFUTED — asserting that no wolf anywhere is tame — from a + domain of one. With it, the honest UNKNOWN. This is the single most + important line of this ADR and it is pinned by a named test. +3. **Completeness within the fragment** lifts exactly as v3-MEM/v5-VP: a + propositional countermodel becomes a first-order countermodel whose domain + is the named individuals, the witnesses, and the arbitrary element. +4. **No existential import.** Universals are read as vacuously true over an + empty class, so the subaltern moods (Darapti, Felapton, Bamalip) are + UNKNOWN, and the two contradictory pairs of the square are decided: an + A-form REFUTES the corresponding O-form, an E-form REFUTES the I-form. + This matches the modern first-order reading, matches what the categorical + band (v1b) already does, and is the conservative choice — it declines to + claim a member exists that no premise asserted. It is disclosed to the user + in the UNKNOWN surface rather than left as a silent convention. +5. **The plural `do not` is read here and refused in v5-VP** — deliberately, + not inconsistently. "All C do not V" is genuinely scope-ambiguous (¬∀ vs + ∀¬) and refuses; "some C do not V" is unambiguously ∃x(C(x) ∧ ¬V(x)). +6. **Cascade honesty** — every arena template and lane case was verified to + fall through all six earlier bands, so this tier is pure widening: every + previously-served argument is served byte-identically. The one previously + DECLINED case it now decides (`ds-mem-0020`) is promoted to its correct + verdict, not a favorable one. + +## 4. License and render + +The four `en_exist_*` bands earned SERVE through the ADR-0199 arena +(720/band committed, wrong=0, θ_SERVE=0.99; ledger resealed at 25 bands). +The by-construction gold is cross-checked template-by-template against the +independent truth-table oracle over each template's INTENDED lowering — every +universal's per-element implications and every query disjunct spelled out — so +a lowering that drops or invents a domain element shows up as a disagreement +rather than passing silently (INV-25). Unearned or ledger-stripped deployments +serve the same sound answer hedged (`_UNVERIFIED_SHAPE_DISCLOSURE`). + +## 5. Findings and scope-outs + +### 5.1 A wrong-answer path found in Band v1b (fixed here) + +Authoring this band's lane surfaced a defect in `to_syllogism` that predates +it. The projector built its premise list by FILTERING the meaning graph's +relations down to the categorical ones — silently discarding anything else, +then answering from what survived. Two consequences, both wrong served +answers rather than declines: + +- "Aristotle is a philosopher. All philosophers are scholars. Therefore some + scholars are philosophers." — the singular `member` premise was dropped, the + argument lost its only witness, and serving replied *"That doesn't follow."* + It does follow. +- "Every mineral is a solid. Some quartzes are minerals. Therefore some + quartzes are solids." — the shared reader misreads "every mineral" as an + individual named `every_mineral` (a separate reader gap, §5.2), the + resulting `member` relation was dropped, and a valid Darii was served as + *"That doesn't follow."* + +The arena never caught it because the CATEGORICAL band's templates are all +purely categorical two-premise syllogisms in the synthetic lexicon — a family +in which nothing is ever dropped. A band can hold an earned license and still +have an unmeasured wrong-answer path if its practice corpus does not span its +reachable inputs; that lesson is the durable part of this finding. + +The fix makes `to_syllogism` behave exactly like its propositional sibling +`to_deductive_logic`, which has always refused on a relation it cannot express: +**refuse, don't drop.** Refused texts fall through to the reader bands that CAN +hold a singular fact — v6-EX decides both examples correctly. The categorical +band re-earned SERVE at 720/720 after the change (no coverage lost), and both +examples are now pinned as regression cases (`ds-ex-0008`, `ds-ex-0011`, plus +a projector unit test and an e2e test). + +### 5.2 Scope-outs (typed refusals today) + +1. **"Every C is a D" misread by the shared reader** — `comprehend` reads the + quantifier phrase as an individual (`every_mineral`). Post-§5.1 this is + harmless (v1b refuses; v6-EX reads the sentence correctly through v3-MEM's + universal parser), so it is recorded, not patched: fixing the shared + reader's template set is its own unit of work with its own lane. +2. **Partitives** — "some of the sailors" refuses `partitive_out_of_band` + rather than reading "of the sailors" as an opaque class run. +3. **Multi-token subjects in verb existentials, PPs, ditransitives** — + `sentence_shape_out_of_band`, inherited from v5-VP's closed grammar. +4. **Tense** — `some C were P` / `some C did not V` refuse + `tense_out_of_band`. +5. **Connective × existential composition** — "If some C are P then …" + refuses `mixed_structure_out_of_band`; fusing v4-CM's connective grammar + over existential leaves is a later composition. +6. **Numeric and proportional quantifiers** (`most`, `few`, `several`, `at + least two`) — `quantifier_out_of_band`. `some` is the only existential + spelling read; "there is a C that …" is not read either. +7. **Universal conclusions** — unchanged from v3-MEM: proving ∀ from these + premises needs the eigenvariable machinery this band uses only for the + refutation direction, and exposing it as a conclusion form is a separate, + testable unit. +8. **Identity / co-reference, existential-import premises** — unchanged + scope-outs; a user who wants the traditional square can state the + existential premise explicitly and this band will use it. + +## 6. Verification + +- `tests/test_exist_argument_reader.py` — 33 tests: gap-is-real cross-check, + flagship Darii lowering (exact formulas and atoms), the arbitrary-element + soundness test, no-existential-import, both contradictory pairs, witness + non-transfer, one-witness-per-premise, verb existentials with plural + `do not`, number linking inside existentials, 4 band classifications, 13 + typed refusals incl. delegated v3-MEM/v5-VP reasons, honesty caps, + determinism. +- `tests/test_meaning_graph_projectors.py` (+1) — the §5.1 refuse-don't-drop + contract. +- Surface/e2e/lane: `tests/test_deduction_surface.py` (+5), + `tests/test_deduction_serve_e2e.py` (+2, one of them the §5.1 regression), + `tests/test_deduction_serve_lane.py` (+1 over the 32-case `v2_exist` split; + `v2_member` docstring updated for the `ds-mem-0020` promotion) — full lane + 166/166, wrong=0, all six splits. +- Arena: 4 × 720 committed, wrong=0, first seal run; all 25 bands still SERVE; + corpus soundness asserted against the independent oracle before sealing + (18,000 cases). diff --git a/docs/research/existential-witness-band-2026-07-24.md b/docs/research/existential-witness-band-2026-07-24.md new file mode 100644 index 00000000..7bd1cb5e --- /dev/null +++ b/docs/research/existential-witness-band-2026-07-24.md @@ -0,0 +1,139 @@ +# Band v6-EX — existential witnesses, and a wrong-answer path found on the way + +**Date:** 2026-07-24 · **ADR:** ADR-0261 · **Arc:** deduction-serve / +generalization Phase 1.2 (Tier O) + +## What shipped + +`some` is decided. The band cascade now reads the whole square of opposition: +"All mammals are vertebrates. Some whales are mammals. Therefore some whales +are vertebrates." comes back **entailed**, and "All unicorns are horned. +Therefore some unicorns are horned." comes back **unsettled** — with the +reason disclosed, not silently assumed. + +Four new bands (`en_exist_negative` / `_chain` / `_universal` / `_witness`) +earned SERVE at 720 × wrong=0 on the first arena seal (25-band ledger). The +hand-authored `v2_exist` split passed 32/32 on its first full run; the whole +deduction-serve lane is 166/166 wrong=0 across six splits. + +## The mechanism, and the one place it could have been unsound + +An existential premise is easy: mint a witness nobody else names and assert +the conjunction about it. An existential *conclusion* is where the design +decision lives, because asking "is ∃x(P(x) ∧ Q(x)) refuted?" means asking +whether ∀x ¬(P(x) ∧ Q(x)) is *derivable* — and a propositional lowering over +the individuals the argument happens to mention cannot tell "derivable" from +"true of everything I bothered to name". + +Concretely, the obvious lowering gets this wrong: + +> Rex is a wolf. Rex is not tame. Therefore some wolves are tame. + +Lower `some wolves are tame` as a disjunction over the named individuals and +the only disjunct is Rex, who is not tame — so the disjunction is refuted, and +the system announces that *no wolf anywhere is tame*. From one wolf. That is a +wrong answer of exactly the kind this arc exists to prevent, and it would have +been invisible: sound-looking machinery, confidently wrong. + +The fix is an old one — an eigenvariable. Every existential conclusion mints +one **arbitrary element**: a domain member no premise mentions, at which every +universal is still instantiated. Because it is arbitrary, anything the +premises force about it they force about everything, so the refutation +direction derives a genuine universal instead of assuming domain closure. And +because domains are non-empty, including it in the entailment direction stays +sound too. One extra domain element buys both directions. + +With it, the Rex argument is **unknown**, which is the truth. The test that +pins this is named `test_arbitrary_element_keeps_the_domain_open`. + +## No existential import — a reading choice, disclosed + +"All C are P. Therefore some C are P." is UNKNOWN here. A universal is +vacuously true over an empty class, so it cannot by itself produce a member. +That is the modern first-order reading; the traditional square (Darapti, +Felapton, Bamalip) assumes otherwise. Both readings are defensible — but only +one of them declines to claim something exists that no premise asserted, and +that is the one this engine takes. The UNKNOWN surface says so in words +("reading … 'some' as claiming a member exists (so 'all' does not)"), because +a user who expects the traditional square would otherwise read the answer as a +bug. A user who wants the classical inference can state the existential +premise; the band will use it. + +## The finding: a licensed band with an unmeasured wrong-answer path + +Authoring the lane turned up something that was not part of the assignment. +Two arguments came back **"That doesn't follow"** when they plainly do: + +> Aristotle is a philosopher. All philosophers are scholars. Therefore some +> scholars are philosophers. + +> Every mineral is a solid. Some quartzes are minerals. Therefore some +> quartzes are solids. + +Both were being answered by Band v1b, the categorical band, which holds an +earned SERVE license. Its projector (`to_syllogism`) built its premise list by +*filtering* the meaning graph down to the categorical relations — quietly +dropping anything else and answering from the remainder. In the first +argument the dropped relation was the singular fact `member(aristotle, +philosopher)`: the argument's only witness. In the second it was a `member` +relation produced by a separate reader gap (the shared reader parses "every +mineral" as an individual named `every_mineral`). Either way, the band decided +a strictly weaker argument than the user wrote, and served the answer as if it +had decided theirs. + +Three things are worth keeping from this: + +1. **Refuse, don't drop.** The propositional sibling `to_deductive_logic` has + always returned `None` the moment it meets a relation it cannot express. + `to_syllogism` now does the same. That is the whole fix — six lines — and + the two arguments above now fall through to v6-EX, which decides both + correctly. +2. **An earned license covers the corpus, not the input space.** The + CATEGORICAL band passed 720/720 because every one of its templates is a + purely categorical two-premise syllogism in the synthetic lexicon — a + family in which nothing is ever dropped. The band's license was honest + about what it measured and silent about what it didn't. When a band's + practice corpus is narrower than its reachable inputs, the gap is exactly + where a wrong answer lives. +3. **The cheapest way to find it was to build the next band.** Nothing in the + existing suite exercised these shapes; they surfaced because authoring + `v2_exist` meant asking, case by case, "which band actually answers this, + and is that answer right?" The band-boundary audit is not bureaucracy — it + is the test. + +The categorical band re-earned SERVE at 720/720 after the change, so no +coverage was lost. Both arguments are pinned as regression cases +(`ds-ex-0008`, `ds-ex-0011`), plus a projector unit test and an e2e test. + +## Wrinkles worth surfacing + +- **The shared reader still misreads "every mineral" as an individual.** Post + fix this is harmless (v1b refuses, v6-EX reads the sentence correctly), so + it is recorded rather than patched — repairing `comprehend`'s template set + is its own unit with its own lane. But it is a live example of the same + class of defect: a reader that produces *something* for input it does not + actually understand. +- **v1b still owns categorical some-syllogisms in its lexicon.** Where every + term is known and the argument is purely categorical, v1b answers first, in + `valid`/`invalid` vocabulary. That is correct precedence, but it means the + `v2_exist` corpus had to be authored deliberately off that path (three + practice templates were rewritten for the same reason). Documented in + `contract.md`; the two vocabularies coexisting for structurally similar + arguments is a seam a future arc may want to close. +- **The atom cap now binds on the query.** An existential conclusion mints up + to two atoms per domain element, so a wide argument can hit `MAX_ATOMS` + where an equivalent v5-VP argument would not. It refuses rather than + truncating — a dropped disjunct is precisely how a false REFUTED would + reappear. +- **Only `some`.** `most`, `few`, `several`, "at least two", and "there is a + C that…" all refuse. Proportional quantifiers are not a lowering problem, + they are a counting problem, and this substrate does not count. + +## Where this leaves Phase 2 + +The reading generalization the plan called for is done: subject matter states +its rules as verb sentences (v5-VP) about classes quantified with all / no / +some (v3-MEM, v6-EX), and the cascade now reads all of it under one earned +license discipline. Physics and biology serve lanes are next, and they need no +further reading work before the curriculum-entailment contract can be built on +top. diff --git a/evals/curriculum_loop_closure/results/v1_dev.json b/evals/curriculum_loop_closure/results/v1_dev.json index 148e3f6d..6444a30a 100644 --- a/evals/curriculum_loop_closure/results/v1_dev.json +++ b/evals/curriculum_loop_closure/results/v1_dev.json @@ -3,7 +3,7 @@ "cases": [ { "case": "positive_basic", - "proposal_id": "23d88e439bdb9394", + "proposal_id": "61a80836bd55e1e0", "source": "curriculum:epistemology_v1", "status": "pass" }, @@ -16,7 +16,7 @@ "rejections": [ { "checker_id": "curriculum_eval_checker_v1", - "finding_id": "53a976ad596075fb", + "finding_id": "53a976ad596075fb67655dc7b83db158ef068a7f4ad8315b54795cc8c2476720", "non_target_turns_changed": [ 1, 3 @@ -34,14 +34,14 @@ "case": "determinism", "equal": true, "first_ids": [ - "23d88e439bdb9394", - "f4b7d702a799268e", - "61a1038fd4cc6cfe" + "61a80836bd55e1e0", + "293dd9d42c8fa1ac", + "0cd932d9ccad4883" ], "second_ids": [ - "23d88e439bdb9394", - "f4b7d702a799268e", - "61a1038fd4cc6cfe" + "61a80836bd55e1e0", + "293dd9d42c8fa1ac", + "0cd932d9ccad4883" ], "status": "pass" } @@ -49,5 +49,5 @@ "failed": 0, "lane": "curriculum_loop_closure", "passed": 5, - "sha256": "cbac54a3722cf3b941c3c5223335171265a942efb53d03bc08128d2d0f3ce298" + "sha256": "533c4e2317c3e22b5f33d59817a954753ad201e2354b826171822a8ea183c706" } diff --git a/evals/deduction_serve/contract.md b/evals/deduction_serve/contract.md index 90fd07d0..a0e4d6ea 100644 --- a/evals/deduction_serve/contract.md +++ b/evals/deduction_serve/contract.md @@ -9,7 +9,8 @@ The **production serving decider** — the exact pipeline → `to_syllogism` + the categorical decider (Band v1b, ADR-0256) → `read_english_argument` (Band v2-EN, ADR-0257) → `read_member_argument` (Band v3-MEM, ADR-0258) → `read_cond_member_argument` (Band v4-CM, -ADR-0259) → `read_verb_argument` (Band v5-VP, ADR-0260) — with +ADR-0259) → `read_verb_argument` (Band v5-VP, ADR-0260) → +`read_exist_argument` (Band v6-EX, ADR-0261) — with `evaluate_entailment_with_trace` (the ROBDD engine, ADR-0201/ADR-0218) deciding every band. `evals/deduction_serve/runner.py::decide` calls these functions directly @@ -34,6 +35,11 @@ against wording-only changes. universals discharged by membership facts across every closed agreement rule (+s, +es, y↔ies, irregular go/goes), transitive objects at face value, and eight typed decline shapes. +- `v2_exist/` — hand-authored existential arguments (ADR-0261): the square + of opposition (Darii, Ferio, both contradictory pairs, the + no-existential-import subaltern), witnesses that never transfer to a + named individual, the arbitrary element that keeps an existential + conclusion's domain open, and eleven typed decline shapes. This is **distinct** from two existing lanes that sound similar: @@ -102,15 +108,34 @@ decides for that exact text. in the shared tokenizer's expansion table, so v5's `n't` guard refuses identically) or structure v5 also guards out; the full lane's prior splits stayed byte-stable. +- **Existential quantifiers** — refused by every band until Band v6-EX + (ADR-0261) decided them (`v2_exist/`). ONE case promoted: `ds-mem-0020` + (`"Some men are wise. Socrates is a man. Therefore Socrates is wise."`), + declined (`quantifier_out_of_band`) since ADR-0258, is now read — and its + honest verdict is **UNKNOWN**, since an anonymous witness never transfers + to a named individual. Promoted declined → unknown, renamed + `exist_witness_does_not_transfer`. The other splits stayed byte-stable. +- **Band boundary with v1b** — a purely categorical some-syllogism whose + every term is in the shared reader's morphology lexicon is decided by the + CATEGORICAL band, which is tried first and answers in its own + `valid`/`invalid` vocabulary; v6-EX's territory is everything else + (unknown vocabulary, singular facts, verb predicates, >3 terms). The + `v2_exist/` corpus is authored on that fall-through path deliberately, so + the split measures the band it names. Related: `to_syllogism` now REFUSES + rather than dropping a premise it cannot express (ADR-0261 §5.1) — before + that fix it answered a strictly weaker argument than the user wrote, which + is how a wrong served verdict got past a licensed band. - **Still-open declines** (honest, typed): verb-phrase contraction negation (`ds-en-0023/0024`), ambiguous `and`/`or` scope (`ds-en-0025`), - nested conditionals (`ds-en-0026`), existential quantifiers / bare - plurals / definite descriptions / relative clauses / tense - (`ds-mem-0020…0023/0025/0026`), a universal clause nested inside a - connective, compound conclusions (`ds-cm-0020…0026`), and the verb - band's own scope-outs — `did not` tense, multi-token subjects, - prepositional/ditransitive shapes, connective×verb composition - (`ds-vb-0021…0028`). + nested conditionals (`ds-en-0026`), bare plurals / definite descriptions / + relative clauses / tense (`ds-mem-0021…0023/0025/0026`), a universal + clause nested inside a connective, compound conclusions + (`ds-cm-0020…0026`), the verb band's own scope-outs — `did not` tense, + multi-token subjects, prepositional/ditransitive shapes, connective×verb + composition (`ds-vb-0021…0028`) — and the existential band's: + partitives, singular agreement under a plural subject, + connective×existential composition, proportional quantifiers, universal + conclusions (`ds-ex-0022…0032`). ## Reproduce diff --git a/evals/deduction_serve/practice/gold.py b/evals/deduction_serve/practice/gold.py index 89869035..381234f6 100644 --- a/evals/deduction_serve/practice/gold.py +++ b/evals/deduction_serve/practice/gold.py @@ -36,6 +36,7 @@ from generate.proof_chain.categorical import CategoricalError, decide_syllogism from generate.proof_chain.cond_member import CondMemberArgument, read_cond_member_argument from generate.proof_chain.english import EnglishArgument, read_english_argument from generate.proof_chain.entail import Entailment, evaluate_entailment_with_trace +from generate.proof_chain.exist import ExistArgument, read_exist_argument from generate.proof_chain.member import MemberArgument, read_member_argument from generate.proof_chain.verb import VerbArgument, read_verb_argument from generate.proof_chain.shape import ( @@ -52,6 +53,10 @@ from generate.proof_chain.shape import ( EN_CONDMEM_DISJUNCTIVE, EN_CONDMEM_FUSED, EN_DISJUNCTIVE, + EN_EXIST_CHAIN, + EN_EXIST_NEGATIVE, + EN_EXIST_UNIVERSAL, + EN_EXIST_WITNESS, EN_MEMBER_ATOMIC, EN_MEMBER_CHAIN, EN_MEMBER_NEGATIVE, @@ -653,14 +658,183 @@ _VERB_TEMPLATES: dict[str, tuple[tuple[str, Any, tuple[str, ...], str], ...]] = } +# --- Band v6-EX (ADR-0261): existential synthetic corpus ---------------------- +# +# Reuses the v3-MEM name/class/state pools and the v5-VP verb pool, and adds +# nothing new to the lexicon: this band's novelty is the LOWERING (a Skolem +# witness per existential premise, one arbitrary element per existential +# conclusion), not the vocabulary. The templates deliberately include both +# subaltern moods ("all C are P, therefore some C are P" ⇒ UNKNOWN, no +# existential import) and both contradictory pairs (A refutes O, E refutes I), +# so the earned license certifies the square of opposition as this band reads +# it. Content is synthetic ON PURPOSE (same posture as every earlier corpus); +# hand-authored real-English cases live in ``evals/deduction_serve/v2_exist``. + + +def _exist_case( + index: int, +) -> tuple[str, tuple[str, str], tuple[str, str], tuple[str, str], tuple[str, str], str]: + """Deterministic (name, class1, class2, class3, verb, state) for case + ``index`` — the three classes are pairwise distinct.""" + n1 = _MEM_NAMES[(index * 3) % len(_MEM_NAMES)] + base = (index * 5) % (len(_MEM_CLASSES) - 2) + c1, c2, c3 = _MEM_CLASSES[base], _MEM_CLASSES[base + 1], _MEM_CLASSES[base + 2] + v1 = _VERB_FORMS[(index * 7) % len(_VERB_FORMS)] + st = _MEM_STATES[(index * 11) % len(_MEM_STATES)] + return n1, c1, c2, c3, v1, st + + +#: Existential-band templates: (gold, text_builder, intended_premises, +#: intended_query). Builders take ``(n1, c1, c2, c3, v1, st)`` from +#: ``_exist_case``; the INTENDED formulas are the template's lowering over +#: fixed placeholder atoms — ``m*`` at the named individual, ``w*``/``x*`` at +#: the first/second witness, ``k*`` at the arbitrary element — cross-checked +#: against the truth-table oracle with no reader in the loop (INV-25). A +#: universal contributes ONE implication per domain element, and an +#: existential conclusion one disjunct per domain element; the intended forms +#: mirror that exactly, so a lowering that drops (or invents) a domain element +#: shows up as a disagreement rather than passing silently. +_EXIST_TEMPLATES: dict[str, tuple[tuple[str, Any, tuple[str, ...], str], ...]] = { + EN_EXIST_WITNESS: ( + # I-form conversion — "some C are S" ⇒ "some S are C". A state word + # (never in the shared reader's morphology) stands in for the second + # term here and in the two other otherwise-all-class templates below: + # a text whose every term IS in that lexicon is read by the CATEGORICAL + # band (v1b) long before this one, and the arena must exercise the + # fall-through path serving actually takes, not a shape v1b keeps. + ("entailed", + lambda n1, c1, c2, c3, v1, st: f"Some {c1[1]} are {st}. Therefore some {st} are {c1[1]}.", + ("wa and wb",), "(wb and wa) or (kb and ka)"), + # A named individual IS a witness. + ("entailed", + lambda n1, c1, c2, c3, v1, st: f"{n1} is a {c1[0]}. {n1} is {st}. Therefore some {c1[1]} are {st}.", + ("ma", "mb"), "(ma and mb) or (ka and kb)"), + # O-form restatement. + ("entailed", + lambda n1, c1, c2, c3, v1, st: f"Some {c1[1]} are not {st}. Therefore some {c1[1]} are not {st}.", + ("wa and (not wb)",), "(wa and (not wb)) or (ka and (not kb))"), + # The witness is anonymous — a stated singular fact still contradicts. + ("refuted", + lambda n1, c1, c2, c3, v1, st: f"Some {c1[1]} are {st}. {n1} is not {st}. Therefore {n1} is {st}.", + ("wa and wb", "not mb"), "mb"), + # The witness never transfers to a named individual (the anti-leak case). + ("unknown", + lambda n1, c1, c2, c3, v1, st: f"Some {c1[1]} are {st}. {n1} is a {c1[0]}. Therefore {n1} is {st}.", + ("wa and wb", "ma"), "mb"), + # Two existentials do not compose — distinct witnesses stay distinct. + ("unknown", + lambda n1, c1, c2, c3, v1, st: f"Some {c1[1]} are {c2[1]}. Some {c1[1]} are {c3[1]}. Therefore some {c2[1]} are {c3[1]}.", + ("wa and wb", "xa and xc"), "(wb and wc) or (xb and xc) or (kb and kc)"), + ), + EN_EXIST_UNIVERSAL: ( + # Darii — the universal fires at the witness. + ("entailed", + lambda n1, c1, c2, c3, v1, st: f"All {c1[1]} are {st}. Some {c2[1]} are {c1[1]}. Therefore some {c2[1]} are {st}.", + ("wa implies wb", "ka implies kb", "wc and wa"), "(wc and wb) or (kc and kb)"), + # "every" spelling, singular class forms — number linking at the witness. + ("entailed", + lambda n1, c1, c2, c3, v1, st: f"Every {c1[0]} is a {c2[0]}. Some {c1[1]} are {st}. Therefore some {c2[1]} are {st}.", + ("wa implies wb", "ka implies kb", "wa and wc"), "(wb and wc) or (kb and kc)"), + # The named individual supplies the existential witness. + ("entailed", + lambda n1, c1, c2, c3, v1, st: f"{n1} is a {c1[0]}. All {c1[1]} are {st}. Therefore some {c1[1]} are {st}.", + ("ma", "ma implies mb", "ka implies kb"), "(ma and mb) or (ka and kb)"), + # Verb universal discharged at the witness. + ("entailed", + lambda n1, c1, c2, c3, v1, st: f"All {c1[1]} {v1[0]}. Some {c2[1]} are {c1[1]}. Therefore some {c2[1]} {v1[0]}.", + ("wa implies wv", "ka implies kv", "wc and wa"), "(wc and wv) or (kc and kv)"), + # NO existential import — the subaltern does not follow. + ("unknown", + lambda n1, c1, c2, c3, v1, st: f"All {c1[1]} are {st}. Therefore some {c1[1]} are {st}.", + ("ka implies kb",), "ka and kb"), + # Undistributed middle with an existential premise. + ("unknown", + lambda n1, c1, c2, c3, v1, st: f"All {c2[1]} are {c1[1]}. Some {c3[1]} are {c1[1]}. Therefore some {c3[1]} are {c2[1]}.", + ("wa implies wb", "ka implies kb", "wc and wb"), "(wc and wa) or (kc and ka)"), + # A-form and O-form are contradictories — the A refutes the O. + ("refuted", + lambda n1, c1, c2, c3, v1, st: f"All {c1[1]} are {st}. Therefore some {c1[1]} are not {st}.", + ("ka implies kb",), "ka and (not kb)"), + # Universal instantiated at the named individual contradicts the query. + ("refuted", + lambda n1, c1, c2, c3, v1, st: f"{n1} is a {c1[0]}. All {c1[1]} are {st}. Some {c2[1]} are {c1[1]}. Therefore {n1} is not {st}.", + ("ma", "ma implies mb", "wa implies wb", "wc and wa"), "not mb"), + ), + EN_EXIST_CHAIN: ( + # Two-hop chain carrying the witness to the conclusion. + ("entailed", + lambda n1, c1, c2, c3, v1, st: f"Some {c1[1]} are {c2[1]}. All {c2[1]} are {c3[1]}. All {c3[1]} are {st}. Therefore some {c1[1]} are {st}.", + ("wa and wb", "wb implies wc", "kb implies kc", "wc implies wd", "kc implies kd"), + "(wa and wd) or (ka and kd)"), + # Chain from a named individual to an existential conclusion. + ("entailed", + lambda n1, c1, c2, c3, v1, st: f"{n1} is a {c1[0]}. All {c1[1]} are {c2[1]}. All {c2[1]} are {st}. Therefore some {c2[1]} are {st}.", + ("ma", "ma implies mb", "ka implies kb", "mb implies mc", "kb implies kc"), + "(mb and mc) or (kb and kc)"), + # Membership chain into a verb universal. + ("entailed", + lambda n1, c1, c2, c3, v1, st: f"Some {c1[1]} are {c2[1]}. All {c2[1]} are {c3[1]}. All {c3[1]} {v1[0]}. Therefore some {c1[1]} {v1[0]}.", + ("wa and wb", "wb implies wc", "kb implies kc", "wc implies wv", "kc implies kv"), + "(wa and wv) or (ka and kv)"), + # Broken chain — the subsumption points the wrong way. + ("unknown", + lambda n1, c1, c2, c3, v1, st: f"Some {c1[1]} are {c2[1]}. All {c3[1]} are {c2[1]}. All {c3[1]} are {st}. Therefore some {c1[1]} are {st}.", + ("wa and wb", "wc implies wb", "kc implies kb", "wc implies wd", "kc implies kd"), + "(wa and wd) or (ka and kd)"), + # Reverse traversal — chains do not run backwards. + ("unknown", + lambda n1, c1, c2, c3, v1, st: f"Some {c1[1]} are {st}. All {c2[1]} are {c1[1]}. All {c3[1]} are {c2[1]}. Therefore some {c3[1]} are {st}.", + ("wa and wb", "wc implies wa", "kc implies ka", "wd implies wc", "kd implies kc"), + "(wd and wb) or (kd and kb)"), + # Chain into a contradicted singular conclusion. + ("refuted", + lambda n1, c1, c2, c3, v1, st: f"{n1} is a {c1[0]}. All {c1[1]} are {c2[1]}. All {c2[1]} are {st}. Some {c3[1]} are {c1[1]}. Therefore {n1} is not {st}.", + ("ma", "ma implies mb", "wa implies wb", "mb implies mc", "wb implies wc", "wd and wa"), + "not mc"), + ), + EN_EXIST_NEGATIVE: ( + # Ferio — E-form plus I-form yields the O-form. + ("entailed", + lambda n1, c1, c2, c3, v1, st: f"No {c1[1]} are {st}. Some {c2[1]} are {c1[1]}. Therefore some {c2[1]} are not {st}.", + ("wa implies not wb", "ka implies not kb", "wc and wa"), + "(wc and (not wb)) or (kc and (not kb))"), + # E-form plus a named individual yields the O-form. + ("entailed", + lambda n1, c1, c2, c3, v1, st: f"{n1} is a {c1[0]}. No {c1[1]} are {st}. Therefore some {c1[1]} are not {st}.", + ("ma", "ma implies not mb", "ka implies not kb"), + "(ma and (not mb)) or (ka and (not kb))"), + # Verb E-form with the plural "do not" conclusion. + ("entailed", + lambda n1, c1, c2, c3, v1, st: f"No {c1[1]} {v1[0]}. Some {c2[1]} are {c1[1]}. Therefore some {c2[1]} do not {v1[0]}.", + ("wa implies not wv", "ka implies not kv", "wc and wa"), + "(wc and (not wv)) or (kc and (not kv))"), + # E-form and I-form are contradictories — the E refutes the I. + ("refuted", + lambda n1, c1, c2, c3, v1, st: f"No {c1[1]} are {st}. Therefore some {c1[1]} are {st}.", + ("ka implies not kb",), "ka and kb"), + # E-form instantiated at the named individual contradicts the query. + ("refuted", + lambda n1, c1, c2, c3, v1, st: f"{n1} is a {c1[0]}. No {c1[1]} are {st}. Some {c2[1]} are {c1[1]}. Therefore {n1} is {st}.", + ("ma", "ma implies not mb", "wa implies not wb", "wc and wa"), "mb"), + # The E-form binds a class the witness never enters. + ("unknown", + lambda n1, c1, c2, c3, v1, st: f"Some {c1[1]} are {c2[1]}. No {c3[1]} are {st}. Therefore some {c1[1]} are not {st}.", + ("wa and wb", "wc implies not wd", "kc implies not kd"), + "(wa and (not wd)) or (ka and (not kd))"), + ), +} + + #: Ledger band order: the five v1 bands, the four v2-EN bands, the four -#: v3-MEM bands, the four v4-CM bands, then the four v5-VP bands. +#: v3-MEM bands, the four v4-CM bands, the four v5-VP bands, then the four +#: v6-EX bands. _ALL_BANDS: tuple[str, ...] = ( CONDITIONAL_SINGLE, CONDITIONAL_CHAIN, DISJUNCTIVE, ATOMIC, CATEGORICAL, EN_CONDITIONAL_SINGLE, EN_CONDITIONAL_CHAIN, EN_DISJUNCTIVE, EN_ATOMIC, EN_MEMBER_SINGLE, EN_MEMBER_CHAIN, EN_MEMBER_NEGATIVE, EN_MEMBER_ATOMIC, EN_CONDMEM_FUSED, EN_CONDMEM_DISJUNCTIVE, EN_CONDMEM_CHAIN, EN_CONDMEM_CONDITIONAL, EN_VERB_NEGATIVE, EN_VERB_CHAIN, EN_VERB_UNIVERSAL, EN_VERB_FACT, + EN_EXIST_NEGATIVE, EN_EXIST_CHAIN, EN_EXIST_UNIVERSAL, EN_EXIST_WITNESS, ) @@ -674,6 +848,25 @@ def generate_problems(band: str, n: int) -> list[Problem]: logical form for the reader-independent oracle cross-check. """ problems: list[Problem] = [] + if band in _EXIST_TEMPLATES: + templates = _EXIST_TEMPLATES[band] + for i in range(n): + gold, builder, intended_premises, intended_query = templates[i % len(templates)] + problems.append( + Problem( + problem_id=f"{band}-{i:04d}", + class_name=band, + payload={ + "text": builder(*_exist_case(i)), + "gold": gold, + "intended": { + "premises": list(intended_premises), + "query": intended_query, + }, + }, + ) + ) + return problems if band in _VERB_TEMPLATES: templates = _VERB_TEMPLATES[band] for i in range(n): @@ -819,6 +1012,9 @@ class DeductionSolver: verb = self._attempt_verb(problem) if verb is not None: return verb + exist = self._attempt_exist(problem) + if exist is not None: + return exist return _DeductionAttempt( committed=False, answer=None, reason=f"reader:{getattr(comp, 'reason', '')}", case_id=problem.problem_id, shape=problem.class_name, @@ -861,6 +1057,9 @@ class DeductionSolver: verb = self._attempt_verb(problem) if verb is not None: return verb + exist = self._attempt_exist(problem) + if exist is not None: + return exist return _DeductionAttempt( committed=False, answer=None, reason="unprojectable", case_id=problem.problem_id, shape=problem.class_name, @@ -927,6 +1126,22 @@ class DeductionSolver: ) + def _attempt_exist(self, problem: Problem) -> _DeductionAttempt | None: + """Band v6-EX: the existential argument path, or ``None`` when the + reader refuses (the caller then records the honest decline).""" + arg = read_exist_argument(problem.payload["text"]) + if not isinstance(arg, ExistArgument): + return None + outcome = evaluate_entailment_with_trace( + arg.premise_formulas, arg.query_formula + ).outcome + return _DeductionAttempt( + committed=outcome is not Entailment.REFUSED, + answer=_OUTCOME_TO_CLASS[outcome], reason="", + case_id=problem.problem_id, shape=arg.band, + ) + + @dataclass(frozen=True, slots=True) class ConstructionGoldTether: """Scores the pipeline's committed outcome against the by-construction gold. diff --git a/evals/deduction_serve/report.json b/evals/deduction_serve/report.json index 18b06f99..ce18245f 100644 --- a/evals/deduction_serve/report.json +++ b/evals/deduction_serve/report.json @@ -1,8 +1,8 @@ { "aggregate": { - "correct": 134, + "correct": 166, "declined": 0, - "n": 134, + "n": 166, "wrong": 0 }, "all_correct": true, @@ -77,19 +77,40 @@ }, "n": 26 }, + "v2_exist": { + "all_cases_correct": true, + "by_gold": { + "declined": 11, + "entailed": 11, + "refuted": 4, + "unknown": 6 + }, + "correct_by_gold": { + "declined": 11, + "entailed": 11, + "refuted": 4, + "unknown": 6 + }, + "counts": { + "correct": 32, + "declined": 0, + "wrong": 0 + }, + "n": 32 + }, "v2_member": { "all_cases_correct": true, "by_gold": { - "declined": 6, + "declined": 5, "entailed": 12, "refuted": 3, - "unknown": 5 + "unknown": 6 }, "correct_by_gold": { - "declined": 6, + "declined": 5, "entailed": 12, "refuted": 3, - "unknown": 5 + "unknown": 6 }, "counts": { "correct": 26, diff --git a/evals/deduction_serve/runner.py b/evals/deduction_serve/runner.py index 9b259965..80cfed6b 100644 --- a/evals/deduction_serve/runner.py +++ b/evals/deduction_serve/runner.py @@ -48,6 +48,7 @@ from generate.proof_chain.categorical import CategoricalError, decide_syllogism from generate.proof_chain.cond_member import CondMemberArgument, read_cond_member_argument from generate.proof_chain.english import EnglishArgument, read_english_argument from generate.proof_chain.entail import Entailment, evaluate_entailment_with_trace +from generate.proof_chain.exist import ExistArgument, read_exist_argument from generate.proof_chain.member import MemberArgument, read_member_argument from generate.proof_chain.verb import VerbArgument, read_verb_argument @@ -71,6 +72,10 @@ _SPLITS: tuple[tuple[str, Path], ...] = ( # content-disjoint discipline (verb agreement across +s/+es/y↔ies and the # irregular table on real verbs: writes, debates, cries, goes). ("v2_verb", _ROOT / "v2_verb" / "cases.jsonl"), + # Band v6-EX (ADR-0261) — hand-authored existential arguments, same + # content-disjoint discipline (the square of opposition on real nouns, + # incl. the no-existential-import subalterns and both contradictory pairs). + ("v2_exist", _ROOT / "v2_exist" / "cases.jsonl"), ) _OUTCOME_TO_CLASS = { @@ -153,9 +158,20 @@ def _decide_cond_member(text: str) -> str: def _decide_verb(text: str) -> str: - """Band v5-VP fallback (ADR-0260) — mirrors ``_verb_band_surface``.""" + """Band v5-VP fallback (ADR-0260) — mirrors ``_verb_band_surface``; + chains into the Band v6-EX fallback exactly as the composer does.""" arg = read_verb_argument(text) if not isinstance(arg, VerbArgument): + return _decide_exist(text) + outcome = evaluate_entailment_with_trace(arg.premise_formulas, arg.query_formula).outcome + return _OUTCOME_TO_CLASS[outcome] + + +def _decide_exist(text: str) -> str: + """Band v6-EX fallback (ADR-0261) — mirrors ``_exist_band_surface``, the + last tier: a refusal here is the pipeline's honest decline.""" + arg = read_exist_argument(text) + if not isinstance(arg, ExistArgument): return "declined" outcome = evaluate_entailment_with_trace(arg.premise_formulas, arg.query_formula).outcome return _OUTCOME_TO_CLASS[outcome] diff --git a/evals/deduction_serve/v2_exist/cases.jsonl b/evals/deduction_serve/v2_exist/cases.jsonl new file mode 100644 index 00000000..a27b8486 --- /dev/null +++ b/evals/deduction_serve/v2_exist/cases.jsonl @@ -0,0 +1,32 @@ +{"id": "ds-ex-0001", "text": "Every mammal is a vertebrate. Some whales are mammals. Therefore some whales are vertebrates.", "gold": "entailed", "class": "exist_darii"} +{"id": "ds-ex-0002", "text": "Some philosophers are Greeks. Zeno is a Greek. Therefore some Greeks are philosophers.", "gold": "entailed", "class": "exist_i_conversion"} +{"id": "ds-ex-0003", "text": "Socrates is a philosopher. Socrates is wise. Therefore some philosophers are wise.", "gold": "entailed", "class": "exist_named_witness"} +{"id": "ds-ex-0004", "text": "Mars is a planet. No planets are stars. Some wanderers are planets. Therefore some wanderers are not stars.", "gold": "entailed", "class": "exist_ferio"} +{"id": "ds-ex-0005", "text": "All metals conduct heat. Some alloys are metals. Therefore some alloys conduct heat.", "gold": "entailed", "class": "exist_verb_universal"} +{"id": "ds-ex-0006", "text": "No reptiles nurse young. Some lizards are reptiles. Therefore some lizards do not nurse young.", "gold": "entailed", "class": "exist_verb_negative"} +{"id": "ds-ex-0007", "text": "Some canaries are songbirds. All songbirds are perchers. All perchers are agile. Therefore some canaries are agile.", "gold": "entailed", "class": "exist_chain"} +{"id": "ds-ex-0008", "text": "Aristotle is a philosopher. All philosophers are scholars. Therefore some scholars are philosophers.", "gold": "entailed", "class": "exist_named_witness_refuse_dont_drop"} +{"id": "ds-ex-0009", "text": "Some tortoises are ancient. Therefore some tortoises are ancient.", "gold": "entailed", "class": "exist_i_restatement"} +{"id": "ds-ex-0010", "text": "Some hermits are not sociable. Therefore some hermits are not sociable.", "gold": "entailed", "class": "exist_o_restatement"} +{"id": "ds-ex-0011", "text": "Every goose is a bird. Some geese are gray. Therefore some birds are gray.", "gold": "entailed", "class": "exist_irregular_number_link"} +{"id": "ds-ex-0012", "text": "No fish are mammals. Therefore some fish are mammals.", "gold": "refuted", "class": "exist_e_refutes_i"} +{"id": "ds-ex-0013", "text": "Every square is a rectangle. Therefore some squares are not rectangles.", "gold": "refuted", "class": "exist_a_refutes_o"} +{"id": "ds-ex-0014", "text": "Bede is a monk. No monks are talkative. Some scribes are monks. Therefore Bede is talkative.", "gold": "refuted", "class": "exist_e_form_at_named"} +{"id": "ds-ex-0015", "text": "Nile is a river. All rivers are wet. Some rivers are wide. Therefore Nile is not wet.", "gold": "refuted", "class": "exist_universal_at_named"} +{"id": "ds-ex-0016", "text": "Some sailors are brave. Magellan is a sailor. Therefore Magellan is brave.", "gold": "unknown", "class": "exist_witness_does_not_transfer"} +{"id": "ds-ex-0017", "text": "All unicorns are horned. Therefore some unicorns are horned.", "gold": "unknown", "class": "exist_no_existential_import"} +{"id": "ds-ex-0018", "text": "Some auks are flightless. Some auks are colorful. Therefore some flightless are colorful.", "gold": "unknown", "class": "exist_two_witnesses"} +{"id": "ds-ex-0019", "text": "Vega is a star. Vega is not visible. Therefore some stars are visible.", "gold": "unknown", "class": "exist_domain_stays_open"} +{"id": "ds-ex-0020", "text": "Some poems are sonnets. No plays rhyme. Therefore some poems do not rhyme.", "gold": "unknown", "class": "exist_unrelated_e_form"} +{"id": "ds-ex-0021", "text": "Some larks sing. Therefore some larks sing sweetly.", "gold": "unknown", "class": "exist_arity_at_face_value"} +{"id": "ds-ex-0022", "text": "Some of the sailors are brave. Therefore some sailors are brave.", "gold": "declined", "class": "partitive_out_of_band"} +{"id": "ds-ex-0023", "text": "Some sailors were brave. Therefore some sailors are brave.", "gold": "declined", "class": "tense_out_of_band"} +{"id": "ds-ex-0024", "text": "Some sailors did not return. Therefore some sailors return.", "gold": "declined", "class": "tense_out_of_band_verb"} +{"id": "ds-ex-0025", "text": "If some sailors are brave then the ship sails. Some sailors are brave. Therefore the ship sails.", "gold": "declined", "class": "mixed_structure_out_of_band"} +{"id": "ds-ex-0026", "text": "Most sailors are brave. Therefore some sailors are brave.", "gold": "declined", "class": "quantifier_out_of_band"} +{"id": "ds-ex-0027", "text": "Some sailors are brave. Therefore all sailors are brave.", "gold": "declined", "class": "universal_conclusion_out_of_band"} +{"id": "ds-ex-0028", "text": "Some sailors does not sail. Therefore some sailors sail.", "gold": "declined", "class": "agreement_out_of_band"} +{"id": "ds-ex-0029", "text": "Some old sailors whittle driftwood. Therefore some sailors whittle driftwood.", "gold": "declined", "class": "multi_token_subject_out_of_band"} +{"id": "ds-ex-0030", "text": "Some sailors who fish are brave. Therefore some sailors are brave.", "gold": "declined", "class": "relative_clause_out_of_band"} +{"id": "ds-ex-0031", "text": "Some sailors are the crew. Therefore some crew are sailors.", "gold": "declined", "class": "definite_description_out_of_band"} +{"id": "ds-ex-0032", "text": "Some sailors are brave. Do some sailors sing?", "gold": "declined", "class": "question_sentence"} diff --git a/evals/deduction_serve/v2_member/cases.jsonl b/evals/deduction_serve/v2_member/cases.jsonl index eb7401d9..8364fcd4 100644 --- a/evals/deduction_serve/v2_member/cases.jsonl +++ b/evals/deduction_serve/v2_member/cases.jsonl @@ -17,7 +17,7 @@ {"id": "ds-mem-0017", "text": "Plato is a man. All men are mortal. Therefore Zeus is mortal.", "gold": "unknown", "class": "wrong_individual"} {"id": "ds-mem-0018", "text": "Rex is a dog. All cats are animals. Therefore Rex is an animal.", "gold": "unknown", "class": "broken_chain"} {"id": "ds-mem-0019", "text": "Milo is a child. All children are curious. Therefore Milo is happy.", "gold": "unknown", "class": "unrelated_predicate"} -{"id": "ds-mem-0020", "text": "Some men are wise. Socrates is a man. Therefore Socrates is wise.", "gold": "declined", "class": "existential_out_of_band"} +{"id": "ds-mem-0020", "text": "Some men are wise. Socrates is a man. Therefore Socrates is wise.", "gold": "unknown", "class": "exist_witness_does_not_transfer"} {"id": "ds-mem-0021", "text": "Dogs are loyal. Rex is a dog. Therefore Rex is loyal.", "gold": "declined", "class": "bare_plural_out_of_band"} {"id": "ds-mem-0022", "text": "Socrates is the philosopher. All philosophers are wise. Therefore Socrates is wise.", "gold": "declined", "class": "definite_description_out_of_band"} {"id": "ds-mem-0023", "text": "Socrates is a man. All men are mortal. Therefore all men are mortal.", "gold": "declined", "class": "universal_conclusion_out_of_band"} diff --git a/generate/meaning_graph/projectors.py b/generate/meaning_graph/projectors.py index 50b15aa1..55bf8dcf 100644 --- a/generate/meaning_graph/projectors.py +++ b/generate/meaning_graph/projectors.py @@ -71,12 +71,23 @@ def to_syllogism(comp: Comprehension) -> tuple[dict[str, Any], dict[str, Any]] | the single categorical query is the conclusion. Returns ``None`` when the comprehension is not exactly one categorical conclusion over >=1 premise — the caller treats that as a refusal (nothing honestly askable of this oracle). + + Refuse-don't-drop (ADR-0261 §5): a relation this projection cannot express — + a singular ``member`` fact, a negated relation — makes the WHOLE projection + refuse, exactly as its propositional sibling ``to_deductive_logic`` already + does. Filtering such a relation out instead would hand the oracle a + STRICTLY WEAKER argument than the user wrote and then answer it: "Aristotle + is a philosopher. All philosophers are scholars. Therefore some scholars + are philosophers." loses its only witness and comes back "that doesn't + follow" — a wrong served answer, not a decline. Refusing lets the later + reader bands (v3-MEM onward), which read singular facts, decide it. """ graph = comp.meaning_graph + if any(r.predicate not in _PRED_FORM or r.negated for r in graph.relations): + return None premises = [ {"form": _PRED_FORM[r.predicate], "subject": r.arguments[0], "predicate": r.arguments[1]} for r in graph.relations - if r.predicate in _PRED_FORM and not r.negated ] conclusions = [q for q in comp.queries if q.predicate in _PRED_FORM and not q.negated] if not premises or len(comp.queries) != 1 or len(conclusions) != 1: diff --git a/generate/proof_chain/exist.py b/generate/proof_chain/exist.py new file mode 100644 index 00000000..4585685f --- /dev/null +++ b/generate/proof_chain/exist.py @@ -0,0 +1,546 @@ +"""Existential-argument reader — Band v6-EX (ADR-0261). + +Completes the all / no / some square. Reads deductive arguments containing +existential ("some") sentences — "All wolves are mammals. Some wolves are +tame. Therefore some mammals are tame." — by extending Band v5-VP's +per-individual propositional lowering with TWO new domain elements: + +- a **witness** per existential PREMISE (Skolem constant): "some C1 are C2" + ⇒ ``mem(w,C1) & mem(w,C2)`` for a fresh ``w`` that nothing else names; +- one **arbitrary individual** ``k``, minted iff the CONCLUSION is + existential: an element about which no fact is asserted and at which every + universal is still instantiated. + +An existential conclusion lowers to the disjunction of its conjunction over +EVERY domain element (named individuals, witnesses, and ``k``). The same +verified ROBDD engine decides. Both atom families of v5-VP carry over +unchanged, so existentials compose with membership facts, is-a universals, +verb facts, and verb universals in one shared atom space. + +Why this is sound (ADR-0261 §3), in the two directions that matter: + +* **ENTAILED.** Let *M* be any first-order model of the argument's premises. + Every witness is interpretable in *M* (its existential premise asserts a + satisfier), universal instantiation is truth-preserving at every element, + and ``k`` may be interpreted as ANY element (domains are non-empty), so + every lowered premise formula holds in *M*. If the lowered premises + propositionally entail the query's disjunction, some domain element + satisfies the conjunction in *M* — which is exactly ∃. Skolem constants + never appear in the original argument, so this is the standard + entailment-preserving Skolemization. +* **REFUTED.** The conjunction dual is entailed only if it is entailed at + ``k`` — and ``k`` is arbitrary (no premise mentions it), so what holds of + ``k`` holds of every element: the universal ∀x¬(…) that refuting ∃ requires + is genuinely derived, never assumed by domain closure. This is the ONE + place a naive witness-only lowering would be unsound: without ``k``, + "Rex is a wolf. Rex is not tame. Therefore some wolves are tame." would + read as REFUTED (the only wolf in the lowering is not tame) instead of the + honest UNKNOWN. ``k`` is what keeps the domain open. + +Completeness within the fragment lifts the same way as v3-MEM/v5-VP: a +propositional countermodel becomes a first-order countermodel whose domain is +exactly the named individuals, witnesses, and ``k``. + +**No existential import.** "All C are P. Therefore some C are P." is UNKNOWN, +not ENTAILED — a universal is vacuously true over an empty class, so the +subaltern moods (Darapti, Felapton, Bamalip) come out UNKNOWN here. That is +the modern first-order reading and the conservative one; the categorical band +(v1b) already reads the square the same way (its own arena carries the +"existential-import overreach" case as INVALID). + +Sentence shapes added over v5-VP, all with a ``some`` lead: +``some are|is [not] [a|an] `` (I-form and O-form) and +``some []`` / ``some do not []``. The +plural ``do not`` is read HERE (unlike v5-VP, which refuses it) because with +an existential subject there is no scope ambiguity: "some C do not V" is +∃x(C(x) ∧ ¬V(x)), full stop. ``all C do not V`` remains refused — that one is +genuinely ambiguous. Every other sentence shape delegates VERBATIM to v3-MEM +and v5-VP's own parsers, refusals included. + +Tried strictly AFTER Bands v1 / v1b / v2-EN / v3-MEM / v4-CM / v5-VP (the +last fallback tier) — pure widening; every previously-served argument is +served byte-identically. Every earlier band refuses a ``some``-led sentence +(``quantifier_out_of_band`` / ``categorical_shape_out_of_band``), and the +categorical band v1b, which does read some-syllogisms, is tried BEFORE this +one and keeps them. Refusal-first, closed reason vocabulary: + + ``empty``, ``question_sentence``, ``no_conclusion``, + ``multiple_conclusions``, ``conclusion_not_last``, ``no_premises``, + ``empty_side``, ``quantifier_out_of_band``, ``bare_plural_out_of_band``, + ``definite_description_out_of_band``, ``relative_clause_out_of_band``, + ``universal_conclusion_out_of_band``, ``mixed_structure_out_of_band``, + ``internal_negation_unread``, ``sentence_shape_out_of_band``, + ``tense_out_of_band``, ``partitive_out_of_band``, ``structural_leak``, + ``too_many_premises``, ``too_many_atoms``. +""" + +from __future__ import annotations + +from dataclasses import dataclass + +# The v2-EN sentence splitter/tokenizer, v3-MEM's copula parsers and shared +# guards, and v5-VP's verb grammar are reused VERBATIM — one normalization +# discipline across every argument band; deliberate private-name imports +# inside the proof_chain package, same precedent as member/cond_member/verb. +from generate.proof_chain.english import _SENTENCE_RE, _tokenize +from generate.proof_chain.member import ( + _A_LEADS, + _COPULA_FORMS, + _E_LEAD, + _QUANTIFIER_TOKENS, + _SENTENTIAL_NOT, + _Singular, + _Universal, + _check_run, + _forms_link, + _parse_singular, + _parse_universal, +) +from generate.proof_chain.member import _Reject as _MemberReject +from generate.proof_chain.shape import ( + EN_EXIST_CHAIN, + EN_EXIST_NEGATIVE, + EN_EXIST_UNIVERSAL, + EN_EXIST_WITNESS, +) +from generate.proof_chain.verb import ( + _AUXILIARIES, + _CONNECTIVES, + _VerbFact, + _VerbUniversal, + _check_term_token, + _check_verb_token, + _parse_fact, + _parse_verb_universal, + _verb_tokens_link, +) +from generate.proof_chain.verb import _Reject as _VerbReject + +#: The one existential lead this band reads. Every other quantifier token +#: keeps v3-MEM's ``quantifier_out_of_band`` refusal. +_SOME = "some" + +#: Partitive marker — "some of the wolves" is a different construction +#: (quantification over a contextually-fixed set, not over a class), so it +#: refuses rather than being read as an opaque class run. +_PARTITIVE = "of" + +#: Honesty caps — beyond these the argument is refused, never truncated. +#: ``MAX_ATOMS`` now also bounds an existential conclusion's disjunction, +#: which mints up to two atoms per domain element, so the cap binds exactly +#: where the lowering multiplies. +MAX_PREMISE_SENTENCES = 16 +MAX_ATOMS = 24 + +#: Display names for the two synthetic domain elements. Presentation only — +#: atom identity is the domain INDEX, so these can never collide with a name +#: the user actually wrote. +_WITNESS_DISPLAY = "witness {n}" +_ARBITRARY_DISPLAY = "any individual" + + +@dataclass(frozen=True, slots=True) +class ExistArgument: + """A successfully-read existential argument, engine-ready. + + Same shape as ``VerbArgument``: ``premise_formulas``/``query_formula`` are + propositional formula strings over minted atom ids; ``atoms[i]`` displays + the fact behind ``a{i}`` (``individual : class`` for membership atoms, + ``individual : verb [object]`` for verb atoms, where ``individual`` may be + a witness or the arbitrary element). + """ + + premise_formulas: tuple[str, ...] + query_formula: str + premise_texts: tuple[str, ...] + query_text: str + band: str + atoms: tuple[str, ...] + + +@dataclass(frozen=True, slots=True) +class ExistRefusal: + """A typed refusal — the argument is not honestly readable by this band.""" + + reason: str + detail: str = "" + + +class _Reject(Exception): + def __init__(self, reason: str, detail: str = "") -> None: + super().__init__(reason) + self.refusal = ExistRefusal(reason, detail) + + +@dataclass(frozen=True, slots=True) +class _ExistCopula: + """``some are|is [not] [a|an] `` — an I-form (or O-form when + ``negated``) over a fresh witness at lowering time.""" + + subject: tuple[str, ...] + predicate: tuple[str, ...] + negated: bool + + +@dataclass(frozen=True, slots=True) +class _ExistVerb: + """``some [do not] []`` — the verb-predicate I/O-form + over a fresh witness at lowering time.""" + + subject: tuple[str, ...] + verb: str + obj: str | None + negated: bool + + +_Existential = _ExistCopula | _ExistVerb +_Record = _Singular | _Universal | _VerbFact | _VerbUniversal | _ExistCopula | _ExistVerb + + +def _check_exist_subject(toks: tuple[str, ...], detail: str) -> None: + """Guard an existential subject run: the shared opaque-run guard plus the + partitive exclusion.""" + if _PARTITIVE in toks: + raise _Reject("partitive_out_of_band", detail) + _check_run(toks, detail) + + +def _parse_exist_copula(toks: list[str], detail: str) -> _ExistCopula: + """``some are|is [not] [a|an] ``. + + Deliberately NOT v3-MEM's ``_parse_universal``: that parser refuses a + predicate-leading ``not`` because "all C are not P" is scope-ambiguous + (¬∀ vs ∀¬). "Some C are not P" has no such ambiguity — it is the O-form, + ∃x(C(x) ∧ ¬P(x)) — so the negation is read here. + """ + rest = toks[1:] + cop_idx = next((i for i, t in enumerate(rest) if t in ("is", "are")), None) + if cop_idx is None: + raise _Reject("sentence_shape_out_of_band", detail) + subject = rest[:cop_idx] + if subject and subject[0] == "the": # "some of the …" is caught below + subject = subject[1:] + predicate = rest[cop_idx + 1 :] + negated = False + if predicate and predicate[0] == "not": + negated = True + predicate = predicate[1:] + if predicate and predicate[0] in ("a", "an"): + predicate = predicate[1:] + elif predicate and predicate[0] == "the": + raise _Reject("definite_description_out_of_band", detail) + _check_exist_subject(tuple(subject), detail) + _check_run(tuple(predicate), detail) + return _ExistCopula(tuple(subject), tuple(predicate), negated) + + +def _parse_exist_verb(toks: list[str], detail: str) -> _ExistVerb: + """``some []`` / ``some do not []`` — no + copula form. Single-token class, verb, and object, exactly as v5-VP's + verb universals.""" + rest = toks[1:] + if rest and rest[0] == "the": + rest = rest[1:] + if _PARTITIVE in rest: + raise _Reject("partitive_out_of_band", detail) + negated = False + if len(rest) >= 3 and rest[1] in _AUXILIARIES and rest[2] == "not": + if rest[1] == "did": + raise _Reject("tense_out_of_band", detail) + if rest[1] == "does": + # "some wolves does not run" — agreement this band does not read. + raise _Reject("sentence_shape_out_of_band", detail) + negated = True + rest = [rest[0], *rest[3:]] + if any(t == "not" or t.endswith("n't") for t in rest): + raise _Reject("internal_negation_unread", detail) + if any(t == "did" for t in rest): + raise _Reject("tense_out_of_band", detail) + if len(rest) < 2 or len(rest) > 3: + raise _Reject("sentence_shape_out_of_band", detail) + cls, verb = rest[0], rest[1] + obj = rest[2] if len(rest) == 3 else None + _check_term_token(cls, detail) + _check_verb_token(verb, detail) + if obj is not None: + _check_term_token(obj, detail) + return _ExistVerb((cls,), verb, obj, negated) + + +def _parse_existential(toks: list[str], detail: str) -> _Existential: + """A ``some``-led sentence: a copula form routes to the I/O-form copula + parser, else the verb grammar.""" + if any(t in _COPULA_FORMS for t in toks): + if any(t in ("was", "were") for t in toks): + raise _Reject("tense_out_of_band", detail) + return _parse_exist_copula(toks, detail) + return _parse_exist_verb(toks, detail) + + +def _parse_sentence(toks: list[str], detail: str) -> _Record: + if any(t in _CONNECTIVES for t in toks): + raise _Reject("mixed_structure_out_of_band", detail) + head = toks[0] + if head == _SOME: + return _parse_existential(toks, detail) + if head in _A_LEADS or head == _E_LEAD: + if any(t in ("is", "are") for t in toks): + return _parse_universal(toks, detail) # is-a universal (v3-MEM's) + return _parse_verb_universal(toks, detail) # verb universal (v5-VP's) + if head in _QUANTIFIER_TOKENS: + raise _Reject("quantifier_out_of_band", detail) + return _parse_fact(toks, detail) # singular membership / verb fact (v5-VP's) + + +def read_exist_argument(text: str) -> ExistArgument | ExistRefusal: + """Read *text* as an existential argument, or refuse (typed). + + Deterministic and pure: same text → same ``ExistArgument``. The conclusion + is the final sentence, the sole "therefore"-led one, and may be a singular + fact (membership or verb) or an existential; universal conclusions stay + out of band. Lowering is two-pass exactly as v3-MEM/v5-VP's — sentences + parse first, THEN the domain (named individuals, one witness per + existential premise, and the arbitrary element when the conclusion is + existential) is fixed, THEN atoms mint and universals instantiate at every + domain element — with premise formulas emitted in sentence order. + """ + if not text or not text.strip(): + return ExistRefusal("empty") + sentences = [ + (m.group(1), m.group(2)) for m in _SENTENCE_RE.finditer(text) if m.group(1).strip() + ] + if not sentences: + return ExistRefusal("empty") + + premises: list[_Record] = [] + premise_texts: list[str] = [] + conclusion: _Singular | _VerbFact | _ExistCopula | _ExistVerb | None = None + query_text: str | None = None + + try: + for idx, (body, terminator) in enumerate(sentences): + if terminator == "?": + raise _Reject("question_sentence", body) + toks = _tokenize(body) + if not toks: + continue + if toks[0] == "therefore": + if conclusion is not None: + raise _Reject("multiple_conclusions", body) + if idx != len(sentences) - 1: + raise _Reject("conclusion_not_last", body) + rest = toks[1:] + if not rest: + raise _Reject("empty_side", body) + if any(t in _CONNECTIVES for t in rest): + raise _Reject("mixed_structure_out_of_band", body) + if rest[0] in _A_LEADS or rest[0] == _E_LEAD: + raise _Reject("universal_conclusion_out_of_band", body) + if rest[0] == _SOME: + conclusion = _parse_existential(rest, body) + elif rest[0] in _QUANTIFIER_TOKENS: + raise _Reject("quantifier_out_of_band", body) + else: + conclusion = _parse_fact(rest, body) + query_text = " ".join(rest) + continue + if len(premises) >= MAX_PREMISE_SENTENCES: + raise _Reject("too_many_premises", body) + premises.append(_parse_sentence(toks, body)) + premise_texts.append(" ".join(toks)) + + if conclusion is None or query_text is None: + return ExistRefusal("no_conclusion") + if not premises: + return ExistRefusal("no_premises") + + records: list[_Record] = [*premises, conclusion] + + # Every argument this band DECIDES contains at least one existential + # construct — a purely universal/singular argument is v3-MEM/v5-VP + # territory (and only ever reaches here when those bands refused it, + # in which case the delegated parsers above raised the same typed + # refusal already; this is a defensive closure of that invariant). + if not any(isinstance(r, (_ExistCopula, _ExistVerb)) for r in records): + raise _Reject("sentence_shape_out_of_band", "no existential read") + + # --- domain (ADR-0261 §2) ------------------------------------------- + # Display name per domain index; named individuals first (first- + # appearance order), then one witness per existential premise, then + # the arbitrary element iff the conclusion is existential. + domain: list[str] = [] + named_index: dict[tuple[str, ...], int] = {} + for rec in records: + if isinstance(rec, (_Singular, _VerbFact)) and rec.ind not in named_index: + named_index[rec.ind] = len(domain) + domain.append(" ".join(rec.ind)) + witness_index: dict[int, int] = {} + for pos, rec in enumerate(premises): + if isinstance(rec, (_ExistCopula, _ExistVerb)): + witness_index[pos] = len(domain) + domain.append(_WITNESS_DISPLAY.format(n=len(witness_index))) + conclusion_is_existential = isinstance(conclusion, (_ExistCopula, _ExistVerb)) + if conclusion_is_existential: + domain.append(_ARBITRARY_DISPLAY) + + # Class groups — the SAME closed noun-morphology relation as v3-MEM. + cls_group_of: dict[tuple[str, ...], int] = {} + cls_reps: list[tuple[str, ...]] = [] + for rec in records: + forms: list[tuple[str, ...]] = [] + if isinstance(rec, _Singular): + forms = [rec.cls] + elif isinstance(rec, (_Universal, _ExistCopula)): + forms = [rec.subject, rec.predicate] + elif isinstance(rec, (_VerbUniversal, _ExistVerb)): + forms = [rec.subject] + for form in forms: + if form in cls_group_of: + continue + for gi, rep in enumerate(cls_reps): + if _forms_link(form, rep): + cls_group_of[form] = gi + break + else: + cls_group_of[form] = len(cls_reps) + cls_reps.append(form) + + # Verb groups — v5-VP's closed agreement relation, unchanged. + verb_group_of: dict[str, int] = {} + verb_reps: list[str] = [] + for rec in records: + if not isinstance(rec, (_VerbFact, _VerbUniversal, _ExistVerb)): + continue + form = rec.verb + if form in verb_group_of: + continue + for gi, rep in enumerate(verb_reps): + if _verb_tokens_link(form, rep): + verb_group_of[form] = gi + break + else: + verb_group_of[form] = len(verb_reps) + verb_reps.append(form) + + mint: dict[tuple, str] = {} + atom_display: list[str] = [] + + def _mint(key: tuple, display: str, detail: str) -> str: + if key not in mint: + if len(atom_display) >= MAX_ATOMS: + raise _Reject("too_many_atoms", detail) + mint[key] = f"a{len(atom_display)}" + atom_display.append(display) + return mint[key] + + def mem_atom(ind_idx: int, group: int, detail: str) -> str: + return _mint( + ("mem", ind_idx, group), + f"{domain[ind_idx]} : {' '.join(cls_reps[group])}", + detail, + ) + + def verb_atom(ind_idx: int, group: int, obj: str | None, detail: str) -> str: + shown = verb_reps[group] if obj is None else f"{verb_reps[group]} {obj}" + return _mint(("verb", ind_idx, group, obj), f"{domain[ind_idx]} : {shown}", detail) + + def literal(atom: str, negated: bool) -> str: + return f"~({atom})" if negated else atom + + def conjunction(ind_idx: int, rec: _Existential, detail: str) -> str: + """``mem(i, subject) & [~](i)`` for one domain element — + the body of both an existential premise and an existential query + disjunct.""" + subject = mem_atom(ind_idx, cls_group_of[rec.subject], detail) + if isinstance(rec, _ExistCopula): + predicate = mem_atom(ind_idx, cls_group_of[rec.predicate], detail) + else: + predicate = verb_atom(ind_idx, verb_group_of[rec.verb], rec.obj, detail) + return f"({subject}) & ({literal(predicate, rec.negated)})" + + premise_formulas: list[str] = [] + for pos, (rec, body_text) in enumerate(zip(premises, premise_texts)): + if isinstance(rec, _Singular): + atom = mem_atom(named_index[rec.ind], cls_group_of[rec.cls], body_text) + premise_formulas.append(literal(atom, rec.negated)) + elif isinstance(rec, _VerbFact): + atom = verb_atom( + named_index[rec.ind], verb_group_of[rec.verb], rec.obj, body_text + ) + premise_formulas.append(literal(atom, rec.negated)) + elif isinstance(rec, (_ExistCopula, _ExistVerb)): + premise_formulas.append(conjunction(witness_index[pos], rec, body_text)) + elif isinstance(rec, _Universal): + for ind_idx in range(len(domain)): + antecedent = mem_atom(ind_idx, cls_group_of[rec.subject], body_text) + consequent = mem_atom(ind_idx, cls_group_of[rec.predicate], body_text) + premise_formulas.append( + f"({antecedent}) -> ({literal(consequent, rec.negative)})" + ) + else: # _VerbUniversal + for ind_idx in range(len(domain)): + antecedent = mem_atom(ind_idx, cls_group_of[rec.subject], body_text) + consequent = verb_atom( + ind_idx, verb_group_of[rec.verb], rec.obj, body_text + ) + premise_formulas.append( + f"({antecedent}) -> ({literal(consequent, rec.negative)})" + ) + + if isinstance(conclusion, (_ExistCopula, _ExistVerb)): + query_formula = " | ".join( + f"({conjunction(ind_idx, conclusion, query_text)})" + for ind_idx in range(len(domain)) + ) + elif isinstance(conclusion, _Singular): + query_formula = literal( + mem_atom( + named_index[conclusion.ind], cls_group_of[conclusion.cls], query_text + ), + conclusion.negated, + ) + else: + query_formula = literal( + verb_atom( + named_index[conclusion.ind], + verb_group_of[conclusion.verb], + conclusion.obj, + query_text, + ), + conclusion.negated, + ) + except (_Reject, _MemberReject, _VerbReject) as rej: + # ``_parse_singular`` / ``_parse_universal`` are v3-MEM's own functions + # and ``_parse_fact`` / ``_parse_verb_universal`` are v5-VP's, all + # reused verbatim — their failures raise THEIR OWN ``_Reject`` classes + # (same shape, different identity), so all three are caught here and + # normalized to THIS band's refusal type (the v4-CM lesson, extended). + return ExistRefusal(rej.refusal.reason, rej.refusal.detail) + + universals = [r for r in premises if isinstance(r, (_Universal, _VerbUniversal))] + if any(u.negative for u in universals): + band = EN_EXIST_NEGATIVE + elif len(universals) >= 2: + band = EN_EXIST_CHAIN + elif len(universals) == 1: + band = EN_EXIST_UNIVERSAL + else: + band = EN_EXIST_WITNESS + + return ExistArgument( + premise_formulas=tuple(premise_formulas), + query_formula=query_formula, + premise_texts=tuple(premise_texts), + query_text=query_text, + band=band, + atoms=tuple(atom_display), + ) + + +__all__ = [ + "MAX_ATOMS", + "MAX_PREMISE_SENTENCES", + "ExistArgument", + "ExistRefusal", + "read_exist_argument", +] diff --git a/generate/proof_chain/render.py b/generate/proof_chain/render.py index e80b1d8c..0c28be39 100644 --- a/generate/proof_chain/render.py +++ b/generate/proof_chain/render.py @@ -169,6 +169,45 @@ def render_entailment_verb( return f"Given: {given}. I can't evaluate {query_text} from that as stated." +def render_entailment_exist( + trace: EntailmentTrace, premise_texts: tuple[str, ...], query_text: str +) -> str: + """The user-facing surface for an existential (Band v6-EX) verdict. + + Same discipline as :func:`render_entailment_verb`; the UNKNOWN template + additionally discloses the ONE reading choice existentials force + (ADR-0261 §3): "some" is read WITHOUT existential import, so a universal + says nothing about whether its class has members. That is precisely what + makes "all C are P, therefore some C are P" come out unsettled rather than + entailed, and a reader who expects the traditional square deserves to be + told which square this is. ENTAILED / REFUTED / inconsistent hold under + the classical reading too (adding existential-import premises only ADDS + premises, and entailment is monotone), so they are stated at full strength. + """ + given = "; ".join(premise_texts) + if trace.outcome is Entailment.ENTAILED: + return f"Given: {given}. Your premises entail: {query_text}." + if trace.outcome is Entailment.REFUTED: + return ( + f"Given: {given}. Your premises entail the opposite of " + f"{query_text} — it cannot hold." + ) + if trace.outcome is Entailment.UNKNOWN: + return ( + f"Given: {given}. Reading each name as one individual, each class " + f"word and verb phrase at face value, and \"some\" as claiming a " + f"member exists (so \"all\" does not), your premises don't settle " + f"whether {query_text} — it holds in some cases and fails in others." + ) + # REFUSED + if trace.reason == INCONSISTENT_PREMISES: + return ( + f"Given: {given}. Those premises are inconsistent — they " + f"can't all be true, so I won't assert anything from them." + ) + return f"Given: {given}. I can't evaluate {query_text} from that as stated." + + def _categorical_clause(prop: dict) -> str: """One categorical proposition dict → its English clause.""" template = _CATEGORICAL_PHRASE.get(prop.get("form", ""), "{s} ~ {p}") @@ -205,6 +244,7 @@ def render_syllogism(trace: EntailmentTrace, structure: dict, query: dict) -> st __all__ = [ "render_entailment", "render_entailment_english", + "render_entailment_exist", "render_entailment_member", "render_entailment_verb", "render_syllogism", diff --git a/generate/proof_chain/shape.py b/generate/proof_chain/shape.py index b7929b49..69074787 100644 --- a/generate/proof_chain/shape.py +++ b/generate/proof_chain/shape.py @@ -113,9 +113,33 @@ EN_VERB_BANDS: tuple[str, ...] = ( EN_VERB_FACT, ) +#: Band v6-EX (ADR-0261) — existential arguments ("All wolves are mammals. +#: Some wolves are tame. Therefore some mammals are tame."), read by +#: ``generate.proof_chain.exist``: v5-VP's per-individual lowering over a +#: domain widened with one Skolem witness per existential premise and one +#: arbitrary element per existential conclusion. Same ``en_`` license +#: discipline: a different reader must earn its own per-shape record. +#: Priority order: negative > chain > universal > witness. +EN_EXIST_NEGATIVE = "en_exist_negative" +EN_EXIST_CHAIN = "en_exist_chain" +EN_EXIST_UNIVERSAL = "en_exist_universal" +EN_EXIST_WITNESS = "en_exist_witness" + +EN_EXIST_BANDS: tuple[str, ...] = ( + EN_EXIST_NEGATIVE, + EN_EXIST_CHAIN, + EN_EXIST_UNIVERSAL, + EN_EXIST_WITNESS, +) + #: Every serving shape-band — the ratified ledger's full key set. ALL_SHAPE_BANDS: tuple[str, ...] = ( - SHAPE_BANDS + EN_SHAPE_BANDS + EN_MEMBER_BANDS + EN_CONDMEM_BANDS + EN_VERB_BANDS + SHAPE_BANDS + + EN_SHAPE_BANDS + + EN_MEMBER_BANDS + + EN_CONDMEM_BANDS + + EN_VERB_BANDS + + EN_EXIST_BANDS ) @@ -159,6 +183,11 @@ __all__ = [ "EN_CONDMEM_DISJUNCTIVE", "EN_CONDMEM_FUSED", "EN_DISJUNCTIVE", + "EN_EXIST_BANDS", + "EN_EXIST_CHAIN", + "EN_EXIST_NEGATIVE", + "EN_EXIST_UNIVERSAL", + "EN_EXIST_WITNESS", "EN_MEMBER_ATOMIC", "EN_MEMBER_BANDS", "EN_MEMBER_CHAIN", diff --git a/scripts/generate_claims.py b/scripts/generate_claims.py index 14e7008d..69920837 100644 --- a/scripts/generate_claims.py +++ b/scripts/generate_claims.py @@ -76,7 +76,7 @@ _LANE_ADR: dict[str, tuple[str, str]] = { ), "deduction_serve_v1": ( "ADR-0256", - "Flag-gated deduction serving decides real English/member/fused arguments end-to-end under earned SERVE licenses; wrong=0 across all splits", + "Flag-gated deduction serving decides real English/member/fused/verb/existential arguments end-to-end under earned SERVE licenses; wrong=0 across all splits", ), } diff --git a/scripts/verify_lane_shas.py b/scripts/verify_lane_shas.py index 10476059..d26394b2 100644 --- a/scripts/verify_lane_shas.py +++ b/scripts/verify_lane_shas.py @@ -51,7 +51,7 @@ PINNED_SHAS: dict[str, str] = { "public_demo": "7d8ba0dbae9287cfe0bf15d231fa78a75abc627121c14900439293e01e1cc1d3", "math_teaching_corpus_v1": "eaf160d145da29f9050ede8d58bf111b0f651dd40aeae9201857d0b97e014dd4", "deductive_logic_v1": "97a230949016e38d5e3f37a69e4245b320575ee70e5af92ff7607f7b05f74b5f", - "deduction_serve_v1": "f4fa7331bbee40c898be9ea2a8cabf36f28c8a19a7500433e0fa966c05905a8a", + "deduction_serve_v1": "0b461a5a49c8f8260ca87d0c9c9f9a17232bd1fdedd982e34649eedf9cca30b5", } diff --git a/tests/test_deduction_serve_e2e.py b/tests/test_deduction_serve_e2e.py index 52c31d75..216ea1a2 100644 --- a/tests/test_deduction_serve_e2e.py +++ b/tests/test_deduction_serve_e2e.py @@ -179,3 +179,30 @@ def test_verb_predicate_is_decided_end_to_end() -> None: ) assert resp.grounding_source == "deduction" assert "Your premises entail: socrates teaches" in resp.surface + + +def test_existential_is_decided_end_to_end() -> None: + """The ADR-0261 flagship: a witness carried through a universal to an + existential conclusion, decided through the real REPL spine.""" + rt = _runtime(True) + resp = rt.chat( + "Every mammal is a vertebrate. Some whales are mammals. " + "Therefore some whales are vertebrates." + ) + assert resp.grounding_source == "deduction" + assert "Your premises entail: some whales are vertebrates" in resp.surface + + +def test_singular_premise_is_not_dropped_by_the_categorical_band() -> None: + """ADR-0261 §5 regression: the categorical projector used to FILTER a + singular ``member`` premise out and answer from what was left, serving + "that doesn't follow" for an argument that does. It now refuses, and the + existential band decides the real argument.""" + rt = _runtime(True) + resp = rt.chat( + "Aristotle is a philosopher. All philosophers are scholars. " + "Therefore some scholars are philosophers." + ) + assert resp.grounding_source == "deduction" + assert "Your premises entail: some scholars are philosophers" in resp.surface + assert "doesn't follow" not in resp.surface diff --git a/tests/test_deduction_serve_lane.py b/tests/test_deduction_serve_lane.py index 1af1aedf..010e0faf 100644 --- a/tests/test_deduction_serve_lane.py +++ b/tests/test_deduction_serve_lane.py @@ -16,6 +16,7 @@ _V2_EN = _ROOT / "v2_en" / "cases.jsonl" _V2_MEMBER = _ROOT / "v2_member" / "cases.jsonl" _V2_CONDMEM = _ROOT / "v2_condmem" / "cases.jsonl" _V2_VERB = _ROOT / "v2_verb" / "cases.jsonl" +_V2_EXIST = _ROOT / "v2_exist" / "cases.jsonl" def test_v1_lane_wrong_is_zero() -> None: @@ -58,10 +59,13 @@ def test_v2_member_lane_wrong_is_zero() -> None: """Band v3-MEM (ADR-0258): hand-authored membership/universal arguments — real nouns exercising every number-link row-type (irregular, invariant, each regular suffix rule) — decided with wrong=0 across all four verdicts - and six distinct honest-decline shapes. (``ds-mem-0024``, a bare + and five distinct honest-decline shapes. (``ds-mem-0024``, a bare conditional with no anchor, was promoted declined->unknown when Band v4-CM landed — ADR-0259; it is genuinely UNKNOWN, not entailed, since the - antecedent is never asserted.)""" + antecedent is never asserted. ``ds-mem-0020``, the ADR-0258 existential + scope-out, was promoted declined->unknown when Band v6-EX landed — + ADR-0261; genuinely UNKNOWN, since an anonymous witness never transfers to + a named individual.)""" report = build_report(_load(_V2_MEMBER)) assert report["n"] == 26 assert report["counts"]["wrong"] == 0 @@ -69,8 +73,8 @@ def test_v2_member_lane_wrong_is_zero() -> None: cbg = report["correct_by_gold"] assert cbg.get("entailed", 0) >= 12 assert cbg.get("refuted", 0) >= 3 - assert cbg.get("unknown", 0) >= 5 - assert cbg.get("declined", 0) >= 6 + assert cbg.get("unknown", 0) >= 6 + assert cbg.get("declined", 0) >= 5 def test_v2_condmem_lane_wrong_is_zero() -> None: @@ -106,6 +110,23 @@ def test_v2_verb_lane_wrong_is_zero() -> None: assert cbg.get("declined", 0) >= 8 +def test_v2_exist_lane_wrong_is_zero() -> None: + """Band v6-EX (ADR-0261): hand-authored existential arguments — the full + square of opposition (Darii, Ferio, both contradictory pairs, the + no-existential-import subaltern), witnesses that never transfer to a named + individual, the arbitrary element that keeps the domain open, and eleven + distinct honest-decline shapes — decided wrong=0.""" + report = build_report(_load(_V2_EXIST)) + assert report["n"] == 32 + assert report["counts"]["wrong"] == 0 + assert report["all_cases_correct"] is True + cbg = report["correct_by_gold"] + assert cbg.get("entailed", 0) >= 11 + assert cbg.get("refuted", 0) >= 4 + assert cbg.get("unknown", 0) >= 6 + assert cbg.get("declined", 0) >= 11 + + def test_runner_treats_wrong_verdict_as_the_only_real_failure() -> None: """A committed disagreement with gold is ``wrong``; a decline never is, even when gold expected a definite verdict (that's a miss, tracked via diff --git a/tests/test_deduction_surface.py b/tests/test_deduction_surface.py index f13e584d..94052766 100644 --- a/tests/test_deduction_surface.py +++ b/tests/test_deduction_surface.py @@ -432,3 +432,60 @@ def test_verb_reader_refusal_keeps_prior_honest_surface() -> None: ) assert surface is not None assert "Your premises entail" not in surface + + +def test_existential_is_decided_band_v6_ex() -> None: + """ADR-0261: an existential premise carried through a universal to an + existential conclusion (Darii), authoritatively — the + ``en_exist_universal`` band holds an earned SERVE license.""" + surface = deduction_grounded_surface( + "Every mammal is a vertebrate. Some whales are mammals. " + "Therefore some whales are vertebrates." + ) + assert surface is not None + assert "Your premises entail: some whales are vertebrates" in surface + assert not surface.startswith(_UNVERIFIED_SHAPE_DISCLOSURE) + + +def test_existential_conclusion_does_not_close_the_domain() -> None: + """The mechanism this band adds: every NAMED individual fails the query, + yet the arbitrary element keeps the answer honestly unsettled instead of + claiming refutation.""" + surface = deduction_grounded_surface( + "Vega is a star. Vega is not visible. Therefore some stars are visible." + ) + assert surface is not None + assert "don't settle" in surface + assert "cannot hold" not in surface + + +def test_existential_unknown_discloses_the_no_import_reading() -> None: + surface = deduction_grounded_surface( + "All unicorns are horned. Therefore some unicorns are horned." + ) + assert surface is not None + assert "don't settle" in surface + assert 'as claiming a member exists' in surface + + +def test_existential_unearned_band_would_be_hedged() -> None: + """The en_exist_* bands ride the SAME earned-license gate.""" + surface = deduction_grounded_surface( + "Every mammal is a vertebrate. Some whales are mammals. " + "Therefore some whales are vertebrates.", + license_lookup=lambda band: None, + ) + assert surface is not None + assert surface.startswith(_UNVERIFIED_SHAPE_DISCLOSURE) + assert "Your premises entail: some whales are vertebrates" in surface + + +def test_existential_reader_refusal_keeps_prior_honest_surface() -> None: + """When the existential band ALSO cannot read the argument (here: a + partitive), the pre-existing honest surface is preserved verbatim — the + last band only widens, like every band before it.""" + surface = deduction_grounded_surface( + "Some of the sailors are brave. Therefore some sailors are brave." + ) + assert surface is not None + assert "Your premises entail" not in surface diff --git a/tests/test_exist_argument_reader.py b/tests/test_exist_argument_reader.py new file mode 100644 index 00000000..63726e6e --- /dev/null +++ b/tests/test_exist_argument_reader.py @@ -0,0 +1,271 @@ +"""Band v6-EX (ADR-0261) — existential argument reader contract. + +The reader completes the all/no/some square by widening v5-VP's per-individual +domain with a Skolem WITNESS per existential premise and one ARBITRARY element +per existential conclusion, then lowering an existential conclusion to the +disjunction over that whole domain. It is pure and deterministic. Soundness +rides on the ROBDD engine; these tests pin that the reader hands it the RIGHT +problem — above all that the arbitrary element is present, since without it an +existential conclusion would be "refuted" by domain closure, which is the one +way this lowering could be unsound. +""" + +from __future__ import annotations + +import pytest + +from generate.proof_chain.entail import Entailment, evaluate_entailment_with_trace +from generate.proof_chain.exist import ( + MAX_ATOMS, + MAX_PREMISE_SENTENCES, + ExistArgument, + ExistRefusal, + read_exist_argument, +) +from generate.proof_chain.shape import ( + EN_EXIST_CHAIN, + EN_EXIST_NEGATIVE, + EN_EXIST_UNIVERSAL, + EN_EXIST_WITNESS, +) +from generate.proof_chain.verb import VerbRefusal, read_verb_argument + + +def _read(text: str) -> ExistArgument: + arg = read_exist_argument(text) + assert isinstance(arg, ExistArgument), arg + return arg + + +def _refusal(text: str) -> ExistRefusal: + ref = read_exist_argument(text) + assert isinstance(ref, ExistRefusal), ref + return ref + + +def _decide(text: str) -> Entailment: + arg = _read(text) + return evaluate_entailment_with_trace(arg.premise_formulas, arg.query_formula).outcome + + +# --- the gap this band fills is real ----------------------------------------- + + +def test_the_gap_this_band_fills_is_real() -> None: + """Every earlier fallback band refuses a ``some``-led sentence (v5-VP is + the last of them, via ``quantifier_out_of_band``); this band reads it. + Both facts hold at once — v5-VP is unchanged, this is a new tier.""" + text = "All mammals are vertebrates. Some whales are mammals. Therefore some whales are vertebrates." + v5 = read_verb_argument(text) + assert isinstance(v5, VerbRefusal) and v5.reason == "quantifier_out_of_band" + assert isinstance(read_exist_argument(text), ExistArgument) + + +# --- the flagship reading ----------------------------------------------------- + + +def test_flagship_darii_lowering() -> None: + arg = _read( + "All mammals are vertebrates. Some whales are mammals. " + "Therefore some whales are vertebrates." + ) + assert arg.band == EN_EXIST_UNIVERSAL + # The universal instantiates at BOTH domain elements (witness + arbitrary); + # the existential premise is the witness conjunction; the query is the + # disjunction of the conclusion's conjunction over the whole domain. + assert arg.premise_formulas == ("(a0) -> (a1)", "(a2) -> (a3)", "(a4) & (a0)") + assert arg.query_formula == "((a4) & (a1)) | ((a5) & (a3))" + assert arg.atoms == ( + "witness 1 : mammals", + "witness 1 : vertebrates", + "any individual : mammals", + "any individual : vertebrates", + "witness 1 : whales", + "any individual : whales", + ) + assert _decide( + "All mammals are vertebrates. Some whales are mammals. " + "Therefore some whales are vertebrates." + ) is Entailment.ENTAILED + + +def test_arbitrary_element_keeps_the_domain_open() -> None: + """THE soundness test. Every NAMED wolf here fails to be tame, so a + witness-only lowering would report REFUTED — asserting that no wolf + anywhere is tame. The arbitrary element is what makes the honest UNKNOWN + come out, and it must be visibly in the atom set.""" + text = "Rex is a wolf. Rex is not tame. Therefore some wolves are tame." + arg = _read(text) + assert "any individual : wolf" in arg.atoms + assert "any individual : tame" in arg.atoms + assert _decide(text) is Entailment.UNKNOWN + + +def test_no_existential_import() -> None: + """A universal says nothing about whether its class has members — the + subaltern moods are UNKNOWN under the modern reading this band uses.""" + assert _decide("All unicorns are horned. Therefore some unicorns are horned.") is ( + Entailment.UNKNOWN + ) + + +@pytest.mark.parametrize( + "text", + [ + # A and O are contradictories — the A-form refutes the O-form. + "All squares are rectangles. Therefore some squares are not rectangles.", + # E and I are contradictories — the E-form refutes the I-form. + "No fish are mammals. Therefore some fish are mammals.", + ], +) +def test_contradictories_of_the_square_refute(text: str) -> None: + assert _decide(text) is Entailment.REFUTED + + +def test_witness_never_transfers_to_a_named_individual() -> None: + text = "Some sailors are brave. Magellan is a sailor. Therefore Magellan is brave." + assert _decide(text) is Entailment.UNKNOWN + + +def test_each_existential_premise_gets_its_own_witness() -> None: + arg = _read( + "Some wolves are tame. Some wolves are swift. Therefore some tame are swift." + ) + assert "witness 1 : wolves" in arg.atoms + assert "witness 2 : wolves" in arg.atoms + # Two witnesses + the arbitrary element ⇒ three query disjuncts. + assert arg.query_formula.count("|") == 2 + assert _decide( + "Some wolves are tame. Some wolves are swift. Therefore some tame are swift." + ) is Entailment.UNKNOWN + + +def test_a_named_individual_can_be_the_witness() -> None: + assert _decide( + "Socrates is a philosopher. Socrates is wise. Therefore some philosophers are wise." + ) is Entailment.ENTAILED + + +def test_i_form_converts() -> None: + arg = _read("Some philosophers are Greeks. Therefore some Greeks are philosophers.") + assert arg.band == EN_EXIST_WITNESS + assert arg.premise_formulas == ("(a0) & (a1)",) + assert arg.query_formula == "((a1) & (a0)) | ((a2) & (a3))" + + +def test_o_form_witness_carries_the_negation() -> None: + arg = _read("Some hermits are not sociable. Therefore some hermits are not sociable.") + assert arg.premise_formulas == ("(a0) & (~(a1))",) + assert arg.query_formula == "((a0) & (~(a1))) | ((a2) & (~(a3)))" + + +def test_verb_existentials_ride_the_verb_atom_family() -> None: + """Ferio over a verb predicate, with the plural ``do not`` O-form that + v5-VP refuses (there it is genuinely ambiguous; under ``some`` it is not).""" + text = ( + "No reptiles nurse young. Some lizards are reptiles. " + "Therefore some lizards do not nurse young." + ) + arg = _read(text) + assert arg.band == EN_EXIST_NEGATIVE + assert "witness 1 : nurse young" in arg.atoms + assert _decide(text) is Entailment.ENTAILED + + +def test_number_linking_applies_inside_existentials() -> None: + """The irregular table (goose/geese) links a singular universal to a plural + existential — the same closed relation v3-MEM earned, no new authority.""" + text = "Every goose is a bird. Some geese are gray. Therefore some birds are gray." + arg = _read(text) + assert "witness 1 : goose" in arg.atoms # both forms landed in ONE group + assert _decide(text) is Entailment.ENTAILED + + +# --- band classification ------------------------------------------------------ + + +@pytest.mark.parametrize( + "text, band", + [ + ("Some poets are Greeks. Therefore some Greeks are poets.", + EN_EXIST_WITNESS), + ("All poets are artists. Some Greeks are poets. Therefore some Greeks are artists.", + EN_EXIST_UNIVERSAL), + ("Some Greeks are poets. All poets are artists. All artists are rare. " + "Therefore some Greeks are rare.", + EN_EXIST_CHAIN), + ("No poets are silent. Some Greeks are poets. Therefore some Greeks are not silent.", + EN_EXIST_NEGATIVE), + ], +) +def test_band_classification(text: str, band: str) -> None: + assert _read(text).band == band + + +# --- typed refusals ----------------------------------------------------------- + + +@pytest.mark.parametrize( + "text, reason", + [ + ("Some of the sailors are brave. Therefore some sailors are brave.", + "partitive_out_of_band"), + ("Some sailors were brave. Therefore some sailors are brave.", + "tense_out_of_band"), + ("Some sailors did not return. Therefore some sailors return.", + "tense_out_of_band"), + # Singular agreement under a plural existential subject is not read. + ("Some sailors does not sail. Therefore some sailors sail.", + "sentence_shape_out_of_band"), + ("Some old sailors whittle driftwood. Therefore some sailors whittle driftwood.", + "sentence_shape_out_of_band"), + ("If some sailors are brave then the ship sails. Some sailors are brave. " + "Therefore the ship sails.", + "mixed_structure_out_of_band"), + ("Most sailors are brave. Therefore some sailors are brave.", + "quantifier_out_of_band"), + ("Some sailors are brave. Therefore all sailors are brave.", + "universal_conclusion_out_of_band"), + ("Some sailors are brave. Do some sailors sing?", "question_sentence"), + # Delegated v3-MEM / v5-VP parses keep their own typed refusals. + ("Some sailors who fish are brave. Therefore some sailors are brave.", + "relative_clause_out_of_band"), + ("Some sailors are the crew. Therefore some crew are sailors.", + "definite_description_out_of_band"), + ("All sailors do not sail. Some sailors are brave. Therefore some sailors sail.", + "internal_negation_unread"), + # An argument with no existential at all is never decided here + # (defensive closure — those texts belong to v3-MEM / v5-VP). + ("Socrates is a man. All men are mortal. Therefore Socrates is mortal.", + "sentence_shape_out_of_band"), + ], +) +def test_typed_refusals(text: str, reason: str) -> None: + assert _refusal(text).reason == reason + + +# --- honesty caps ------------------------------------------------------------- + + +def test_premise_cap_refuses_not_truncates() -> None: + body = " ".join(f"Zed{i} naps." for i in range(MAX_PREMISE_SENTENCES + 1)) + ref = _refusal(body + " Therefore some sailors nap.") + assert ref.reason == "too_many_premises" + + +def test_atom_cap_refuses_not_truncates() -> None: + """Existential conclusions mint up to two atoms per domain element, so the + cap binds on the query too — and refuses rather than dropping a disjunct + (a dropped disjunct is exactly how a false REFUTED would appear).""" + body = " ".join(f"Some crews{i} are brave." for i in range(8)) + ref = _refusal(body + " Therefore some crews0 are swift.") + assert ref.reason in ("too_many_atoms", "too_many_premises") + + +# --- determinism -------------------------------------------------------------- + + +def test_reading_is_deterministic() -> None: + text = "All poets are artists. Some Greeks are poets. Therefore some Greeks are artists." + assert read_exist_argument(text) == read_exist_argument(text) + assert MAX_ATOMS == 24 and MAX_PREMISE_SENTENCES == 16 diff --git a/tests/test_meaning_graph_projectors.py b/tests/test_meaning_graph_projectors.py index 8fe22459..bfc7c48c 100644 --- a/tests/test_meaning_graph_projectors.py +++ b/tests/test_meaning_graph_projectors.py @@ -68,6 +68,20 @@ def test_to_syllogism_none_for_membership_only() -> None: assert to_syllogism(_comp("Rhea is a raven.")) is None +def test_to_syllogism_refuses_rather_than_dropping_an_unreadable_premise() -> None: + """ADR-0261 §5. A singular ``member`` premise alongside categorical ones + used to be FILTERED OUT, leaving a strictly weaker argument that the + oracle then answered: this text's only witness vanished and serving + replied "that doesn't follow" — a wrong answer, not a decline. Refusing + hands the argument to the reader bands that can hold a singular fact.""" + comp = _comp( + "Aristotle is a philosopher. All philosophers are scholars. " + "Therefore some scholars are philosophers." + ) + assert any(r.predicate == "member" for r in comp.meaning_graph.relations) + assert to_syllogism(comp) is None + + # --------------------------------------------------------------------------- # # to_total_ordering # --------------------------------------------------------------------------- #