∀≤

Topic 001 · Standalone Paper

Working Paper · 2026

A Logic of Bounded Quantification: Syntax, Semantics, and Metatheory

Bounded First-Order Logic

A principled restriction of first-order logic in which every quantifier carries an explicit bounding term. Unbounded quantifier forms are not merely restricted — they are absent from the language. The grammar enforces what convention cannot: a variable may not range without a named limit. Full metatheory established: soundness, completeness, decidability, cut-elimination, Craig interpolation, and Beth definability.

Read the Paper Finite Philosophy → Bounded Set Theory →

Modification

One change — quantifier forms

Quantifiers

∀x ≤ t and ∃x ≤ t only

Metatheory

9 theorems established

Supersedes

AFB Part III

Proof method

Direct Maehara on BFOL

One change. Substantial consequences.

BFOL differs from standard first-order logic in exactly one structural respect: the primitive quantifier forms. Everything else is identical — term formation, atomic formulas, connectives, equality, proof rules. The modification aligns the grammar of the logic with settings where quantification is always over a bounded region.

The result: a logic that enforces bounded quantification at the level of well-formedness, not convention. An unbounded quantification cannot be written — not because it is prohibited, but because it is not a formula of the language.

The single modification

∀x φ(x) Not well-formed in BFOL ∃x φ(x) Not well-formed in BFOL ∀x ≤ t φ(x) Well-formed — bound explicit ∃x ≤ t φ(x) Well-formed — bound explicit

The bound t is not optional. It is part of the syntax of quantification. A variable cannot range without a named limit.

Structural Consequences

What follows from one syntactic change.

Two gains — one syntactic, one semantic — follow from promoting bounded quantifiers from abbreviation to primitive status.

Syntactic gain

Grammatical enforcement

In standard FOL, a formula like ∀x φ(x) is well-formed regardless of whether the intended application restricts x to a bounded range. In BFOL, the formation rules require an explicit bound. The discipline is grammatical rather than conventional — you cannot accidentally write an unbounded quantification.

Semantic gain

No forced infinite models

Standard FOL's compactness theorem guarantees that any theory with arbitrarily large finite models also has infinite models. Under BFOL's Global Boundedness Principle, the compactness argument does not apply. A theory formulated in BFOL can have models of every finite size without being forced into infinite ones.

Example derivation — bounded ∀-elimination

1. ∀x ≤ c R(x) [from Γ] 2. a ≤ c [assumption] 3. R(a) [∀-E on 1, 2]

Proposition 0

Nonemptiness from grammar.

In standard FOL, nonemptiness of the domain is imposed as a convention. In BFOL, it is a consequence of the grammar. Every BFOL sentence contains at least one constant symbol (because outermost bounding terms must be closed), and constants require domain elements. Nonemptiness follows from the grammar of bounded quantification rather than from a semantic stipulation.

Metatheory

The full metatheoretic suite.

BFOL has the standard metatheoretic properties of first-order logic, while possessing distinctive behaviour when intended models are finite.

Theorem 1

Soundness

Every derivable sentence is true in every structure satisfying its assumptions. The BFOL deductive system never leads from true assumptions to a false conclusion.

Proof by induction on derivation length

Theorem 2

Decidability in Finite Structures

For any fixed finite structure and any BFOL sentence, truth is decidable. Every quantifier ranges over a finite set, every connective is a truth table, every atomic formula is a finite lookup.

Proof by induction on formula complexity

Theorem 3

Completeness

If a sentence is true in every BFOL-structure satisfying assumptions Γ, then it is derivable from Γ. Proved via embedding into FOL and Gödel's completeness theorem.

Via FOL embedding + Gödel (1930)

Theorem 4

Cut-Elimination

Every proof in the BFOL sequent calculus can be transformed into a cut-free proof. No unbounded quantifier is introduced at any stage. The subformula property holds.

Standard Gentzen argument (1935)

Theorem 5

Craig Interpolation

If φ entails ψ, there exists a BFOL interpolant θ using only shared vocabulary, with all quantifiers bounded. Proved directly by Maehara's method on the BFOL sequent calculus — not by round-trip through FOL.

Direct Maehara partition (1960)

Theorem 6

Beth Definability

If a relation is uniquely determined by a BFOL theory, it can be explicitly expressed by a bounded formula. Implicit and explicit definability coincide.

Immediate from Theorem 5

The Global Boundedness Principle

What changes when intended models are finite.

The GBP is a metatheoretic semantic restriction — every intended model has a finite domain. Under GBP, two classical metatheorems fail, and a characteristic contrast emerges.

BFOL (general)

All Models

Yes Soundness

Yes Completeness (all models)

Yes Cut-elimination

Yes Craig interpolation

Yes Beth definability

Yes Compactness (via FOL)

Yes Löwenheim-Skolem (via FOL)

BFOL + GBP

Finite Models Only

Yes Soundness

Yes Completeness (all models)

Yes Cut-elimination

Yes Craig interpolation

Yes Beth definability

No Compactness fails

No Löwenheim-Skolem fails

The Trakhtenbrot Contrast

Decidable per model. Not enumerable across all models.

Truth in any single finite structure is decidable by exhaustive computation. But the set of sentences true in all finite structures is not recursively enumerable. This gap — between single-model decidability and all-finite-model non-enumerability — is where any theory built on BFOL with finite intended models must confront its own incompleteness.

The logic is defined. It works.

Complete syntax, semantics, and proof theory in both natural deduction and sequent calculus. Nine metatheoretic results established. The relationship to standard FOL made precise. What is built on it is a separate question — and it is answered by Bounded Set Theory.

Read the Paper (PDF) Download PDF

Working Paper · 2026
Supersedes AFB Part III