BIT predicate¶

A binary relation that returns the zero-based j-th binary digit of a nonnegative integer i, enabling finite-set membership tests by bit position.

Version: v1 · 2026-10-07 · History
Domain-specific #: 13810
Domain group: Formal Sciences
Origin domain: Mathematics
Subdomains: Mathematical Logic, Arithmetic Coding → Mathematics
Aliases: BIT relation, Binary digit predicate

Core Idea¶

BIT(i,j) returns the binary digit at zero-based position j of a nonnegative integer i, counted from the least significant digit: BIT(i,j)=floor(i/2^j) mod 2. It is 1 when that position is set. The first argument is the number; the second is the position. The 1 positions of i form a finite subset of N, so BIT tests membership in that coded subset.[^ref-955c1cb34af7]

Scope of Application¶

Use BIT when a nonnegative integer or indexed bit vector assigns meanings to numbered binary positions. In simple finite-set coding, position j is the element j. In recursive Ackermann coding of hereditarily finite sets, position j is the code of a candidate member. A software bitset uses positions for application-defined flags or keys. These interpretations require their own conventions.[^{ref-955c1cb34af7][}ref-4ab367005a8b]

Clarity¶

Since 42 has 1 bits at positions 1, 3, and 5, BIT(42,3)=1 and BIT(42,2)=0. Reversing the arguments asks a different question. Any finite subset S corresponds to i=Σ_{j∈S}2^j, although a sparse set with a very large member can require a very long binary representation. A fixed-width machine word also has its own capacity boundary.[^ref-955c1cb34af7]

Manages Complexity¶

The digit test replaces an explicit membership search in the mathematical finite-subset code. With matching position conventions, bitwise OR and AND give union and intersection. Complement relative to all N is generally infinite and cannot fit in one finite integer; choose a finite mask or interval before using NOT or a range flip as set complement.[^{ref-955c1cb34af7][}ref-4ab367005a8b]

Abstract Reasoning¶

First specify i, j, and zero-based indexing; then compute floor(i/2^j) mod 2. Under Ackermann coding, f(∅)=0 and f(x)=Σ_{a∈x}2^{f(a)}. Thus BIT(f(x),f(a))=1 exactly when a∈x. The second argument is the member's numeric code f(a), rather than the set a itself.[^ref-955c1cb34af7]

Knowledge Transfer¶

Ackermann coding and Java BitSet share an indexed yes/no membership test. In one case positions denote codes of nested finite sets; in the other they denote application-defined indices. A Java BitSet can grow and exposes get(j), OR, AND, and finite-range flip, so its current state need not be one fixed-width integer.[^{ref-955c1cb34af7][}ref-4ab367005a8b]

Example¶

Tarau maps {1,3,5} to 42; in the recursive hereditarily finite interpretation, those are member codes. For a candidate member a with f(a)=3, BIT(42,3)=1. A BitSet with positions 1, 3, and 5 set likewise returns true from get(3) and false from get(2), although its positions can stand for different application keys.[^{ref-955c1cb34af7][}ref-4ab367005a8b]

Relationships to Other Abstractions¶

Current abstraction BIT predicate Domain-specific

Parents (1) — more general patterns this builds on

BIT predicate is a kind of Relation Prime

BIT is a particular binary relation on nonnegative integers with a specified digit-membership rule.

Hierarchy path (1) — routes to 1 parentless root

BIT predicate → Relation

Neighborhood in Abstraction Space¶

BIT predicate sits in a sparse region of the domain-specific corpus (98^th percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.

Family — Numeral Systems & Digit Algorithms (11 abstractions)

Nearest neighbors

Computed from structural-signature embeddings · 2026-10-08

Not to Be Confused With¶

BIT is a two-place relation, not a property of one number or an entire set representation. Do not reverse its arguments, silently use one-based indexing, or claim unbounded complement from finite bits. Its approved strict DAG parent is the live Relation Prime; the nearby Predicate Prime currently emphasizes a one-place property. Uses in ordered finite-model logic need the specified structure and theorem before any expressiveness claim.[^{ref-955c1cb34af7][}ref-7685de42d270]

References¶

[^ref-955c1cb34af7]: Paul Tarau, A Functional Hitchhiker's Guide to Hereditarily Finite Sets, Ackermann Encodings and Pairing Functions (2008), arXiv:0808.0754, §3.1 PDF pp. 2–3 for set2nat, nat2set, the pure Ackermann recurrence, and the example 42↔{1,3,5}; §2 PDF p. 2 for least-significant-first bit notation. https://arxiv.org/pdf/0808.0754

[^ref-4ab367005a8b]: Oracle, BitSet (Java Platform SE 8) (Java SE 8 API), class description and methods get(int), or(BitSet), and(BitSet), flip(int,int), and valueOf(long[]) for indexed membership, set operations, finite-range flip, and representation. https://docs.oracle.com/javase/8/docs/api/java/util/BitSet.html

[^ref-7685de42d270]: Albert Atserias and Phokion G. Kolaitis, First-Order Logic vs. Fixed-Point Logic in Finite Set Theory (LICS 1999), abstract on built-in BIT and ordered finite structures; cited only for the scope boundary, not for an unverified complexity-class equivalence. https://lics.siglog.org/archive/1999/AtseriasKolaitis-FirstOrderLogicvsFi.html