predicates.yaml

# Canonical LRA predicate registry.
# Governed by capabilities/reference/predicate-standards.md.

predicates:
  - id: pred:at-point-operation
    name: AtPointOperation
    kind: predicate
    category: function
    arguments:
      - name: Op
        role: operation
      - name: f_tuple
        role: functions
      - name: x
        role: point
    returns: truth_value
    polymorphic: true
    surface_forms:
      - at-point operation
      - operation applied at a point
    description: >
      A value-level operation is applied to the values of a tuple of functions
      at a single input.

  - id: pred:pointwise-operation
    name: PointwiseOperation
    kind: predicate
    category: function
    arguments:
      - name: Op
        role: operation
      - name: f_tuple
        role: functions
      - name: A
        role: domain
    returns: truth_value
    ambient_argument: A
    polymorphic: true
    surface_forms:
      - pointwise operation
      - operation applied pointwise
    description: >
      A value-level operation is lifted to functions by applying it at every
      input in the domain.

  - id: pred:at-point-relation
    name: AtPointRelation
    kind: predicate
    category: function
    arguments:
      - name: Rel
        role: relation
      - name: f_tuple
        role: functions
      - name: x
        role: point
    returns: truth_value
    polymorphic: true
    surface_forms:
      - at-point relation
      - relation at a point
    description: >
      A value-level relation is checked on the values of a tuple of functions
      at a single input.

  - id: pred:pointwise-relation
    name: PointwiseRelation
    kind: predicate
    category: function
    arguments:
      - name: Rel
        role: relation
      - name: f_tuple
        role: functions
      - name: A
        role: domain
    returns: truth_value
    ambient_argument: A
    polymorphic: true
    surface_forms:
      - pointwise relation
      - relation on a set pointwise
    description: >
      A value-level relation holds on a tuple of function values at every input
      in the domain.

  - id: pred:pointwise-relation-near
    name: PointwiseRelationNear
    kind: predicate
    category: function
    arguments:
      - name: Rel
        role: relation
      - name: f_tuple
        role: functions
      - name: c
        role: base_point
      - name: A
        role: domain
    returns: truth_value
    ambient_argument: A
    polymorphic: true
    surface_forms:
      - pointwise relation near a point
      - relation near a point
    description: >
      A value-level relation holds for function values throughout some deleted
      neighbourhood of a base point inside the domain.

  - id: pred:bounded-near
    name: BoundedNear
    kind: predicate
    category: function
    arguments:
      - name: f
        role: function
      - name: c
        role: base_point
      - name: A
        role: domain
    returns: truth_value
    ambient_argument: A
    polymorphic: true
    surface_forms:
      - bounded near
      - locally bounded
    description: >
      A real-valued function is bounded on some deleted neighbourhood of a base
      point inside the domain.

  - id: pred:bounded-away-from-zero
    name: BoundedAwayFromZero
    kind: predicate
    category: function
    arguments:
      - name: f
        role: function
      - name: A
        role: domain
    returns: truth_value
    ambient_argument: A
    polymorphic: true
    surface_forms:
      - bounded away from zero
      - separated from zero
    description: >
      The absolute value of a real-valued function has a positive lower bound
      on the domain.

  - id: pred:bounded-away-from-zero-near
    name: BoundedAwayFromZeroNear
    kind: predicate
    category: function
    arguments:
      - name: f
        role: function
      - name: c
        role: base_point
      - name: A
        role: domain
    returns: truth_value
    ambient_argument: A
    polymorphic: true
    surface_forms:
      - bounded away from zero near
      - locally separated from zero
    description: >
      A real-valued function is bounded away from zero on some deleted
      neighbourhood of a base point inside the domain.

  - id: pred:uniformly-bounded-family
    name: UniformlyBoundedFamily
    kind: predicate
    category: function
    arguments:
      - name: F
        role: family
      - name: I
        role: index_set
      - name: A
        role: domain
    returns: truth_value
    ambient_argument: A
    polymorphic: true
    surface_forms:
      - uniformly bounded family
      - family uniformly bounded on a set
    description: >
      One real bound controls every function in the family at every input in
      the domain.

  - id: pred:within
    name: Within
    kind: predicate
    category: topology
    arguments:
      - name: x
        role: point
      - name: W
        role: local_region
      - name: X
        role: ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - within
      - lies within
      - belongs to a local region
    description: >
      The point x lies within the local region W in the ambient object X.
      The local region may be a tolerance ball, punctured ball, neighborhood,
      punctured neighborhood, or another named localizing object.

  - id: pred:is-ball
    name: IsBall
    kind: predicate
    category: topology
    arguments:
      - name: B
        role: ball
      - name: c
        role: center
      - name: r
        role: radius
      - name: X
        role: ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - is a ball
      - metric ball
      - open ball
    description: >
      The object B is the ball centered at c with radius r in the ambient
      space X.

  - id: pred:is-punctured-ball
    name: IsPuncturedBall
    kind: predicate
    category: topology
    arguments:
      - name: B_dot
        role: punctured_ball
        surface: 'B^\times'
      - name: B
        role: underlying_ball
      - name: c
        role: center
      - name: r
        role: radius
      - name: X
        role: ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - is a punctured ball
      - is a deleted ball
    description: >
      The object B_dot is the ball B centered at c with radius r in X after
      removing the center c.

  - id: pred:is-closed-ball
    name: IsClosedBall
    kind: predicate
    category: topology
    arguments:
      - name: B_bar
        role: closed_ball
        surface: '\overline{B}'
      - name: c
        role: center
      - name: r
        role: radius
      - name: X
        role: ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - is a closed ball
      - closed ball
      - metric closed ball
    description: >
      The object B_bar is the closed ball centered at c with radius r in the
      ambient space X.

  - id: pred:is-punctured-closed-ball
    name: IsPuncturedClosedBall
    kind: predicate
    category: topology
    arguments:
      - name: B_bar_dot
        role: punctured_closed_ball
        surface: '\overline{B}^{\times}'
      - name: B_bar
        role: underlying_closed_ball
        surface: '\overline{B}'
      - name: c
        role: center
      - name: r
        role: radius
      - name: X
        role: ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - is a punctured closed ball
      - is a deleted closed ball
      - punctured closed ball
      - deleted closed ball
    description: >
      The object B_bar_dot is the closed ball B_bar centered at c with radius r
      in X after removing the center c.

  - id: pred:is-neighborhood
    name: IsNeighborhood
    kind: predicate
    category: topology
    arguments:
      - name: U
        role: neighborhood
      - name: c
        role: center
      - name: X
        role: ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - is a neighborhood
      - is a neighbourhood
    description: >
      The object U is a neighborhood of c in the ambient topological space X.

  - id: pred:is-punctured-neighborhood
    name: IsPuncturedNeighborhood
    kind: predicate
    category: topology
    arguments:
      - name: U_dot
        role: punctured_neighborhood
        surface: 'U^\times'
      - name: U
        role: underlying_neighborhood
      - name: c
        role: center
      - name: X
        role: ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - is a punctured neighborhood
      - is a punctured neighbourhood
      - is a deleted neighborhood
      - is a deleted neighbourhood
    description: >
      The object U_dot is the neighborhood U of c in X after removing the
      center c.

  - id: pred:is-topology
    name: IsTopology
    kind: predicate
    category: topology
    arguments:
      - name: tau
        role: topology
        surface: '\tau'
      - name: X
        role: carrier
    returns: truth_value
    ambient_argument: X
    surface_forms:
      - Topology
      - is a topology
      - topology axioms
    description: >
      The collection tau is a topology on the carrier set X.

  - id: pred:is-metric
    name: IsMetric
    kind: predicate
    category: topology
    arguments:
      - name: d
        role: metric
      - name: X
        role: carrier
    returns: truth_value
    ambient_argument: X
    surface_forms:
      - Metric
      - is a metric
      - metric axioms
    description: >
      The function d is a metric on the carrier set X.

  - id: pred:is-pseudo-metric
    name: IsPseudoMetric
    kind: predicate
    category: topology
    arguments:
      - name: d
        role: pseudo_metric
      - name: X
        role: carrier
    returns: truth_value
    ambient_argument: X
    surface_forms:
      - PseudoMetric
      - is a pseudo-metric
      - pseudo-metric axioms
    description: >
      The function d is a pseudo-metric on the carrier set X.

  - id: pred:is-pointlike
    name: IsPointlike
    kind: predicate
    category: topology
    arguments:
      - name: u
        role: function
      - name: X
        role: metric_space
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - pointlike
      - is pointlike
      - pointlike function
    description: >
      The function u satisfies the pointlike inequalities with respect to the
      metric-space context X.

  - id: pred:is-norm
    name: IsNorm
    kind: predicate
    category: topology
    arguments:
      - name: norm
        role: norm
        surface: '\|\cdot\|'
      - name: V
        role: vector_space
    returns: truth_value
    ambient_argument: V
    surface_forms:
      - Norm
      - is a norm
      - norm axioms
    description: >
      The function norm is a norm on the ambient vector space V.

  - id: pred:is-euclidean-space
    name: IsEuclideanSpace
    kind: predicate
    category: topology
    arguments:
      - name: E
        role: euclidean_space_structure
    returns: truth_value
    ambient_argument: E
    surface_forms:
      - EuclideanSpace
      - is a Euclidean space
      - Euclidean space structure
    description: >
      The packaged object E satisfies the Euclidean space structure expected
      in the ambient metric or topological context.

  - id: pred:is-interval
    name: IsInterval
    kind: predicate
    category: topology
    arguments:
      - name: I
        role: interval
      - name: X
        role: ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - is an interval
      - interval
    description: >
      The object I is an interval in the ambient ordered or topological space
      X.

  - id: pred:is-open-interval
    name: IsOpenInterval
    kind: predicate
    category: topology
    arguments:
      - name: I
        role: interval
      - name: X
        role: ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - is an open interval
      - open interval
    description: >
      The object I is an interval in X whose finite endpoints are excluded.

  - id: pred:is-closed-interval
    name: IsClosedInterval
    kind: predicate
    category: topology
    arguments:
      - name: I
        role: interval
      - name: X
        role: ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - is a closed interval
      - closed interval
    description: >
      The object I is an interval in X whose finite endpoints are included.

  - id: pred:is-centered-open-interval
    name: IsCenteredOpenInterval
    kind: predicate
    category: topology
    arguments:
      - name: I
        role: interval
      - name: c
        role: center
      - name: r
        role: radius
      - name: X
        role: ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - is a centered open interval
      - centered open interval
      - symmetric open interval
      - open interval centered at a point
    description: >
      The object I is the open interval centered at c with radius r in the
      ambient ordered or topological space X.

  - id: pred:is-punctured-centered-open-interval
    name: IsPuncturedCenteredOpenInterval
    kind: predicate
    category: topology
    arguments:
      - name: I_dot
        role: punctured_interval
        surface: 'I^\times'
      - name: I
        role: underlying_interval
      - name: c
        role: center
      - name: r
        role: radius
      - name: X
        role: ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - is a punctured centered open interval
      - is a deleted centered open interval
      - punctured centered open interval
      - deleted centered open interval
      - punctured symmetric open interval
      - deleted symmetric open interval
    description: >
      The object I_dot is the centered open interval I centered at c with
      radius r in X after removing the center c.

  - id: pred:is-centered-closed-interval
    name: IsCenteredClosedInterval
    kind: predicate
    category: topology
    arguments:
      - name: I
        role: interval
      - name: c
        role: center
      - name: r
        role: radius
      - name: X
        role: ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - is a centered closed interval
      - centered closed interval
      - symmetric closed interval
      - closed interval centered at a point
    description: >
      The object I is the closed interval centered at c with radius r in the
      ambient ordered or topological space X.

  - id: pred:is-bounded-interval
    name: IsBoundedInterval
    kind: predicate
    category: topology
    arguments:
      - name: I
        role: interval
      - name: X
        role: ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - is a bounded interval
      - bounded interval
    description: >
      The object I is an interval in X with finite left and right endpoints.

  - id: pred:is-empty
    name: IsEmpty
    kind: predicate
    category: set
    arguments:
      - name: A
        role: object_or_collection
    returns: truth_value
    ambient_argument: A
    polymorphic: true
    surface_forms:
      - empty
      - is empty
      - has no elements
      - has no members
    description: >
      The object or collection A has no elements, members, points, or
      admissible inputs in the relevant ambient context.

  - id: pred:is-nonempty
    name: IsNonempty
    kind: predicate
    category: set
    arguments:
      - name: A
        role: object_or_collection
    returns: truth_value
    ambient_argument: A
    polymorphic: true
    surface_forms:
      - nonempty
      - is nonempty
      - has elements
      - has members
    description: >
      The object or collection A has at least one element, member, point, or
      admissible input in the relevant ambient context.

  - id: pred:converges-to
    name: ConvergesTo
    kind: predicate
    category: sequence
    arguments:
      - name: x
        role: sequence
      - name: L
        role: limit
      - name: X
        role: ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - converges to
      - tends to a limit
    description: >
      The sequence or indexed object x converges to L in the ambient object X.

  - id: pred:is-cauchy
    name: IsCauchy
    kind: predicate
    category: sequence
    arguments:
      - name: x
        role: sequence
      - name: X
        role: ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - CauchySequence
      - is cauchy
      - cauchy condition
    description: >
      The sequence or indexed object x satisfies the Cauchy condition in X.

  - id: pred:is-null
    name: IsNull
    kind: predicate
    category: sequence
    arguments:
      - name: x
        role: sequence_or_object
      - name: X
        role: ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - is null
      - null sequence
      - converges to zero
    description: >
      The object x is null in X, typically meaning it converges to the zero
      object of X.

  - id: pred:is-constant
    name: IsConstant
    kind: predicate
    category: function
    arguments:
      - name: x
        role: object
      - name: c
        role: constant_value
      - name: X
        role: ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - is constant
      - constant object
      - constant sequence
      - constant function
    description: >
      The object x has constant value c in the ambient object X.

  - id: pred:is-ultimately-constant
    name: IsUltimatelyConstant
    kind: predicate
    category: sequence
    arguments:
      - name: x
        role: sequence
      - name: c
        role: eventual_value
      - name: X
        role: ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - is ultimately constant
      - eventually constant
    description: >
      The sequence x is eventually equal to the value c in X.

  - id: pred:is-subsequence
    name: IsSubsequence
    kind: predicate
    category: sequence
    arguments:
      - name: y
        role: subsequence
      - name: x
        role: sequence
    returns: truth_value
    surface_forms:
      - is a subsequence
      - subsequence
    description: >
      The sequence y is obtained from x by a strictly increasing index map.

  - id: pred:has-convergent-subsequence
    name: HasConvergentSubsequence
    kind: predicate
    category: sequence
    arguments:
      - name: x
        role: sequence
      - name: X
        role: ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - has a convergent subsequence
    description: >
      Some subsequence of x converges in the ambient object X.

  - id: pred:is-divergent
    name: IsDivergent
    kind: predicate
    category: sequence
    arguments:
      - name: x
        role: sequence_or_object
      - name: X
        role: ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - is divergent
      - diverges
    description: >
      The object x fails to converge in the ambient object X.

  - id: pred:diverges-to-positive-infinity
    name: DivergesToPositiveInfinity
    kind: predicate
    category: sequence
    arguments:
      - name: x
        role: sequence_or_function
      - name: P
        role: ambient_ordered_structure
    returns: truth_value
    ambient_argument: P
    polymorphic: true
    surface_forms:
      - diverges to positive infinity
      - tends to positive infinity
    description: >
      The object x eventually exceeds every bound in the ambient ordered
      structure P.

  - id: pred:diverges-to-negative-infinity
    name: DivergesToNegativeInfinity
    kind: predicate
    category: sequence
    arguments:
      - name: x
        role: sequence_or_function
      - name: P
        role: ambient_ordered_structure
    returns: truth_value
    ambient_argument: P
    polymorphic: true
    surface_forms:
      - diverges to negative infinity
      - tends to negative infinity
    description: >
      The object x eventually lies below every bound in the ambient ordered
      structure P.

  - id: pred:is-oscillatory
    name: IsOscillatory
    kind: predicate
    category: sequence
    arguments:
      - name: x
        role: sequence_or_function
      - name: X
        role: ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - is oscillatory
      - oscillatory behavior
    description: >
      The object x exhibits oscillatory behavior in the ambient object X.

  - id: pred:limsup
    name: Limsup
    kind: predicate
    category: analysis
    arguments:
      - name: L
        role: limit_superior
      - name: x
        role: object
      - name: A
        role: ambient
    returns: truth_value
    ambient_argument: A
    polymorphic: true
    surface_forms:
      - limsup
      - limit superior
    description: >
      The object L is the limit superior of x in the ambient object A.

  - id: pred:liminf
    name: Liminf
    kind: predicate
    category: analysis
    arguments:
      - name: L
        role: limit_inferior
      - name: x
        role: object
      - name: A
        role: ambient
    returns: truth_value
    ambient_argument: A
    polymorphic: true
    surface_forms:
      - liminf
      - limit inferior
    description: >
      The object L is the limit inferior of x in the ambient object A.

  - id: pred:is-cluster-value
    name: IsClusterValue
    kind: predicate
    category: analysis
    arguments:
      - name: L
        role: cluster_value
      - name: x
        role: object
      - name: X
        role: ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - is a cluster value
      - cluster value
    description: >
      The value L occurs as a cluster value of x in X.

  - id: pred:eventually
    name: Eventually
    kind: predicate
    category: analysis
    arguments:
      - name: phi
        role: property
        surface: '\varphi'
      - name: I
        role: index_or_filter
    returns: truth_value
    polymorphic: true
    surface_forms:
      - eventually
      - eventually true
    description: >
      The property phi holds eventually along the index or filter I.

  - id: pred:frequently
    name: Frequently
    kind: predicate
    category: analysis
    arguments:
      - name: phi
        role: property
        surface: '\varphi'
      - name: I
        role: index_or_filter
    returns: truth_value
    polymorphic: true
    surface_forms:
      - frequently
      - infinitely often
    description: >
      The property phi holds frequently along the index or filter I.

  - id: pred:eventually-equal
    name: EventuallyEqual
    kind: predicate
    category: analysis
    arguments:
      - name: x
        role: left_object
      - name: y
        role: right_object
      - name: I
        role: index_or_filter
    returns: truth_value
    polymorphic: true
    surface_forms:
      - eventually equal
      - equal eventually
    description: >
      The objects x and y agree eventually along the index or filter I.

  - id: pred:is-open
    name: IsOpen
    kind: predicate
    category: topology
    arguments:
      - name: U
        role: subset
      - name: X
        role: ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - is open
      - open set
    description: >
      The subset U is open in the ambient topological object X.

  - id: pred:is-closed
    name: IsClosed
    kind: predicate
    category: topology
    arguments:
      - name: C
        role: subset
      - name: X
        role: ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - is closed
      - closed set
    description: >
      The subset C is closed in the ambient topological object X.

  - id: pred:is-compact
    name: IsCompact
    kind: predicate
    category: topology
    arguments:
      - name: K
        role: subset
      - name: X
        role: ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - is compact
      - compact set
    description: >
      The subset K is compact in the ambient topological object X.

  - id: pred:is-interior
    name: IsInterior
    kind: predicate
    category: topology
    arguments:
      - name: x
        role: point
      - name: A
        role: subset
      - name: X
        role: ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - is interior
      - interior point
    description: >
      The point x lies in the interior of A relative to X.

  - id: pred:is-on-boundary
    name: IsOnBoundary
    kind: predicate
    category: topology
    arguments:
      - name: x
        role: point
      - name: A
        role: subset
      - name: X
        role: ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - is on boundary
      - boundary point
    description: >
      The point x lies on the boundary of A relative to X.

  - id: pred:is-cluster
    name: IsCluster
    kind: predicate
    category: topology
    arguments:
      - name: x
        role: point
      - name: A
        role: subset
      - name: X
        role: ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - is cluster
      - cluster point
      - accumulation point
    description: >
      The point x is a cluster point of A relative to X.

  - id: pred:is-adherent
    name: IsAdherent
    kind: predicate
    category: topology
    arguments:
      - name: x
        role: point
      - name: A
        role: subset
      - name: X
        role: ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - is adherent
      - adherent point
      - closure point
    description: >
      The point x is adherent to A relative to X.

  - id: pred:is-isolated
    name: IsIsolated
    kind: predicate
    category: topology
    arguments:
      - name: x
        role: point
      - name: A
        role: subset
      - name: X
        role: ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - is isolated
      - isolated point
    description: >
      The point x is isolated in A relative to X.

  - id: pred:is-dense
    name: IsDense
    kind: predicate
    category: topology
    arguments:
      - name: A
        role: subset
      - name: X
        role: ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - is dense
      - dense subset
    description: >
      The subset A is dense in the ambient topological object X.

  - id: pred:is-sequentially-compact
    name: IsSequentiallyCompact
    kind: predicate
    category: topology
    arguments:
      - name: K
        role: subset
      - name: X
        role: ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - is sequentially compact
      - sequentially compact
    description: >
      The subset K is sequentially compact in the ambient topological object X.

  - id: pred:tends-to
    name: TendsTo
    kind: predicate
    category: analysis
    arguments:
      - name: f
        role: function_or_object
      - name: a
        role: source_point
      - name: L
        role: target_limit
      - name: X
        role: source_ambient
      - name: Y
        role: target_ambient
    returns: truth_value
    ambient_argument: Y
    domain_convention:
      kind: typed_function_domain
      function_argument: f
      source_point_argument: a
      source_ambient_argument: X
      quantification_scope: admissible inputs in the declared domain of f
      notes: >
        When f is a typed function datum, for example f:A -> Y, the domain A
        is intrinsic to f and is not a separate TendsTo argument. The source
        ambient X records the ambient space in which the source point and
        approach live; semantic artifacts must make any restricted-domain
        quantification explicit in their quantified form.
    carried_context:
      - kind: domain
        source: type_of_argument
        argument: f
        exposes_as: admissible_input_domain
      - kind: source_ambient
        source: argument
        argument: X
        exposes_as: approach_ambient
      - kind: target_ambient
        source: argument
        argument: Y
        exposes_as: value_ambient
    polymorphic: true
    surface_forms:
      - tends to
      - function limit
    description: >
      The object f tends to L as its input tends to a from the source ambient
      object X, with values in Y.

  - id: pred:negligible-at
    name: NegligibleAt
    kind: predicate
    category: analysis
    arguments:
      - name: f
        role: function
      - name: g
        role: comparison_scale
      - name: lp
        role: limit_point_datum
        surface: '\ell p'
    returns: truth_value
    ambient_argument: lp
    polymorphic: true
    surface_forms:
      - negligible at
      - little-o at a point
      - asymptotically negligible at a point
    description: >
      The function f is asymptotically negligible relative to the comparison
      scale g at the limit-point datum lp. The datum lp carries the basepoint
      and domain, so the non-vacuity/accumulation-point condition is part of
      the input rather than a hidden side condition.

  - id: pred:left-limit
    name: LeftLimit
    kind: predicate
    category: analysis
    arguments:
      - name: L
        role: limit
      - name: f
        role: function
      - name: a
        role: source_point
      - name: X
        role: source_ambient
      - name: Y
        role: target_ambient
    returns: truth_value
    ambient_argument: Y
    carried_context:
      - kind: domain
        source: type_of_argument
        argument: f
        exposes_as: admissible_input_domain
      - kind: side
        source: predicate
        argument: X
        exposes_as: left_hand_approach
      - kind: source_ambient
        source: argument
        argument: X
        exposes_as: approach_ambient
      - kind: target_ambient
        source: argument
        argument: Y
        exposes_as: value_ambient
    polymorphic: true
    surface_forms:
      - left limit
      - left-hand limit
    description: >
      The left-hand limit of f at a is L, with source ambient X and target
      ambient Y.

  - id: pred:right-limit
    name: RightLimit
    kind: predicate
    category: analysis
    arguments:
      - name: L
        role: limit
      - name: f
        role: function
      - name: a
        role: source_point
      - name: X
        role: source_ambient
      - name: Y
        role: target_ambient
    returns: truth_value
    ambient_argument: Y
    carried_context:
      - kind: domain
        source: type_of_argument
        argument: f
        exposes_as: admissible_input_domain
      - kind: side
        source: predicate
        argument: X
        exposes_as: right_hand_approach
      - kind: source_ambient
        source: argument
        argument: X
        exposes_as: approach_ambient
      - kind: target_ambient
        source: argument
        argument: Y
        exposes_as: value_ambient
    polymorphic: true
    surface_forms:
      - right limit
      - right-hand limit
    description: >
      The right-hand limit of f at a is L, with source ambient X and target
      ambient Y.

  - id: pred:limit-at-infinity
    name: LimitAtInfinity
    kind: predicate
    category: analysis
    arguments:
      - name: L
        role: limit
      - name: f
        role: function
      - name: Y
        role: target_ambient
    returns: truth_value
    ambient_argument: Y
    carried_context:
      - kind: domain
        source: type_of_argument
        argument: f
        exposes_as: admissible_input_domain
      - kind: target_ambient
        source: argument
        argument: Y
        exposes_as: target_ambient
    polymorphic: true
    surface_forms:
      - limit at infinity
      - tends at infinity
    description: >
      The function f tends to L along an unbounded direction, with values in
      the target ambient object Y.

  - id: pred:is-continuous
    name: IsContinuous
    kind: predicate
    category: analysis
    arguments:
      - name: f
        role: function
      - name: Locus
        role: locus
      - name: X
        role: source_ambient
      - name: Y
        role: target_ambient
    returns: truth_value
    ambient_argument: Y
    carried_context:
      - kind: domain
        source: type_of_argument
        argument: f
        exposes_as: admissible_input_domain
      - kind: locus
        source: argument
        argument: Locus
        exposes_as: continuity_locus
      - kind: source_ambient
        source: argument
        argument: X
        exposes_as: source_ambient
      - kind: target_ambient
        source: argument
        argument: Y
        exposes_as: target_ambient
    polymorphic: true
    surface_forms:
      - is continuous
      - continuous
    description: >
      The function f is continuous on the indicated locus, with source ambient
      X and target ambient Y. The locus may be a point, set, interval, local
      region, or the whole source ambient object.

  - id: pred:is-uniformly-continuous
    name: IsUniformlyContinuous
    kind: predicate
    category: analysis
    arguments:
      - name: f
        role: function
      - name: Locus
        role: locus
      - name: X
        role: source_ambient
      - name: Y
        role: target_ambient
    returns: truth_value
    ambient_argument: Y
    carried_context:
      - kind: domain
        source: type_of_argument
        argument: f
        exposes_as: admissible_input_domain
      - kind: locus
        source: argument
        argument: Locus
        exposes_as: uniformity_locus
      - kind: source_ambient
        source: argument
        argument: X
        exposes_as: source_ambient
      - kind: target_ambient
        source: argument
        argument: Y
        exposes_as: target_ambient
    polymorphic: true
    surface_forms:
      - is uniformly continuous
      - uniformly continuous
    description: >
      The function f is uniformly continuous on the indicated locus, with
      source ambient X and target ambient Y.

  - id: pred:is-lipschitz
    name: IsLipschitz
    kind: predicate
    category: analysis
    arguments:
      - name: f
        role: function
        type: function
      - name: Locus
        role: locus
        type: set
      - name: X
        role: source_ambient
        type: ambient
      - name: Y
        role: target_ambient
        type: ambient
      - name: C
        role: lipschitz_constant
        type: scalar
    returns: truth_value
    ambient_argument: Y
    carried_context:
      - kind: domain
        source: type_of_argument
        argument: f
        exposes_as: admissible_input_domain
      - kind: locus
        source: argument
        argument: Locus
        exposes_as: lipschitz_locus
      - kind: source_ambient
        source: argument
        argument: X
        exposes_as: source_ambient
      - kind: target_ambient
        source: argument
        argument: Y
        exposes_as: target_ambient
      - kind: constant
        source: argument
        argument: C
        exposes_as: lipschitz_constant
    polymorphic: true
    surface_forms:
      - is lipschitz
      - lipschitz
    description: >
      The function f satisfies a Lipschitz condition with constant C on the
      indicated locus.

  - id: pred:is-bi-lipschitz
    name: IsBiLipschitz
    kind: predicate
    category: analysis
    arguments:
      - name: f
        role: function
        type: function
      - name: Locus
        role: locus
        type: set
      - name: X
        role: source_ambient
        type: ambient
      - name: Y
        role: target_ambient
        type: ambient
      - name: c
        role: lower_lipschitz_constant
        type: scalar
      - name: C
        role: upper_lipschitz_constant
        type: scalar
    returns: truth_value
    ambient_argument: Y
    carried_context:
      - kind: domain
        source: type_of_argument
        argument: f
        exposes_as: admissible_input_domain
      - kind: locus
        source: argument
        argument: Locus
        exposes_as: bilipschitz_locus
      - kind: source_ambient
        source: argument
        argument: X
        exposes_as: source_ambient
      - kind: target_ambient
        source: argument
        argument: Y
        exposes_as: target_ambient
      - kind: lower_constant
        source: argument
        argument: c
        exposes_as: lower_lipschitz_constant
      - kind: upper_constant
        source: argument
        argument: C
        exposes_as: upper_lipschitz_constant
    polymorphic: true
    surface_forms:
      - is bi-lipschitz
      - bi-lipschitz
    description: >
      The function f satisfies two-sided Lipschitz bounds with constants c and
      C on the indicated locus.

  - id: pred:peano-system
    name: PeanoSystem
    kind: predicate
    category: discrete_algebra
    arguments:
      - name: P
        role: carrier
        type: set
      - name: S
        role: successor_function
        type: function
      - name: e
        role: base_element
        type: object
    returns: truth_value
    carried_context:
      - kind: carrier
        source: argument
        argument: P
        exposes_as: carrier
      - kind: operation
        source: argument
        argument: S
        exposes_as: successor_function
      - kind: base_element
        source: argument
        argument: e
        exposes_as: base_element
    surface_forms:
      - Peano system
      - peano system
    description: >
      The carrier P, successor function S, and distinguished base element e
      satisfy the Peano-system axioms.

  - id: pred:is-discontinuous
    name: IsDiscontinuous
    kind: predicate
    category: analysis
    arguments:
      - name: f
        role: function
      - name: Locus
        role: locus
      - name: X
        role: source_ambient
      - name: Y
        role: target_ambient
    returns: truth_value
    ambient_argument: Y
    carried_context:
      - kind: domain
        source: type_of_argument
        argument: f
        exposes_as: admissible_input_domain
      - kind: locus
        source: argument
        argument: Locus
        exposes_as: discontinuity_locus
      - kind: source_ambient
        source: argument
        argument: X
        exposes_as: source_ambient
      - kind: target_ambient
        source: argument
        argument: Y
        exposes_as: target_ambient
    polymorphic: true
    surface_forms:
      - is discontinuous
      - discontinuous
    description: >
      The function f is discontinuous on the indicated locus.

  - id: pred:is-removable-discontinuity
    name: IsRemovableDiscontinuity
    kind: predicate
    category: analysis
    arguments:
      - name: f
        role: function
      - name: Locus
        role: locus
      - name: X
        role: source_ambient
      - name: Y
        role: target_ambient
    returns: truth_value
    ambient_argument: Y
    polymorphic: true
    surface_forms:
      - removable discontinuity
      - is a removable discontinuity
    description: >
      The function f has a removable discontinuity at or on the indicated
      locus.

  - id: pred:is-jump-discontinuity
    name: IsJumpDiscontinuity
    kind: predicate
    category: analysis
    arguments:
      - name: f
        role: function
      - name: Locus
        role: locus
      - name: X
        role: source_ambient
      - name: Y
        role: target_ambient
    returns: truth_value
    ambient_argument: Y
    polymorphic: true
    surface_forms:
      - jump discontinuity
      - is a jump discontinuity
    description: >
      The function f has a jump discontinuity at or on the indicated locus.

  - id: pred:is-essential-discontinuity
    name: IsEssentialDiscontinuity
    kind: predicate
    category: analysis
    arguments:
      - name: f
        role: function
      - name: Locus
        role: locus
      - name: X
        role: source_ambient
      - name: Y
        role: target_ambient
    returns: truth_value
    ambient_argument: Y
    polymorphic: true
    surface_forms:
      - essential discontinuity
      - is an essential discontinuity
    description: >
      The function f has an essential discontinuity at or on the indicated
      locus.

  - id: pred:oscillation
    name: Oscillation
    kind: predicate
    category: analysis
    arguments:
      - name: omega
        role: oscillation_value
        surface: '\omega'
      - name: f
        role: function
      - name: Locus
        role: locus
      - name: X
        role: source_ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - oscillation
      - oscillation on a locus
    description: >
      The value omega is the oscillation of f on the indicated locus in X.

  - id: pred:is-convex
    name: IsConvex
    kind: predicate
    category: analysis
    arguments:
      - name: f
        role: function_or_set
      - name: Locus
        role: locus
    returns: truth_value
    polymorphic: true
    surface_forms:
      - is convex
      - convex
    description: >
      The object f is convex on the indicated locus.

  - id: pred:is-concave
    name: IsConcave
    kind: predicate
    category: analysis
    arguments:
      - name: f
        role: function_or_set
      - name: Locus
        role: locus
    returns: truth_value
    polymorphic: true
    surface_forms:
      - is concave
      - concave
    description: >
      The object f is concave on the indicated locus.

  - id: pred:derivative
    name: Derivative
    kind: predicate
    category: analysis
    arguments:
      - name: D
        role: derivative
      - name: f
        role: function
      - name: Locus
        role: locus
      - name: X
        role: source_ambient
      - name: Y
        role: target_ambient
    returns: truth_value
    ambient_argument: Y
    carried_context:
      - kind: derivative
        source: argument
        argument: D
        exposes_as: derivative_object
      - kind: domain
        source: type_of_argument
        argument: f
        exposes_as: admissible_input_domain
      - kind: locus
        source: argument
        argument: Locus
        exposes_as: derivative_locus
      - kind: source_ambient
        source: argument
        argument: X
        exposes_as: source_ambient
      - kind: target_ambient
        source: argument
        argument: Y
        exposes_as: target_ambient
    polymorphic: true
    surface_forms:
      - derivative
      - has derivative
    description: >
      The object D is the derivative of f at or on the indicated locus.

  - id: pred:left-derivative
    name: LeftDerivative
    kind: predicate
    category: analysis
    arguments:
      - name: D
        role: derivative
      - name: f
        role: function
      - name: Locus
        role: locus
      - name: X
        role: source_ambient
      - name: Y
        role: target_ambient
    returns: truth_value
    ambient_argument: Y
    carried_context:
      - kind: derivative
        source: argument
        argument: D
        exposes_as: derivative_object
      - kind: domain
        source: type_of_argument
        argument: f
        exposes_as: admissible_input_domain
      - kind: locus
        source: argument
        argument: Locus
        exposes_as: derivative_locus
      - kind: side
        source: predicate
        argument: X
        exposes_as: left_hand_approach
      - kind: source_ambient
        source: argument
        argument: X
        exposes_as: source_ambient
      - kind: target_ambient
        source: argument
        argument: Y
        exposes_as: target_ambient
    polymorphic: true
    surface_forms:
      - left derivative
      - left-hand derivative
    description: >
      The object D is the left derivative of f at or on the indicated locus.

  - id: pred:right-derivative
    name: RightDerivative
    kind: predicate
    category: analysis
    arguments:
      - name: D
        role: derivative
      - name: f
        role: function
      - name: Locus
        role: locus
      - name: X
        role: source_ambient
      - name: Y
        role: target_ambient
    returns: truth_value
    ambient_argument: Y
    carried_context:
      - kind: derivative
        source: argument
        argument: D
        exposes_as: derivative_object
      - kind: domain
        source: type_of_argument
        argument: f
        exposes_as: admissible_input_domain
      - kind: locus
        source: argument
        argument: Locus
        exposes_as: derivative_locus
      - kind: side
        source: predicate
        argument: X
        exposes_as: right_hand_approach
      - kind: source_ambient
        source: argument
        argument: X
        exposes_as: source_ambient
      - kind: target_ambient
        source: argument
        argument: Y
        exposes_as: target_ambient
    polymorphic: true
    surface_forms:
      - right derivative
      - right-hand derivative
    description: >
      The object D is the right derivative of f at or on the indicated locus.

  - id: pred:is-differentiable
    name: IsDifferentiable
    kind: predicate
    category: analysis
    arguments:
      - name: f
        role: function
      - name: Locus
        role: locus
      - name: X
        role: source_ambient
      - name: Y
        role: target_ambient
    returns: truth_value
    ambient_argument: Y
    carried_context:
      - kind: domain
        source: type_of_argument
        argument: f
        exposes_as: admissible_input_domain
      - kind: locus
        source: argument
        argument: Locus
        exposes_as: differentiability_locus
      - kind: source_ambient
        source: argument
        argument: X
        exposes_as: source_ambient
      - kind: target_ambient
        source: argument
        argument: Y
        exposes_as: target_ambient
    polymorphic: true
    surface_forms:
      - is differentiable
      - differentiable
    description: >
      The function f is differentiable at or on the indicated locus.

  - id: pred:has-linear-approximation
    name: HasLinearApproximation
    kind: predicate
    category: analysis
    arguments:
      - name: f
        role: function
      - name: D
        role: linear_approximation
      - name: Locus
        role: locus
      - name: X
        role: source_ambient
      - name: Y
        role: target_ambient
    returns: truth_value
    ambient_argument: Y
    polymorphic: true
    surface_forms:
      - has linear approximation
      - linear approximation
    description: >
      The object D is a linear approximation to f at or on the indicated locus.

  - id: pred:secant-line
    name: SecantLine
    kind: predicate
    category: analysis
    arguments:
      - name: ell
        role: line
        surface: '\ell'
      - name: f
        role: function
      - name: a
        role: first_point
      - name: b
        role: second_point
    returns: truth_value
    surface_forms:
      - secant line
    description: >
      The line ell is the secant line for f through the points indexed by a
      and b.

  - id: pred:is-local-maximum
    name: IsLocalMaximum
    kind: predicate
    category: analysis
    arguments:
      - name: f
        role: function
      - name: Locus
        role: locus
      - name: A
        role: domain_locus
    returns: truth_value
    surface_forms:
      - is local maximum
      - local maximum
    description: >
      The function f has a local maximum at or on the indicated locus relative
      to A.

  - id: pred:is-local-minimum
    name: IsLocalMinimum
    kind: predicate
    category: analysis
    arguments:
      - name: f
        role: function
      - name: Locus
        role: locus
      - name: A
        role: domain_locus
    returns: truth_value
    surface_forms:
      - is local minimum
      - local minimum
    description: >
      The function f has a local minimum at or on the indicated locus relative
      to A.

  - id: pred:is-local-extremum
    name: IsLocalExtremum
    kind: predicate
    category: analysis
    arguments:
      - name: f
        role: function
      - name: Locus
        role: locus
      - name: A
        role: domain_locus
    returns: truth_value
    surface_forms:
      - is local extremum
      - local extremum
    description: >
      The function f has a local maximum or local minimum at or on the
      indicated locus relative to A.

  - id: pred:is-strict-relative-maximum
    name: IsStrictRelativeMaximum
    kind: predicate
    category: analysis
    arguments:
      - name: f
        role: function
      - name: Locus
        role: locus
      - name: A
        role: domain_locus
    returns: truth_value
    surface_forms:
      - is strict relative maximum
      - strict relative maximum
    description: >
      The function f has a strict relative maximum at or on the indicated
      locus relative to A.

  - id: pred:is-strict-relative-minimum
    name: IsStrictRelativeMinimum
    kind: predicate
    category: analysis
    arguments:
      - name: f
        role: function
      - name: Locus
        role: locus
      - name: A
        role: domain_locus
    returns: truth_value
    surface_forms:
      - is strict relative minimum
      - strict relative minimum
    description: >
      The function f has a strict relative minimum at or on the indicated
      locus relative to A.

  - id: pred:is-inflection
    name: IsInflection
    kind: predicate
    category: analysis
    arguments:
      - name: f
        role: function
      - name: Locus
        role: locus
      - name: A
        role: domain_locus
    returns: truth_value
    surface_forms:
      - is inflection
      - inflection point
    description: >
      The function f has an inflection at or on the indicated locus relative
      to A.

  - id: pred:is-bounded-derivative
    name: IsBoundedDerivative
    kind: predicate
    category: analysis
    arguments:
      - name: f
        role: function
      - name: Locus
        role: locus
    returns: truth_value
    surface_forms:
      - is bounded derivative
      - bounded derivative
    description: >
      The derivative of f is bounded on the indicated locus.

  - id: pred:is-class-c
    name: IsClassC
    kind: predicate
    category: analysis
    arguments:
      - name: f
        role: function
      - name: k
        role: differentiability_order
      - name: Locus
        role: locus
    returns: truth_value
    surface_forms:
      - is class c
      - continuously differentiable
    description: >
      The function f is of class C^k on the indicated locus.

  - id: pred:has-archimedean-property
    name: HasArchimedeanProperty
    kind: predicate
    category: analysis
    arguments:
      - name: P
        role: ambient_ordered_structure
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - has archimedean property
      - archimedean
    description: >
      The ordered structure P satisfies the Archimedean property.

  - id: pred:is-order-complete
    name: IsOrderComplete
    kind: predicate
    category: analysis
    arguments:
      - name: P
        role: ambient_ordered_structure
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - OrderComplete
      - is order complete
      - order complete
    description: >
      The ordered structure P is complete with respect to its order.

  - id: pred:has-least-upper-bound-property
    name: HasLeastUpperBoundProperty
    kind: predicate
    category: analysis
    arguments:
      - name: P
        role: ambient_ordered_structure
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - has least upper bound property
      - lub property
      - supremum property
    description: >
      Every nonempty bounded-above subset of P has a least upper bound in P.

  - id: pred:is-dedekind-separation
    name: IsDedekindSeparation
    kind: predicate
    category: analysis
    arguments:
      - name: A
        role: lower_part
      - name: B
        role: upper_part
      - name: P
        role: ambient_ordered_structure
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - is dedekind separation
      - dedekind separation
    description: >
      The pair A and B forms a Dedekind separation in the ordered structure P.

  - id: pred:is-dedekind-gap
    name: IsDedekindGap
    kind: predicate
    category: analysis
    arguments:
      - name: A
        role: lower_part
      - name: B
        role: upper_part
      - name: P
        role: ambient_ordered_structure
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - is dedekind gap
      - dedekind gap
    description: >
      The pair A and B forms a Dedekind gap in the ordered structure P.

  - id: pred:is-dedekind-separator
    name: IsDedekindSeparator
    kind: predicate
    category: analysis
    arguments:
      - name: c
        role: separator
      - name: A
        role: lower_part
      - name: B
        role: upper_part
      - name: P
        role: ambient_ordered_structure
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - is dedekind separator
      - dedekind separator
      - separator point
    description: >
      The point c in the ordered structure P separates the lower part A from
      the upper part B: every element of A is at or below c, and c is at or
      below every element of B.

  - id: pred:has-dedekind-separator
    name: HasDedekindSeparator
    kind: predicate
    category: analysis
    arguments:
      - name: A
        role: lower_part
      - name: B
        role: upper_part
      - name: P
        role: ambient_ordered_structure
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - has dedekind separator
      - admits dedekind separator
      - has separator point
    description: >
      The lower part A and upper part B admit at least one Dedekind separator
      in the ordered structure P.

  - id: pred:nested-closed-intervals
    name: NestedClosedIntervals
    kind: predicate
    category: analysis
    arguments:
      - name: F
        role: interval_family
      - name: P
        role: ambient_ordered_structure
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - nested closed intervals
    description: >
      The family F is a nested family of closed intervals in P.

  - id: pred:nested
    name: Nested
    kind: predicate
    category: analysis
    arguments:
      - name: F
        role: family_or_sequence
      - name: R
        role: nesting_relation_or_order
    returns: truth_value
    ambient_argument: R
    polymorphic: true
    surface_forms:
      - nested
      - nested family
      - decreasing family
    description: >
      The family or sequence F is nested with respect to the relation or order
      R: later members are contained in, refine, or otherwise lie below
      earlier members according to R.

  - id: pred:nested-closed-bounded-intervals
    name: NestedClosedBoundedIntervals
    kind: predicate
    category: analysis
    arguments:
      - name: F
        role: interval_family
      - name: P
        role: ambient_ordered_structure
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - nested closed bounded intervals
    description: >
      The family F is a nested family of closed bounded intervals in P.

  - id: pred:is-delta-fine
    name: IsDeltaFine
    kind: predicate
    category: integration
    arguments:
      - name: T
        role: tagged_partition
      - name: delta
        role: gauge
        surface: '\delta'
      - name: I
        role: interval
    returns: truth_value
    surface_forms:
      - is delta fine
      - delta-fine
    description: >
      The tagged partition T is delta-fine on interval I.

  - id: pred:is-integrable
    name: IsIntegrable
    kind: predicate
    category: integration
    arguments:
      - name: f
        role: function
      - name: I
        role: interval
      - name: C
        role: integration_criterion
    returns: truth_value
    carried_context:
      - kind: domain
        source: type_of_argument
        argument: f
        exposes_as: admissible_input_domain
      - kind: interval
        source: argument
        argument: I
        exposes_as: integration_domain
      - kind: criterion
        source: argument
        argument: C
        exposes_as: integration_criterion
    surface_forms:
      - is integrable
      - integrable by criterion
    description: >
      The function f is integrable over interval I by the integration
      criterion C.

  - id: pred:has-definite-integral
    name: HasDefiniteIntegral
    kind: predicate
    category: integration
    arguments:
      - name: f
        role: function
      - name: I
        role: interval
      - name: C
        role: integration_criterion
      - name: A
        role: integral_value
    returns: truth_value
    surface_forms:
      - has definite integral
      - definite integral equals
    description: >
      The function f has definite integral value A over interval I by the
      integration criterion C.

  - id: pred:is-primitive-of
    name: IsPrimitiveOf
    kind: predicate
    category: integration
    arguments:
      - name: F
        role: primitive
      - name: f
        role: derivative_function
      - name: I
        role: interval
    returns: truth_value
    surface_forms:
      - is primitive of
      - is antiderivative of
      - primitive
      - antiderivative
    description: >
      The function F is a primitive, or antiderivative, of f on interval I.

  - id: pred:has-forward-difference
    name: HasForwardDifference
    kind: predicate
    category: discrete_calculus
    arguments:
      - name: f
        role: discrete_function
      - name: I
        role: discrete_domain
      - name: g
        role: forward_difference
    returns: truth_value
    surface_forms:
      - has forward difference
      - forward difference
      - discrete derivative
    description: >
      The discrete function f has forward difference g on the discrete domain
      I, meaning g records the one-step change of f.

  - id: pred:has-higher-difference
    name: HasHigherDifference
    kind: predicate
    category: discrete_calculus
    arguments:
      - name: f
        role: discrete_function
      - name: I
        role: discrete_domain
      - name: k
        role: order
      - name: g
        role: higher_difference
    returns: truth_value
    surface_forms:
      - has higher difference
      - has iterated difference
      - higher difference
    description: >
      The k-th iterated finite difference of f on the discrete domain I is g.

  - id: pred:is-antidifference-of
    name: IsAntidifferenceOf
    kind: predicate
    category: discrete_calculus
    arguments:
      - name: F
        role: antidifference
      - name: f
        role: summand_or_difference
      - name: I
        role: discrete_domain
    returns: truth_value
    surface_forms:
      - is antidifference of
      - is discrete antiderivative of
      - is indefinite sum of
    description: >
      The discrete function F is an antidifference, or discrete
      antiderivative, of f on the discrete domain I.

  - id: pred:has-finite-sum
    name: HasFiniteSum
    kind: predicate
    category: discrete_calculus
    arguments:
      - name: f
        role: summand
      - name: I
        role: finite_index_region
      - name: S
        role: sum_value
    returns: truth_value
    surface_forms:
      - has finite sum
      - finite summation
      - discrete definite integral
    description: >
      The summand f has finite sum S over the finite index region I.

  - id: pred:linear-operator
    name: LinearOperator
    kind: predicate
    category: operator
    arguments:
      - name: T
        role: operator
    returns: truth_value
    surface_forms:
      - linear operator
      - operator is linear
    description: >
      The operator T preserves the relevant linear combinations in its
      ambient function or vector space context.

  - id: pred:constant-rule
    name: ConstantRule
    kind: predicate
    category: discrete_calculus
    arguments:
      - name: Delta
        role: difference_operator
        surface: '\Delta'
    returns: truth_value
    surface_forms:
      - constant rule
      - constants have zero difference
    description: >
      The difference operator Delta sends constant discrete functions to zero.

  - id: pred:operator-identity
    name: OperatorIdentity
    kind: predicate
    category: operator
    arguments:
      - name: T
        role: left_operator
      - name: U
        role: right_operator
    returns: truth_value
    surface_forms:
      - operator identity
      - operators are identical
    description: >
      The operators T and U agree on their intended common domain.

  - id: pred:polynomial-degree
    name: PolynomialDegree
    kind: predicate
    category: polynomial
    arguments:
      - name: f
        role: polynomial_or_polynomial_sequence
      - name: d
        role: degree
    returns: truth_value
    surface_forms:
      - polynomial degree
      - has polynomial degree
    description: >
      The object f is polynomial of degree d in the relevant polynomial
      context.

  - id: pred:polynomial-detection
    name: PolynomialDetection
    kind: predicate
    category: discrete_calculus
    arguments:
      - name: f
        role: discrete_function
      - name: d
        role: degree
    returns: truth_value
    surface_forms:
      - polynomial detection
      - detects polynomial degree by differences
    description: >
      Repeated finite differences of f exhibit the constant and vanishing
      pattern associated with polynomial degree d.

  - id: pred:is-measure-zero
    name: IsMeasureZero
    kind: predicate
    category: integration
    arguments:
      - name: A
        role: subset
      - name: X
        role: ambient_space
    returns: truth_value
    ambient_argument: X
    surface_forms:
      - is measure zero
      - has measure zero
      - null set
    description: >
      The subset A has measure zero in the ambient space X.

  - id: pred:sector-parameter
    name: SectorParameter
    kind: predicate
    category: geometry
    arguments:
      - name: P
        role: point
      - name: t
        role: parameter
      - name: C
        role: geometry_context
    returns: truth_value
    ambient_argument: C
    surface_forms:
      - sector parameter
      - has sector parameter
      - hyperbolic sector parameter
    description: >
      The point P has sector parameter t in the relevant hyperbolic geometry
      context.

  - id: pred:has-bounded-variation
    name: HasBoundedVariation
    kind: predicate
    category: integration
    arguments:
      - name: f
        role: function
      - name: I
        role: interval
    returns: truth_value
    surface_forms:
      - has bounded variation
      - bounded variation
    description: >
      The function f has bounded variation on interval I.

  - id: pred:is-refinement
    name: IsRefinement
    kind: predicate
    category: integration
    arguments:
      - name: Q
        role: refined_partition
      - name: P
        role: original_partition
    returns: truth_value
    surface_forms:
      - is refinement
      - refinement
    description: >
      The partition Q refines the partition P.

  - id: pred:is-common-refinement
    name: IsCommonRefinement
    kind: predicate
    category: integration
    arguments:
      - name: R
        role: common_refinement
      - name: P
        role: first_partition
      - name: Q
        role: second_partition
    returns: truth_value
    surface_forms:
      - is common refinement
      - common refinement
    description: >
      The partition R is a common refinement of P and Q.

  - id: pred:is-step-function
    name: IsStepFunction
    kind: predicate
    category: integration
    arguments:
      - name: f
        role: function
      - name: P
        role: partition
    returns: truth_value
    surface_forms:
      - is step function
      - step function
    description: >
      The function f is a step function relative to partition P.

  - id: pred:is-piecewise-linear
    name: IsPiecewiseLinear
    kind: predicate
    category: integration
    arguments:
      - name: f
        role: function
      - name: P
        role: partition
    returns: truth_value
    surface_forms:
      - is piecewise linear
      - piecewise linear
    description: >
      The function f is piecewise linear relative to partition P.

  - id: pred:subset
    name: Subset
    kind: predicate
    category: set
    arguments:
      - name: A
        role: subset
      - name: B
        role: ambient_set
    returns: truth_value
    surface_forms:
      - subset
      - contained in
      - inclusion
    description: >
      The set A is contained in the set B.

  - id: pred:empty-set
    name: EmptySet
    kind: predicate
    category: set
    arguments:
      - name: E
        role: set
    returns: truth_value
    surface_forms:
      - empty set
      - null set
    description: >
      The set E has no elements.

  - id: pred:pairing-set
    name: PairingSet
    kind: predicate
    category: set
    arguments:
      - name: C
        role: pair_set
      - name: A
        role: left_object
      - name: B
        role: right_object
    returns: truth_value
    surface_forms:
      - pairing set
      - unordered pair set
    description: >
      The set C contains exactly the objects A and B.

  - id: pred:proper-subset
    name: ProperSubset
    kind: predicate
    category: set
    arguments:
      - name: A
        role: subset
      - name: B
        role: ambient_set
    returns: truth_value
    surface_forms:
      - proper subset
      - strict subset
    description: >
      The set A is contained in B and is not equal to B.

  - id: pred:set-equal
    name: SetEqual
    kind: predicate
    category: set
    arguments:
      - name: A
        role: left_set
      - name: B
        role: right_set
    returns: truth_value
    surface_forms:
      - set equality
      - equal sets
      - extensional equality
    description: >
      The sets A and B have exactly the same elements.

  - id: pred:union-set
    name: UnionSet
    kind: predicate
    category: set
    arguments:
      - name: C
        role: result_set
      - name: A
        role: left_set
      - name: B
        role: right_set
    returns: truth_value
    surface_forms:
      - union
      - union set
    description: >
      The set C is the union of A and B.

  - id: pred:union-family-set
    name: UnionFamilySet
    kind: predicate
    category: set
    arguments:
      - name: U
        role: result_set
      - name: A
        role: family_set
    returns: truth_value
    surface_forms:
      - union of a family
      - family union
    description: >
      The set U contains exactly the elements of members of the family set A.

  - id: pred:indexed-union-set
    name: IndexedUnionSet
    kind: predicate
    category: set
    arguments:
      - name: U
        role: result_set
      - name: F
        role: indexed_family
      - name: I
        role: index_set
    returns: truth_value
    surface_forms:
      - indexed union
    description: >
      The set U contains exactly the elements belonging to at least one member
      of the indexed family F over I.

  - id: pred:intersection-set
    name: IntersectionSet
    kind: predicate
    category: set
    arguments:
      - name: C
        role: result_set
      - name: A
        role: left_set
      - name: B
        role: right_set
    returns: truth_value
    surface_forms:
      - intersection
      - intersection set
    description: >
      The set C is the intersection of A and B.

  - id: pred:indexed-intersection-set
    name: IndexedIntersectionSet
    kind: predicate
    category: set
    arguments:
      - name: J
        role: result_set
      - name: F
        role: indexed_family
      - name: I
        role: index_set
    returns: truth_value
    surface_forms:
      - indexed intersection
    description: >
      The set J contains exactly the elements belonging to every member of the
      indexed family F over I.

  - id: pred:set-difference
    name: SetDifference
    kind: predicate
    category: set
    arguments:
      - name: C
        role: result_set
      - name: A
        role: minuend
      - name: B
        role: subtrahend
    returns: truth_value
    surface_forms:
      - set difference
      - relative complement
    description: >
      The set C contains exactly the elements of A that are not elements of B.

  - id: pred:symmetric-difference
    name: SymmetricDifference
    kind: predicate
    category: set
    arguments:
      - name: C
        role: result_set
      - name: A
        role: left_set
      - name: B
        role: right_set
    returns: truth_value
    surface_forms:
      - symmetric difference
    description: >
      The set C contains exactly the elements that belong to exactly one of A
      and B.

  - id: pred:complement-set
    name: ComplementSet
    kind: predicate
    category: set
    arguments:
      - name: C
        role: complement
      - name: A
        role: set
      - name: U
        role: ambient_set
    returns: truth_value
    surface_forms:
      - complement
      - set complement
    description: >
      The set C is the complement of A relative to the ambient set U.

  - id: pred:power-set
    name: PowerSet
    kind: predicate
    category: set
    arguments:
      - name: P
        role: power_set
      - name: A
        role: set
    returns: truth_value
    surface_forms:
      - power set
    description: >
      The set P contains exactly the subsets of A.

  - id: pred:inductive-set
    name: InductiveSet
    kind: predicate
    category: set
    arguments:
      - name: A
        role: set
    returns: truth_value
    surface_forms:
      - inductive set
    description: >
      The set A contains the empty set and is closed under the successor
      operation x maps to x union {x}.

  - id: pred:separation-subset
    name: SeparationSubset
    kind: predicate
    category: set
    arguments:
      - name: B
        role: subset
      - name: A
        role: ambient_set
      - name: phi
        role: defining_property
    returns: truth_value
    surface_forms:
      - separation subset
      - definable subset
    description: >
      The set B consists exactly of the elements of A satisfying the defining
      property phi.

  - id: pred:replacement-image
    name: ReplacementImage
    kind: predicate
    category: set
    arguments:
      - name: B
        role: image_set
      - name: A
        role: domain_set
      - name: phi
        role: functional_formula
    returns: truth_value
    surface_forms:
      - replacement image
      - definable image
    description: >
      The set B is the image of A under the definable functional relation phi.

  - id: pred:foundation-minimal-element
    name: FoundationMinimalElement
    kind: predicate
    category: set
    arguments:
      - name: x
        role: minimal_element
      - name: A
        role: set
    returns: truth_value
    surface_forms:
      - foundation minimal element
      - membership minimal element
    description: >
      The element x belongs to A and is disjoint from A.

  - id: pred:choice-function
    name: ChoiceFunction
    kind: predicate
    category: function
    arguments:
      - name: f
        role: function
      - name: A
        role: family_set
    returns: truth_value
    surface_forms:
      - choice function
      - selection function
    description: >
      The function f selects an element from each member of the family set A.

  - id: pred:pairwise-disjoint-family
    name: PairwiseDisjointFamily
    kind: predicate
    category: set
    arguments:
      - name: F
        role: indexed_family
      - name: I
        role: index_set
    returns: truth_value
    surface_forms:
      - pairwise disjoint family
      - pairwise disjoint
    description: >
      Distinct indices in I identify sets in F with empty pairwise intersections.

  - id: pred:inclusion-monotone-operation
    name: InclusionMonotoneOperation
    kind: predicate
    category: set
    arguments:
      - name: F
        role: operation
    returns: truth_value
    surface_forms:
      - inclusion-monotone
      - monotone set operation
    description: >
      The operation F preserves set inclusion in the indicated argument.

  - id: pred:inclusion-antitone-operation
    name: InclusionAntitoneOperation
    kind: predicate
    category: set
    arguments:
      - name: F
        role: operation
    returns: truth_value
    surface_forms:
      - inclusion-antitone
      - antitone set operation
    description: >
      The operation F reverses set inclusion in the indicated argument.

  - id: pred:set-dual
    name: SetDual
    kind: predicate
    category: set
    arguments:
      - name: E
        role: expression
      - name: E_prime
        role: dual_expression
        surface: "E'"
      - name: U
        role: ambient_set
    returns: truth_value
    surface_forms:
      - set duality
      - dual expression
    description: >
      The expression E_prime is obtained from E by interchanging the set
      operations and constants specified by set duality over U.

  - id: pred:covers
    name: Covers
    kind: predicate
    category: set
    arguments:
      - name: C
        role: cover_family
      - name: A
        role: covered_set
    returns: truth_value
    surface_forms:
      - cover
      - covers
      - set cover
    description: >
      The family C covers A, meaning every point of A belongs to at least one
      member of C.

  - id: pred:open-cover
    name: OpenCover
    kind: predicate
    category: topology
    arguments:
      - name: C
        role: cover_family
      - name: A
        role: covered_set
      - name: T
        role: ambient
    returns: truth_value
    ambient_argument: T
    surface_forms:
      - open cover
      - topological cover
    description: >
      The family C covers A and each member of C is open in the ambient
      topological structure T.

  - id: pred:finite-set
    name: FiniteSet
    kind: predicate
    category: set
    arguments:
      - name: A
        role: set
    returns: truth_value
    surface_forms:
      - finite set
      - finite
    description: >
      The set A has finitely many elements.

  - id: pred:infinite-set
    name: InfiniteSet
    kind: predicate
    category: set
    arguments:
      - name: A
        role: set
    returns: truth_value
    logical_negation_of: pred:finite-set
    surface_forms:
      - infinite set
      - infinite
    description: >
      The set A is not finite.

  - id: pred:same-cardinality
    name: SameCardinality
    kind: predicate
    category: set
    arguments:
      - name: A
        role: left_set
      - name: B
        role: right_set
    returns: truth_value
    surface_forms:
      - same cardinality
      - equinumerous
      - bijective correspondence
    description: >
      The sets A and B admit a bijection between them.

  - id: pred:cardinality-leq
    name: CardinalityLeq
    kind: predicate
    category: set
    arguments:
      - name: A
        role: left_set
      - name: B
        role: right_set
    returns: truth_value
    surface_forms:
      - cardinality at most
      - cardinality less than or equal
      - injection exists
    description: >
      The cardinality of A is at most the cardinality of B, usually witnessed
      by an injection from A into B.

  - id: pred:cardinality-lt
    name: CardinalityLt
    kind: predicate
    category: set
    arguments:
      - name: A
        role: left_set
      - name: B
        role: right_set
    returns: truth_value
    surface_forms:
      - cardinality less than
      - strictly smaller cardinality
    description: >
      The cardinality of A is at most the cardinality of B, but A and B do not
      have the same cardinality.

  - id: pred:countably-infinite-set
    name: CountablyInfiniteSet
    kind: predicate
    category: set
    arguments:
      - name: A
        role: set
    returns: truth_value
    surface_forms:
      - countably infinite set
      - countably infinite
    description: >
      The set A has the same cardinality as the natural numbers.

  - id: pred:countable-set
    name: CountableSet
    kind: predicate
    category: set
    arguments:
      - name: A
        role: set
    returns: truth_value
    surface_forms:
      - countable set
      - countable
    description: >
      The set A is finite or countably infinite.

  - id: pred:uncountable-set
    name: UncountableSet
    kind: predicate
    category: set
    arguments:
      - name: A
        role: set
    returns: truth_value
    logical_negation_of: pred:countable-set
    surface_forms:
      - uncountable set
      - uncountable
    description: >
      The set A is infinite and not countable.

  - id: pred:finite-intersection-property
    name: FiniteIntersectionProperty
    kind: predicate
    category: set
    arguments:
      - name: F
        role: family
    returns: truth_value
    surface_forms:
      - finite intersection property
      - fip
    description: >
      Every finite subfamily of F has nonempty intersection.

  - id: pred:relation-on
    name: RelationOn
    kind: predicate
    category: relation
    arguments:
      - name: R
        role: relation
      - name: A
        role: carrier
    returns: truth_value
    surface_forms:
      - relation on
      - binary relation
    description: >
      The object R is a binary relation on A.

  - id: pred:ordered-pair
    name: OrderedPair
    kind: predicate
    category: relation
    arguments:
      - name: p
        role: ordered_pair
      - name: a
        role: first_component
      - name: b
        role: second_component
    returns: truth_value
    surface_forms:
      - ordered pair
      - ordered pair encoding
    description: >
      The object p is the ordered pair with first component a and second
      component b.

  - id: pred:cartesian-product
    name: CartesianProduct
    kind: predicate
    category: set
    arguments:
      - name: P
        role: product_set
      - name: A
        role: left_set
      - name: B
        role: right_set
    returns: truth_value
    surface_forms:
      - cartesian product
      - product set
    description: >
      The set P is the Cartesian product of A and B.

  - id: pred:relation-from
    name: RelationFrom
    kind: predicate
    category: relation
    arguments:
      - name: R
        role: relation
      - name: A
        role: domain_carrier
      - name: B
        role: codomain_carrier
    returns: truth_value
    surface_forms:
      - relation from
      - relation between
    description: >
      The object R is a binary relation from A to B.

  - id: pred:relation-domain-element
    name: RelationDomainElement
    kind: predicate
    category: relation
    arguments:
      - name: a
        role: element
      - name: R
        role: relation
      - name: A
        role: domain_carrier
      - name: B
        role: codomain_carrier
    returns: truth_value
    surface_forms:
      - relation domain element
      - domain of a relation
    description: >
      The element a belongs to the domain of the relation R from A to B.

  - id: pred:relation-range-element
    name: RelationRangeElement
    kind: predicate
    category: relation
    arguments:
      - name: b
        role: element
      - name: R
        role: relation
      - name: A
        role: domain_carrier
      - name: B
        role: codomain_carrier
    returns: truth_value
    surface_forms:
      - relation range element
      - range of a relation
    description: >
      The element b belongs to the range of the relation R from A to B.

  - id: pred:converse-relation-element
    name: ConverseRelationElement
    kind: predicate
    category: relation
    arguments:
      - name: b
        role: first_component
      - name: a
        role: second_component
      - name: R
        role: relation
    returns: truth_value
    surface_forms:
      - converse relation
      - inverse relation
    description: >
      The ordered pair (b,a) belongs to the converse of R.

  - id: pred:identity-relation
    name: IdentityRelation
    kind: predicate
    category: relation
    arguments:
      - name: Delta
        role: relation
        surface: '\Delta'
      - name: A
        role: carrier
    returns: truth_value
    surface_forms:
      - identity relation
      - diagonal relation
    description: >
      The relation Delta is the identity relation on A.

  - id: pred:relation-composition-element
    name: RelationCompositionElement
    kind: predicate
    category: relation
    arguments:
      - name: a
        role: first_component
      - name: c
        role: second_component
      - name: S
        role: outer_relation
      - name: R
        role: inner_relation
    returns: truth_value
    surface_forms:
      - relation composition
      - composed relation
    description: >
      The ordered pair (a,c) belongs to the composition S composed with R.

  - id: pred:null-relation
    name: NullRelation
    kind: predicate
    category: relation
    arguments:
      - name: R
        role: relation
      - name: A
        role: domain_carrier
      - name: B
        role: codomain_carrier
    returns: truth_value
    surface_forms:
      - null relation
      - empty relation
    description: >
      The relation R from A to B has no related pairs.

  - id: pred:universal-relation
    name: UniversalRelation
    kind: predicate
    category: relation
    arguments:
      - name: R
        role: relation
      - name: A
        role: domain_carrier
      - name: B
        role: codomain_carrier
    returns: truth_value
    surface_forms:
      - universal relation
      - full relation
    description: >
      The relation R from A to B is all of A times B.

  - id: pred:relation-inclusion
    name: RelationInclusion
    kind: predicate
    category: relation
    arguments:
      - name: R
        role: subrelation
      - name: S
        role: superrelation
      - name: A
        role: domain_carrier
      - name: B
        role: codomain_carrier
    returns: truth_value
    surface_forms:
      - relation inclusion
      - subrelation
    description: >
      Every ordered pair in R is also an ordered pair in S.

  - id: pred:relation-equality
    name: RelationEquality
    kind: predicate
    category: relation
    arguments:
      - name: R
        role: left_relation
      - name: S
        role: right_relation
      - name: A
        role: domain_carrier
      - name: B
        role: codomain_carrier
    returns: truth_value
    surface_forms:
      - relation equality
      - equal relations
    description: >
      The relations R and S have exactly the same ordered pairs.

  - id: pred:relation-extension
    name: RelationExtension
    kind: predicate
    category: relation
    arguments:
      - name: R_B
        role: extended_relation
        surface: 'R_B'
      - name: R_A
        role: original_relation
        surface: 'R_A'
      - name: A
        role: original_carrier
      - name: B
        role: extended_carrier
    returns: truth_value
    ambient_argument: B
    surface_forms:
      - relation extension
      - extends relation
      - relation agrees on a subcarrier
    description: >
      The relation R_B on B extends the relation R_A on A by agreeing with
      R_A whenever all compared elements lie in A.

  - id: pred:one-to-many-relation
    name: OneToManyRelation
    kind: predicate
    category: relation
    arguments:
      - name: R
        role: relation
      - name: A
        role: domain_carrier
      - name: B
        role: codomain_carrier
    returns: truth_value
    surface_forms:
      - one-to-many relation
      - one to many
    description: >
      Some element of A is related by R to two distinct elements of B.

  - id: pred:many-to-one-relation
    name: ManyToOneRelation
    kind: predicate
    category: relation
    arguments:
      - name: R
        role: relation
      - name: A
        role: domain_carrier
      - name: B
        role: codomain_carrier
    returns: truth_value
    surface_forms:
      - many-to-one relation
      - many to one
    description: >
      Two distinct elements of A are related by R to the same element of B.

  - id: pred:many-to-many-relation
    name: ManyToManyRelation
    kind: predicate
    category: relation
    arguments:
      - name: R
        role: relation
      - name: A
        role: domain_carrier
      - name: B
        role: codomain_carrier
    returns: truth_value
    surface_forms:
      - many-to-many relation
      - many to many
    description: >
      The relation R is both one-to-many and many-to-one.

  - id: pred:many-place-relation
    name: ManyPlaceRelation
    kind: predicate
    category: relation
    arguments:
      - name: R
        role: relation
      - name: n
        role: arity
      - name: A_i
        role: carriers
    returns: truth_value
    surface_forms:
      - many-place relation
      - n-place relation
      - ternary relation
    description: >
      The relation R is a subset of a finite Cartesian product of n carrier
      sets.

  - id: pred:reflexive
    name: Reflexive
    kind: predicate
    category: relation
    arguments:
      - name: R
        role: relation
      - name: A
        role: carrier
    returns: truth_value
    surface_forms:
      - reflexive
      - reflexive relation
    description: >
      Every element of A is related to itself by R.

  - id: pred:irreflexive
    name: Irreflexive
    kind: predicate
    category: relation
    arguments:
      - name: R
        role: relation
      - name: A
        role: carrier
    returns: truth_value
    surface_forms:
      - irreflexive
      - irreflexive relation
    description: >
      No element of A is related to itself by R.

  - id: pred:symmetric
    name: Symmetric
    kind: predicate
    category: relation
    arguments:
      - name: R
        role: relation
      - name: A
        role: carrier
    returns: truth_value
    surface_forms:
      - symmetric
      - symmetric relation
    description: >
      Whenever one element of A is related to another by R, the reverse
      relation also holds.

  - id: pred:antisymmetric
    name: Antisymmetric
    kind: predicate
    category: relation
    arguments:
      - name: R
        role: relation
      - name: A
        role: carrier
    returns: truth_value
    surface_forms:
      - antisymmetric
      - antisymmetric relation
    description: >
      Two elements of A that are related in both directions by R must be equal.

  - id: pred:asymmetric
    name: Asymmetric
    kind: predicate
    category: relation
    arguments:
      - name: R
        role: relation
      - name: A
        role: carrier
    returns: truth_value
    surface_forms:
      - asymmetric
      - asymmetric relation
    description: >
      Whenever one element of A is related to another by R, the reverse
      relation does not hold.

  - id: pred:transitive
    name: Transitive
    kind: predicate
    category: relation
    arguments:
      - name: R
        role: relation
      - name: A
        role: carrier
    returns: truth_value
    surface_forms:
      - transitive
      - transitive relation
    description: >
      The relation R can be chained across three elements of A.

  - id: pred:total-relation
    name: TotalRelation
    kind: predicate
    category: relation
    arguments:
      - name: R
        role: relation
      - name: A
        role: carrier
    returns: truth_value
    surface_forms:
      - total relation
      - connex relation
      - comparable relation
    description: >
      Any two elements of A are comparable by the relation R.

  - id: pred:equivalence-relation
    name: EquivalenceRelation
    kind: predicate
    category: relation
    arguments:
      - name: R
        role: relation
      - name: A
        role: carrier
    returns: truth_value
    surface_forms:
      - equivalence relation
    description: >
      The relation R is reflexive, symmetric, and transitive on A.

  - id: pred:equivalence-class
    name: EquivalenceClass
    kind: predicate
    category: relation
    arguments:
      - name: C
        role: class
      - name: a
        role: representative
      - name: R
        role: relation
      - name: A
        role: carrier
    returns: truth_value
    surface_forms:
      - equivalence class
      - class of a representative
    description: >
      The set C is the equivalence class of a under R on A.

  - id: pred:quotient-set
    name: QuotientSet
    kind: predicate
    category: relation
    arguments:
      - name: Q
        role: quotient_set
      - name: A
        role: carrier
      - name: R
        role: relation
    returns: truth_value
    surface_forms:
      - quotient set
      - set of equivalence classes
    description: >
      The set Q consists of the equivalence classes of A under R.

  - id: pred:canonical-quotient-map
    name: CanonicalQuotientMap
    kind: predicate
    category: function
    arguments:
      - name: pi
        role: function
        surface: '\pi'
      - name: A
        role: domain
      - name: R
        role: relation
      - name: Q
        role: quotient_set
    returns: truth_value
    surface_forms:
      - canonical surjection
      - quotient map
      - canonical quotient map
    description: >
      The function pi maps each element of A to its equivalence class in Q.

  - id: pred:constant-on-equivalence-classes
    name: ConstantOnEquivalenceClasses
    kind: predicate
    category: function
    arguments:
      - name: f
        role: function
      - name: R
        role: relation
      - name: A
        role: carrier
    returns: truth_value
    surface_forms:
      - constant on equivalence classes
      - respects equivalence
    description: >
      The function f takes equal values on elements of A that are related by R.

  - id: pred:preorder
    name: Preorder
    kind: predicate
    category: relation
    arguments:
      - name: R
        role: relation
      - name: A
        role: carrier
    returns: truth_value
    surface_forms:
      - preorder
      - preordered relation
    description: >
      The relation R is reflexive and transitive on A.

  - id: pred:partial-order
    name: PartialOrder
    kind: predicate
    category: relation
    arguments:
      - name: R
        role: relation
      - name: A
        role: carrier
    returns: truth_value
    surface_forms:
      - partial order
      - poset order
    description: >
      The relation R is reflexive, antisymmetric, and transitive on A.

  - id: pred:strict-partial-order
    name: StrictPartialOrder
    kind: predicate
    category: relation
    arguments:
      - name: R
        role: relation
      - name: A
        role: carrier
    returns: truth_value
    surface_forms:
      - strict partial order
      - strict order
    description: >
      The relation R is irreflexive and transitive on A.

  - id: pred:total-order
    name: TotalOrder
    kind: predicate
    category: relation
    arguments:
      - name: R
        role: relation
      - name: A
        role: carrier
    returns: truth_value
    surface_forms:
      - total order
      - linear order
    description: >
      The relation R is a partial order on A and any two elements of A are
      comparable by R.

  - id: pred:is-well-ordered-set
    name: IsWellOrderedSet
    kind: predicate
    category: order
    arguments:
      - name: W
        role: well_ordered_set_structure
    returns: truth_value
    ambient_argument: W
    surface_forms:
      - is a well-ordered set
      - well-ordering principle
      - well-order laws
    description: >
      The packaged well-ordered-set data satisfies the well-order condition:
      every nonempty subset of the carrier has a least element.

  - id: pred:function
    name: Function
    kind: predicate
    category: function
    arguments:
      - name: f
        role: function
      - name: A
        role: domain
      - name: B
        role: codomain
    returns: truth_value
    surface_forms:
      - function
      - map
      - mapping
    description: >
      The object f is a function with domain A and codomain B.

  - id: pred:function-space
    name: FunctionSpace
    kind: predicate
    category: function
    arguments:
      - name: F
        role: function_space
      - name: A
        role: domain
      - name: B
        role: codomain
    returns: truth_value
    surface_forms:
      - function space
      - set of functions
    description: >
      The set F consists exactly of the functions with domain A and codomain B.

  - id: pred:functional-relation
    name: FunctionalRelation
    kind: predicate
    category: function
    arguments:
      - name: R
        role: relation
      - name: A
        role: domain
      - name: B
        role: codomain
    returns: truth_value
    surface_forms:
      - functional relation
      - right-unique relation
    description: >
      The relation R assigns at most one output in B to each input in A.

  - id: pred:total-on-domain
    name: TotalOnDomain
    kind: predicate
    category: function
    arguments:
      - name: R
        role: relation
      - name: A
        role: domain
      - name: B
        role: codomain
    returns: truth_value
    surface_forms:
      - total on domain
      - left-total relation
    description: >
      The relation R assigns at least one output in B to each input in A.

  - id: pred:partial-function
    name: PartialFunction
    kind: predicate
    category: function
    arguments:
      - name: R
        role: relation
      - name: A
        role: domain
      - name: B
        role: codomain
    returns: truth_value
    surface_forms:
      - partial function
      - partial map
    description: >
      The relation R is single-valued from A to B but need not be defined on
      every input in A.

  - id: pred:function-equal
    name: FunctionEqual
    kind: predicate
    category: function
    arguments:
      - name: f
        role: left_function
      - name: g
        role: right_function
    returns: truth_value
    surface_forms:
      - function equality
      - equal functions
    description: >
      The functions f and g have the same domain, codomain, and pointwise
      values.

  - id: pred:domain-of-function
    name: DomainOfFunction
    kind: predicate
    category: function
    arguments:
      - name: f
        role: function
      - name: A
        role: domain
    returns: truth_value
    surface_forms:
      - domain of a function
      - function domain
    description: >
      The set A is the declared domain of the function f.

  - id: pred:codomain-of-function
    name: CodomainOfFunction
    kind: predicate
    category: function
    arguments:
      - name: f
        role: function
      - name: B
        role: codomain
    returns: truth_value
    surface_forms:
      - codomain of a function
      - function codomain
    description: >
      The set B is the declared codomain of the function f.

  - id: pred:empty-function
    name: EmptyFunction
    kind: predicate
    category: function
    arguments:
      - name: E
        role: function
      - name: B
        role: codomain
    returns: truth_value
    surface_forms:
      - empty function
    description: >
      The empty relation is viewed as the unique function from the empty set to
      B.

  - id: pred:many-place-functional-relation
    name: ManyPlaceFunctionalRelation
    kind: predicate
    category: function
    arguments:
      - name: R
        role: relation
      - name: A
        role: input_domains
      - name: B
        role: output_codomain
    returns: truth_value
    surface_forms:
      - many-place functional relation
      - functional in the last coordinate
    description: >
      The relation R is single-valued in its output coordinate for each tuple
      of input coordinates.

  - id: pred:injective
    name: Injective
    kind: predicate
    category: function
    arguments:
      - name: f
        role: function
      - name: A
        role: domain
      - name: B
        role: codomain
    returns: truth_value
    surface_forms:
      - injective
      - one-to-one
    description: >
      The function f maps distinct elements of A to distinct elements of B.

  - id: pred:surjective
    name: Surjective
    kind: predicate
    category: function
    arguments:
      - name: f
        role: function
      - name: A
        role: domain
      - name: B
        role: codomain
    returns: truth_value
    surface_forms:
      - surjective
      - onto
    description: >
      Every element of B is attained as f(a) for some a in A.

  - id: pred:bijective
    name: Bijective
    kind: predicate
    category: function
    arguments:
      - name: f
        role: function
      - name: A
        role: domain
      - name: B
        role: codomain
    returns: truth_value
    surface_forms:
      - bijective
      - bijection
    description: >
      The function f is both injective and surjective from A to B.

  - id: pred:inverse-function
    name: InverseFunction
    kind: predicate
    category: function
    arguments:
      - name: g
        role: inverse_candidate
      - name: f
        role: function
      - name: A
        role: domain
      - name: B
        role: codomain
    returns: truth_value
    surface_forms:
      - inverse function
      - two-sided inverse
    description: >
      The function g from B to A is a two-sided inverse of f from A to B.

  - id: pred:left-inverse
    name: LeftInverse
    kind: predicate
    category: function
    arguments:
      - name: g
        role: inverse_candidate
      - name: f
        role: function
      - name: A
        role: domain
      - name: B
        role: codomain
    returns: truth_value
    surface_forms:
      - left inverse
    description: >
      The function g is a left inverse of f, so g composed with f is the
      identity on A.

  - id: pred:right-inverse
    name: RightInverse
    kind: predicate
    category: function
    arguments:
      - name: h
        role: inverse_candidate
      - name: f
        role: function
      - name: A
        role: domain
      - name: B
        role: codomain
    returns: truth_value
    surface_forms:
      - right inverse
    description: >
      The function h is a right inverse of f, so f composed with h is the
      identity on B.

  - id: pred:constant-function
    name: ConstantFunction
    kind: predicate
    category: function
    arguments:
      - name: f
        role: function
      - name: A
        role: domain
      - name: B
        role: codomain
    returns: truth_value
    surface_forms:
      - constant function
      - constant map
    description: >
      The function f takes the same value in B on every input from A.

  - id: pred:constant-on
    name: ConstantOn
    kind: predicate
    category: function
    arguments:
      - name: X
        role: object_or_operator
      - name: A
        role: region_or_domain
    returns: truth_value
    ambient_argument: A
    polymorphic: true
    surface_forms:
      - constant on
      - locally constant on
      - constant over
    description: >
      The object, expression, function, operator, or set-valued assignment X
      has the same value on every admissible input from the region or domain A.
      This covers functions constant on intervals or sets, operators constant
      on a class of inputs, and formation rules that return the same output
      over a specified domain.

  - id: pred:composition-compatible
    name: CompositionCompatible
    kind: predicate
    category: function
    arguments:
      - name: f
        role: inner_function
      - name: g
        role: outer_function
    returns: truth_value
    surface_forms:
      - composable functions
      - composition compatible
    description: >
      The codomain of f and domain of g are compatible so that g composed with
      f is defined.

  - id: pred:image-element
    name: ImageElement
    kind: predicate
    category: function
    arguments:
      - name: b
        role: element
      - name: f
        role: function
      - name: S
        role: subset
    returns: truth_value
    surface_forms:
      - image element
      - belongs to image
    description: >
      The element b lies in the image of S under f.

  - id: pred:preimage-element
    name: PreimageElement
    kind: predicate
    category: function
    arguments:
      - name: a
        role: element
      - name: f
        role: function
      - name: T
        role: subset
    returns: truth_value
    surface_forms:
      - preimage element
      - belongs to preimage
    description: >
      The element a lies in the preimage of T under f.

  - id: pred:cover-relation
    name: CoverRelation
    kind: predicate
    category: order
    arguments:
      - name: a
        role: lower_element
      - name: b
        role: upper_element
      - name: P
        role: ambient
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - cover relation
      - covers
    description: >
      The element b covers a in the ambient ordered structure P, with no
      element strictly between them.

  - id: pred:hasse-diagram
    name: HasseDiagram
    kind: predicate
    category: order
    arguments:
      - name: G
        role: graph
      - name: P
        role: ambient
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - Hasse diagram
      - order diagram
    description: >
      The graph G records the cover relations of the finite ambient ordered
      structure P.

  - id: pred:order-duality
    name: OrderDuality
    kind: predicate
    category: order
    arguments:
      - name: phi
        role: original_statement
        surface: '\Phi'
      - name: phi_star
        role: dual_statement
        surface: '\Phi^*'
      - name: P
        role: ambient
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - order duality
      - duality principle
    description: >
      The statement phi over an ordered structure corresponds to the dual
      statement phi_star over the dual order.

  - id: pred:induced-order
    name: InducedOrder
    kind: predicate
    category: order
    arguments:
      - name: R
        role: induced_relation
      - name: f
        role: inducing_function
      - name: Q
        role: codomain_ambient
    returns: truth_value
    ambient_argument: Q
    surface_forms:
      - induced order
      - pullback order
    description: >
      The relation R compares domain elements by applying f and then comparing
      their images in the ambient ordered structure Q.

  - id: pred:function-indistinguishable
    name: FunctionIndistinguishable
    kind: predicate
    category: order
    arguments:
      - name: x
        role: first_element
      - name: y
        role: second_element
      - name: f
        role: function
      - name: Q
        role: codomain_ambient
    returns: truth_value
    ambient_argument: Q
    surface_forms:
      - f-indistinguishable
      - indistinguishable through f
    description: >
      The elements x and y cannot be separated by the order of Q after applying
      f.

  - id: pred:suborder
    name: Suborder
    kind: predicate
    category: order
    arguments:
      - name: R
        role: restricted_relation
      - name: S
        role: subset
      - name: P
        role: ambient
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - suborder
      - inherited order
      - restricted order
    description: >
      The relation R is the order inherited by the subset S from the ambient
      ordered structure P.

  - id: pred:symmetric-part
    name: SymmetricPart
    kind: predicate
    category: relation
    arguments:
      - name: I
        role: symmetric_part
      - name: R
        role: relation
      - name: X
        role: carrier
    returns: truth_value
    surface_forms:
      - symmetric part
      - indifference part
    description: >
      The relation I contains exactly the pairs of R whose reverse pair also
      belongs to R.

  - id: pred:asymmetric-part
    name: AsymmetricPart
    kind: predicate
    category: relation
    arguments:
      - name: P
        role: asymmetric_part
      - name: R
        role: relation
      - name: X
        role: carrier
    returns: truth_value
    surface_forms:
      - asymmetric part
      - strict part
    description: >
      The relation P contains exactly the pairs of R whose reverse pair does
      not belong to R.

  - id: pred:preorder-extension
    name: PreorderExtension
    kind: predicate
    category: order
    arguments:
      - name: R_prime
        role: extension_relation
        surface: "R'"
      - name: R
        role: original_relation
      - name: X
        role: carrier
    returns: truth_value
    surface_forms:
      - preorder extension
      - extension of a preorder
    description: >
      The preorder R_prime extends R by preserving weak comparisons and strict
      comparisons on X.

  - id: pred:complete-preorder-extension
    name: CompletePreorderExtension
    kind: predicate
    category: order
    arguments:
      - name: R_prime
        role: complete_extension_relation
        surface: "R'"
      - name: R
        role: original_relation
      - name: X
        role: carrier
    returns: truth_value
    surface_forms:
      - complete preorder extension
      - complete extension
    description: >
      The relation R_prime is a complete preorder on X and extends the original
      preorder R.

  - id: pred:only-weak-cycles
    name: OnlyWeakCycles
    kind: predicate
    category: order
    arguments:
      - name: R
        role: relation
      - name: X
        role: carrier
    returns: truth_value
    surface_forms:
      - only weak cycles
      - OWC
    description: >
      No finite chain in the transitive closure of R is reversed by a strict
      comparison from the asymmetric part of R.

  - id: pred:upper-bound
    name: UpperBound
    kind: predicate
    category: order
    arguments:
      - name: u
        role: upper_bound_candidate
      - name: S
        role: subset
      - name: P
        role: ambient
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - upper bound
      - bounded above
    description: >
      The element u is an upper bound of S in the ambient ordered structure P.

  - id: pred:lower-bound
    name: LowerBound
    kind: predicate
    category: order
    arguments:
      - name: ell
        role: lower_bound_candidate
        surface: '\ell'
      - name: S
        role: subset
      - name: P
        role: ambient
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - lower bound
      - bounded below
    description: >
      The element ell is a lower bound of S in the ambient ordered structure P.

  - id: pred:bounded-above
    name: BoundedAbove
    kind: predicate
    category: order
    arguments:
      - name: S
        role: subset
      - name: P
        role: ambient
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - bounded above
      - has an upper bound
    description: >
      The subset S has at least one upper bound in the ambient ordered
      structure P.

  - id: pred:bounded-below
    name: BoundedBelow
    kind: predicate
    category: order
    arguments:
      - name: S
        role: subset
      - name: P
        role: ambient
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - bounded below
      - has a lower bound
    description: >
      The subset S has at least one lower bound in the ambient ordered
      structure P.

  - id: pred:bounded
    name: Bounded
    kind: predicate
    category: order
    arguments:
      - name: S
        role: subset
      - name: P
        role: ambient
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - bounded
      - bounded set
      - bounded subset
    description: >
      The subset S is both bounded above and bounded below in the ambient
      ordered structure P.

  - id: pred:minimal-element
    name: MinimalElement
    kind: predicate
    category: order
    arguments:
      - name: m
        role: minimal_element_candidate
      - name: S
        role: subset
      - name: P
        role: ambient
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - minimal element
    description: >
      The element m belongs to S and no element of S is strictly below m in the
      ambient ordered structure P.

  - id: pred:maximal-element
    name: MaximalElement
    kind: predicate
    category: order
    arguments:
      - name: M
        role: maximal_element_candidate
      - name: S
        role: subset
      - name: P
        role: ambient
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - maximal element
    description: >
      The element M belongs to S and no element of S is strictly above M in the
      ambient ordered structure P.

  - id: pred:least-element
    name: LeastElement
    kind: predicate
    category: order
    arguments:
      - name: ell
        role: least_element_candidate
        surface: '\ell'
      - name: S
        role: subset
      - name: P
        role: ambient
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - least element
      - minimum element
    description: >
      The element ell belongs to S and lies below every element of S in the
      ambient ordered structure P.

  - id: pred:greatest-element
    name: GreatestElement
    kind: predicate
    category: order
    arguments:
      - name: g
        role: greatest_element_candidate
      - name: S
        role: subset
      - name: P
        role: ambient
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - greatest element
      - maximum element
    description: >
      The element g belongs to S and lies above every element of S in the
      ambient ordered structure P.

  - id: pred:least-upper-bound
    name: LeastUpperBound
    kind: predicate
    category: order
    arguments:
      - name: u_star
        role: supremum_candidate
        surface: 'u^*'
      - name: S
        role: subset
      - name: P
        role: ambient
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - least upper bound
      - supremum
      - sup
    description: >
      The element u_star is the least upper bound of S in the ambient ordered
      structure P.

  - id: pred:epsilon-characterization-of-supremum
    name: EpsilonCharacterizationOfSupremum
    kind: predicate
    category: order
    arguments:
      - name: u_star
        role: supremum_candidate
        surface: 'u^*'
      - name: S
        role: subset
      - name: P
        role: ambient
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - epsilon characterization of supremum
      - epsilon characterization of least upper bound
    description: >
      Epsilon-characterization alias for LeastUpperBound(u_star,S,P): u_star
      is an upper bound of S in P and S has points arbitrarily close below
      u_star.

  - id: pred:greatest-lower-bound
    name: GreatestLowerBound
    kind: predicate
    category: order
    arguments:
      - name: ell_star
        role: infimum_candidate
        surface: '\ell^*'
      - name: S
        role: subset
      - name: P
        role: ambient
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - greatest lower bound
      - infimum
      - inf
    description: >
      The element ell_star is the greatest lower bound of S in the ambient
      ordered structure P.

  - id: pred:epsilon-characterization-of-infimum
    name: EpsilonCharacterizationOfInfimum
    kind: predicate
    category: order
    arguments:
      - name: ell_star
        role: infimum_candidate
        surface: '\ell^*'
      - name: S
        role: subset
      - name: P
        role: ambient
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - epsilon characterization of infimum
      - epsilon characterization of greatest lower bound
    description: >
      Epsilon-characterization alias for GreatestLowerBound(ell_star,S,P):
      ell_star is a lower bound of S in P and S has points arbitrarily close
      above ell_star.

  - id: pred:chain
    name: Chain
    kind: predicate
    category: order
    arguments:
      - name: C
        role: subset
      - name: P
        role: ambient
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - chain
      - totally ordered subset
    description: >
      The subset C is pairwise comparable in the ambient ordered structure P.

  - id: pred:antichain
    name: Antichain
    kind: predicate
    category: order
    arguments:
      - name: C
        role: subset
      - name: P
        role: ambient
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - antichain
    description: >
      No two distinct elements of C are comparable in the ambient ordered
      structure P.

  - id: pred:initial-segment
    name: InitialSegment
    kind: predicate
    category: order
    arguments:
      - name: I
        role: subset
      - name: P
        role: ambient
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - initial segment
      - down-set
      - downward closed
    description: >
      The subset I is downward closed in the ambient ordered structure P.

  - id: pred:trichotomy
    name: Trichotomy
    kind: predicate
    category: order
    arguments:
      - name: lt
        role: strict_order_relation
        surface: '<'
      - name: A
        role: carrier
    returns: truth_value
    surface_forms:
      - trichotomy
      - trichotomy law
    description: >
      Every pair of elements of A satisfies exactly one of the two strict
      comparisons or equality.

  - id: pred:directed-set
    name: DirectedSet
    kind: predicate
    category: order
    arguments:
      - name: I
        role: index_set
      - name: le
        role: preorder_relation
        surface: '\leq'
    returns: truth_value
    surface_forms:
      - directed set
      - directed preorder
    description: >
      The preorder on I gives every pair of elements a common upper bound in I.

  - id: pred:net
    name: Net
    kind: predicate
    category: order
    arguments:
      - name: x
        role: net
      - name: I
        role: directed_index_set
      - name: X
        role: codomain
    returns: truth_value
    surface_forms:
      - net
      - generalized sequence
    description: >
      The object x is a function from the directed index set I into X.

  - id: pred:knaster-tarski-fixed-point
    name: KnasterTarskiFixedPoint
    kind: predicate
    category: order
    arguments:
      - name: f
        role: monotone_self_map
      - name: L
        role: complete_lattice
    returns: truth_value
    surface_forms:
      - Knaster-Tarski fixed point
      - least and greatest fixed points
    description: >
      The monotone self-map f of the complete lattice L has least and greatest
      fixed points.

  - id: pred:upper-set
    name: UpperSet
    kind: predicate
    category: order
    arguments:
      - name: U
        role: subset
      - name: P
        role: ambient
      - name: le
        role: order_relation
        surface: '\leq'
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - upper set
      - upward closed
    description: >
      The subset U contains every element of P above each of its members.

  - id: pred:lower-set
    name: LowerSet
    kind: predicate
    category: order
    arguments:
      - name: L
        role: subset
      - name: P
        role: ambient
      - name: le
        role: order_relation
        surface: '\leq'
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - lower set
      - downward closed set
    description: >
      The subset L contains every element of P below each of its members.

  - id: pred:order-embedding
    name: OrderEmbedding
    kind: predicate
    category: order
    arguments:
      - name: f
        role: function
      - name: P
        role: domain_ambient
      - name: Q
        role: codomain_ambient
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - order embedding
      - embeds order
    description: >
      The function f preserves and reflects the order between the ambient
      ordered structures P and Q.

  - id: pred:order-isomorphism
    name: OrderIsomorphism
    kind: predicate
    category: order
    arguments:
      - name: f
        role: function
      - name: P
        role: domain_ambient
      - name: Q
        role: codomain_ambient
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - order isomorphism
      - isomorphic ordered sets
    description: >
      The function f is a bijective order embedding between the ambient ordered
      structures P and Q.

  - id: pred:order-preserving
    name: OrderPreserving
    kind: predicate
    category: order
    arguments:
      - name: f
        role: function
      - name: P
        role: domain_ambient
      - name: Q
        role: codomain_ambient
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - order preserving
      - monotone map
      - monotone function
    description: >
      The function f preserves order from the ambient ordered structure P to Q.

  - id: pred:is-order-dense-subset
    name: IsOrderDenseSubset
    kind: predicate
    category: order
    arguments:
      - name: A
        role: subset
      - name: X
        role: ambient_order
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - order dense subset
      - is order dense in
    description: >
      The subset A is order dense in the ordered ambient object X: every
      nonempty open interval of X contains a point of A.

  - id: pred:has-dense-order
    name: HasDenseOrder
    kind: predicate
    category: order
    arguments:
      - name: X
        role: ambient_order
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - dense order
      - has dense order
      - order dense
    description: >
      The ordered ambient object X has dense order: between any two distinct
      comparable points of X there is a third point of X.

  - id: pred:order-reversing
    name: OrderReversing
    kind: predicate
    category: order
    arguments:
      - name: f
        role: function
      - name: P
        role: domain_ambient
      - name: Q
        role: codomain_ambient
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - order reversing
      - antitone map
      - antitone function
    description: >
      The function f reverses order from the ambient ordered structure P to Q.

  - id: pred:increasing
    name: Increasing
    kind: predicate
    category: order
    arguments:
      - name: X
        role: sequence_function_or_operator
      - name: C
        role: ordered_context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - increasing
      - nondecreasing
      - monotone increasing
    description: >
      The sequence, function, operator, or other ordered assignment X is
      monotone increasing in the ordered context C. The context supplies the
      relevant input/index order and output/value order when they are implicit.
      When both ordered ambients must be named explicitly, use
      OrderPreserving.

  - id: pred:decreasing
    name: Decreasing
    kind: predicate
    category: order
    arguments:
      - name: X
        role: sequence_function_or_operator
      - name: C
        role: ordered_context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - decreasing
      - nonincreasing
      - monotone decreasing
    description: >
      The sequence, function, operator, or other ordered assignment X is
      monotone decreasing in the ordered context C. The context supplies the
      relevant input/index order and output/value order when they are implicit.
      When both ordered ambients must be named explicitly, use OrderReversing.

  - id: pred:strictly-increasing
    name: StrictlyIncreasing
    kind: predicate
    category: order
    arguments:
      - name: X
        role: sequence_function_or_operator
      - name: C
        role: ordered_context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - strictly increasing
      - strictly monotone increasing
    description: >
      The sequence, function, operator, or other ordered assignment X is
      strictly monotone increasing in the ordered context C. The context
      supplies the relevant input/index order and output/value order when they
      are implicit. When both ordered ambients must be named explicitly, use
      StrictOrderPreserving.

  - id: pred:strictly-decreasing
    name: StrictlyDecreasing
    kind: predicate
    category: order
    arguments:
      - name: X
        role: sequence_function_or_operator
      - name: C
        role: ordered_context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - strictly decreasing
      - strictly monotone decreasing
    description: >
      The sequence, function, operator, or other ordered assignment X is
      strictly monotone decreasing in the ordered context C. The context
      supplies the relevant input/index order and output/value order when they
      are implicit. When both ordered ambients must be named explicitly, use
      StrictOrderReversing.

  - id: pred:strict-order-preserving
    name: StrictOrderPreserving
    kind: predicate
    category: order
    arguments:
      - name: f
        role: function
      - name: P
        role: domain_ambient
      - name: Q
        role: codomain_ambient
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - strictly order preserving
      - strictly increasing
    description: >
      The function f sends strict order comparisons in P to strict order
      comparisons in Q with the same direction.

  - id: pred:strict-order-reversing
    name: StrictOrderReversing
    kind: predicate
    category: order
    arguments:
      - name: f
        role: function
      - name: P
        role: domain_ambient
      - name: Q
        role: codomain_ambient
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - strictly order reversing
      - strictly decreasing
    description: >
      The function f sends strict order comparisons in P to strict order
      comparisons in Q with the opposite direction.

  - id: pred:order-reflecting
    name: OrderReflecting
    kind: predicate
    category: order
    arguments:
      - name: f
        role: function
      - name: P
        role: domain_ambient
      - name: Q
        role: codomain_ambient
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - order reflecting
      - reflects order
    description: >
      The function f reflects order from the ambient ordered structure Q back
      to P.

  - id: pred:satisfies
    name: Satisfies
    kind: predicate
    category: logic
    arguments:
      - name: M
        role: structure
      - name: phi
        role: formula
        surface: '\varphi'
    returns: truth_value
    ambient_argument: M
    surface_forms:
      - satisfies
      - models
      - satisfaction
    description: >
      The structure M satisfies the formula phi.

  - id: pred:theory-entails
    name: TheoryEntails
    kind: predicate
    category: logic
    arguments:
      - name: T
        role: theory
      - name: phi
        role: formula
        surface: '\varphi'
    returns: truth_value
    surface_forms:
      - entails
      - semantic consequence
      - logical consequence
    description: >
      Every model of the theory T satisfies the formula phi.

  - id: pred:derives
    name: Derives
    kind: predicate
    category: logic
    arguments:
      - name: T
        role: theory
      - name: phi
        role: formula
        surface: '\varphi'
    returns: truth_value
    surface_forms:
      - derives
      - proves
      - syntactic consequence
    description: >
      The formula phi is derivable from the theory T in the proof system under
      discussion.

  - id: pred:consistent
    name: Consistent
    kind: predicate
    category: logic
    arguments:
      - name: T
        role: theory
    returns: truth_value
    surface_forms:
      - consistent
      - consistency
    description: >
      The theory T does not prove a contradiction, or equivalently satisfies
      the local notion of consistency being used.

  - id: pred:relatively-consistent
    name: RelativelyConsistent
    kind: predicate
    category: logic
    arguments:
      - name: T
        role: target_theory
      - name: U
        role: base_theory
    returns: truth_value
    surface_forms:
      - relatively consistent
      - relative consistency
    description: >
      The consistency of U implies the consistency of T in the intended
      relative-consistency sense.

  - id: pred:free-for
    name: FreeFor
    kind: predicate
    category: logic
    arguments:
      - name: t
        role: term
      - name: x
        role: variable
      - name: phi
        role: formula
        surface: '\varphi'
    returns: truth_value
    surface_forms:
      - free for
      - substitutable
      - capture avoiding
    description: >
      The term t is free for the variable x in phi, so substitution does not
      cause variable capture.

  - id: pred:is-magma
    name: IsMagma
    kind: predicate
    category: algebra
    arguments:
      - name: M
        role: magma_structure
    returns: truth_value
    ambient_argument: M
    surface_forms:
      - is a magma
      - magma laws
    description: >
      The packaged magma data has a binary operation closed on its carrier.

  - id: pred:is-semigroup
    name: IsSemigroup
    kind: predicate
    category: algebra
    arguments:
      - name: S
        role: semigroup_structure
    returns: truth_value
    ambient_argument: S
    surface_forms:
      - is a semigroup
      - semigroup laws
    description: >
      The packaged semigroup data satisfies the semigroup laws.

  - id: pred:is-monoid
    name: IsMonoid
    kind: predicate
    category: algebra
    arguments:
      - name: M
        role: monoid_structure
    returns: truth_value
    ambient_argument: M
    surface_forms:
      - is a monoid
      - monoid laws
    description: >
      The packaged monoid data satisfies the monoid laws.

  - id: pred:is-commutative-monoid
    name: IsCommutativeMonoid
    kind: predicate
    category: algebra
    arguments:
      - name: M
        role: commutative_monoid_structure
    returns: truth_value
    ambient_argument: M
    surface_forms:
      - is a commutative monoid
      - commutative monoid laws
    description: >
      The packaged commutative monoid data satisfies the commutative monoid
      laws.

  - id: pred:is-group
    name: IsGroup
    kind: predicate
    category: algebra
    arguments:
      - name: G
        role: group_structure
    returns: truth_value
    ambient_argument: G
    surface_forms:
      - is a group
      - group laws
    description: >
      The packaged group data satisfies the group laws.

  - id: pred:is-abelian-group
    name: IsAbelianGroup
    kind: predicate
    category: algebra
    arguments:
      - name: G
        role: abelian_group_structure
    returns: truth_value
    ambient_argument: G
    surface_forms:
      - is an abelian group
      - is a commutative group
    description: >
      The packaged abelian group data satisfies the abelian group laws.

  - id: pred:is-semiring
    name: IsSemiring
    kind: predicate
    category: algebra
    arguments:
      - name: S
        role: semiring_structure
    returns: truth_value
    ambient_argument: S
    surface_forms:
      - is a semiring
      - semiring laws
    description: >
      The packaged semiring data satisfies the semiring laws.

  - id: pred:is-commutative-semiring
    name: IsCommutativeSemiring
    kind: predicate
    category: algebra
    arguments:
      - name: S
        role: commutative_semiring_structure
    returns: truth_value
    ambient_argument: S
    surface_forms:
      - is a commutative semiring
      - commutative semiring laws
    description: >
      The packaged commutative semiring data satisfies the commutative
      semiring laws.

  - id: pred:is-ring
    name: IsRing
    kind: predicate
    category: algebra
    arguments:
      - name: R
        role: ring_structure
    returns: truth_value
    ambient_argument: R
    surface_forms:
      - is a ring
      - ring laws
    description: >
      The packaged ring data satisfies the ring laws.

  - id: pred:is-commutative-ring
    name: IsCommutativeRing
    kind: predicate
    category: algebra
    arguments:
      - name: R
        role: commutative_ring_structure
    returns: truth_value
    ambient_argument: R
    surface_forms:
      - is a commutative ring
      - commutative ring laws
    description: >
      The packaged commutative ring data satisfies the commutative ring laws.

  - id: pred:is-field
    name: IsField
    kind: predicate
    category: algebra
    arguments:
      - name: F
        role: field_structure
    returns: truth_value
    ambient_argument: F
    surface_forms:
      - is a field
      - field laws
    description: >
      The packaged field data satisfies the field laws.

  - id: pred:is-ordered-field
    name: IsOrderedField
    kind: predicate
    category: algebra
    arguments:
      - name: F
        role: ordered_field_structure
    returns: truth_value
    ambient_argument: F
    surface_forms:
      - is an ordered field
      - ordered field laws
    description: >
      The packaged ordered field data satisfies the ordered field laws.

  - id: pred:is-complete-ordered-field
    name: IsCompleteOrderedField
    kind: predicate
    category: algebra
    arguments:
      - name: F
        role: complete_ordered_field_structure
    returns: truth_value
    ambient_argument: F
    surface_forms:
      - is a complete ordered field
      - complete ordered field laws
    description: >
      The packaged complete ordered field data satisfies the complete ordered
      field laws.

  - id: pred:associative
    name: Associative
    kind: predicate
    category: algebra
    arguments:
      - name: A
        role: carrier
      - name: star
        role: binary_operation
        surface: '\star'
    returns: truth_value
    ambient_argument: A
    surface_forms:
      - associative
      - associativity
    description: >
      The binary operation star is associative on the carrier A.

  - id: pred:commutative
    name: Commutative
    kind: predicate
    category: algebra
    arguments:
      - name: A
        role: carrier
      - name: star
        role: binary_operation
        surface: '\star'
    returns: truth_value
    ambient_argument: A
    surface_forms:
      - commutative
      - commutativity
    description: >
      The binary operation star is commutative on the carrier A.

  - id: pred:left-identity
    name: LeftIdentity
    kind: predicate
    category: algebra
    arguments:
      - name: e
        role: candidate_identity
      - name: A
        role: carrier
      - name: star
        role: binary_operation
        surface: '\star'
    returns: truth_value
    ambient_argument: A
    surface_forms:
      - left identity
      - left identity element
    description: >
      The element e is a left identity for the operation star on A.

  - id: pred:right-identity
    name: RightIdentity
    kind: predicate
    category: algebra
    arguments:
      - name: e
        role: candidate_identity
      - name: A
        role: carrier
      - name: star
        role: binary_operation
        surface: '\star'
    returns: truth_value
    ambient_argument: A
    surface_forms:
      - right identity
      - right identity element
    description: >
      The element e is a right identity for the operation star on A.

  - id: pred:identity
    name: Identity
    kind: predicate
    category: algebra
    arguments:
      - name: e
        role: candidate_identity
      - name: A
        role: carrier
      - name: star
        role: binary_operation
        surface: '\star'
    returns: truth_value
    ambient_argument: A
    surface_forms:
      - identity
      - identity element
      - two-sided identity
    description: >
      The element e is both a left and right identity for the operation star
      on A.

  - id: pred:left-inverse-element
    name: LeftInverse
    kind: predicate
    category: algebra
    arguments:
      - name: y
        role: candidate_inverse
      - name: x
        role: element
      - name: e
        role: identity_element
      - name: A
        role: carrier
      - name: star
        role: binary_operation
        surface: '\star'
    returns: truth_value
    ambient_argument: A
    surface_forms:
      - left inverse
      - left inverse element
    description: >
      The element y is a left inverse of x with respect to identity e and
      operation star on A.

  - id: pred:right-inverse-element
    name: RightInverse
    kind: predicate
    category: algebra
    arguments:
      - name: y
        role: candidate_inverse
      - name: x
        role: element
      - name: e
        role: identity_element
      - name: A
        role: carrier
      - name: star
        role: binary_operation
        surface: '\star'
    returns: truth_value
    ambient_argument: A
    surface_forms:
      - right inverse
      - right inverse element
    description: >
      The element y is a right inverse of x with respect to identity e and
      operation star on A.

  - id: pred:inverse-element
    name: Inverse
    kind: predicate
    category: algebra
    arguments:
      - name: y
        role: candidate_inverse
      - name: x
        role: element
      - name: e
        role: identity_element
      - name: A
        role: carrier
      - name: star
        role: binary_operation
        surface: '\star'
    returns: truth_value
    ambient_argument: A
    surface_forms:
      - inverse
      - two-sided inverse
      - inverse element
    description: >
      The element y is both a left and right inverse of x with respect to
      identity e and operation star on A.

  - id: pred:left-distributive
    name: LeftDistributive
    kind: predicate
    category: algebra
    arguments:
      - name: A
        role: carrier
      - name: plus
        role: additive_operation
        surface: '+'
      - name: dot
        role: multiplicative_operation
        surface: '\cdot'
    returns: truth_value
    ambient_argument: A
    surface_forms:
      - left distributive
      - left distributivity
    description: >
      The operation dot is left-distributive over plus on A.

  - id: pred:right-distributive
    name: RightDistributive
    kind: predicate
    category: algebra
    arguments:
      - name: A
        role: carrier
      - name: plus
        role: additive_operation
        surface: '+'
      - name: dot
        role: multiplicative_operation
        surface: '\cdot'
    returns: truth_value
    ambient_argument: A
    surface_forms:
      - right distributive
      - right distributivity
    description: >
      The operation dot is right-distributive over plus on A.

  - id: pred:distributive
    name: Distributive
    kind: predicate
    category: algebra
    arguments:
      - name: A
        role: carrier
      - name: plus
        role: additive_operation
        surface: '+'
      - name: dot
        role: multiplicative_operation
        surface: '\cdot'
    returns: truth_value
    ambient_argument: A
    surface_forms:
      - distributive
      - distributivity
    description: >
      The operation dot is both left- and right-distributive over plus on A.

  - id: pred:zero-absorbing
    name: ZeroAbsorbing
    kind: predicate
    category: algebra
    arguments:
      - name: z
        role: absorbing_element
        surface: '0'
      - name: A
        role: carrier
      - name: star
        role: binary_operation
        surface: '\star'
    returns: truth_value
    ambient_argument: A
    surface_forms:
      - zero absorbing
      - absorbing element
    description: >
      The element z absorbs the operation star on both sides over A.

  - id: pred:left-cancellation
    name: LeftCancellation
    kind: predicate
    category: algebra
    arguments:
      - name: A
        role: carrier
      - name: star
        role: binary_operation
        surface: '\star'
    returns: truth_value
    ambient_argument: A
    surface_forms:
      - left cancellation
      - left cancellative
    description: >
      The operation star satisfies left cancellation on A.

  - id: pred:right-cancellation
    name: RightCancellation
    kind: predicate
    category: algebra
    arguments:
      - name: A
        role: carrier
      - name: star
        role: binary_operation
        surface: '\star'
    returns: truth_value
    ambient_argument: A
    surface_forms:
      - right cancellation
      - right cancellative
    description: >
      The operation star satisfies right cancellation on A.

  - id: pred:operation-extension
    name: OperationExtension
    kind: predicate
    category: algebra
    arguments:
      - name: star_B
        role: extended_operation
        surface: '\star_B'
      - name: star_A
        role: original_operation
        surface: '\star_A'
      - name: A
        role: original_carrier
      - name: B
        role: extended_carrier
    returns: truth_value
    ambient_argument: B
    surface_forms:
      - operation extension
      - extends operation
      - operation agrees on a subcarrier
    description: >
      The operation star_B on B extends the operation star_A on A by agreeing
      with star_A whenever all inputs lie in A.

  - id: pred:unique-value-relation
    name: UniqueValueRelation
    kind: predicate
    category: well_definedness
    arguments:
      - name: R
        role: relation
      - name: A
        role: domain
      - name: B
        role: codomain
    returns: truth_value
    ambient_argument: R
    surface_forms:
      - unique value relation
      - single-valued relation
    description: >
      For every input in A, the relation R has at most one output in B.

  - id: pred:exists-unique-value-relation
    name: ExistsUniqueValueRelation
    kind: predicate
    category: well_definedness
    arguments:
      - name: R
        role: relation
      - name: A
        role: domain
      - name: B
        role: codomain
    returns: truth_value
    ambient_argument: R
    surface_forms:
      - exists unique value relation
      - total single-valued relation
    description: >
      For every input in A, there exists a unique output in B related by R.

  - id: pred:representative-independent
    name: RepresentativeIndependent
    kind: predicate
    category: well_definedness
    arguments:
      - name: F
        role: rule_or_operation
      - name: Q_A
        role: domain_quotient
      - name: Q_B
        role: codomain_quotient
    returns: truth_value
    ambient_argument: F
    surface_forms:
      - representative independent
      - independent of representatives
    description: >
      Equivalent representatives in the domain quotient determine equivalent
      outputs in the codomain quotient under F.

  - id: pred:closed-under
    name: ClosedUnder
    kind: predicate
    category: algebra
    arguments:
      - name: F
        role: rule_or_operation
      - name: A
        role: stable_collection
      - name: C
        role: closure_context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - closed under
      - stable under
      - closure under an operation
      - closure under a formation rule
    description: >
      The collection A is closed under the mapping, operation, or formation
      rule F in the context C: every admissible input determined by C and
      drawn from A is sent by F to an output still in A.

  - id: pred:members-satisfy
    name: MembersSatisfy
    kind: predicate
    category: set
    arguments:
      - name: F
        role: family_or_collection
      - name: Phi
        role: property_specification
        surface: '\Phi'
      - name: X
        role: ambient
    returns: truth_value
    ambient_argument: X
    polymorphic: true
    surface_forms:
      - members satisfy
      - every member satisfies
      - family members satisfy
    description: >
      Every member of the family or collection F satisfies the property
      specification Phi in the ambient context X. Property specifications may
      abbreviate conjunctions of existing predicates, such as interval,
      openness, boundedness, and nonemptiness.

  - id: pred:closed-under-unary-operation
    name: ClosedUnderUnaryOperation
    kind: predicate
    category: algebra
    arguments:
      - name: u
        role: unary_operation
      - name: A
        role: carrier
    returns: truth_value
    ambient_argument: A
    surface_forms:
      - closed under unary operation
      - unary closure
    description: >
      The unary operation u sends elements of A to elements of A.

  - id: pred:closed-under-binary-operation
    name: ClosedUnderBinaryOperation
    kind: predicate
    category: algebra
    arguments:
      - name: star
        role: binary_operation
        surface: '\star'
      - name: A
        role: carrier
    returns: truth_value
    ambient_argument: A
    surface_forms:
      - closed under binary operation
      - binary closure
    description: >
      The binary operation star sends pairs of elements of A to elements of A.

  - id: pred:well-defined-function
    name: WellDefinedFunction
    kind: predicate
    category: well_definedness
    arguments:
      - name: f
        role: function
      - name: A
        role: domain
      - name: B
        role: codomain
    returns: truth_value
    ambient_argument: f
    surface_forms:
      - well-defined function
      - function is well defined
    description: >
      The function f assigns a unique element of B to each intended input in A.

  - id: pred:well-defined-unary-operation
    name: WellDefinedUnaryOperation
    kind: predicate
    category: well_definedness
    arguments:
      - name: u
        role: unary_operation
      - name: A
        role: carrier
    returns: truth_value
    ambient_argument: u
    surface_forms:
      - well-defined unary operation
    description: >
      The unary operation u produces a unique value in A for each input in A.

  - id: pred:well-defined-binary-operation
    name: WellDefinedBinaryOperation
    kind: predicate
    category: well_definedness
    arguments:
      - name: star
        role: binary_operation
        surface: '\star'
      - name: A
        role: carrier
    returns: truth_value
    ambient_argument: star
    surface_forms:
      - well-defined binary operation
    description: >
      The binary operation star produces a unique value in A for each pair of
      inputs in A.

  - id: pred:well-defined-quotient-operation
    name: WellDefinedQuotientOperation
    kind: predicate
    category: well_definedness
    arguments:
      - name: star_bar
        role: quotient_operation
        surface: '\overline{\star}'
      - name: star
        role: representative_operation
        surface: '\star'
      - name: Q
        role: quotient_structure
    returns: truth_value
    ambient_argument: Q
    surface_forms:
      - well-defined quotient operation
      - operation descends to the quotient
    description: >
      The quotient operation star_bar is induced by star on the quotient
      structure Q and is independent of representative choices.

  - id: pred:successor-covers-nonbase
    name: SuccessorCoversNonbase
    kind: predicate
    category: peano
    arguments:
      - name: S
        role: successor_function
      - name: e
        role: base_element
      - name: A
        role: carrier
    returns: truth_value
    ambient_argument: A
    surface_forms:
      - every non-base element is a successor
      - successor covers nonbase elements
    description: >
      Every element of A other than the base element e is in the image of the
      successor function S.

  - id: pred:successor-system-properties
    name: SuccessorSystemProperties
    kind: predicate
    category: peano
    arguments:
      - name: A
        role: carrier
      - name: e
        role: base_element
      - name: S
        role: successor_function
    returns: truth_value
    ambient_argument: A
    surface_forms:
      - successor-side properties
      - successor system properties
    description: >
      The carrier A, base element e, and successor function S satisfy the
      successor-side Peano properties: e lies in A, S maps A to A, e is not a
      successor value, and S is injective on A.

  - id: pred:satisfiable
    name: Satisfiable
    kind: predicate
    category: logic
    arguments:
      - name: X
        role: object
      - name: C
        role: logic_context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - satisfiable
      - has a satisfying assignment
      - has a model
    description: >
      The object X, such as a formula, sentence, set of formulas, or theory, is
      satisfiable in the logical context C.

  - id: pred:is-tautology
    name: IsTautology
    kind: predicate
    category: logic
    arguments:
      - name: phi
        role: formula
        surface: '\varphi'
      - name: C
        role: logic_context
    returns: truth_value
    ambient_argument: C
    surface_forms:
      - is a tautology
      - tautological
      - true under every truth assignment
    description: >
      The formula phi is true under every admissible interpretation or truth
      assignment in the logical context C.

  - id: pred:unsatisfiable
    name: Unsatisfiable
    kind: predicate
    category: logic
    arguments:
      - name: X
        role: object
      - name: C
        role: logic_context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - unsatisfiable
      - has no satisfying assignment
      - has no model
    description: >
      The object X, such as a formula, sentence, set of formulas, or theory, is
      not satisfiable in the logical context C.

  - id: pred:finitely-satisfiable
    name: FinitelySatisfiable
    kind: predicate
    category: logic
    arguments:
      - name: Gamma
        role: formula_family
        surface: '\Gamma'
      - name: C
        role: logic_context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - finitely satisfiable
      - every finite subset is satisfiable
    description: >
      Every finite subfamily of Gamma is satisfiable in the logical context C.

  - id: pred:witness
    name: Witness
    kind: predicate
    category: logic
    arguments:
      - name: W
        role: witness
      - name: X
        role: witnessed_object
      - name: C
        role: context
    returns: truth_value
    semantics: assertion
    polymorphic: true
    surface_forms:
      - witness
      - is a witness for
      - witnesses
    description: >
      The object W witnesses the relevant property or obstruction of X in the
      ambient context C.

  - id: pred:logical-equivalence
    name: LogicalEquivalence
    kind: predicate
    category: logic
    arguments:
      - name: phi
        role: left_formula
        surface: '\varphi'
      - name: psi
        role: right_formula
        surface: '\psi'
      - name: C
        role: logic_context
    returns: truth_value
    ambient_argument: C
    surface_forms:
      - logically equivalent
      - logical equivalence
    description: >
      The formulas phi and psi have the same truth behavior in the logical
      context C.

  - id: pred:logical-consequence
    name: LogicalConsequence
    kind: predicate
    category: logic
    arguments:
      - name: Gamma
        role: premises
        surface: '\Gamma'
      - name: phi
        role: conclusion
        surface: '\varphi'
      - name: C
        role: logic_context
    returns: truth_value
    ambient_argument: C
    surface_forms:
      - logical consequence
      - semantically entails
    description: >
      The conclusion phi follows semantically from the premises Gamma in the
      logical context C.

  - id: pred:functionally-complete
    name: FunctionallyComplete
    kind: predicate
    category: logic
    arguments:
      - name: B
        role: connective_basis
      - name: C
        role: logic_context
    returns: truth_value
    ambient_argument: C
    surface_forms:
      - functionally complete
      - complete connective basis
    description: >
      The connective basis B can represent every Boolean truth function in the
      logical context C.

  - id: pred:valid
    name: Valid
    kind: predicate
    category: logic
    arguments:
      - name: X
        role: object
      - name: C
        role: logic_context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - valid
      - validity
      - semantically valid
    description: >
      The object X, such as a formula, argument, or argument form, satisfies
      the appropriate validity condition in the logical context C.

  - id: pred:comparable
    name: Comparable
    kind: predicate
    category: order
    arguments:
      - name: a
        role: left_element
      - name: b
        role: right_element
      - name: P
        role: ambient_ordered_structure
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - comparable
      - comparable elements
    description: >
      The elements a and b are related in at least one direction by the order
      of the ambient ordered structure P.

  - id: pred:incomparable
    name: Incomparable
    kind: predicate
    category: order
    arguments:
      - name: a
        role: left_element
      - name: b
        role: right_element
      - name: P
        role: ambient_ordered_structure
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - incomparable
      - incomparable elements
    description: >
      Neither element is related to the other by the order of the ambient
      ordered structure P.

  - id: pred:preserves-union
    name: PreservesUnion
    kind: predicate
    category: function
    arguments:
      - name: F
        role: operator
      - name: C
        role: ambient_context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - preserves unions
      - union preserving
    description: >
      The operator F sends unions in its source context to the corresponding
      unions in its target context.

  - id: pred:preserves-intersection
    name: PreservesIntersection
    kind: predicate
    category: function
    arguments:
      - name: F
        role: operator
      - name: C
        role: ambient_context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - preserves intersections
      - intersection preserving
    description: >
      The operator F sends intersections in its source context to the
      corresponding intersections in its target context.

  - id: pred:preserves-difference
    name: PreservesDifference
    kind: predicate
    category: function
    arguments:
      - name: F
        role: operator
      - name: C
        role: ambient_context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - preserves differences
      - difference preserving
    description: >
      The operator F sends set differences in its source context to the
      corresponding differences in its target context.

  - id: pred:preserves-complement
    name: PreservesComplement
    kind: predicate
    category: function
    arguments:
      - name: F
        role: operator
      - name: C
        role: ambient_context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - preserves complements
      - complement preserving
    description: >
      The operator F sends complements in its source context to the
      corresponding complements in its target context.

  - id: pred:preserves-indexed-union
    name: PreservesIndexedUnion
    kind: predicate
    category: function
    arguments:
      - name: F
        role: operator
      - name: C
        role: ambient_context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - preserves indexed unions
      - indexed-union preserving
    description: >
      The operator F sends indexed unions in its source context to the
      corresponding indexed unions in its target context.

  - id: pred:preserves-indexed-intersection
    name: PreservesIndexedIntersection
    kind: predicate
    category: function
    arguments:
      - name: F
        role: operator
      - name: C
        role: ambient_context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - preserves indexed intersections
      - indexed-intersection preserving
    description: >
      The operator F sends indexed intersections in its source context to the
      corresponding indexed intersections in its target context.

  - id: pred:maps-into
    name: MapsInto
    kind: predicate
    category: function
    arguments:
      - name: F
        role: operator
      - name: S
        role: source_object
      - name: T
        role: target_object
      - name: C
        role: ambient_context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - maps into
      - sends into
      - one-sided inclusion
    description: >
      The operator F sends the source object S into the target object T in the
      ambient context C.

  - id: pred:image-preimage-adjunction
    name: ImagePreimageAdjunction
    kind: predicate
    category: function
    arguments:
      - name: f
        role: function
      - name: C
        role: ambient_context
    returns: truth_value
    ambient_argument: C
    surface_forms:
      - image-preimage adjunction
      - direct and inverse image adjunction
    description: >
      The direct image and inverse image operations associated with f satisfy
      the local adjunction relation in context C.

  - id: pred:associative-composition
    name: AssociativeComposition
    kind: predicate
    category: function
    arguments:
      - name: f
        role: inner_function
      - name: g
        role: middle_function
      - name: h
        role: outer_function
    returns: truth_value
    surface_forms:
      - associativity of composition
      - composition is associative
    description: >
      The two parenthesizations of the composable triple h, g, f agree as
      functions.

  - id: pred:identity-neutral-for-composition
    name: IdentityNeutralForComposition
    kind: predicate
    category: function
    arguments:
      - name: f
        role: function
      - name: id_A
        role: domain_identity
        surface: '\id_A'
      - name: id_B
        role: codomain_identity
        surface: '\id_B'
    returns: truth_value
    surface_forms:
      - identity neutral for composition
      - identity functions are neutral
    description: >
      The identity on the domain and the identity on the codomain are neutral
      for composing with f.

  - id: pred:contradiction
    name: Contradiction
    kind: predicate
    category: logic
    arguments:
      - name: phi
        role: formula
        surface: '\varphi'
      - name: C
        role: logic_context
    returns: truth_value
    ambient_argument: C
    surface_forms:
      - contradiction
      - contradictory formula
    description: >
      The formula phi is false under every admissible interpretation in the
      logical context C.

  - id: pred:contingency
    name: Contingency
    kind: predicate
    category: logic
    arguments:
      - name: phi
        role: formula
        surface: '\varphi'
      - name: C
        role: logic_context
    returns: truth_value
    ambient_argument: C
    surface_forms:
      - contingency
      - contingent formula
    description: >
      The formula phi is true under some admissible interpretations and false
      under others in the logical context C.

  - id: pred:represents
    name: Represents
    kind: predicate
    category: logic
    arguments:
      - name: X
        role: representative
      - name: Y
        role: represented_object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - represents
      - representation
    description: >
      The object X represents the object Y in the relevant context C.

  - id: pred:definable-from
    name: DefinableFrom
    kind: predicate
    category: logic
    arguments:
      - name: X
        role: definable_object
      - name: B
        role: basis
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    surface_forms:
      - definable from
      - expressible from
    description: >
      The object X is definable using the basis B in context C.

  - id: pred:minimal-complete
    name: MinimalComplete
    kind: predicate
    category: logic
    arguments:
      - name: B
        role: basis
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    surface_forms:
      - minimally complete
      - minimal complete basis
    description: >
      The basis B is complete, and no proper subbasis of B is complete, in
      context C.

  - id: pred:incomplete
    name: Incomplete
    kind: predicate
    category: logic
    arguments:
      - name: B
        role: basis
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    surface_forms:
      - incomplete
      - not complete
    description: >
      The basis B fails to be complete in context C.

  - id: pred:monotone
    name: Monotone
    kind: predicate
    category: order
    arguments:
      - name: f
        role: function
      - name: P
        role: ambient_order
    returns: truth_value
    ambient_argument: P
    surface_forms:
      - monotone
      - order preserving
    description: >
      The function f preserves the relevant order in the ambient ordered
      context P.

  - id: pred:satisfaction
    name: Satisfaction
    kind: predicate
    category: logic
    arguments:
      - name: M
        role: structure
      - name: s
        role: assignment
      - name: phi
        role: formula
        surface: '\varphi'
    returns: truth_value
    surface_forms:
      - satisfaction
      - satisfies formula under assignment
    description: >
      The structure M with assignment s satisfies the formula phi.

  - id: pred:truth-in-structure
    name: TruthInStructure
    kind: predicate
    category: logic
    arguments:
      - name: M
        role: structure
      - name: phi
        role: sentence
        surface: '\varphi'
    returns: truth_value
    surface_forms:
      - truth in structure
      - true in a structure
    description: >
      The sentence phi is true in the structure M.

  - id: pred:model-of-sentence
    name: ModelOfSentence
    kind: predicate
    category: logic
    arguments:
      - name: M
        role: structure
      - name: phi
        role: sentence
        surface: '\varphi'
    returns: truth_value
    surface_forms:
      - model of sentence
    description: >
      The structure M is a model of the sentence phi.

  - id: pred:model-of-theory
    name: ModelOfTheory
    kind: predicate
    category: logic
    arguments:
      - name: M
        role: structure
      - name: T
        role: theory
    returns: truth_value
    surface_forms:
      - model of theory
    description: >
      The structure M is a model of every sentence in the theory T.

  - id: pred:definable-relation
    name: DefinableRelation
    kind: predicate
    category: logic
    arguments:
      - name: R
        role: relation
      - name: phi
        role: formula
        surface: '\varphi'
      - name: M
        role: structure
    returns: truth_value
    surface_forms:
      - definable relation
    description: >
      The relation R is defined by the formula phi in the structure M.

  - id: pred:satisfies-formula
    name: SatisfiesFormula
    kind: predicate
    category: logic
    arguments:
      - name: v
        role: assignment
      - name: phi
        role: formula
        surface: '\varphi'
    returns: truth_value
    surface_forms:
      - satisfies formula
    description: >
      The assignment v satisfies the formula phi.

  - id: pred:satisfies-set
    name: SatisfiesSet
    kind: predicate
    category: logic
    arguments:
      - name: v
        role: assignment
      - name: Gamma
        role: formula_set
        surface: '\Gamma'
    returns: truth_value
    surface_forms:
      - satisfies set
    description: >
      The assignment v satisfies every formula in Gamma.

  - id: pred:proper-subformula
    name: ProperSubformula
    kind: predicate
    category: logic
    arguments:
      - name: psi
        role: subformula
        surface: '\psi'
      - name: phi
        role: formula
        surface: '\varphi'
    returns: truth_value
    surface_forms:
      - proper subformula
    description: >
      The formula psi is a proper subformula of phi.

  - id: pred:main-connective
    name: MainConnective
    kind: predicate
    category: logic
    arguments:
      - name: phi
        role: formula
        surface: '\varphi'
      - name: c
        role: connective
    returns: truth_value
    surface_forms:
      - main connective
      - outermost connective
    description: >
      The connective c is the main or outermost connective of phi.

  - id: pred:quantifier-order
    name: QuantifierOrder
    kind: predicate
    category: logic
    arguments:
      - name: Phi
        role: formula
        surface: '\Phi'
      - name: Q
        role: quantifier_order
    returns: truth_value
    surface_forms:
      - quantifier order
    description: >
      The formula Phi has the listed quantifier order.

  - id: pred:stronger-formula
    name: StrongerFormula
    kind: predicate
    category: logic
    arguments:
      - name: A
        role: stronger_formula
      - name: B
        role: weaker_formula
    returns: truth_value
    surface_forms:
      - stronger formula
    description: >
      Formula A entails formula B and is logically stronger in context.

  - id: pred:weaker-formula
    name: WeakerFormula
    kind: predicate
    category: logic
    arguments:
      - name: B
        role: weaker_formula
      - name: A
        role: stronger_formula
    returns: truth_value
    surface_forms:
      - weaker formula
    description: >
      Formula B is entailed by formula A and is logically weaker in context.

  - id: pred:scope-ambiguity
    name: ScopeAmbiguity
    kind: predicate
    category: logic
    arguments:
      - name: E
        role: expression
      - name: phi
        role: first_reading
        surface: '\varphi'
      - name: psi
        role: second_reading
        surface: '\psi'
    returns: truth_value
    surface_forms:
      - scope ambiguity
    description: >
      The expression E admits distinct readings phi and psi due to scope.

  - id: pred:contradictory-pair
    name: ContradictoryPair
    kind: predicate
    category: logic
    arguments:
      - name: phi
        role: left_formula
        surface: '\varphi'
      - name: psi
        role: right_formula
        surface: '\psi'
    returns: truth_value
    surface_forms:
      - contradictory pair
    description: >
      The formulas phi and psi are contradictories.

  - id: pred:contrary-with-existential-import
    name: ContraryWithExistentialImport
    kind: predicate
    category: logic
    arguments:
      - name: phi
        role: left_formula
        surface: '\varphi'
      - name: psi
        role: right_formula
        surface: '\psi'
    returns: truth_value
    surface_forms:
      - contrary with existential import
    description: >
      The formulas phi and psi are contraries under an existential-import
      assumption.

  - id: pred:complementary-literals
    name: ComplementaryLiterals
    kind: predicate
    category: logic
    arguments:
      - name: ell_1
        role: first_literal
        surface: '\ell_1'
      - name: ell_2
        role: second_literal
        surface: '\ell_2'
    returns: truth_value
    surface_forms:
      - complementary literals
    description: >
      The literals ell_1 and ell_2 are complementary.

  - id: pred:negation-normal-form-exists
    name: NegationNormalFormExists
    kind: predicate
    category: logic
    arguments:
      - name: phi
        role: formula
        surface: '\varphi'
    returns: truth_value
    surface_forms:
      - negation normal form exists
    description: >
      The formula phi has an equivalent formula in negation normal form.

  - id: pred:nand-only
    name: NANDOnly
    kind: predicate
    category: logic
    arguments:
      - name: phi
        role: formula
        surface: '\varphi'
    returns: truth_value
    surface_forms:
      - NAND only
    description: >
      Every connective occurrence in phi is a NAND connective occurrence.

  - id: pred:nor-only
    name: NOROnly
    kind: predicate
    category: logic
    arguments:
      - name: phi
        role: formula
        surface: '\varphi'
    returns: truth_value
    surface_forms:
      - NOR only
    description: >
      Every connective occurrence in phi is a NOR connective occurrence.

  - id: pred:extension
    name: Extension
    kind: predicate
    category: function
    arguments:
      - name: g
        role: extending_function
      - name: f
        role: extended_function
    returns: truth_value
    surface_forms:
      - extension
      - extends
    description: >
      The function g extends the function f.

  - id: pred:invertible
    name: Invertible
    kind: predicate
    category: function
    arguments:
      - name: f
        role: function
    returns: truth_value
    surface_forms:
      - invertible
    description: >
      The function f has an inverse in the relevant function context.

  - id: pred:truth-function-of-formula
    name: TruthFunctionOfFormula
    kind: predicate
    category: logic
    arguments:
      - name: f
        role: truth_function
      - name: phi
        role: formula
        surface: '\varphi'
    returns: truth_value
    surface_forms:
      - truth function of formula
    description: >
      The truth function f is represented by the formula phi.

  - id: pred:associates
    name: Associates
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - Associates
    description: >
      Volume II predicate or assertion named Associates.

  - id: pred:between
    name: Between
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - Between
    description: >
      Volume II predicate or assertion named Between.

  - id: pred:bounds-by-absolute-value
    name: BoundsByAbsoluteValue
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - BoundsByAbsoluteValue
    description: >
      Volume II predicate or assertion named BoundsByAbsoluteValue.

  - id: pred:bracket-independent
    name: BracketIndependent
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - BracketIndependent
    description: >
      Volume II predicate or assertion named BracketIndependent.

  - id: pred:cancellative
    name: Cancellative
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - Cancellative
    description: >
      Volume II predicate or assertion named Cancellative.

  - id: pred:characterizes-real-numbers
    name: CharacterizesRealNumbers
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - CharacterizesRealNumbers
    description: >
      Volume II predicate or assertion named CharacterizesRealNumbers.

  - id: pred:closed
    name: Closed
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - Closed
    description: >
      Volume II predicate or assertion named Closed.

  - id: pred:closed-segment-convex
    name: ClosedSegmentConvex
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - ClosedSegmentConvex
    description: >
      Volume II predicate or assertion named ClosedSegmentConvex.

  - id: pred:distinct
    name: Distinct
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - Distinct
    description: >
      Volume II predicate or assertion named Distinct.

  - id: pred:divides
    name: Divides
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - Divides
    description: >
      Volume II predicate or assertion named Divides.

  - id: pred:divides-zero
    name: DividesZero
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - DividesZero
    description: >
      Volume II predicate or assertion named DividesZero.

  - id: pred:divisibility-closed-under-addition
    name: DivisibilityClosedUnderAddition
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - DivisibilityClosedUnderAddition
    description: >
      Volume II predicate or assertion named DivisibilityClosedUnderAddition.

  - id: pred:divisibility-closed-under-linear-combinations
    name: DivisibilityClosedUnderLinearCombinations
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - DivisibilityClosedUnderLinearCombinations
    description: >
      Volume II predicate or assertion named DivisibilityClosedUnderLinearCombinations.

  - id: pred:divisibility-invariant-under-negated-dividend
    name: DivisibilityInvariantUnderNegatedDividend
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - DivisibilityInvariantUnderNegatedDividend
    description: >
      Volume II predicate or assertion named DivisibilityInvariantUnderNegatedDividend.

  - id: pred:divisibility-invariant-under-negated-divisor
    name: DivisibilityInvariantUnderNegatedDivisor
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - DivisibilityInvariantUnderNegatedDivisor
    description: >
      Volume II predicate or assertion named DivisibilityInvariantUnderNegatedDivisor.

  - id: pred:divisibility-invariant-under-negation
    name: DivisibilityInvariantUnderNegation
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - DivisibilityInvariantUnderNegation
    description: >
      Volume II predicate or assertion named DivisibilityInvariantUnderNegation.

  - id: pred:element-of
    name: ElementOf
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - ElementOf
    description: >
      Volume II predicate or assertion named ElementOf.

  - id: pred:equality
    name: Equality
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - Equality
    description: >
      Volume II predicate or assertion named Equality.

  - id: pred:equivalent
    name: Equivalent
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - Equivalent
    description: >
      Volume II predicate or assertion named Equivalent.

  - id: pred:even-under-negation
    name: EvenUnderNegation
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - EvenUnderNegation
    description: >
      Volume II predicate or assertion named EvenUnderNegation.

  - id: pred:exactly-one
    name: ExactlyOne
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - ExactlyOne
    description: >
      Volume II predicate or assertion named ExactlyOne.

  - id: pred:extended-leq
    name: ExtendedLeq
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - ExtendedLeq
    description: >
      Volume II predicate or assertion named ExtendedLeq.

  - id: pred:extends
    name: Extends
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - Extends
    description: >
      Volume II predicate or assertion named Extends.

  - id: pred:finite
    name: Finite
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - Finite
    description: >
      Volume II predicate or assertion named Finite.

  - id: pred:finite-leq
    name: FiniteLeq
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - FiniteLeq
    description: >
      Volume II predicate or assertion named FiniteLeq.

  - id: pred:formal-difference-equivalent
    name: FormalDifferenceEquivalent
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - FormalDifferenceEquivalent
    description: >
      Volume II predicate or assertion named FormalDifferenceEquivalent.

  - id: pred:fraction-comparison
    name: FractionComparison
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - FractionComparison
    description: >
      Volume II predicate or assertion named FractionComparison.

  - id: pred:fraction-equivalent
    name: FractionEquivalent
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - FractionEquivalent
    description: >
      Volume II predicate or assertion named FractionEquivalent.

  - id: pred:has-inverses
    name: HasInverses
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - HasInverses
    description: >
      Volume II predicate or assertion named HasInverses.

  - id: pred:has-nonnegative-square-root
    name: HasNonnegativeSquareRoot
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - HasNonnegativeSquareRoot
    description: >
      Volume II predicate or assertion named HasNonnegativeSquareRoot.

  - id: pred:indiscernible
    name: Indiscernible
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - Indiscernible
    description: >
      Volume II predicate or assertion named Indiscernible.

  - id: pred:induction-from-base
    name: InductionFromBase
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - InductionFromBase
    description: >
      Volume II predicate or assertion named InductionFromBase.

  - id: pred:integer-canonical-trichotomy
    name: IntegerCanonicalTrichotomy
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - IntegerCanonicalTrichotomy
    description: >
      Volume II predicate or assertion named IntegerCanonicalTrichotomy.

  - id: pred:irrational
    name: Irrational
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - Irrational
    description: >
      Volume II predicate or assertion named Irrational.

  - id: pred:left-cancellative
    name: LeftCancellative
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - LeftCancellative
    description: >
      Volume II predicate or assertion named LeftCancellative.

  - id: pred:left-cancellative-on-nonzero
    name: LeftCancellativeOnNonzero
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - LeftCancellativeOnNonzero
    description: >
      Volume II predicate or assertion named LeftCancellativeOnNonzero.

  - id: pred:left-monotone
    name: LeftMonotone
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - LeftMonotone
    description: >
      Volume II predicate or assertion named LeftMonotone.

  - id: pred:left-negation-distributes-over-product
    name: LeftNegationDistributesOverProduct
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - LeftNegationDistributesOverProduct
    description: >
      Volume II predicate or assertion named LeftNegationDistributesOverProduct.

  - id: pred:left-order-reflecting
    name: LeftOrderReflecting
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - LeftOrderReflecting
    description: >
      Volume II predicate or assertion named LeftOrderReflecting.

  - id: pred:left-representative-independent
    name: LeftRepresentativeIndependent
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - LeftRepresentativeIndependent
    description: >
      Volume II predicate or assertion named LeftRepresentativeIndependent.

  - id: pred:left-solvable
    name: LeftSolvable
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - LeftSolvable
    description: >
      Volume II predicate or assertion named LeftSolvable.

  - id: pred:multiplicative
    name: Multiplicative
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - Multiplicative
    description: >
      Volume II predicate or assertion named Multiplicative.

  - id: pred:negation-distributes-over-product
    name: NegationDistributesOverProduct
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - NegationDistributesOverProduct
    description: >
      Volume II predicate or assertion named NegationDistributesOverProduct.

  - id: pred:negative-one-acts-by-negation
    name: NegativeOneActsByNegation
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - NegativeOneActsByNegation
    description: >
      Volume II predicate or assertion named NegativeOneActsByNegation.

  - id: pred:nonnegative
    name: Nonnegative
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - Nonnegative
    description: >
      Volume II predicate or assertion named Nonnegative.

  - id: pred:nonnegative-square-root
    name: NonnegativeSquareRoot
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - NonnegativeSquareRoot
    description: >
      Volume II predicate or assertion named NonnegativeSquareRoot.

  - id: pred:nonnegative-value
    name: NonnegativeValue
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - NonnegativeValue
    description: >
      Volume II predicate or assertion named NonnegativeValue.

  - id: pred:no-nonzero-zero-divisors
    name: NoNonzeroZeroDivisors
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - NoNonzeroZeroDivisors
    description: >
      Volume II predicate or assertion named NoNonzeroZeroDivisors.

  - id: pred:nonzero-carrier
    name: NonzeroCarrier
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - NonzeroCarrier
    description: >
      Volume II predicate or assertion named NonzeroCarrier.

  - id: pred:not-well-ordered
    name: NotWellOrdered
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - NotWellOrdered
    description: >
      Volume II predicate or assertion named NotWellOrdered.

  - id: pred:no-zero-divisors
    name: NoZeroDivisors
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - NoZeroDivisors
    description: >
      Volume II predicate or assertion named NoZeroDivisors.

  - id: pred:one-sided-rational-approximation
    name: OneSidedRationalApproximation
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - OneSidedRationalApproximation
    description: >
      Volume II predicate or assertion named OneSidedRationalApproximation.

  - id: pred:order-compatible
    name: OrderCompatible
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - OrderCompatible
    description: >
      Volume II predicate or assertion named OrderCompatible.

  - id: pred:order-preserving-left-addition
    name: OrderPreservingLeftAddition
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - OrderPreservingLeftAddition
    description: >
      Volume II predicate or assertion named OrderPreservingLeftAddition.

  - id: pred:order-preserving-right-addition
    name: OrderPreservingRightAddition
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - OrderPreservingRightAddition
    description: >
      Volume II predicate or assertion named OrderPreservingRightAddition.

  - id: pred:permutation-independent
    name: PermutationIndependent
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - PermutationIndependent
    description: >
      Volume II predicate or assertion named PermutationIndependent.

  - id: pred:positive
    name: Positive
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - Positive
    description: >
      Volume II predicate or assertion named Positive.

  - id: pred:positive-cone-multiplicatively-closed
    name: PositiveConeMultiplicativelyClosed
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - PositiveConeMultiplicativelyClosed
    description: >
      Volume II predicate or assertion named PositiveConeMultiplicativelyClosed.

  - id: pred:preserves-one
    name: PreservesOne
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - PreservesOne
    description: >
      Volume II predicate or assertion named PreservesOne.

  - id: pred:preserves-zero
    name: PreservesZero
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - PreservesZero
    description: >
      Volume II predicate or assertion named PreservesZero.

  - id: pred:product-of-negatives-law
    name: ProductOfNegativesLaw
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - ProductOfNegativesLaw
    description: >
      Volume II predicate or assertion named ProductOfNegativesLaw.

  - id: pred:quotient-equality-criterion
    name: QuotientEqualityCriterion
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - QuotientEqualityCriterion
    description: >
      Volume II predicate or assertion named QuotientEqualityCriterion.

  - id: pred:refines
    name: Refines
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - Refines
    description: >
      Volume II predicate or assertion named Refines.

  - id: pred:right-cancellative
    name: RightCancellative
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - RightCancellative
    description: >
      Volume II predicate or assertion named RightCancellative.

  - id: pred:right-monotone
    name: RightMonotone
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - RightMonotone
    description: >
      Volume II predicate or assertion named RightMonotone.

  - id: pred:right-negation-distributes-over-product
    name: RightNegationDistributesOverProduct
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - RightNegationDistributesOverProduct
    description: >
      Volume II predicate or assertion named RightNegationDistributesOverProduct.

  - id: pred:right-order-reflecting
    name: RightOrderReflecting
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - RightOrderReflecting
    description: >
      Volume II predicate or assertion named RightOrderReflecting.

  - id: pred:right-representative-independent
    name: RightRepresentativeIndependent
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - RightRepresentativeIndependent
    description: >
      Volume II predicate or assertion named RightRepresentativeIndependent.

  - id: pred:right-solvable
    name: RightSolvable
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - RightSolvable
    description: >
      Volume II predicate or assertion named RightSolvable.

  - id: pred:same-square
    name: SameSquare
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - SameSquare
    description: >
      Volume II predicate or assertion named SameSquare.

  - id: pred:sign-decomposition
    name: SignDecomposition
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - SignDecomposition
    description: >
      Volume II predicate or assertion named SignDecomposition.

  - id: pred:sign-trichotomy
    name: SignTrichotomy
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - SignTrichotomy
    description: >
      Volume II predicate or assertion named SignTrichotomy.

  - id: pred:solvable
    name: Solvable
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - Solvable
    description: >
      Volume II predicate or assertion named Solvable.

  - id: pred:strictly-monotone
    name: StrictlyMonotone
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - StrictlyMonotone
    description: >
      Volume II predicate or assertion named StrictlyMonotone.

  - id: pred:strict-total-order
    name: StrictTotalOrder
    kind: predicate
    category: order
    arguments:
      - name: R
        role: relation
      - name: A
        role: carrier
    returns: truth_value
    surface_forms:
      - StrictTotalOrder
      - strict total order
    description: >
      The relation R is a strict total order on A; exact-name predicate form
      used by Volume II.

  - id: pred:total
    name: Total
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - Total
    description: >
      Volume II predicate or assertion named Total.

  - id: pred:triangle-inequality
    name: TriangleInequality
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - TriangleInequality
    description: >
      Volume II predicate or assertion named TriangleInequality.

  - id: pred:trichotomous
    name: Trichotomous
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - Trichotomous
    description: >
      Volume II predicate or assertion named Trichotomous.

  - id: pred:unique
    name: Unique
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - Unique
    description: >
      Volume II predicate or assertion named Unique.

  - id: pred:unique-inverse
    name: UniqueInverse
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - UniqueInverse
    description: >
      Volume II predicate or assertion named UniqueInverse.

  - id: pred:unique-limit
    name: UniqueLimit
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - UniqueLimit
    description: >
      Volume II predicate or assertion named UniqueLimit.

  - id: pred:unique-nonnegative-square-root
    name: UniqueNonnegativeSquareRoot
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - UniqueNonnegativeSquareRoot
    description: >
      Volume II predicate or assertion named UniqueNonnegativeSquareRoot.

  - id: pred:unit
    name: Unit
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - Unit
    description: >
      Volume II predicate or assertion named Unit.

  - id: pred:units-divide-all
    name: UnitsDivideAll
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - UnitsDivideAll
    description: >
      Volume II predicate or assertion named UnitsDivideAll.

  - id: pred:units-exactly
    name: UnitsExactly
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - UnitsExactly
    description: >
      Volume II predicate or assertion named UnitsExactly.

  - id: pred:well-defined
    name: WellDefined
    kind: predicate
    category: well_definedness
    arguments:
      - name: X
        role: construction_or_map
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - WellDefined
    description: >
      The construction, map, operation, or induced object X is well-defined in
      context C; exact-name generic form used when a more specific
      well-definedness predicate is not intended.

  - id: pred:well-defined-predicate
    name: WellDefinedPredicate
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - WellDefinedPredicate
    description: >
      Volume II predicate or assertion named WellDefinedPredicate.

  - id: pred:well-order
    name: WellOrder
    kind: predicate
    category: order
    arguments:
      - name: R
        role: relation
      - name: A
        role: carrier
    returns: truth_value
    surface_forms:
      - WellOrder
      - well-order
    description: >
      The relation R well-orders A; exact-name predicate form used by Volume II.

  - id: pred:zero-criterion
    name: ZeroCriterion
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - ZeroCriterion
    description: >
      Volume II predicate or assertion named ZeroCriterion.

  - id: pred:zero-divisor
    name: ZeroDivisor
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - ZeroDivisor
    description: >
      Volume II predicate or assertion named ZeroDivisor.

  - id: pred:zero-kernel
    name: ZeroKernel
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - ZeroKernel
    description: >
      Volume II predicate or assertion named ZeroKernel.

  - id: pred:absorbing-element
    name: AbsorbingElement
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - AbsorbingElement
    description: >
      Volume II predicate or assertion named AbsorbingElement.

  - id: pred:bezout-identity
    name: BezoutIdentity
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - BezoutIdentity
    description: >
      Volume II predicate or assertion named BezoutIdentity.

  - id: pred:bottom
    name: Bottom
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - Bottom
    description: >
      Volume II predicate or assertion named Bottom.

  - id: pred:canonical-embedding
    name: CanonicalEmbedding
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - CanonicalEmbedding
    description: >
      Volume II predicate or assertion named CanonicalEmbedding.

  - id: pred:compatible-embedding-chain
    name: CompatibleEmbeddingChain
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - CompatibleEmbeddingChain
    description: >
      Volume II predicate or assertion named CompatibleEmbeddingChain.

  - id: pred:division-algorithm
    name: DivisionAlgorithm
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - DivisionAlgorithm
    description: >
      Volume II predicate or assertion named DivisionAlgorithm.

  - id: pred:ext-interval
    name: ExtInterval
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - ExtInterval
    description: >
      Volume II predicate or assertion named ExtInterval.

  - id: pred:general-recursive-function
    name: GeneralRecursiveFunction
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - GeneralRecursiveFunction
    description: >
      Volume II predicate or assertion named GeneralRecursiveFunction.

  - id: pred:stage-dependent-recursion-solution
    name: StageDependentRecursionSolution
    kind: predicate
    category: volume_ii
    arguments:
      - name: f
        role: function
      - name: peano_system
        role: structure
      - name: W
        role: codomain
      - name: c
        role: initial_value
      - name: Phi
        role: transition_function
    returns: truth_value
    polymorphic: true
    surface_forms:
      - StageDependentRecursionSolution
    description: >
      Volume II predicate for a function satisfying the base and successor
      clauses of a stage-dependent recursion on a Peano system.

  - id: pred:greatest-common-divisor
    name: GreatestCommonDivisor
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - GreatestCommonDivisor
    description: >
      Volume II predicate or assertion named GreatestCommonDivisor.

  - id: pred:homomorphism
    name: Homomorphism
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - Homomorphism
    description: >
      Volume II predicate or assertion named Homomorphism.

  - id: pred:identity-homomorphism
    name: IdentityHomomorphism
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - IdentityHomomorphism
    description: >
      Volume II predicate or assertion named IdentityHomomorphism.

  - id: pred:image-equals-nonnegative-cone
    name: ImageEqualsNonnegativeCone
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - ImageEqualsNonnegativeCone
    description: >
      Volume II predicate or assertion named ImageEqualsNonnegativeCone.

  - id: pred:injective-homomorphism
    name: InjectiveHomomorphism
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - InjectiveHomomorphism
    description: >
      Volume II predicate or assertion named InjectiveHomomorphism.

  - id: pred:is-integral-domain
    name: IsIntegralDomain
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - IsIntegralDomain
    description: >
      Volume II predicate or assertion named IsIntegralDomain.

  - id: pred:isomorphism
    name: Isomorphism
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - Isomorphism
    description: >
      Volume II predicate or assertion named Isomorphism.

  - id: pred:iterator-function
    name: IteratorFunction
    kind: predicate
    category: volume_ii
    arguments:
      - name: f
        role: function
      - name: peano_system
        role: structure
      - name: W
        role: set
      - name: c
        role: value
      - name: g
        role: function
    returns: truth_value
    polymorphic: true
    surface_forms:
      - IteratorFunction
    description: >
      The function f is the iterator function along the supplied Peano
      system, with codomain or value set W, base value c, and step map g.

  - id: pred:iterator-generated-function
    name: IteratorGeneratedFunction
    kind: predicate
    category: volume_ii
    arguments:
      - name: f
        role: function
      - name: peano_system
        role: structure
      - name: W
        role: set
      - name: c
        role: value
      - name: g
        role: function
    returns: truth_value
    polymorphic: true
    surface_forms:
      - IteratorGeneratedFunction
    description: >
      The function f is the unique iterator-generated function along the
      supplied Peano system, with codomain or value set W, base value c, and
      step map g.

  - id: pred:left-absorbing-element
    name: LeftAbsorbingElement
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - LeftAbsorbingElement
    description: >
      Volume II predicate or assertion named LeftAbsorbingElement.

  - id: pred:monotone-operation
    name: MonotoneOperation
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - MonotoneOperation
    description: >
      Volume II predicate or assertion named MonotoneOperation.

  - id: pred:negative-factor-reverses-order
    name: NegativeFactorReversesOrder
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - NegativeFactorReversesOrder
    description: >
      Volume II predicate or assertion named NegativeFactorReversesOrder.

  - id: pred:one-element
    name: OneElement
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - OneElement
    description: >
      Volume II predicate or assertion named OneElement.

  - id: pred:order-reflecting-operation
    name: OrderReflectingOperation
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - OrderReflectingOperation
    description: >
      Volume II predicate or assertion named OrderReflectingOperation.

  - id: pred:positive-factor-preserves-order
    name: PositiveFactorPreservesOrder
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - PositiveFactorPreservesOrder
    description: >
      Volume II predicate or assertion named PositiveFactorPreservesOrder.

  - id: pred:positive-left-factor-preserves-order
    name: PositiveLeftFactorPreservesOrder
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - PositiveLeftFactorPreservesOrder
    description: >
      Volume II predicate or assertion named PositiveLeftFactorPreservesOrder.

  - id: pred:positive-right-factor-preserves-order
    name: PositiveRightFactorPreservesOrder
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - PositiveRightFactorPreservesOrder
    description: >
      Volume II predicate or assertion named PositiveRightFactorPreservesOrder.

  - id: pred:right-absorbing-element
    name: RightAbsorbingElement
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - RightAbsorbingElement
    description: >
      Volume II predicate or assertion named RightAbsorbingElement.

  - id: pred:strong-induction
    name: StrongInduction
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - StrongInduction
    description: >
      Volume II predicate or assertion named StrongInduction.

  - id: pred:strong-induction-principle
    name: StrongInductionPrinciple
    kind: predicate
    category: volume_ii
    arguments:
      - name: P
        role: carrier
      - name: order
        role: relation
      - name: phi
        role: predicate
    returns: truth_value
    polymorphic: true
    surface_forms:
      - StrongInductionPrinciple
    description: >
      Volume II predicate or assertion named StrongInductionPrinciple.

  - id: pred:structure-embedding
    name: StructureEmbedding
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - StructureEmbedding
    description: >
      Volume II predicate or assertion named StructureEmbedding.

  - id: pred:structure-preserving-map
    name: StructurePreservingMap
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - StructurePreservingMap
    description: >
      Volume II predicate or assertion named StructurePreservingMap.

  - id: pred:top
    name: Top
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - Top
    description: >
      Volume II predicate or assertion named Top.

  - id: pred:unique-order-isomorphism
    name: UniqueOrderIsomorphism
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - UniqueOrderIsomorphism
    description: >
      Volume II predicate or assertion named UniqueOrderIsomorphism.

  - id: pred:well-ordering-principle
    name: WellOrderingPrinciple
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - WellOrderingPrinciple
    description: >
      Volume II predicate or assertion named WellOrderingPrinciple.

  - id: pred:zero-element
    name: ZeroElement
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - ZeroElement
    description: >
      Volume II predicate or assertion named ZeroElement.

  - id: pred:zero-multiplication-collapses-order
    name: ZeroMultiplicationCollapsesOrder
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - ZeroMultiplicationCollapsesOrder
    description: >
      Volume II predicate or assertion named ZeroMultiplicationCollapsesOrder.

  - id: pred:least-upper-bound-property
    name: LeastUpperBoundProperty
    kind: predicate
    category: volume_ii
    arguments:
      - name: X
        role: object
      - name: C
        role: context
    returns: truth_value
    ambient_argument: C
    polymorphic: true
    surface_forms:
      - LeastUpperBoundProperty
    description: >
      Volume II predicate or assertion named LeastUpperBoundProperty.

  - id: pred:has-ieee-class
    name: HasIEEEClass
    kind: predicate
    category: numerical_analysis
    arguments:
      - name: x
        role: datum
      - name: F
        role: format
      - name: C
        role: encoding_class
    returns: truth_value
    ambient_argument: F
    polymorphic: false
    surface_forms:
      - has IEEE class
      - IEEE encoding class
      - normal IEEE datum
      - subnormal IEEE datum
      - IEEE infinity encoding
      - IEEE NaN encoding
    description: >
      The IEEE binary datum x in format F has encoding class C. Standard
      classes include normal, subnormal, infinity, and NaN; these are class
      objects rather than separate predicate names.

  - id: pred:test-predicate-1
    name: TestPredicate01
    kind: predicate
    category: synthetic_test_predicate
    testing: true
    arguments:
      - name: arg1_element
        role: element
      - name: arg2_element
        role: element
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestPredicate01
      - P_{1}
      - P_1
    description: >
      Registered synthetic predicate symbol TestPredicate01 used by parser validation campaigns.

  - id: pred:test-predicate-2
    name: TestPredicate02
    kind: predicate
    category: synthetic_test_predicate
    testing: true
    arguments: []
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestPredicate02
      - P_{2}
      - P_2
    description: >
      Registered synthetic predicate symbol TestPredicate02 used by parser validation campaigns.

  - id: pred:test-predicate-3
    name: TestPredicate03
    kind: predicate
    category: synthetic_test_predicate
    testing: true
    arguments: []
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestPredicate03
      - P_{3}
      - P_3
    description: >
      Registered synthetic predicate symbol TestPredicate03 used by parser validation campaigns.

  - id: pred:test-predicate-4
    name: TestPredicate04
    kind: predicate
    category: synthetic_test_predicate
    testing: true
    arguments:
      - name: arg1_element
        role: element
      - name: arg2_element
        role: element
      - name: arg3_element
        role: element
      - name: arg4_element
        role: element
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestPredicate04
      - P_{4}
      - P_4
    description: >
      Registered synthetic predicate symbol TestPredicate04 used by parser validation campaigns.

  - id: pred:test-predicate-5
    name: TestPredicate05
    kind: predicate
    category: synthetic_test_predicate
    testing: true
    arguments:
      - name: arg1_element
        role: element
      - name: arg2_element
        role: element
      - name: arg3_element
        role: element
      - name: arg4_element
        role: element
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestPredicate05
      - P_{5}
      - P_5
    description: >
      Registered synthetic predicate symbol TestPredicate05 used by parser validation campaigns.

  - id: pred:test-predicate-6
    name: TestPredicate06
    kind: predicate
    category: synthetic_test_predicate
    testing: true
    arguments: []
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestPredicate06
      - P_{6}
      - P_6
    description: >
      Registered synthetic predicate symbol TestPredicate06 used by parser validation campaigns.

  - id: pred:test-predicate-7
    name: TestPredicate07
    kind: predicate
    category: synthetic_test_predicate
    testing: true
    arguments: []
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestPredicate07
      - P_{7}
      - P_7
    description: >
      Registered synthetic predicate symbol TestPredicate07 used by parser validation campaigns.

  - id: pred:test-predicate-8
    name: TestPredicate08
    kind: predicate
    category: synthetic_test_predicate
    testing: true
    arguments:
      - name: arg1_element
        role: element
      - name: arg2_element
        role: element
      - name: arg3_element
        role: element
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestPredicate08
      - P_{8}
      - P_8
    description: >
      Registered synthetic predicate symbol TestPredicate08 used by parser validation campaigns.

  - id: pred:test-predicate-9
    name: TestPredicate09
    kind: predicate
    category: synthetic_test_predicate
    testing: true
    arguments:
      - name: arg1_element
        role: element
      - name: arg2_element
        role: element
      - name: arg3_element
        role: element
      - name: arg4_element
        role: element
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestPredicate09
      - P_{9}
      - P_9
    description: >
      Registered synthetic predicate symbol TestPredicate09 used by parser validation campaigns.

  - id: pred:test-predicate-10
    name: TestPredicate10
    kind: predicate
    category: synthetic_test_predicate
    testing: true
    arguments:
      - name: arg1_element
        role: element
      - name: arg2_element
        role: element
      - name: arg3_element
        role: element
      - name: arg4_element
        role: element
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestPredicate10
      - P_{10}
      - P_10
    description: >
      Registered synthetic predicate symbol TestPredicate10 used by parser validation campaigns.

  - id: pred:test-predicate-11
    name: TestPredicate11
    kind: predicate
    category: synthetic_test_predicate
    testing: true
    arguments:
      - name: arg1_element
        role: element
      - name: arg2_element
        role: element
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestPredicate11
      - P_{11}
      - P_11
    description: >
      Registered synthetic predicate symbol TestPredicate11 used by parser validation campaigns.

  - id: pred:test-predicate-12
    name: TestPredicate12
    kind: predicate
    category: synthetic_test_predicate
    testing: true
    arguments:
      - name: arg1_element
        role: element
      - name: arg2_element
        role: element
      - name: arg3_element
        role: element
      - name: arg4_element
        role: element
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestPredicate12
      - P_{12}
      - P_12
    description: >
      Registered synthetic predicate symbol TestPredicate12 used by parser validation campaigns.

  - id: pred:test-predicate-13
    name: TestPredicate13
    kind: predicate
    category: synthetic_test_predicate
    testing: true
    arguments: []
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestPredicate13
      - P_{13}
      - P_13
    description: >
      Registered synthetic predicate symbol TestPredicate13 used by parser validation campaigns.

  - id: pred:test-predicate-14
    name: TestPredicate14
    kind: predicate
    category: synthetic_test_predicate
    testing: true
    arguments:
      - name: arg1_element
        role: element
      - name: arg2_element
        role: element
      - name: arg3_element
        role: element
      - name: arg4_element
        role: element
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestPredicate14
      - P_{14}
      - P_14
    description: >
      Registered synthetic predicate symbol TestPredicate14 used by parser validation campaigns.

  - id: pred:test-predicate-15
    name: TestPredicate15
    kind: predicate
    category: synthetic_test_predicate
    testing: true
    arguments:
      - name: arg1_element
        role: element
      - name: arg2_element
        role: element
      - name: arg3_element
        role: element
      - name: arg4_element
        role: element
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestPredicate15
      - P_{15}
      - P_15
    description: >
      Registered synthetic predicate symbol TestPredicate15 used by parser validation campaigns.

  - id: pred:test-predicate-16
    name: TestPredicate16
    kind: predicate
    category: synthetic_test_predicate
    testing: true
    arguments:
      - name: arg1_element
        role: element
      - name: arg2_element
        role: element
      - name: arg3_element
        role: element
      - name: arg4_element
        role: element
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestPredicate16
      - P_{16}
      - P_16
    description: >
      Registered synthetic predicate symbol TestPredicate16 used by parser validation campaigns.

  - id: pred:test-predicate-17
    name: TestPredicate17
    kind: predicate
    category: synthetic_test_predicate
    testing: true
    arguments:
      - name: arg1_element
        role: element
      - name: arg2_element
        role: element
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestPredicate17
      - P_{17}
      - P_17
    description: >
      Registered synthetic predicate symbol TestPredicate17 used by parser validation campaigns.

  - id: pred:test-predicate-18
    name: TestPredicate18
    kind: predicate
    category: synthetic_test_predicate
    testing: true
    arguments:
      - name: arg1_element
        role: element
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestPredicate18
      - P_{18}
      - P_18
    description: >
      Registered synthetic predicate symbol TestPredicate18 used by parser validation campaigns.

  - id: pred:test-predicate-19
    name: TestPredicate19
    kind: predicate
    category: synthetic_test_predicate
    testing: true
    arguments:
      - name: arg1_element
        role: element
      - name: arg2_element
        role: element
      - name: arg3_element
        role: element
      - name: arg4_element
        role: element
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestPredicate19
      - P_{19}
      - P_19
    description: >
      Registered synthetic predicate symbol TestPredicate19 used by parser validation campaigns.

  - id: pred:test-predicate-20
    name: TestPredicate20
    kind: predicate
    category: synthetic_test_predicate
    testing: true
    arguments: []
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestPredicate20
      - P_{20}
      - P_20
    description: >
      Registered synthetic predicate symbol TestPredicate20 used by parser validation campaigns.

  - id: pred:test-predicate-21
    name: TestPredicate21
    kind: predicate
    category: synthetic_test_predicate
    testing: true
    arguments:
      - name: arg1_element
        role: element
      - name: arg2_element
        role: element
      - name: arg3_element
        role: element
      - name: arg4_element
        role: element
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestPredicate21
      - P_{21}
      - P_21
    description: >
      Registered synthetic predicate symbol TestPredicate21 used by parser validation campaigns.

  - id: pred:test-predicate-22
    name: TestPredicate22
    kind: predicate
    category: synthetic_test_predicate
    testing: true
    arguments:
      - name: arg1_element
        role: element
      - name: arg2_element
        role: element
      - name: arg3_element
        role: element
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestPredicate22
      - P_{22}
      - P_22
    description: >
      Registered synthetic predicate symbol TestPredicate22 used by parser validation campaigns.

  - id: pred:test-predicate-23
    name: TestPredicate23
    kind: predicate
    category: synthetic_test_predicate
    testing: true
    arguments:
      - name: arg1_element
        role: element
      - name: arg2_element
        role: element
      - name: arg3_element
        role: element
      - name: arg4_element
        role: element
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestPredicate23
      - P_{23}
      - P_23
    description: >
      Registered synthetic predicate symbol TestPredicate23 used by parser validation campaigns.

  - id: pred:test-predicate-24
    name: TestPredicate24
    kind: predicate
    category: synthetic_test_predicate
    testing: true
    arguments: []
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestPredicate24
      - P_{24}
      - P_24
    description: >
      Registered synthetic predicate symbol TestPredicate24 used by parser validation campaigns.

  - id: pred:test-predicate-25
    name: TestPredicate25
    kind: predicate
    category: synthetic_test_predicate
    testing: true
    arguments: []
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestPredicate25
      - P_{25}
      - P_25
    description: >
      Registered synthetic predicate symbol TestPredicate25 used by parser validation campaigns.

  - id: pred:test-predicate-26
    name: TestPredicate26
    kind: predicate
    category: synthetic_test_predicate
    testing: true
    arguments:
      - name: arg1_element
        role: element
      - name: arg2_element
        role: element
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestPredicate26
      - P_{26}
      - P_26
    description: >
      Registered synthetic predicate symbol TestPredicate26 used by parser validation campaigns.

  - id: pred:test-predicate-27
    name: TestPredicate27
    kind: predicate
    category: synthetic_test_predicate
    testing: true
    arguments:
      - name: arg1_element
        role: element
      - name: arg2_element
        role: element
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestPredicate27
      - P_{27}
      - P_27
    description: >
      Registered synthetic predicate symbol TestPredicate27 used by parser validation campaigns.

  - id: pred:test-predicate-28
    name: TestPredicate28
    kind: predicate
    category: synthetic_test_predicate
    testing: true
    arguments:
      - name: arg1_element
        role: element
      - name: arg2_element
        role: element
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestPredicate28
      - P_{28}
      - P_28
    description: >
      Registered synthetic predicate symbol TestPredicate28 used by parser validation campaigns.

  - id: pred:test-relation-1
    name: TestRelation01
    kind: predicate
    category: synthetic_test_relation
    testing: true
    arguments:
      - name: arg1_element
        role: element
      - name: arg2_element
        role: element
      - name: arg3_element
        role: element
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestRelation01
      - R_{1}
      - R_1
    description: >
      Registered synthetic relation symbol TestRelation01 used by parser validation campaigns.

  - id: pred:test-relation-2
    name: TestRelation02
    kind: predicate
    category: synthetic_test_relation
    testing: true
    arguments:
      - name: arg1_element
        role: element
      - name: arg2_element
        role: element
      - name: arg3_element
        role: element
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestRelation02
      - R_{2}
      - R_2
    description: >
      Registered synthetic relation symbol TestRelation02 used by parser validation campaigns.

  - id: pred:test-relation-3
    name: TestRelation03
    kind: predicate
    category: synthetic_test_relation
    testing: true
    arguments:
      - name: arg1_element
        role: element
      - name: arg2_element
        role: element
      - name: arg3_element
        role: element
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestRelation03
      - R_{3}
      - R_3
    description: >
      Registered synthetic relation symbol TestRelation03 used by parser validation campaigns.

  - id: pred:test-relation-4
    name: TestRelation04
    kind: predicate
    category: synthetic_test_relation
    testing: true
    arguments:
      - name: arg1_element
        role: element
      - name: arg2_element
        role: element
      - name: arg3_element
        role: element
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestRelation04
      - R_{4}
      - R_4
    description: >
      Registered synthetic relation symbol TestRelation04 used by parser validation campaigns.

  - id: pred:test-relation-5
    name: TestRelation05
    kind: predicate
    category: synthetic_test_relation
    testing: true
    arguments:
      - name: arg1_element
        role: element
      - name: arg2_element
        role: element
      - name: arg3_element
        role: element
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestRelation05
      - R_{5}
      - R_5
    description: >
      Registered synthetic relation symbol TestRelation05 used by parser validation campaigns.

  - id: pred:test-relation-6
    name: TestRelation06
    kind: predicate
    category: synthetic_test_relation
    testing: true
    arguments:
      - name: arg1_element
        role: element
      - name: arg2_element
        role: element
      - name: arg3_element
        role: element
      - name: arg4_element
        role: element
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestRelation06
      - R_{6}
      - R_6
    description: >
      Registered synthetic relation symbol TestRelation06 used by parser validation campaigns.

  - id: pred:test-relation-7
    name: TestRelation07
    kind: predicate
    category: synthetic_test_relation
    testing: true
    arguments:
      - name: arg1_element
        role: element
      - name: arg2_element
        role: element
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestRelation07
      - R_{7}
      - R_7
    description: >
      Registered synthetic relation symbol TestRelation07 used by parser validation campaigns.

  - id: pred:test-relation-8
    name: TestRelation08
    kind: predicate
    category: synthetic_test_relation
    testing: true
    arguments:
      - name: arg1_element
        role: element
      - name: arg2_element
        role: element
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestRelation08
      - R_{8}
      - R_8
    description: >
      Registered synthetic relation symbol TestRelation08 used by parser validation campaigns.

  - id: pred:test-relation-9
    name: TestRelation09
    kind: predicate
    category: synthetic_test_relation
    testing: true
    arguments:
      - name: arg1_element
        role: element
      - name: arg2_element
        role: element
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestRelation09
      - R_{9}
      - R_9
    description: >
      Registered synthetic relation symbol TestRelation09 used by parser validation campaigns.

  - id: pred:test-relation-10
    name: TestRelation10
    kind: predicate
    category: synthetic_test_relation
    testing: true
    arguments:
      - name: arg1_element
        role: element
      - name: arg2_element
        role: element
      - name: arg3_element
        role: element
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestRelation10
      - R_{10}
      - R_10
    description: >
      Registered synthetic relation symbol TestRelation10 used by parser validation campaigns.

  - id: pred:test-relation-11
    name: TestRelation11
    kind: predicate
    category: synthetic_test_relation
    testing: true
    arguments:
      - name: arg1_element
        role: element
      - name: arg2_element
        role: element
      - name: arg3_element
        role: element
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestRelation11
      - R_{11}
      - R_11
    description: >
      Registered synthetic relation symbol TestRelation11 used by parser validation campaigns.

  - id: pred:test-relation-12
    name: TestRelation12
    kind: predicate
    category: synthetic_test_relation
    testing: true
    arguments:
      - name: arg1_element
        role: element
      - name: arg2_element
        role: element
      - name: arg3_element
        role: element
    returns: truth_value
    polymorphic: true
    surface_forms:
      - TestRelation12
      - R_{12}
      - R_12
    description: >
      Registered synthetic relation symbol TestRelation12 used by parser validation campaigns.