Language Reference

Status: Current v0.5 canonical

Practical cheat sheet for the Gaia Language v0.5 Python DSL. For the generated API reference, see Gaia Lang DSL API.

Package Structure

Every Gaia package is a Python project with this layout:

my-package-gaia/
  pyproject.toml              # [tool.gaia] metadata
  src/my_package/
    __init__.py               # package entrypoint and export surface
    motivation.py             # module: settings + questions
    s2_methods.py             # module: methods and setup
    s3_results.py             # module: claims + strategies
  artifacts/                  # source material (PDF, markdown)
  .gaia/                      # compiled output (created by gaia build compile)
    ir.json
    ir_hash

pyproject.toml — package manifest:

[project]
name = "my-package-gaia"
version = "1.0.0"
requires-python = ">=3.12"

[tool.gaia]
type = "knowledge-package"
uuid = "..."                  # auto-generated by gaia build init

[build-system]
requires = ["hatchling"]
build-backend = "hatchling.build"

__init__.py — imports package modules and declares the package export surface:

from .motivation import *
from .s2_methods import *
from .s3_results import *

The package root __all__ is the curated cross-package interface: names listed there are exported into the compiled package manifests. Each name must resolve to a local Knowledge object through normal root-module attribute lookup, and the public name must match the object's Gaia label. Returned relation helpers from equal, contradict, exclusive, and associate are still Knowledge objects; if exported, the manifest marks them as typed relation interfaces. Empty or missing root __all__ means no exported public surface. Sibling modules may also carry their own literal __all__ blocks when they are CLI authoring targets: gaia pkg add-module creates __all__: list[str] = [], and gaia author --file <module.py> --export can insert new bindings into that module's list. Keep these lists literal and static; the CLI intentionally does not edit dynamically constructed __all__ values.

Migration (breaking). Root __all__ is now strictly validated at load / compile time. A package whose root __all__ lists a strategy (deduction(...), support(...), composites), a fills(...)/bridge relation, a name imported from a dependency package, an aliased Knowledge (export name ≠ label), an implicit Formula / BoolExpr operand-lift helper, or a typo now fails with a GaiaPackagingError that names the offending entry. Older loaders silently ignored such names. To migrate, drop everything that is not a local headline claim or explicitly public relation helper from root __all__ and run gaia build compile <pkg>. See Curated Package Exports Design.

Imports

from gaia.engine.lang import (
    claim, note, question, artifact, figure,                # Knowledge
    Variable, Nat, Real, Probability, Bool,                 # Formula terms
    parameter,                                              # Structured formula claims
    ClaimAtom, land, lnot, lor, implies, iff, equals,       # Propositional formula helpers
    forall, exists,                                         # First-order quantifiers
    contradict, equal, exclusive, associate,                # Reviewable relations
    depends_on, candidate_relation, materialize,            # Scaffold annotations
    observe, derive, compute, infer, decompose,             # Recommended actions
    compose, composition,                                   # Action composition
    register_prior,                                         # External prior records
    Normal, LogNormal, Beta, Exponential, Gamma,            # Distribution factories
    StudentT, Cauchy, ChiSquared, Binomial, Poisson,
    Distribution, BoolExpr, DerivedDistribution,            # Continuous helpers
)

import gaia.engine.bayes as bayes                           # Bayes hypothesis comparison

For unit-aware continuous quantities, import quantities from gaia.unit:

from gaia.unit import q

For the full enumerated public surface (every symbol, with signatures and docstrings), see the auto-generated gaia.engine.lang API reference. This page focuses on how to choose the right action and what each one compiles to; the reference page is the source of truth for parameter names and types.

Knowledge Types

`note(content, *, title=None, format="markdown", **metadata)`

Background context. No probability, does not participate in BP. Use for: math definitions, experimental conditions, established principles.

setup = note("A ball is dropped from 10m height in vacuum.")
definition = note("Let G = 6.674e-11 N m^2 kg^-2.")

Referenced via background= on claims or strategies, never as premises.

setting(...) and context(...) remain available only as deprecated compatibility aliases for note(...).

`question(content, *, title=None, **metadata)`

Open inquiry. No probability, does not participate in BP.

q = question("What is the critical temperature of this material?")

`claim(content, *, title=None, background=None, parameters=None, provenance=None, **metadata)`

The only type that carries probability in BP. Use for anything that can be questioned or falsified.

# Simple claim
tc = claim("Tc of MgB2 is 39K.")

# Claim with background context
result = claim(
    "The ball reaches the ground in 1.4s.",
    background=[experimental_setup, newtonian_gravity],
)

# Claim with title
titled = claim("H = p^2/2m + V(x)", title="Hamiltonian of the system")

Content supports markdown: tables, $...$ math, bullet points, bold/italic.

References, Citations, and Artifacts

Use references.json for external sources and [@key] markers in prose:

{
  "Aspect1982": {"type": "article-journal", "title": "Experimental Realization"}
}

bell_test = claim("Bell inequalities are violated in experiment [@Aspect1982].")

[@key] is strict: if the key is neither a references.json citation key nor a local Gaia label, compile fails. Bare @key is opportunistic and remains literal when unresolved. Citation keys and local labels share one namespace, so a package must not define both Aspect1982 in references.json and a local Aspect1982 = claim(...).

Use local labels for Gaia knowledge references:

setup = note("The experiment uses spacelike-separated polarization analyzers.")
result = claim("The conclusion depends on the setup [@setup].", background=[setup])

Use artifact notes for figures, tables, datasets, notebooks, and attachments. Artifacts are still note(...) nodes; figure(...) and artifact(...) only create structured metadata["gaia"]["artifact"] for you:

liu2015_fig3 = figure(
    source="Liu2015",
    locator="Fig. 3",
    path="artifacts/figures/liu2015_fig3.png",
    caption="Fibonacci scaling of the order parameter.",
)

analysis_data = artifact(
    kind="attachment",
    source="Liu2015",
    locator="Supplementary Data 1",
    path="artifacts/attachments/liu2015_supplement.xlsx",
    description="Digitized source data used for the pressure-temperature curve.",
)

claim("The trend follows the source figure [@liu2015_fig3].")

Artifact labels resolve through the same local-label syntax as notes and claims, but compiled provenance records them under artifact_refs, separate from referenced_claims.

Run gaia build check --refs to see a focused citation/local-reference/artifact diagnostic report for a package. In CI, use gaia build check --refs --gate to fail on hard reference findings such as unresolved bare refs, missing artifact files, invalid artifact refs, or legacy reference metadata.

Do not use observe(source_refs=...) for new code; put citation markers in rationale. Also do not put bibliographic citations in claim(provenance=[...]); that field is for Gaia package/version provenance, not paper citations.

Continuous Quantities and Bayes Helpers

Gaia has two related surfaces for probabilistic quantities:

Use Distribution objects when you want to describe one uncertain quantity and make threshold or equation claims about it.
Use gaia.engine.bayes when you want to compare competing hypotheses by the likelihood of observed data under each hypothesis.

These are ordinary Python authoring helpers. They compile into regular Gaia claims, helper claims, metadata, priors, and reviewable relations; they do not introduce a separate IR dialect.

Distribution factories

The top-level gaia.engine.lang import exposes named distribution factories: Normal, LogNormal, Beta, Exponential, Gamma, StudentT, Cauchy, ChiSquared, Binomial, and Poisson.

Use them when the uncertain object is a scalar quantity:

from gaia.engine.lang import Normal, claim, register_prior
from gaia.unit import q

T_c = Normal("T_c of H3S at 200 GPa", mu=q(200, "K"), sigma=q(50, "K"))

high_Tc = claim(
    "The material is high-temperature superconducting.",
    T_c > q(77, "K"),
)

During compilation, a predicate claim such as T_c > 77 K is lowered through the distribution CDF. Gaia writes a generated prior record with source_id="continuous_inference" on the predicate claim. For the example above, the prior is P(T_c > 77 K) under the declared Normal distribution.

If you have a stronger author judgment for the same predicate, use register_prior(...); the prior resolver will pick the winning source and keep the other records in metadata["prior_records"] for audit:

register_prior(
    high_Tc,
    0.8,
    justification="The reported sample quality makes the CDF-only estimate too optimistic.",
)

Unit rules are strict:

If a distribution has a unit, predicate thresholds must be gaia.unit.q(...) quantities compatible with that unit. Gaia will convert compatible units such as Celsius to Kelvin.
If a distribution is unitless, thresholds must be bare numeric scalars.
Distribution-vs-distribution thresholds are not implemented; compare one distribution against a scalar threshold, or introduce an explicit model.

Continuous observations

observe(...) is polymorphic. With a Claim, it marks the claim as observed. With a Distribution, it records a measurement event and returns a new pinned observation claim:

from gaia.engine.lang import Normal, observe
from gaia.unit import q

T_c = Normal("T_c of H3S at 200 GPa", mu=q(200, "K"), sigma=q(50, "K"))

measured_Tc = observe(
    T_c,
    value=q(203, "K"),
    error=q(5, "K"),
    rationale="Reported superconducting transition temperature [@Drozdov2015].",
)

The returned claim is pinned to 1 - CROMWELL_EPS because the measurement event happened. Its metadata links back to the target distribution and records the measured value, optional error, and unit. error= may be omitted, may be a positive scalar or unit-aware quantity, or may be another Distribution used as a custom noise model.

Continuous observations are unconditional measurement events. Do not pass given= to observe(distribution, value=...); if a measurement depends on a premise, model that premise as a separate claim.

Bayes hypothesis comparison

Use bayes.model(...) and bayes.compare(...) when the problem is not "what is the probability this quantity exceeds a threshold?" but rather "which hypothesis predicts the observed data better?"

import gaia.engine.bayes as bayes
from gaia.engine.lang import Binomial, Nat, Probability, Variable, observe, parameter

theta = Variable(symbol="theta", domain=Probability)
k = Variable(symbol="k", domain=Nat)
n = 395

h_3_1 = parameter(theta, 0.75, describe="Mendelian 3:1 segregation.")
h_null = parameter(theta, 0.5, describe="Null 1:1 segregation.")

data = observe(
    k,
    value=295,
    rationale="F2 count table reports 295 dominant phenotypes.",
)

model_3_1 = bayes.model(
    h_3_1,
    observable=k,
    distribution=Binomial("k under Mendel 3:1", n=n, p=theta),
    rationale="If h_3_1 holds, k follows Binomial(n=395, p=0.75).",
)
model_null = bayes.model(
    h_null,
    observable=k,
    distribution=Binomial("k under null 1:1", n=n, p=theta),
    rationale="If h_null holds, k follows Binomial(n=395, p=0.5).",
)

comparison = bayes.compare(
    data,
    models=[model_3_1, model_null],
    exclusivity="exhaustive_pairwise_complement",
    rationale="Compare the observed count under the two competing models.",
)

bayes.model(...) returns a predictive-model helper claim. bayes.compare(...) returns a comparison helper claim and can also emit reviewable exclusivity or contradiction relations among the compared hypotheses. The exclusivity= argument controls the structural contract and changes the posterior because it changes which joint hypothesis states the factor graph allows:

"exhaustive_pairwise_complement" (default, 2 hypotheses only) — exactly one of the listed hypotheses is true. Posterior odds equal the (Cromwell-clamped) likelihood ratio; this is the standard Bayesian model-selection contract. With three or more hypotheses compare() raises NotImplementedError until an N-ary Exclusive operator lands; pass pairwise_contradiction explicitly for now.
"pairwise_contradiction" — at most one listed hypothesis is true. Pairwise odds are meaningful, but the listed marginals can sum to less than one because the "all-false" joint state carries probability mass. Use this when you do not believe your model set is exhaustive.

compare() deduplicates against same-type external exclusive(...) or contradict(...) declarations covering the same hypothesis pair — if you have already declared the structural action upstream (with its own rationale and background), compare() skips emitting a second helper. Cross-type coexistence is allowed: an external contradict() plus an auto-emitted exclusive() is logically consistent (Exclusive implies Contradict), and the IR's structural-relation consistency checks govern legality of the combined graph.

The example leaves the two hypotheses without external priors. Gaia then uses the maximum-entropy starting point subject to the declared exclusivity relation. If you have an informative source for a hypothesis prior, put it in priors.py with register_prior(...) instead of writing 0.5 just to mean "neutral."

Structured Formula Claims

Formula claim sugar creates ordinary Claim objects with structured formula payloads. The compiler lowers them into today's IR: source claims keep their priors, and primitive bindings become IR parameters.

`parameter(variable, value, *, describe=None, prior=None, ...)`

Use when a claim asserts a primitive variable value.

from gaia.engine.lang import Probability, Variable, parameter

p = Variable(symbol="p", domain=Probability)
mendelian_p = parameter(
    p,
    0.75,
    describe="Mendelian 3:1 segregation fixes P(dominant) at 0.75.",
)

This compiles to a source claim with an IR parameter for p = 0.75 and a serializable formula_bindings metadata entry.

Structured observed values

Use a normal formula claim for structured measured values, then mark it with observe(...). Observation is an action, not a ClaimKind.

from gaia.engine.lang import Constant, Nat, Variable, claim, equals, land, observe

n = Variable(symbol="n", domain=Nat)
k = Variable(symbol="k", domain=Nat)
f2_count = observe(
    claim(
        "Observed 295 dominant phenotypes out of 395 F2 plants.",
        formula=land(equals(n, Constant(395, Nat)), equals(k, Constant(295, Nat))),
    ),
    rationale="Extracted from the reported count table.",
)

The formula bindings still merge onto the source claim as IR parameters. A zero-premise observe(...) pins the claim to 1 - CROMWELL_EPS.

Causal mechanism authoring is intentionally not represented by a marker-only ClaimKind or formula predicate. Until the first-class causal mechanism surface lands, write causal statements as ordinary claim(...) prose and connect their support with reviewable reasoning actions.

Recommended Actions

Actions are how you connect claims. A claim says "this statement may be true or false"; an action says why that claim is observed, derived, related to another claim, or still waiting for more formalization.

The most important habit is to choose the weakest action that honestly matches what you know. Do not hide uncertainty inside prose. If the step is unfinished, mark it as scaffold. If it is logical, make it a hard constraint. If it is probabilistic, write down the probability model that justifies the update.

Choosing the right kind of action

Kind	Functions	Use when	Enters inference?
Scaffold notes	`depends_on`, `candidate_relation`, `materialize`	You know there is a dependency or relation, but you are not ready to make it formal, or you want to link scaffold to its formal record	No. Stored in `.gaia/formalization_manifest.json`
Empirical observations	`observe`	A measurement, data extraction, or reported fact grounds a claim	Yes. A zero-premise observation pins the claim near true
Logical hard constraints	`derive`, `compute`, `decompose`, `equal`, `contradict`, `exclusive`, formula claims	If the premises are true, the conclusion or relation should follow as a matter of logic or definition	Yes. Lowered as deterministic factors
Hand-written probabilistic soft constraints	`infer`, `associate`	You are directly committing to conditional probabilities or an association strength	Yes. Lowered as probabilistic factors
Model-based Bayesian soft constraints	`bayes.model`, `bayes.compare`	The probabilities come from a statistical model, distribution, and observed data	Yes. Lowered to likelihood-style probabilistic factors and reviewable relations
Composed workflows	`@compose`	A Python function groups several actions into one named workflow	The child actions enter inference according to their own kinds

This split exists for a practical reason: reviewers and downstream users need to know what kind of commitment each line makes. A scaffold note says "work remains." A hard constraint says "this relation should always hold." A soft constraint says "this relation changes probabilities, and here is the numeric model." Gaia keeps those roles separate so that unfinished work does not silently become evidence, and probabilistic assumptions do not look like logic.

Scaffold actions: record work that is not formal yet

Use scaffold actions while drafting. They are honest placeholders: they tell Gaia and reviewers that a dependency or relation matters, but they do not add a belief-propagation edge.

from gaia.engine.lang import candidate_relation, claim, depends_on

model_prediction = claim("The model predicts a transition near 200 K.")
reported_result = claim("The experiment reports a transition near 203 K.")
calibration = claim("The thermometer calibration is reliable.")

depends_on(
    reported_result,
    given=[calibration],
    rationale="The result depends on a calibration argument that still needs formalization.",
)

candidate_relation(
    claims=[model_prediction, reported_result],
    pattern="equal",
    rationale="These may describe the same transition after unit and regime checks.",
)

candidate_relation(
    claims=[model_prediction, reported_result],
    pattern="contradict",
    rationale="If the regimes differ, this may become a real disagreement.",
)

Use scaffold actions when you would otherwise write a vague claim like "this is supported somehow." Later, replace them with derive, observe, equal, contradict, associate, or a Bayes model once the relation is precise.

Empirical observations: say what was seen or measured

Use observe(...) for empirical grounding. With no given, it means the claim records an observation or measurement event, so Gaia pins the claim near true using Cromwell's rule. The observation still has a reviewable rationale.

from gaia.engine.lang import claim, observe

reported_count = claim("The paper reports 295 dominant phenotypes out of 395 F2 plants.")

observe(
    reported_count,
    rationale="Extracted from the experiment's count table.",
)

Use observe(distribution, value=..., error=...) when the observed object is a continuous quantity. That form creates an observed claim for the measurement event and records the value, uncertainty, unit, and source metadata.

Do not use observe to mean "I believe this theory." Observations are for data, measurements, extracted facts, and reported results. A theory hypothesis should usually be a normal claim(...) with a prior in priors.py, or left unset so MaxEnt can treat it as neutral.

Logical hard constraints: say what must follow

Use logical actions when the connection is deterministic. The test is simple: if the premises are all true, should the conclusion or relation be true as a matter of logic, definition, or exact computation?

from gaia.engine.lang import claim, contradict, derive, equal

law = claim("In the model, all bodies in vacuum fall with the same acceleration.")
case = claim("The two balls are in vacuum.")
prediction = claim("The two balls hit the ground at the same time.")

derive(
    prediction,
    given=[law, case],
    rationale="Apply the model law to this case.",
)

reported = claim("The experiment reports simultaneous impact.")
equal(
    prediction,
    reported,
    rationale="The predicted and reported qualitative outcome match.",
)

contradict(
    prediction,
    claim("The heavier ball lands earlier in the same setup."),
    rationale="Both outcomes cannot hold for the same pair of balls and setup.",
)

Hard constraints are not priors. Do not assign external priors to helper claims created by equal, contradict, exclusive, formula expressions, or decompose. Inference treats the declared structure as deterministic; review and gaia build check --gate decide whether that structure is publish-quality.

Use decompose(...) when a composite claim has a precise internal truth condition. It is better than making one broad claim with hidden assumptions. It compiles to a generated formula helper plus an equivalence operator, but gaia build check --hole treats the atomic parts as the independent prior candidates and skips the generated helpers.

composite = claim("The model succeeds in the stated regime.")
prediction = claim("The model predicts the observed trend.")
calibration = claim("The calibration applies.")
measurement = claim("The measurement is reliable.")

decompose(
    composite,
    parts=(prediction, calibration, measurement),
    formula=land(ClaimAtom(prediction), implies(ClaimAtom(calibration), ClaimAtom(measurement))),
    rationale="Success means prediction holds, and calibration implies measurement reliability.",
)

Hand-written probabilistic soft constraints: use sparingly

Use infer(...) or associate(...) when the relationship is genuinely probabilistic and you are willing to write the numbers yourself.

infer(...) is directional: a hypothesis predicts evidence with one probability, and the evidence would appear under not hypothesis with another probability.

from gaia.engine.lang import claim, infer, observe

hypothesis = claim("The material follows the proposed mechanism.")
evidence = claim("The observed spectrum shows the predicted peak.")

observe(
    evidence,
    rationale="The peak is extracted from the measured spectrum.",
)

infer(
    evidence,
    hypothesis=hypothesis,
    p_e_given_h=0.9,
    p_e_given_not_h=0.2,
    rationale="The peak is common under the mechanism and rare otherwise.",
)

If p_e_given_not_h is omitted, Gaia uses the neutral background likelihood 0.5 and emits a warning during gaia build check / gaia run infer. This is valid for a least-committal preview, but an explicit false-positive/background rate is preferable when you know it.

associate(...) is symmetric. Use it when neither claim is naturally the hypothesis and neither is naturally the evidence, but the two are statistically linked.

from gaia.engine.lang import associate, claim

high_pressure = claim("The sample was synthesized above 150 GPa.")
high_tc = claim("The sample has a transition temperature above 200 K.")

associate(
    high_pressure,
    high_tc,
    p_a_given_b=0.8,
    p_b_given_a=0.6,
    rationale="In this family, high-Tc reports mostly come from high-pressure samples.",
)

Before using either function, try to extract hidden assumptions into separate claims. If you are tempted to write "this seems likely because many things line up," you probably need more claims and hard relations first. Use a soft constraint only for the remaining numeric uncertainty.

infer(...) returns the evidence claim and creates an internal likelihood warrant for review. associate(...) returns an association helper claim because the association itself is the review target. If that helper is listed in root __all__, .gaia/manifests/exports.json marks it as export_kind="probabilistic_relation" and records the endpoint QIDs plus p_a_given_b / p_b_given_a. These helper claims are not independent probabilistic inputs, so do not put priors on them.

The endpoint claims do not need declared priors solely to make associate(...) lowerable. When both endpoint marginals are missing, Gaia uses a local Jaynes MaxEnt closure for the 2x2 association table and emits a warning recommending register_prior(...) on at least one endpoint. Explicit endpoint priors remain preferable when you know the marginal prevalence; they participate in the usual Bayes-consistency checks.

Model-based Bayesian soft constraints: prefer this for real data likelihoods

Use the bayes module when the probability comes from a statistical model rather than from a hand-written judgment. This is the right tool for questions like "which hypothesis makes this count, measurement, or dataset more likely?"

import gaia.engine.bayes as bayes
from gaia.engine.lang import Nat, Probability, Variable, parameter

theta = Variable(symbol="theta", domain=Probability)
k = Variable(symbol="k", domain=Nat)
n = 395

h_3_1 = parameter(theta, 0.75, describe="Mendelian 3:1 segregation.")
h_null = parameter(theta, 0.5, describe="Null 1:1 segregation.")

data = observe(
    k,
    value=295,
    rationale="F2 count table reports 295 dominant phenotypes.",
)

model_3_1 = bayes.model(
    h_3_1,
    observable=k,
    distribution=Binomial("k under Mendel 3:1", n=n, p=theta),
    rationale="If h_3_1 holds, k follows Binomial(n=395, p=0.75).",
)
model_null = bayes.model(
    h_null,
    observable=k,
    distribution=Binomial("k under null 1:1", n=n, p=theta),
    rationale="If h_null holds, k follows Binomial(n=395, p=0.5).",
)

bayes.compare(
    data,
    models=[model_3_1, model_null],
    exclusivity="exhaustive_pairwise_complement",
    rationale="Compare the observed count under both hypotheses.",
)

Prefer bayes.model(...) + bayes.compare(...) over hand-written infer(...) when you have a real likelihood function. It makes the model, the observable, the data, and the competing hypotheses explicit, which gives reviewers something concrete to inspect.

Return values and priors

Support-like actions (observe, derive, compute, and infer) return the claim they produce or affect. Relation-shaped actions (associate, equal, contradict, and exclusive) return generated helper claims because the relation itself is the public review target. decompose(...) returns the whole claim; its formula structure is attached through lowering, not returned as a separate public claim. Scaffold actions return scaffold records and do not create BP factors.

The returned helpers from associate, equal, contradict, and exclusive may be explicitly exported when the relation belongs in the package interface. Helpers created only by _lift_to_claim to adapt a direct Formula or BoolExpr operand, such as the anonymous helper behind equal(a & b, c), are internal and cannot be exported. Name public formulas yourself with claim(..., formula=...); those explicit formula bindings export as claims, not as returned relation helpers.

External priors belong on independent input claims, usually through priors.py. They do not belong on derived conclusions, helper claims, scaffold records, or deterministic relation helpers.

Operators (Deterministic Constraints)

Structured formula replacements

For new packages, prefer formula claims when you need a structural Boolean expression over existing claims. Propositional connectives auto-wrap referenced Claim operands as ClaimAtom(...), so the compiler can connect the formula truth variable to the existing IR node without extra boilerplate. You can still write ClaimAtom(...) explicitly when you want the bridge to be visible.

from gaia.engine.lang import ClaimAtom, claim, land, lor

not_classical = claim(
    "The classical prediction does not hold.",
    formula=~classical_prediction,
)
joint_case = claim(
    "Both pieces of evidence hold.",
    formula=land(evidence_a, evidence_b),  # equivalent to evidence_a & evidence_b
)
either_mechanism = claim(
    "At least one mechanism holds.",
    formula=lor(ClaimAtom(mech_a), ClaimAtom(mech_b)),  # explicit bridge still works
)

The modern Claim shortcuts ~a, a & b, and a | b return Formula nodes and do not emit DeprecationWarning. They do not create first-class Claim nodes until you wrap them in claim(..., formula=...). The deprecated function-call helpers not_(a), and_(...), and or_(...) remain compatibility-only: they still compile to structural helper claims and still emit DeprecationWarning. Python keywords not, and, and or still cannot be overloaded, and Claim objects intentionally reject truth-value checks such as if claim:.

First-order quantifiers

forall(...) and exists(...) build quantified formula nodes for predicate-logic claims. Use them inside claim(..., formula=...) when the proposition ranges over a Variable rather than over named claim atoms:

from gaia.engine.lang import (
    ClaimKind,
    Domain,
    PredicateSymbol,
    UserPredicate,
    Variable,
    claim,
    exists,
    forall,
    implies,
)

System = Domain(content="Systems in this package", members=["s1", "s2"])
x = Variable(symbol="x", domain=System)
P = PredicateSymbol(name="P", arg_domains=(System,))
Q = PredicateSymbol(name="Q", arg_domains=(System,))
universal = claim(
    "All systems satisfy P implies Q.",
    formula=forall(x, implies(UserPredicate(P, (x,)), UserPredicate(Q, (x,)))),
    kind=ClaimKind.QUANTIFIED,
)
witness = claim(
    "There exists a system that satisfies P.",
    formula=exists(x, UserPredicate(P, (x,))),
    kind=ClaimKind.QUANTIFIED,
)

For the full predicate-logic surface (variables, domains, predicates, ground/lower boundary semantics), see gaia-lang/predicate-logic.md and the formula AST API reference.

Propositional analysis

Compiled operator graphs can be analyzed with gaia.engine.ir.logic. The API keeps Gaia IR as the stored representation and uses a mature Boolean backend for normalization and checks. The snippet assumes pkg is an already-collected package object:

from gaia.engine.lang.compiler import compile_package_artifact
from gaia.engine.ir.logic import (
    are_equivalent,
    is_satisfiable,
    simplify_proposition,
    to_cnf_proposition,
)

graph = compile_package_artifact(pkg).graph

simplified = simplify_proposition(graph, "github:pkg::double_negation")
cnf = to_cnf_proposition(graph, "github:pkg::formula", simplify=True)
same = are_equivalent(graph, "github:pkg::left", "github:pkg::right")
consistent = is_satisfiable(graph, "github:pkg::formula")

This is useful for lints, formula comparison, and checking whether a composed expression is internally inconsistent. The returned expression is a backend object; it is not persisted into Gaia IR.

Reviewable relations

Relation verbs declare semantic judgments between claims. They return warrant helper claims and are included in review manifests:

Function	Semantics	Meaning
`contradict(a, b)`	NOT (A AND B)	both cannot be true
`equal(a, b)`	A = B	same truth value
`exclusive(a, b)`	A XOR B	closed binary partition, exactly one true

not_both = contradict(hypothesis_a, hypothesis_b,
    rationale="Incompatible mechanisms.")

same = equal(prediction, observation,
    rationale="The predicted and observed signatures match.")

one_of = exclusive(conventional_sc, unconventional_sc,
    rationale="This package treats the two cases as an exhaustive binary split.")

If one of these returned helpers is listed in root __all__, the export manifest keeps the helper claim and adds export_kind="structural_relation", the relation kind, endpoint QIDs, and the backing operator ID. This makes the public interface say "these claims stand in this relation" instead of treating the helper as an ordinary headline conclusion.

Use scaffold relations when the relation is worth tracking but not ready to enter inference:

maybe_same = candidate_relation(
    claims=[prediction, observation],
    pattern="equal",
    rationale="They may state the same observable after unit normalization.",
)

open_tension = candidate_relation(
    claims=[model_prediction, measured_result],
    pattern="contradict",
    background=[same_regime],
    rationale="The stated prediction and measurement disagree in the same regime.",
)

Allowed pattern values are None, equal, contradict, and exclusive. These records remain in the formalization manifest until a human or agent upgrades them to a formal relation or records the link with materialize(...). Older packages that used the removed tension(a, b) helper should use candidate_relation(claims=[a, b], pattern="contradict") when the intended shape is explicit, or pattern=None when the author only wants an unresolved "look here later" marker.

v5 compatibility operators

The older operator functions remain for existing packages but emit DeprecationWarning. New packages should use relation verbs for reviewable semantic judgments, or formula claims for structural Boolean expressions. The compatibility functions take Knowledge inputs and optional reason + prior (must be paired: both or neither), then return a helper claim.

Function	Semantics	Meaning
`contradiction(a, b)`	NOT (A AND B)	both cannot be true (but both can be false)
`equivalence(a, b)`	A = B	same truth value
`complement(a, b)`	A XOR B	exactly one must be true
`disjunction(*claims)`	OR	at least one must be true

# Mutually exclusive hypotheses
not_both = contradiction(hypothesis_a, hypothesis_b,
    reason="Incompatible mechanisms.", prior=0.99)

# Exhaustive binary choice
one_of = complement(conventional_sc, unconventional_sc,
    reason="Exhaustive classification.", prior=0.95)

# At least one explanation holds
at_least_one = disjunction(mech_a, mech_b, mech_c,
    reason="These exhaust known possibilities.", prior=0.9)

Legacy / Experimental Strategy APIs

The v5 named-strategy DSL is preserved for backward compatibility under gaia.engine.lang.compat while existing packages migrate. New v0.5 packages should not use these helpers. Top-level fallback access (e.g. from gaia.engine.lang import support) emits a DeprecationWarning; the explicit gaia.engine.lang.compat.<name> import is what migrating packages should use until they finish moving off them.

For the full migration table (every legacy verb mapped to its v0.5 replacement), see Migration to alpha 0 §Layer 3. For per-symbol signatures of the canonical replacements, use the auto-generated gaia.engine.lang reference and focused gaia.engine.lang.dsl reference. The compat facade is a deprecated migration import, not a separate generated authoring contract.

from gaia.engine.lang.compat import (
    # background-context aliases (replaced by note)
    setting, context,
    # operator helpers (replaced by relation verbs and formula AST)
    contradiction, equivalence, complement, disjunction,
    # named-strategy DSL (replaced by derive / infer / bayes.compare)
    support, compare, deduction, abduction, induction,
    analogy, extrapolation, elimination, case_analysis,
    mathematical_induction, composite,
    # cross-package bridging (still in use; will be promoted in a later release)
    fills,
)

Notable migration rows

Legacy helper	v0.5 replacement	Notes
`setting(...)` / `context(...)`	`note(...)`	Background context only; never participates in BP.
`support([P], C, prior=...)`	`derive(C, given=[P])` (deterministic) or `infer(P, hypothesis=C, p_e_given_h=..., p_e_given_not_h=...)` / `bayes.compare(...)` (probabilistic)	`P` is the evidence; `C` is the hypothesis whose belief gets updated.
`deduction([P], C)`	`derive(C, given=[P])`	Strict logical entailment lowers to a hard conditional implication.
`compare / abduction / induction / analogy / extrapolation / elimination / case_analysis / mathematical_induction`	Author the deterministic skeleton with `derive(...)` + relation verbs, or `bayes.compare(...)` for explicit Bayesian comparisons	Do not use these as shortcuts for uncertainty that hasn't been spelled out as claims.
`composite(..., sub_strategies=[...])`	Plain `derive(...)` chains plus `@compose` for the workflow boundary	Sub-strategy priors are no longer the v0.5 surface for soft leaves; use `infer(...)` / `bayes.compare(...)` instead.
`infer([premises], conclusion, ...)` (legacy positional)	`infer(evidence, hypothesis=..., given=..., p_e_given_h=..., p_e_given_not_h=...)`	The legacy positional form is preserved as a deprecated path; the keyword form is the v0.5 contract.
`contradiction(a, b)` / `equivalence(a, b)` / `complement(a, b)`	`contradict(a, b)` / `equal(a, b)` / `exclusive(a, b)`	The relation-verb forms appear in review manifests and emit reviewable warrant helpers.
`disjunction(*claims)` / `and_(...)` / `or_(...)` / `not_(...)`	`claim(..., formula=lor(...))` / `claim(..., formula=land(...))` / `claim(..., formula=lnot(...))`, or the dunder formula sugar `a \\| b`, `a & b`, `~a`	Formula AST is the v0.5 way to express structural Boolean expressions; dunders now return Formula nodes, not legacy helper claims.
`noisy_and(...)`	`derive(...)` for deterministic conjunction; `infer(...)` / `bayes.compare(...)` for probabilistic evidence aggregation	Currently delegates to legacy `support()`.

fills(...) (cross-package interface bridging) is still the v0.5 surface for declaring local_hole-resolving relations between packages. See Hole and Bridge Tutorial for the end-to-end walkthrough. Until it is promoted out of compat, treat gaia.engine.lang.compat.fills as a compatibility import rather than a top-level generated reference entry.

Module Organization

One module per chapter/section of source material
Module docstring becomes section title in rendered output
Each knowledge node goes in the module where it first appears
Later modules import from earlier ones: from .motivation import some_claim

src/my_package/
    __init__.py          # package entrypoint and export surface
    motivation.py        # "Introduction and Motivation"
    s2_background.py     # "Section 2: Background"
    s3_results.py        # "Section 3: Results"

Labels and Exports

Labels are auto-assigned from Python variable names by gaia build compile. Never set .label manually.

# Label "tc_prediction" is auto-assigned
tc_prediction = claim("Tc of MgB2 is 39K.")

Visibility levels:

Convention	Visibility	Example
In root `__all__`	Exported cross-package claim or typed relation interface	`__all__ = ["main_theorem"]` or `__all__ = export(main_theorem)`
No `_` prefix	Package-scope binding; may receive an inferred label	`supporting_lemma = claim(...)`
`_` prefix	Python private convention only; do not export it	`_helper = claim(...)`

Relation helpers returned by equal, contradict, exclusive, and associate can be exported explicitly. Implicit operand-lift helpers generated from Formula / BoolExpr arguments cannot; use an explicit claim(..., formula=...) binding if that formula is part of the public surface.

Legacy strategy naming: Assign legacy strategies to named variables so they appear in gaia build check --brief output:

strat_tc = support(...)      # gets label "strat_tc"
abd_main = abduction(...)    # gets label "abd_main"

Priors

External priors belong only on independent probabilistic inputs to exported goals. A zero-premise observe(...) claim is already pinned to 1 - CROMWELL_EPS; do not give it a separate external prior. Claims concluded by derive(...), compute(...), or observe(..., given=...) get their belief from the graph.

Use priors.py for those inputs, and call register_prior(...) on claims that already exist in the package:

# src/my_package/priors.py
from gaia.engine.lang import register_prior

from . import high_quality_dataset, mechanism_plausible

register_prior(
    high_quality_dataset,
    0.9,
    justification="Independent replication confirms the dataset quality.",
)

register_prior(
    mechanism_plausible,
    0.7,
    justification="Previous measurements in the same material family support this mechanism.",
)

Each call records a source-specific prior on the claim. The default source_id is user_priors; engines, reviewers, calibration jobs, and agents can register other source IDs. At compile time, Gaia applies the package's ResolutionPolicy, writes the winning value to metadata["prior"], and keeps all records in metadata["prior_records"].

Do not export PRIORS = {...} from priors.py. v0.5+ rejects that legacy dict with a migration error because it cannot preserve per-source provenance.

Do not assign manual priors to derived claims, structural expression helpers, relation helper claims, or generated formalization internals. Run gaia build check --hole . to inspect the independent degrees of freedom. Any independent input left without an external prior is handled by MaxEnt, subject to the package's hard logical constraints.

Common Anti-Patterns

Anti-pattern	Correct approach
`setting` or `question` as strategy premises	Use `background=` parameter
Manually setting `.label = "name"`	Assign to a named variable
Assigning priors to derived/helper claims	Put priors only on independent probabilistic inputs
`PRIORS = {...}` in `priors.py`	Use `register_prior(claim, value, justification=...)`
`reason` without `prior` in legacy APIs (or vice versa)	Provide both or neither
Dynamic or computed `__all__`	Keep `__all__` literal and static, or use `export(...)` with module-scope `Knowledge` objects. Root `__all__` is the cross-package export surface; CLI target submodules may also keep literal lists for `gaia author --file`.
`from gaia.gaia_ir import ...`	Use `from gaia.engine.ir import ...`
`noisy_and()`	Deprecated legacy compatibility path

Next Steps

Quick Start — create your first package end-to-end
CLI Commands — workflow-oriented guide to the gaia command groups
Hole And Bridge Tutorial — cross-package dependency resolution