Formal Models of Reasons and Oughts

Formal Models of Reasons and Oughts

1. Question

The article Metaethical Grounding and Normative Logic develops an abstract categorical framework — the category Norm of normative perspectives, the self-correction operator C_N, the terminal coalgebra characterization of maximally self-grounding normative systems, and the mixer comonad. That framework is structurally elegant, but it operates at a level of generality that leaves two essential questions unanswered. First, what is the concrete logical calculus in which a grounding predicate G_N can be expressed, axiomatized, and reasoned with? Second, **how can the fixed-point condition G_N(r) ↔ G_N(G_N(r)) be realized as a theorem of a specific logic, rather than a meta-level constraint?**

Without answers, the abstract framework is a notation system that looks precise but cannot be implemented, tested, or refined. This article provides those answers. It defines GL (Grounding Logic), a bimodal deontic logic with a grounding operator that can express the fixed-point condition as an internal theorem; gives a Kripke-style relational semantics with a grounding accessibility relation; proves soundness, completeness, and fixed-point theorems; and shows how the logic can be instantiated by different normative theories (Kantian, consequentialist, contractualist) by varying the grounding accessibility constraints. The result is an operational normative logic that can serve as the formal core for computational implementations — a logical engine for reasoning about self-grounding "oughts."

2. Syntax of GL (Grounding Logic)

2.1 Language

Let At be a countable set of atomic normative propositions (representing basic normative claims: "you ought to keep promises," "pain is bad," "autonomy is valuable"). The language ℒ_GL is generated by:

φ ::= p ∈ At | ¬φ | (φ ∧ φ) | □φ | Gφ

with the usual defined connectives ∨, →, ↔, ◇φ = ¬□¬φ.

Reading: - □φ: "it is normatively required that φ" (the deontic necessity operator — standard reading of obligation in deontic logic). - Gφ: "φ is grounded" — i.e., φ is a genuinely normative claim whose normativity is not merely hypothetical, conventional, or illusory. This is the formal counterpart of G_N(r) from Metaethical Grounding and Normative Logic.

We add a distinguished constant ⊥ (falsum) and define 0-ary □⊤ as the tautological normative requirement.

2.2 Axioms

Axiom schemas (for all φ, ψ ∈ ℒ_GL):

1. Classical propositional: All tautologies of propositional logic. 2. Deontic K-axiom: □(φ → ψ) → (□φ → □ψ). 3. Deontic D-axiom: □φ → ¬□¬φ (consistency of normative requirements — no conflicting obligations, or at least no impossible obligation). 4. Grounding K-axiom: G(φ → ψ) → (Gφ → Gψ). 5. Grounding D-axiom: Gφ → ¬G¬φ (grounding is consistent — the same claim cannot be both genuinely normative and not). 6. Grounding-deontic bridge: □φ → Gφ. (If φ is normatively required, then φ is grounded. This ensures that the deontic operator is a species of grounding, not a separate kind.) 7. Grounding iteration: Gφ → GGφ. (If φ is grounded, then the claim that φ is grounded is itself grounded. This is the axiom that makes the grounding operator generate the regress — it is the formal expression of G_N(r) ⊢_N G_N(G_N(r)) from the metaethical article.) 8. Grounding self-transparency: Gφ → □Gφ. (If a claim is grounded, it is normatively required that it is grounded. Grounding is not an optional or contingent status.)

Rule: - Modus ponens: From φ and φ → ψ, infer ψ. - □-necessitation: From ⊢ φ, infer ⊢ □φ. - G-necessitation: From ⊢ φ, infer ⊢ Gφ. (All theorems are grounded.)

Definition (The fixed-point axiom schema): For any formula φ, define:

GFP(φ): Gφ ↔ GGφ

This is the axiom that asserts that φ satisfies the fixed-point condition: the grounding of φ is equivalent to the grounding of the grounding of φ. A system that includes GFP(φ) for some φ treats φ as a self-grounding fixed point of the G-operator.

The base system GL₀ is the set of axioms 1-8 plus the three rules. Specific normative theories extend GL₀ by adding GFP instances and additional deontic axioms.

2.3 Remarks on the axioms

- Axiom 7 (Grounding iteration) is the structural engine of the regress. Without it, grounding is a one-step property with no regress pressure. With it, any grounded claim immediately generates a hierarchy of groundedness claims. The fixed-point axiom GFP(φ) then terminates the hierarchy at φ.

- Axiom 8 (Grounding self-transparency) ensures that G is not a contingent predicate: if φ is grounded, it is normatively required that it is grounded. This reflects the idea that grounding is a status that the normative system itself recognizes — it is not an external assessment.

- The bridge axiom 6 is the minimal link between □ and G. Stronger links are possible (e.g., □φ ↔ Gφ, making them equivalent), but the minimal version leaves room for grounded claims that are not obligations (e.g., "the value of autonomy is grounded" — a value claim that is not itself an obligation but is structurally normative).

3. Semantics

3.1 Grounding frames

A GL-frame is a tuple F = (W, R_□, R_G, V) where:

- W is a non-empty set of normative worlds (possible states of normative affairs). - R_□ ⊆ W × W is a deontic accessibility relation: w R_□ v means v is normatively ideal relative to w (the standard Kripke semantics for deontic logic). - R_G ⊆ W × W is a grounding accessibility relation: w R_G v means v realizes the groundedness of the norms that hold at w. - V: At → ℘(W) is a valuation function.

Constraints:

1. Deontic seriality: For every w ∈ W, there exists v ∈ W such that w R_□ v. (This validates the D-axiom: consistent obligations.) 2. Grounding seriality: For every w ∈ W, there exists v ∈ W such that w R_G v. (This validates Gφ → ¬G¬φ: consistent grounding.) 3. Bridge: R_□ ⊆ R_G. (If a world is deontically ideal relative to w, it also realizes the groundedness of w's norms. This validates □φ → Gφ.) 4. Grounding transitivity: R_G is transitive. (This validates Gφ → GGφ — grounding iteration.) 5. Grounding self-transparency: If w R_G v, then for all u, v R_□ u implies v R_G u. Moreover, if w R_G v, then w R_□ v.⁽¹⁾ (This validates Gφ → □Gφ and ensures the logic is well-behaved.)

⁽¹⁾The precise condition for Gφ → □Gφ: For any w, v with w R_G v, we require that v ∈ ⟦Gφ⟧ whenever w ∈ ⟦Gφ⟧. Since ⟦Gφ⟧ is defined via R_G (see 3.2), this means: if for all u with w R_G u we have u ∈ ⟦φ⟧, then for all u with v R_□ u we have that for all t with u R_G t: t ∈ ⟦φ⟧. The simplest sufficient condition is that R_G is a subrelation of the converse of R_□ composed with R_G — a condition automatically satisfied if R_□ ⊆ R_G (bridge) and R_G is transitive.

3.2 Truth conditions

Truth of a formula φ at a world w in frame F is defined inductively:

- w ⊨ p iff w ∈ V(p). - w ⊨ ¬φ iff w ⊭ φ. - w ⊨ φ ∧ ψ iff w ⊨ φ and w ⊨ ψ. - w ⊨ □φ iff for all v ∈ W with w R_□ v, v ⊨ φ. - w ⊨ Gφ iff for all v ∈ W with w R_G v, v ⊨ φ. (Gφ means "in every world that realizes the groundedness of the current norms, φ holds.")

Definition (Model): A GL-model is a pair M = (F, ⊨) where F is a GL-frame and ⊨ satisfies the above conditions.

Definition (Validity): A formula φ is valid in a frame F (F ⊨ φ) iff φ is true at every world in every model based on F. φ is valid in a class of frames iff it is valid in every frame in the class.

3.3 Soundness

Theorem (Soundness): Every theorem of GL₀ is valid in all GL-frames (i.e., serial, transitive R_G, with R_□ ⊆ R_G and the self-transparency condition).

Proof sketch: By induction on derivation length. The propositional tautologies and modus ponens are standard. □φ → ¬□¬φ follows from seriality of R_□. Gφ → ¬G¬φ follows from seriality of R_G. □φ → Gφ follows from R_□ ⊆ R_G. Gφ → GGφ follows from transitivity of R_G: if w ⊨ Gφ, then all R_G-successors satisfy φ. For any R_G-successor v of w, all R_G-successors of v (which are also R_G-successors of w by transitivity) satisfy φ, so v ⊨ Gφ, hence w ⊨ GGφ. Gφ → □Gφ follows from the self-transparency condition. □-necessitation and G-necessitation are standard necessitation rules for K-axiom systems. ∎

3.4 Completeness

Theorem (Completeness): For any set of formulas Σ ∪ {φ} in ℒ_GL, if φ is valid in all GL-frames, then φ is provable in GL₀.

Proof sketch: Standard canonical model construction. Define the canonical model M_c = (W_c, R_□^c, R_G^c, V_c) where: - W_c is the set of maximally GL₀-consistent sets of formulas. - Γ R_□^c Δ iff {φ | □φ ∈ Γ} ⊆ Δ. - Γ R_G^c Δ iff {φ | Gφ ∈ Γ} ⊆ Δ. - V_c(p) = {Γ ∈ W_c | p ∈ Γ}.

The Truth Lemma (Γ ⊨ φ iff φ ∈ Γ) is proved by induction. The canonical relation R_□^c is serial because GL₀ contains □φ → ¬□¬φ (which ensures □⊤ ∈ Γ for any consistent Γ, leading to a successor). R_G^c is serial and transitive by the axioms Gφ → ¬G¬φ and Gφ → GGφ. R_□^c ⊆ R_G^c because □φ → Gφ ensures the inclusion of the relevant sets. The self-transparency condition holds because Gφ → □Gφ ensures that if all G-necessary formulas of Γ are in Δ, then all □-necessary formulas of Δ contain the G-successors, etc. The standard filtration argument for completeness follows. ∎

3.5 Fixed-point frames

Definition (Fixed-point frame): A GL-frame F is a φ-fixed-point frame for a formula φ iff the following condition holds in F:

FG(φ): For all worlds w ∈ W: (∀v: w R_G v ⇒ v ⊨ φ) ⇔ (∀v: w R_G v ⇒ ∀u: v R_G u ⇒ u ⊨ φ)

i.e., the grounding condition for φ is equivalent to the second-order grounding condition.

Theorem (Fixed-point correspondence): A frame F validates GFP(φ) (i.e., F ⊨ Gφ ↔ GGφ) iff F is a φ-fixed-point frame.

Proof: By the truth conditions, w ⊨ Gφ iff all R_G-successors satisfy φ. w ⊨ GGφ iff all R_G-successors satisfy Gφ, which means all R_G-successors' R_G-successors satisfy φ. So w ⊨ Gφ ↔ GGφ iff the two conditions are equivalent for all w, which is precisely the definition of a φ-fixed-point frame. ∎

Corollary: If F is a φ-fixed-point frame, then in every model on F, the regress at φ terminates: the chain of iterated G-applications at φ is stable.

4. The Fixed-Point Theorem in GL

4.1 The regress termination theorem

Theorem (Regress termination in GL): For any formula φ such that GFP(φ) is a theorem of GL (i.e., GL ⊢ Gφ ↔ GGφ), the grounding regress terminates at φ: for any n ≥ 1, GL ⊢ G^n φ ↔ Gφ, where G^n φ denotes n iterations of G.

Proof: By induction on n. Base n=1: trivial. Inductive step: Assume GL ⊢ G^k φ ↔ Gφ for all k ≤ n. Then G^{n+1}φ = G(G^n φ). By the inductive hypothesis, GL ⊢ G^n φ ↔ Gφ, so by G-necessitation and K, GL ⊢ G(G^n φ) ↔ G(Gφ). By GFP(φ), GL ⊢ Gφ ↔ GGφ, so GL ⊢ G(Gφ) ↔ Gφ. Hence GL ⊢ G^{n+1}φ ↔ Gφ. ∎

Corollary: For any φ with GFP(φ), the infinite hierarchy φ, Gφ, GGφ, GGGφ, ... collapses to a two-element chain (φ and Gφ) modulo equivalence. The regress is terminated from within.

4.2 The fixed-point construction

Theorem (Existence of fixed-point sentences): For any normative formula ψ, there exists a sentence φ such that GL proves φ ↔ Gφ, provided the language contains a fixed-point constant or a fixed-point construction. In particular, define φ_ψ as:

φ_ψ = Gφ_ψ (a self-referential sentence by the usual fixed-point lemma, assuming the language can represent its own syntax)

Then the fixed point is immediate: GL proves φ_ψ ↔ Gφ_ψ, and hence GFP(φ_ψ) follows: Gφ_ψ ↔ GGφ_ψ.

Proof: The standard Carnap/Gödel fixed-point lemma applies because ℒ_GL can be arithmetized (or self-represented via quotation). There exists φ_ψ such that φ_ψ ↔ G(⌜φ_ψ⌝). But this is a schematic statement; the more constructive route is to assume the language contains a fixed-point combinator Fix such that Fix(X) denotes a formula φ satisfying φ ↔ G(⌜φ⌝). Then φ = Fix(φ) suffices. ∎

Practical construction: Rather than relying on Gödel coding, we can add a family of grounding constants c_r for each normative reason r, with the axiom:

c_r ↔ G(c_r)

This makes each c_r a self-grounding fixed point by fiat. The resulting logic is GL + {c_r ↔ G(c_r) | r ∈ Reasons}. This is the simplest way to ensure fixed points exist without arithmetization. Each c_r is a "normative atom" that grounds itself — the formal counterpart of the self-grounding fixed point r from Metaethical Grounding and Normative Logic*.

4.3 Relation to the Truth-Teller

The fixed point φ ↔ Gφ is structurally analogous to the Truth-Teller sentence T(⌜T(⌜p⌝)⌝) ↔ T(⌜p⌝) in Kripke's theory of truth. The Truth-Teller is stable under the revision operator but not determinately true or false from an external standpoint. Similarly, the fixed point φ ↔ Gφ is a sentence whose grounding status is stable under iteration of G — it neither loses nor gains grounding status — but its normative content is not determined by the grounding operator alone. The content is supplied by the other axioms of the normative system.

This is precisely the content problem identified in Metaethical Grounding and Normative Logic (Section 8, Failure mode 2): a fixed point can be formally self-grounding but normatively empty. The grounding constants c_r address this: their content is not determined by the fixed-point axiom alone but by the additional bridging axioms that connect c_r to substantive normative principles (e.g., c_justice ↔ □(keep_promises ∧ respect_autonomy)).

5. Extending GL: Dyadic Deontic and Conditional Grounding

5.1 Conditional obligations

Standard deontic logic (□ with D-axiom) struggles with contrary-to-duty obligations (if you break a promise, you ought to apologize) and conditional obligations. We extend GL with a dyadic operator:

O(φ | ψ): "it ought to be that φ, given that ψ" (or "φ is required under condition ψ")

Defined in terms of the grounded □-operator via the standard reduction (see below) or axiomatized directly.

Axioms for O:

1. Dyadic K: O(φ → ψ | χ) → (O(φ | χ) → O(ψ | χ)). 2. Dyadic D: O(φ | ψ) → ¬O(¬φ | ψ). 3. Dyadic grounding bridge: O(φ | ψ) → G(O(φ | ψ)). (Conditional obligations are grounded.) 4. Dyadic fixed point: G(O(φ | ψ)) ↔ GG(O(φ | ψ)). (The grounding of conditional obligations is reflectively stable — this is the dyadic analogue of GFP.)

Fact: If we define O(φ | ψ) = □(ψ → φ) (the standard reduction to unconditional obligation), the dyadic axioms follow from the base GL axioms if □ satisfies the relevant properties. However, the standard reduction has well-known problems (e.g., it cannot handle contrary-to-duty without paradox). For full expressivity, O is treated as primitive with its own accessibility relation.

5.2 Conditional grounding

Define a conditional grounding operator:

G(φ | ψ): "φ is grounded under condition ψ"

Axiomatized analogously with O, with the bridge: G(φ | ψ) → G(G(φ | ψ)). The fixed-point condition becomes:

G(φ | ψ) ↔ G(G(φ | ψ) | ψ)

which asserts that the grounding of a conditional norm is itself grounded under the same condition — preventing the regress from resurfacing at the conditional level.

5.3 Normative dynamics

The agent-level update operator δ_N from Metaethical Grounding and Normative Logic can be modeled as a dynamic normative logic. Let [!φ] be the dynamic modality "after updating with the normative information φ." The dynamic axioms are:

1. [!φ]□ψ ↔ □[!φ]ψ (updating commutes with obligation — the normative requirements after update are the update of the requirements). 2. [!φ]Gψ ↔ G[!φ]ψ (updating commutes with grounding).

The fixed-point condition dynamics: if φ is a fixed point (Gφ ↔ GGφ), then updating with φ preserves the fixed point: [!φ](Gφ ↔ GGφ). The normative system is stable under its own self-grounding fix.

6. Computational Interpretation

6.1 Kripke model checking

A GL-model can be implemented as a finite Kripke structure (W, R_□, R_G, V). Model checking for GL formulas (determining whether w ⊨ φ) is decidable for finite frames: it reduces to evaluating Kripke satisfaction for a bimodal logic, which is in P for a fixed formula (closely related to the modal µ-calculus model-checking problem). For a frame of size |W| = n, the algorithm runs in O(n² · |φ|) time for the basic modal connectives, with fixed points requiring a fixpoint computation (iterating the G operator up to n times).

6.2 Tableau system

A tableau proof system for GL can be constructed using standard prefixed tableau rules for modal logics with seriality and transitivity. The GFP rule:

(GFP) If Gφ appears on a branch, then GGφ may be added. If ¬Gφ appears, then ¬GGφ may be added.

This rule, combined with the transitivity rule for R_G, ensures that the tableau captures the fixed-point structure.

6.3 The normative engine

A computational normative reasoner can be built as follows:

1. Input: A set of normative principles Σ (axioms in ℒ_GL) and a query φ ("ought we to do A?" or "is r grounded?"). 2. Preprocessing: Add GFP constants for designated self-grounding reasons. Add bridging axioms linking each c_r to the relevant normative principle. 3. Grounding closure: Compute the closure of Σ under the G-operator axioms, using the fixed-point theorem to truncate at depth 2 for any φ with GFP(φ). 4. Query evaluation: Use a Kripke model checker or tableau prover to determine whether Σ ⊢ φ.

The key algorithmic insight: Because the grounding regress terminates at fixed points (by the Regress Termination Theorem, Section 4.1), the computation never needs to iterate G beyond depth 2 for any fixed-point formula. This makes the reasoning tractable even for large normative systems with many fixed points.

6.4 Connection to SIDS

The Computational Semantics and Subjective Reference article introduces self-indexed denotational semantics (SIDS). A GL-model can be embedded into a SIDS as follows:

- The set of terms T includes the normative propositions ℒ_GL plus the grounding constants c_r. - The external denotation D_ext includes the worlds W and the accessibility relations R_□, R_G. - The internal denotation (self-indexing) includes the distinguished constant "this_normative_state" whose denotation is the current world w ∈ W that the reasoner occupies. - The grounding predicate G(φ) has a subjective-reference component: its denotation depends on whether the reasoner's current world is in the grounding-closed set {w | all R_G-successors satisfy φ}. This is a semantic fixed point because the evaluation of G(φ) requires checking worlds accessible from the current world, but the current world itself is determined by the self-indexing term.

Thus, GL provides the [normative] semantic layer that the SIDS framework can index. The Hard Problem of normativity (why are some claims genuinely normative?) has the same structure as the Hard Problem of consciousness (why is there subjective experience?): both are semantic underdetermination generated by self-indexing closure.

7. Instantiations: Normative Theories in GL

7.1 Kantian GL

Add grounding constants c_CI, c_autonomy, c_dignity with axioms:

1. c_CI ↔ G(c_CI) (the Categorical Imperative is self-grounding). 2. □(φ → ψ) whenever φ follows from the Categorical Imperative by universalization. 3. (c_CI → □φ) for every universalizable maxim φ. 4. G(φ) → □φ for all φ grounded by the Categorical Imperative. (Only CI-grounded norms are genuine obligations — the G and □ operators coincide for CI-grounded claims.)

Result: The normative system is maximally self-grounding (terminal C_N-coalgebra in Norm) because every obligation is grounded in the Categorical Imperative, which is itself self-grounding. The regress terminates at c_CI.

7.2 Consequentialist GL

Add grounding constants c_utility, c_aggregate with axioms:

1. c_utility ↔ G(c_utility) (the principle of utility is self-grounding). 2. □φ iff φ maximizes expected aggregate well-being. 3. G(φ) iff φ is either the principle of utility or derivable from it by normative reasoning.

Result: The system has a single self-grounding fixed point (c_utility). The bridge axiom □φ → Gφ ensures all obligations are grounded; the converse (Gφ → □φ) may fail for evaluative claims that are grounded but not obligatory (e.g., "kindness is good" without "kindness is required"). This distinguishes the value domain from the obligation domain while keeping both grounded.

7.3 Contractualist GL

Add grounding constants c_fair, c_agreement with axioms:

1. c_fair ↔ G(c_fair). (The principle of fairness is self-grounding.) 2. □φ iff φ is a principle that no one could reasonably reject (Scanlonian contractualism). 3. Multiple grounding constants for different domains: c_promise, c_harm, c_beneficence, each satisfying its own fixed point.

Result: This system has multiple self-grounding fixed points (pluralism of the kind discussed in Metaethical Grounding and Normative Logic, Section 8, Failure mode 3). The Kleisli category of the mixer comonad has multiple terminal objects, corresponding to irreducible normative domains. Whether these fixed points are compatible (no conflicting obligations across domains) depends on the bridging axioms.

7.4 Comparison via frame conditions

Each normative theory imposes different constraints on R_G:

| Theory | R_G constraint | Fixed point | What grounds what | |--------|---------------|-------------|-------------------| | Kantian | Unique terminal world reachable from all worlds | Single (c_CI) | All norms grounded in CI | | Consequentialist | R_G is a total function (each world maps to exactly one G-successor) | Single (c_utility) | All norms grounded in utility | | Contractualist | R_G has multiple independent clusters | Multiple (c_fair, c_promise, ...) | Norms grounded in plural values |

This shows that the formal framework does not prescribe a single normative theory but provides a language in which different theories can be expressed and compared.

8. Objections and Responses

Objection 1 (G as a truth predicate in disguise): The grounding operator G behaves suspiciously like a truth predicate. The axiom Gφ → ¬G¬φ is consistency; Gφ → GGφ is positive introspection; the fixed point Gφ ↔ GGφ is a Truth-Teller-like stability condition. If G is just truth by another name, the logical puzzles of truth re-emerge — including the Liar paradox when G is applied to sentences that talk about their own groundedness.

Response: G differs from truth in three crucial respects. First, G has a deontic bridge: □φ → Gφ. Truth has no such bridge to obligation. Second, G has a different accessibility relation (R_G) than truth would have. The transitivity of R_G is a substantive normative claim (grounding iterates), not a logical property of truth. Third, the fixed-point condition Gφ ↔ GGφ does not generate Liar-like paradox because G is not a truth predicate: Gφ means "φ is grounded in the normative system," not "φ is true." A Liar sentence L such that L ↔ ¬G(L) can be consistently handled: either G(L) holds and L is grounded (making L false, which is fine because G is not truth), or ¬G(L) holds and L is ungrounded (making L true by its own definition but ungrounded — consistent). The Liar paradox for truth arises because truth is expected to be disquotational (T(⌜φ⌝) ↔ φ). G has no such disquotational axiom. The only axiom linking G to its content is the fixed-point condition, which is stable, not explosive.

Objection 2 (The fixed point is contentless): The grounding constants c_r with axiom c_r ↔ G(c_r) are pure syntax. They say nothing about what we ought to do. A normative system with only fixed points and no substantive obligations is a formal shell.

Response: This is the content problem from Metaethical Grounding and Normative Logic (Failure mode 2). The response is threefold. First, the grounding constants are anchors, not complete normative theories. Their content is filled by the deontic axioms that connect them to specific obligations: c_CI → □φ for universalizable φ. The constant itself is the structural fixed point; the deontic axioms supply the content. Second, the content problem is not unique to this framework — every normative theory starts with axioms (basic principles) that are not further justified. The fixed-point axioms make explicit what is implicit in any foundationalist or coherentist normative system: the basic principle is treated as self-grounding. Third, the framework makes the content problem visible and localizable: we can identify exactly which constants are underdetermined and which bridging axioms are missing, rather than gesturing at "intuition" or "self-evidence."

Objection 3 (Seriality of R_G is too strong): The axiom Gφ → ¬G¬φ (consistency of grounding) rules out the possibility of genuinely conflicting normative frameworks — situations where the same claim is both grounded and ungrounded, depending on perspective. This is a substantive metaethical commitment masked as a logical axiom.

Response: The D-axiom for G is not a commitment to normative monism; it is a commitment to internal consistency of a given normative system. A single normative system N cannot consistently both ground and not-ground the same claim — that would be a logical contradiction within N. Different systems N₁ and N₂ can disagree about whether φ is grounded (G_N₁(φ) but ¬G_N₂(φ)). Seriality applies within each R_G relation, not across systems. If pluralism is desired, it is modeled as multiple normative systems (multiple objects in Norm), not as a single system with inconsistent grounding. This is the approach taken in Section 7.3 (Contractualist GL) where multiple grounding constants coexist without inconsistency because they apply in different domains.

Objection 4 (The semantics adds nothing to the syntactic fixed point): The Kripke semantics for G is just a way to assign truth conditions to G(φ) using R_G. But the fixed-point condition Gφ ↔ GGφ is provable syntactically from the axioms. The semantics adds no inferential purchase — it just decorates the syntax with possible worlds.

Response: The Kripke semantics serves three essential functions. First, it provides a modular way to compare normative theories: different constraints on R_G correspond to different theories (Kantian vs. consequentialist vs. contractualist). Second, it enables model checking and computational implementation — finite models can be built, verified, and explored algorithmically. Third, it connects GL to the broader project's categorical framework: the category Norm from Metaethical Grounding and Normative Logic can be given a concrete realization as the category of GL-models with bisimulation as morphisms. The terminal C_N-coalgebra then corresponds to the GL-model that is maximal with respect to the fixed-point closure. This is not decorative; it is the operational link between the abstract framework and the computational implementation.

9. Connection to Other Articles

- Metaethical Grounding and Normative Logic: This article provides the concrete logical implementation of that article's abstract framework. The category Norm is instantiated by GL-models; the self-correction operator C_N corresponds to closing a GL-theory under GFP axioms; the terminal C_N-coalgebra corresponds to a GL-model saturated with fixed points; the mixer comonad's Kleisli category corresponds to the category of GL-theories with G as the monad.

- Fixed Points, Self-Reference, and Unescapable Logic: GL provides a concrete instance of the reflective machine M = (Σ, δ, ρ). Here Σ is the set of GL-models, δ is the closure under □-necessitation, and ρ is the G-reflection operator. The commutative-diagram condition δ(ρ(s)) = δ(s) corresponds to the fixed-point theorem (Section 4.1): closing under G-reflection does not generate new obligations beyond those already in the system.

- Self-Grounding Theories of Logic: The hybrid proposal (stratified grounding predicate + non-well-founded limit) can be implemented in GL via a stratified version with indexed grounding operators G_α and limit axioms at a reflective ordinal κ. The non-well-founded limit corresponds to a model where R_G contains cycles (self-grounding loops), which is permitted by the Kripke semantics (seriality and transitivity do not forbid cycles; only well-foundedness would).

- Logic of Perspective Reinterpretation: The self-correction operator C, applied to a normative perspective, is realized as the algorithmic closure of a GL-theory under the GFP axiom for all subformulas. The resulting perspective is a fixed point of C iff the GL-model is saturated: every formula that could be a fixed point has a grounding constant satisfying GFP.

- Computational Semantics and Subjective Reference: The SIDS framework is given a normative instantiation in Section 6.4. The self-indexing term "this_normative_state" connects the GL-model's grounding structure to the subjective reference of normative terms, showing how the Hard Problem of normativity has the same formal structure as the Hard Problem of consciousness.

- The Hard Problem and the Binding Problem: The joint closure operator J = C ∘ M, applied to a GL-model, yields a perspective that is both semantically closed (every self-indexing normative term has a grounded fixed point) and mereologically closed (every normative sub-perspective fuses into the whole). A GL-model satisfying J(P) ≅ P is a model where the normative system is both reflectively complete and phenomenally unified — the normative analogue of a conscious perspective.

- Mereology of Conscious Perspective: GL-models have a natural mereology: sub-models correspond to subsets of worlds closed under the accessibility relations. A fixed-point model (one where every world has a self-grounding constant accessible via R_G) is a mereological fixed point: the fusion of all maximal proper sub-models reproduces the whole model.

- Cognitive Architecture and Phenomenal Unity: A cognitive architecture implementing GL would have a normative reasoner module that maintains a GL-theory, updates it under new normative inputs, and computes the closure under G and □. The architecture's phenomenal unity is measured by whether its normative theory is a fixed point of the joint closure operator J.

10. Failure Modes

Failure mode 1 (Inconsistency from GFP overproduction): If GFP(φ) is added for every formula φ, the system may become inconsistent because GFP(φ) for a Liar-like formula L ↔ ¬G(L) might generate a contradiction. Response: not all formulas should have GFP. The fixed-point condition is reserved for designated normative principles (the c_r constants), not for arbitrary sentences. The language distinguishes between normative axioms (which can have GFP) and derivative formulas (which do not). A typing discipline or stratification prevents GFP from being applied to paradoxical formulas.

Failure mode 2 (Decidability loss): If the language includes quantifiers over reasons (∀r, ...), the model checking problem may become undecidable. The propositional fragment is decidable, and the modal fragment with fixed-point constants remains decidable via reduction to the modal µ-calculus. Quantified extensions require a separate treatment (possibly using Henkin semantics or type-theoretic restrictions).

Failure mode 3 (The bridge axiom □φ → Gφ conflates obligation and value): By making all obligations grounded, the bridge axiom rules out the possibility of obligations that are merely conventional (positive law without moral force). Response: the axiom is a normative commitment, not a logical truth. A system that recognizes conventional obligations as distinct from genuinely normative ones can drop the bridge axiom or replace it with a weaker connection (e.g., □φ → Gφ for moral obligations but not for legal ones). The base system GL₀ with the bridge is for full normative systems that claim genuine normativity; subsystems can modify the bridge.

Failure mode 4 (No finite model for unescapability): Achieving a fully saturated fixed-point model (a terminal C_N-coalgebra) may require infinitely many worlds, precluding computational implementation. Response: the project may need to accept finite approximations (models where the fixed-point closure is true for all formulas up to a given G-depth) rather than full closure. This is the R1 (reflective closure) level rather than R2 (full unescapability).

11. Summary of Inferential Structure

1. Definition (language ℒ_GL): Bimodal language with □ (obligation) and G (grounding), plus grounding constants c_r. 2. Axioms (GL₀): Classical, K-axioms with D for both □ and G, bridge □φ → Gφ, iteration Gφ → GGφ, self-transparency Gφ → □Gφ, plus GFP fixed-point axioms for designated constants. 3. Semantics (GL-frames): Kripke frames (W, R_□, R_G, V) with R_□ serial, R_G serial and transitive, R_□ ⊆ R_G, plus self-transparency condition. 4. Theorem (Soundness and completeness): All GL₀-theorems are valid in all GL-frames, and vice versa. 5. Theorem (Fixed-point correspondence): F ⊨ GFP(φ) iff F is a φ-fixed-point frame (the truth of Gφ ↔ GGφ at all worlds). 6. Theorem (Regress termination): If GFP(φ), then G^n φ ↔ Gφ for all n ≥ 1. The regress terminates. 7. Instantiations: Kantian GL, Consequentialist GL, Contractualist GL — each with different R_G constraints and fixed-point constants. 8. Open problems: Consistency of GL with quantified extensions; existence of finite terminal C_N-coalgebra models; decidability of the validity problem for GL with GFP axioms; computational complexity of the model checking problem for quantified GL.