dialectica

dialectica is a skill for Codex from plurigrid/asi. It costs 14 tokens per session (962 once invoked), scanned A, original, MIT.

A formal logic method that represents a proof as a game between a proposer and a challenger. It extracts strategies from proofs and describes how those strategies respond to challenges.

In plain words
What is it for?
Use it for studying proof theory, translating logical statements into game-like forms, and reasoning about composed proof strategies.
Why use it?
It gives a structured way to study what a proof must provide and how its parts fit together. The description does not specify a concrete coding or runtime feature.

Skill for Codex

Written for Codex: installed under .codex/.

Good fit Use it for studying proof theory, translating logical statements into game-like forms, and reasoning about composed proof strategies.

Compare 6 skills from other repositories ↓
Install with agentmods
npx agentmods add skills/plurigrid/asi/dialectica
Install

Getting it into your agent

One page per mod, every tool's command on it. A separate URL per tool would split the same page into five that compete with each other.

Any agent
npx skills add plurigrid/asi --skill dialectica
Clone the repo
git clone --depth 1 https://github.com/plurigrid/asi

Made for: Codex.

Wrote this? Show the measurements

A badge with what this costs and how it scanned, read live from this page, so it follows the numbers instead of freezing them. Markdown for a README, HTML for a documentation site or a project page.

agentmods badge for dialectica

README.md
[![agentmods](https://agentmods.dev/badge/skills/plurigrid/asi/dialectica/github.svg)](https://agentmods.dev/skills/plurigrid/asi/dialectica)
Your own site
<a href="https://agentmods.dev/skills/plurigrid/asi/dialectica"><img src="https://agentmods.dev/badge/skills/plurigrid/asi/dialectica/github.svg" alt="Measured on agentmods" height="20"></a>

Or the 80×15 button, for a site that already has a row of RSS and ATOM ones. Only the verdict fits; the numbers stay here.

agentmods 80×15 button for dialectica

Your own site · 80×15
<a href="https://agentmods.dev/skills/plurigrid/asi/dialectica"><img src="https://agentmods.dev/badge/skills/plurigrid/asi/dialectica.svg" alt="Reviewed on agentmods" width="80" height="20"></a>
Per session 14 Skills are progressive disclosure: only the name and description are preloaded; the body loads when the skill is used.
When invoked 962 The whole file, excluding the scripts and references it only reads on demand.
Security scan A 0 findings. A grade says what 26 rules found in the file — not that it is safe.
Origin original No closer match found in the catalogue.
Token cost

What it costs to keep this loaded

Counted locally with the o200k_base tokenizer, which is exact for GPT models; Claude uses its own tokenizer and its counts differ. Treat this as one consistent yardstick across the catalogue rather than a bill. Prices are per million input tokens.

ModelPer sessionOnce invoked
Fable 5.1 $0.00014 $0.00962
Opus 5 $0.00007 $0.00481
Sonnet 5 $0.00003 $0.00192
Haiku 4.5 $0.00001 $0.00096

Measured 6d ago against content hash a49fcca89452, method: parsed. Prices are Anthropic first-party input rates as of 2026-09-09, from the pricing page.

Security

Grade A, and why

dialectica scanned grade A with 0 findings against 26 rules in 11 categories — prompt injection, anti-refusal, data exfiltration, privilege escalation, supply chain, agent snooping, system-prompt leakage, SSRF and excessive agency — measured 6d ago.

A static scan of the body, not an audit. Every finding is printed with the line that produced it so you can judge whether it matters here. A mod is markdown that instructs an agent; that is exactly why what it instructs is worth reading.

Nothing flagged

None of the 26 patterns this scan looks for appear in this file: no shell pipes, no recursive deletes, no credential paths, no hidden text, no instruction-override or anti-refusal phrasing, no agent-config snooping. That is not a guarantee, it is the absence of the things that are checkable.

ies/music-topos/.codex/skills/dialectica/SKILL.md · 140 lines

How it starts

The opening of the file, as written. The whole thing — 140 lines — stays where its author put it; the contents beside it link to each section on GitHub.

Dialectica Skill (ERGODIC 0)

Proof-as-game interpretation via Gödel's Dialectica

Trit: 0 (ERGODIC)
Color: #26D826 (Green)
Role: Coordinator/Transporter

Core Concept

Dialectica transforms proofs into games:

A ⊢ B  becomes  ∃x. ∀y. R(x, y)

Where:

  • x = Proponent's move (witness/strategy)
  • y = Opponent's challenge
  • R(x,y) = Winning condition (atomic)

The Dialectica Interpretation

For Logical Connectives

D(A ∧ B) = ∃(x,x').∀(y,y'). D(A)[x,y] ∧ D(B)[x',y']

D(A → B) = ∃f,F. ∀x,y. D(A)[x, F(x,y)] → D(B)[f(x), y]

D(∀z.A) = ∃f. ∀z,y. D(A)[f(z), y]

D(∃z.A) = ∃(z,x). ∀y. D(A)[x, y]

Key Insight: Functions as Strategies

  • f extracts witnesses from proofs
  • F back-propagates challenges
  • Composition = strategy composition

Integration with Glass Bead Game

# World hop via Dialectica
def dialectica_hop(proposition, world_state)
  # Transform proposition to game
  game = {
    proponent_moves: extract_witnesses(proposition),
    opponent_moves: extract_challenges(proposition),
    winning: atomic_condition(proposition)
  }
  
  # Play generates new world
  new_world = play_game(game, world_state)
  
  # GF(3) conservation check
  verify_gf3(world_state, new_world)
end

Attack/Defense Structure

        Proponent (∃)
            ↓ witness x
        Opponent (∀)
            ↓ challenge y
        Proponent
            ↓ response (via f, F)
           ...
        Atomic check R(x,y)

Linear Logic Decomposition

Dialectica splits into multiplicative/additive:

A ⊸ B = (A⊥ ⅋ B)    # Linear implication
A ⊗ B               # Tensor (both needed)
A & B               # With (choice)
A ⊕ B               # Plus (given)
!A                  # Of course (reusable)
?A                  # Why not (garbage)

Chu Construction

Chu(Set, ⊥) ≃ *-autonomous category
Objects: (A⁺, A⁻, ⟨-,-⟩: A⁺ × A⁻ → ⊥)

GF(3) Triads

three-match (-1) ⊗ dialectica (0) ⊗ gay-mcp (+1) = 0 ✓
proofgeneral-narya (-1) ⊗ dialectica (0) ⊗ rubato-composer (+1) = 0 ✓
clj-kondo-3color (-1) ⊗ dialectica (0) ⊗ cider-clojure (+1) = 0 ✓

Read the full file on GitHub · 140 lines

Changes

What this file has done since we first saw it

Hashed on every crawl. A supply-chain change to an agent config is a question of when, not whether, so the history is kept rather than the latest state alone.

  1. 6d ago First seen · 140 lines · 14 tokens per session scan A a49fcca89452

Subscribe to this mod's changes

dialectica is a skill published in the GitHub repository plurigrid/asi (62 stars, last pushed 2mo ago), licensed MIT. It adds 14 tokens to every session and 962 once invoked, about $0.0001 per session on Opus 5. A static security scan graded it A with 0 findings. No closer match exists in the catalogue, so it is treated as the original; first seen 2026-09-03.

Related

Other skills, from other repositories

hr-onboarding

A new-hire onboarding plan as a single page — first week schedule, buddy + manager intro, learning track, equipment checklist, and "you're set when…" outcomes. Use when the brief mentions "onboarding", "new hire", "first week plan", or "入职".

nexu-io/open-design · 62 tokens

book-mirror

Take any book (EPUB/PDF), produce a personalized chapter-by-chapter analysis. Each chapter is preserved in detail (The Chapter) and mirrored back to the reader's actual life (The Mirror) using brain context. The mirror observes and resonates — a friend pointing out parallels, NOT a consultant rearranging the reader's…

garrytan/gbrain · 138 tokens

miniapp

Build a tiny interactive HTML playground only when someone asks to see, play with, or step through a mechanism.

yc-software/qm · 25 tokens

eli5

Explain research, papers, or technical ideas in plain English with minimal jargon, concrete analogies, and clear takeaways. Use when the user says "ELI5 this", asks for a simple explanation of a paper or research result, wants jargon removed, or asks what something technically dense actually means.

companion-inc/feynman · 63 tokens

deck-course-module

A course or workshop slide template with persistent learning goals, teaching pages, multiple-choice self-tests, and a wrap-up.

nexu-io/html-anything · 25 tokens

master-yinguang

A reference-based assistant for questions about Yinguang and Pure Land Buddhism, a Buddhist tradition focused on faith, ethical living, and practice connected with rebirth in the Pure Land. It can answer in Yinguang’s historical teaching style.

xr843/Master-skill · 274 tokens