Predicates

A predicate says what is true about a symbol or between symbols.

predicate reviewed(by: symbol)
 
proposal is :reviewed(:ada) = report
design before launch
parcel inside district

There is one concept with two shapes:

• a unary predicate applies to one symbol: proposal is :reviewed;
• a binary predicate relates two symbols: design before launch.

predicate is the canonical declaration word. Read structured state through PREDICATES(x) or x.predicates, and traverse all extensional Predicate state through MODEL.PREDICATES. The older tag and relation declarations, TAGS(x), x.tags, and MODEL.TAGS remain accepted compatibility names; they expose Predicate state rather than a separate language concept.

Unary predicates

A fieldless unary predicate is open and needs no declaration:

invoice is :urgent :approved = total
ready = invoice is :approved

Declare a schema when the predicate carries fields:

predicate reviewed(by: symbol, score: number)
 
proposal is :reviewed(:ada, 0.95) = report
reviewer = proposal.predicates.reviewed.by
score = PREDICATES(proposal).reviewed.score

The optional article in is a :reviewed or is an :approved is readability sugar. Predicates attach to the authored symbol, not its current value, so they do not flow through arithmetic or aliases to a different symbol.

Structured predicates are single-valued by default. Use many by (...) when a symbol may retain several identified instances:

predicate reviewed(id: symbol, by: symbol) many by (id)
 
proposal is :reviewed(:r1, :ada) :reviewed(:r2, :lin) = report
reviewers = proposal.predicates.reviewed.by  # [:ada, :lin]

Rules mutate unary predicates with the ordinary compound surface:

WHEN approved THEN
  proposal += :reviewed(:r3, :sam)
END
 
WHEN retracted THEN
  proposal -= :reviewed(:r1)
END

For many, += upserts by the declared identity, keyed -= removes one identity, and bare -= removes every instance. All reads and the unified MODEL.PREDICATES graph update reactively. MODEL.TAGS exposes the same live unary membership through its compatibility view.

Derived predicates

Define truth once and query it anywhere:

predicate releasable means
  reviewed
  AND NOT blocked
  AND EVERY dependency IS :releasable

The subject is implicit throughout a predicate ... means definition. Bare reviewed means “the subject is reviewed,” and a subjectless graph quantifier starts from that same subject. The explicit unification form releasable(x) := ... remains accepted for generated and advanced source, but it is not the canonical authoring form.

A derived predicate answers the same reads an asserted one does. service IS :releasable, MUST(service IS :releasable), and service.predicates.releasable all report the derived truth, and all of them re-derive when a fact underneath them changes. The only requirement is that the subject be a symbol or cell — a derived predicate is a property of an authored symbol, so reading one off a computed expression is a compile error rather than a silent FALSE.

A rule may refer to fieldless or structured predicate state. Structured payloads remain available through .predicates, while logical inference observes their presence.

Rules range over the finite symbols in the model. Ordinary recursive predicate components use the least fixed point. A mutually recursive component whose recursive dependencies occur through EVERY uses one greatest fixed point, which is the useful reading for dependency cycles: a cycle is releasable only while every member satisfies the local conditions. Fixed-point polarity is decided for the complete predicate dependency component, never one rule in isolation. Mixed inductive/coinductive recursion and negative recursive cycles are rejected instead of receiving order-dependent meaning.

Rules and laws may live in .gs libraries. Facts and checked conclusions are model state, so they remain in .grid files.

Grid ships one deliberately small policy vocabulary:

USE "shared/governance.gs" AS policy
 
service is :reviewed(:operations) = 1
ready = MUST(service IS :releasable)

It defines structured reviewed and blocked predicates, recursive releasable, and transitive dependency. The module supplies vocabulary and policy only; each model continues to own its facts, evidence, and decisions.

Predicate laws

Binary predicates may declare their algebra in ordinary language:

predicate touches is symmetric
predicate contains is inverse of inside
predicate before is transitive AND asymmetric
predicate owner is functional

• symmetric derives the reverse fact;
• inverse of links two predicates in opposite directions;
• transitive closes chains;
• asymmetric rejects a reverse pair or self-edge;
• functional permits at most one object for each subject.

The predicate introducer explicitly selects an open logical predicate when a name is also used by a qualitative family. A legacy bare declaration such as before is transitive is rejected; without the introducer, before retains its built-in temporal meaning. Put that declaration before its facts and queries, so every use has the same meaning from the moment it is read.

Graph quantifiers

Quantifiers operate directly over binary predicate facts and explicit model relationships:

has_vulnerability =
  EXISTS dependency OF service WHERE dependency IS :vulnerable
 
approved = EVERY predecessor OF release IS :approved
 
safe = NO path VIA flow* FROM public_input TO secret_output AVOIDS :sanitized
 
path publication = ingress THEN (transform OR archive)* THEN store
 
published = MUST(public_input publication ledger)
sensitive = EXISTS publication OF public_input IS :sensitive
 
sealed = NO path VIA publication
  FROM public_input TO secret_output AVOIDS :sanitized
 
exposed = REACHABLE VIA publication FROM public_input
 
upstream_safe = NO path VIA REVERSE flow
  FROM secret_output TO public_input AVOIDS :sanitized

EXISTS needs one matching neighbor. EVERY is vacuously true when there are no matching neighbors. NO path ... AVOIDS :p removes nodes carrying :p, then checks whether the selected path can still connect the endpoints.

Path expressions stay deliberately small:

• a THEN b follows a, then b;
• a OR b accepts either route;
• a* accepts zero or more a steps;
• REVERSE a follows a backward;
• parentheses group a route.

path name = ... gives a route a reusable name. It is compile-time vocabulary: the compiler expands the route, so it adds no new runtime state. Path declarations may live in .gs libraries and import through their module alias. Declarations are lexical: a name denotes a route from its declaration forward; earlier uses denote an ordinary relationship with that name. A declared route shadows that relationship in later path expressions. This makes path flow = flow* the natural way to name a closure without losing access to the underlying flow relationship on the declaration's right-hand side. Duplicate local names and colliding flat imports are errors; aliased imports remain namespaced.

After its declaration, the name is also a read-only binary predicate. It can appear anywhere a logical relation can be queried: in MUST, MAY, CANNOT, EVIDENCE, rule bodies, and EXISTS/EVERY. Its truth is closed over the current graph projection: a matching route supports the atom; no matching route refutes it. Path predicates cannot be asserted as facts, used as rule heads, or given independent laws—the route is their complete definition. They remain lazy: using one does not materialize an all-pairs relation.

REACHABLE VIA route FROM origin returns the sorted symbols accepted by the route. Omitting VIA selects dependency*; an optional AVOIDS :p excludes nodes carrying that predicate during traversal.

The precedence is *, REVERSE, THEN, then OR. Every relation is one edge; repetition is always explicit in canonical source. Write VIA flow* for zero or more flow edges. Bare VIA flow remains accepted for Predicate v3 compatibility, and gridctl fmt rewrites it to VIA flow*. The shorter NO path FROM ... form selects dependency reachability. Unnamed or unrelated logical facts never become path edges.

The model dependency projection supplies the natural binary predicates dependency(x, y) and predecessor(x, y), both read as “y is an immediate input of x.” Explicit relationship labels and directly authored facts keep their own names.

Facts, conclusions, and modalities

Arbitrary facts need no schema declaration:

service depends_on api
api depends_on database
predicate blocked(reason: string)
database is :blocked(reason: "migration")

That structured fact is the same predicate attachment used by database.predicates.blocked.reason, reactive mutation, and the Predicate graph; inference does not copy it into a payload-free Boolean atom. A named literal payload can establish a local single-valued schema, but an explicit declaration is clearer and required for nonliteral fields or reusable modules.

therefore checks a conclusion. It does not assume it:

predicate at_risk means
  blocked
  OR EXISTS depends_on IS :at_risk
 
therefore service IS :at_risk

A fully static failed conclusion is a compile-time contradiction. A conclusion that depends on live predicate state is checked on each revision and fails its component atomically.

At top level, modalities declare constraints:

MUST(design before launch)
MAY(shipment arrive_before deadline)
CANNOT(account access secret)

On the right of an assignment they ask a question:

required = MUST(design before launch)
allowed = MAY(shipment arrive_before deadline)
forbidden = CANNOT(account access secret)
evidence = EVIDENCE(account access secret)

Open logical predicates keep support and refutation as independent evidence bits. That gives four states: neither, supported, refuted, and both. EVIDENCE(atom) returns that stable lowercase state name. MUST projects the support bit, CANNOT projects the refutation bit, and MAY is true when the refutation bit is absent. Failure to prove a proposition leaves it at least unsupported; it does not manufacture refutation.

General MAY, CANNOT, and EVIDENCE query one ground atomic proposition. MUST may check a compound proposition because entailment already has ordinary logical meaning. Top-level modal declarations are atomic facts, permissions, or refutations; EVIDENCE is a query, not a declaration.

A top-level MUST adds an entailed fact, MAY records permission without entailing it, and CANNOT records a prohibition. Assigned forms only query the current state. Support and refutation of the same atom produce both without explosion and without invalidating the component. Permission plus refutation, violated asymmetric/functional laws, and failed conclusions remain integrity contradictions isolated to their predicate dependency component, so independent publications continue to evaluate normally. Symmetric and inverse laws preserve refutation in the reverse direction; transitivity does not use contraposition.

Evidence may also be authored as attributable, time-bounded events:

EVIDENCE qa_42 SUPPORTS (release approved deployment) BY qa OBSERVED 1721426400000 VALID FROM 1721422800000 UNTIL 1721512800000
EVIDENCE sec_9 REFUTES (release approved deployment) BY security
EVIDENCE correction SUPPORTS (release approved deployment) BY security SUPERSEDES sec_9
EVIDENCE withdrawal RETRACTS correction BY security
EVIDENCE AS OF 1721430000000

The canonical event forms are SUPPORTS (...) BY authority, REFUTES (...) BY authority, and RETRACTS claim_id BY authority. An atom-bearing event may also repeat RETRACTS claim_id or SUPERSEDES claim_id after the authority. Times are signed Unix milliseconds. OBSERVED is provenance; VALID FROM … UNTIL … controls whether the event participates at EVIDENCE AS OF. Without an AS OF coordinate, validity is retained but not filtered.

Claim ids are unique and may only target earlier claims. Retraction is itself an event: retracting a retraction restores the original claim. WHY keeps supporting and refuting roots separate, including authority, observation and validity coordinates, source order, and source span. Derived rule/law lineage continues from those roots in the ordinary proof DAG.

The runtime also accepts the same events without recompiling source. The appendPredicateEvidence RPC is optimistic and append-only: callers provide an expectedRevision, event identity, optional ground atom and polarity, validity coordinates, and retraction/supersession targets. For durable HTTP models Grid first fsyncs a prepared intent, assigns the authenticated actor and observation time at the server boundary; client-sent values for either field are ignored. It then assigns source order after compiled events, updates the indexed retraction overlay, validates the compact active Predicate module, and advances the stateless and incremental lanes together. Use getPredicateEvidenceJournal for export, or getPredicateEvidenceJournalPage(modelId, afterRevision, limit) for bounded history reads, and replayPredicateEvidence for atomic recovery. A stale revision, duplicate id, ambiguous Predicate region, or invalid target leaves both the model and journal unchanged.

HTTP-hosted models persist accepted events themselves in the model home's predicate-evidence/ segmented WAL and restore reduced activation/blocker state from its semantic checkpoint plus only the committed tail before serving the model after a restart or residency reload. Covered segments remain as immutable paginated cold history. The atomically published manifest, not raw segment length, defines the visible revision. Clients may still read and export the journal, but they are not responsible for making ordinary evidence edits durable. Records carry a schema version, model id, source hash, and event checksum so copied, corrupted, or misrouted journals fail closed while preserving the compile lineage under which each event was accepted. On a source change, Grid replays the complete audit history against the recompiled model and updates the lineage only after that validation succeeds. Legacy predicate-evidence.jsonl bare-event and v1 envelope records remain readable for migration. Cell Explain can add supporting/refuting evidence and retract an attributable claim directly; an optimistic conflict refreshes the journal head before the user retries. Mutations echo the explained Predicate region id, so the same predicate name in independent regions is never edited ambiguously.

Cell Explain shows the represented journal revision, active four-state roots, authorities, downstream publication cells, and the complete relevant event timeline—including inactive retractions and supersessions.

The evaluator derives evidence-aware graph results from that DAG: contradiction hotspots (both), queried atoms with missing evidence (neither), direct evidence roots mapped to downstream publication cells, and uncontested MUST/CANNOT decisions. Retained evaluation emits exact previous → current evidence transitions with those downstream cells, so a subscriber does not diff complete fixed points.

MODEL.PREDICATES projects every atom-bearing evidence claim as a parallel edge. Its properties include predicate, claim_id, authority, polarity, active, observed_at, valid_from, valid_until, and source metadata. Unary claims are self-loops. Both polarities remain visible, making hotspots a normal multigraph motif instead of a destructive conflict collapse.

The finite temporal, topological, and conceptual-set families retain their sharper possible-relation-set meanings described below.

Temporal predicates

A bare clause asserts a fact. The same clause on the right of an assignment is a definite query:

design before build
build before launch
 
ready = design before launch  # TRUE by inference

Temporal phrases always read from the subject interval X to the object interval Y:

• X before Y ends before Y begins; after is its converse.
• X meets Y ends exactly when Y begins; met by is its converse.
• X overlaps Y begins first and ends inside Y; overlapped by is its converse.
• X starts Y begins with Y and ends first; started by is its converse.
• X during Y begins later and ends earlier; contains is its converse.
• X finishes Y begins later and ends with Y; finished by is its converse.
• X equals Y has the same beginning and end.

These thirteen cases are exhaustive for non-empty intervals. The inverse phrases are ordinary spaced language; the older finished_by, started_by, overlapped_by, and met_by spellings remain accepted for compatibility.

Facts may be qualitative, derived from values, or both. INTERVAL(start, end) creates a nonempty numeric, date, or datetime interval. When interval-valued symbols participate in a temporal component, Grid derives their exact relation from the live endpoints and intersects it with any authored facts:

design = INTERVAL(@2026-07-01, @2026-07-05)
build = INTERVAL(@2026-07-05, @2026-07-12)
 
ready = design meets build       # TRUE
where = RELATION(design, build)  # meets
family = where.family            # temporal

Endpoint changes recompute the same predicate component. Start must precede end, and both endpoints must use the same representation. Use explicit MUST(x overlaps y) when overlaps could otherwise be read as the collection operator in an ordinary expression.

Topological predicates

Topology uses ordinary spatial language:

island separate from mainland
porch touches house
meadow partially overlaps floodplain
copy coincides with original
parcel inside district
district encloses parcel
road intersects property

inside, encloses, and intersects are useful broad predicates. Refine containment only when boundary contact matters:

shed inside lot with boundary contact
house inside lot without boundary contact
lot encloses shed with boundary contact
lot encloses house without boundary contact

encloses is the topological converse of inside. Grid deliberately does not reuse contains here because contains already has temporal and collection meanings.

Native regions ground the same predicates directly:

parcel = GEOM_FROM_WKT("POLYGON((0 0, 1 0, 1 1, 0 1, 0 0))")
district = GEOM_FROM_WKT("POLYGON((-1 -1, 2 -1, 2 2, -1 2, -1 -1))")
 
within = parcel inside district without boundary contact  # TRUE
where  = RELATION(parcel, district, topology)

Polygon and MultiPolygon values are regular closed regions and participate reactively without a conversion function or separate declaration. Both values must use the same EPSG coordinate system. Points, lines, invalid regions, and mixed coordinate systems fail closed rather than being forced into a spatial meaning they cannot support.

Conceptual set predicates

Predicates can relate the membership extents of cohorts, categories, scopes, or any other conceptual sets without enumerating their members:

vip_customers included in active_customers
active_customers includes vip_customers
employees disjoint from contractors
campaign_a overlaps with campaign_b
audience_a same members as audience_b

included in and includes allow equal membership. Add strictly when the larger extent must contain at least one additional member:

trial_customers strictly included in active_customers
active_customers strictly includes trial_customers

overlaps with means the sets share at least one member. partially overlaps with additionally says that each has members outside the other. disjoint from means they share none. same members as includes the case where both sets are empty.

Empty extents are part of the algebra rather than an error or an unstated nonempty assumption. This keeps authored facts sound when a live cohort later has no rows.

When both names hold values, Grid reads their current members directly:

vip = VECTOR("Ada", "Grace")
active = VECTOR("Ada", "Grace", "Linus")
ready = vip strictly included in active

Ordinary collections and Graph projections work the same way. For example, MODEL.PREDICATES.NEIGHBORS(:reviewed) can be named and compared without a new conversion or predicate declaration. If either value changes, the relationship is grounded again before dependent results are published.

Grounding fails closed. If a live interval, region, or extent is an error, the connected predicate component publishes that same error instead of quietly treating the fact as absent. Independent components continue normally, and the component recomputes as soon as the value becomes valid.

The word with is meaningful: it distinguishes conceptual-set overlaps with from temporal overlaps, topological partially overlaps, and the ordinary collection OVERLAPS operator.

Alternatives, uncertainty, and reactivity

Alternatives and complement work within the selected predicate family:

packing (before OR meets) pickup
parcel (separate from OR touches) park
parcel (NOT separate from) preserve

Plain queries mean MUST. Use the explicit modalities when uncertainty is part of the model:

certain = MUST(parcel touches park)
possible = MAY(parcel partially overlaps park)
ruled_out = CANNOT(parcel separate from park)

Facts may use ordinary reactive conditions:

parcel separate from park UNLESS connected
parcel touches park IF connected

Changing connected recomputes the affected predicate component and its downstream cells atomically.

Inspection and explanation

RELATION returns the possibilities left after finite-family inference as a first-class relation_set, not formatted text. Its stable fields are family, state, and relations; ordinary display uses the same natural phrases as source. For example, a singleton converse displays finished by while its stable relation identifier is finished_by. RELATION_STATUS reports realizable after exact bounded scenario search, unrealizable when the complete search has no model, undetermined when its budget expires, or contradictory when algebraic closure directly finds an empty relation. WHY explains the active authored facts and retained inference steps. Bind the result once:

where = RELATION(shed, lot)
state = RELATION_STATUS(shed)

Then inspect it without adding provenance to model state:

gridctl cell why <model-id> where

For a derived logical proposition, the same pattern applies:

risk = MUST(service IS :at_risk)

gridctl cell why <model-id> risk

The proof contains authored facts, rule and law steps, graph edges used by quantifiers, and the recursive chain. Thus the conceptual request “why is service at risk?” is served without creating a second explanation language: risk is the ordinary query cell and the provenance root. WHY is a resident inspection command and host/UI API, not a workbook formula; writing proof = WHY(risk) is rejected before lowering.

The family is normally inferred. A selector is needed only if the same symbols belong to more than one qualitative component:

when = RELATION(phase, release, temporal)
where = RELATION(phase, release, topology)
who = RELATION(cohort_a, cohort_b, sets)

Modal queries do not need a selector because their relation phrase already identifies the family.

Graph views

An explicit GraphHandle may also provide the finite grounding domain and extensional binary facts for this program:

KNOWLEDGE GRAPH knowledge VIA edge.relation WITH PROPERTIES
 
predicate reaches is transitive
connected = MUST("origin" reaches "destination")

Every current graph edge becomes a ground binary atom named by the selected string/symbol edge property. String and integer graph identities are accepted directly in logical atoms and remain type-sensitive. This projection is revision-reactive and bounded; it does not copy inferred closure back into the source graph. WITH PROPERTIES also publishes graph_node, graph_edge, graph_node_property, and graph_edge_property facts, including stable edge identity and typed scalar values, for indexed joins in ordinary rules. Repeated resolution caches the materialized fact program by Predicate region and the exact ordered set of resident GraphHandle revisions. A graph patch invalidates both the inferred result and that materialization; target-only queries reuse both. WHY retains the exact graph revision and contributing edge identities, and its knowledgeFacts collection also identifies graph_node and graph_node_property premises that have no edge ID. See Graph computing.

Graph-backed REACHABLE returns ordinary authored values, never Predicate's internal identity encoding. String nodes return strings and integer nodes return exact bigint values, including identities outside the lossless f64 range. Their distinct internal identities remain intact during inference. WHY renders those nodes with unambiguous source spelling and retains the stable graph edges used by each witness route.

The built-in graph views keep knowledge distinct from model topology:

• MODEL.PREDICATES projects current unary-predicate membership and authored binary facts, including open logical facts;
• MODEL.TAGS is the unary-only compatibility view;
• MODEL.GRAPH remains model dependencies and explicit relationships.

MODEL.PREDICATES does not expand inferred closure into edges. Ask the predicate engine through a plain query, MUST, MAY, CANNOT, RELATION, or WHY when inferred knowledge is required.

Predicate inference is bounded. If a component exceeds its admitted size or work budget, Grid reports that limit explicitly rather than returning an incomplete answer as though it were definitive. WHY retains bounded, deterministic proof detail for the result it explains. For NO path, that detail is a checked product-frontier certificate when the proposition is true and an ordered counterexample route when it is false. If the explanation budget cannot retain the complete frontier, the Boolean result remains exact and WHY falls back to bounded path-cut evidence rather than presenting a partial certificate as complete. The displayed explanation remains natural — for example, “no matching route reaches the target without crossing :sanitized” — while the certificate stays available as structured evidence. WHY on REACHABLE reports the result count and a concrete witness route for each returned symbol while the explanation budget permits. The witness set states whether it is complete. If it is truncated, the returned symbols remain exact; only the optional explanation is partial.

Connected rules use indexed joins and incremental fixed-point rounds; authors do not select an execution strategy. In a resident model, resolving another query reuses the same inferred facts and proofs until a condition, bound family value, or unary predicate read by that component changes. This does not weaken reactivity: a relevant change invalidates the component before its next result is published.

Complete example

examples/canonical/17-predicate-knowledge.grid is an executable model of the unified surface: structured unary predicates, recursive model reasoning, authored relationships, property-graph facts, transitive inference, reachability, MODEL.PREDICATES, evidence, and graph-edge provenance all participate without a second reasoning language.