Skills DirectorySkills Directory
SkillsLearnSecurityCategoriesDocsBlogPro
Sign InSubmit Skill
Skills Directory

Security-tested agent skills for Claude, coding agents, and AI workflows.

Directory

  • Browse Skills
  • All Skills A–Z
  • Claude Skills
  • Claude Code Skills
  • Agent Skills
  • Categories
  • Authors
  • Submit a Skill

Learn

  • Learn Hub
  • Install Claude Skills
  • Write SKILL.md
  • Skills vs MCP
  • Directories Compared

Security

  • Security
  • Methodology
  • Secure Claude Skills
  • Security Badges
  • Chrome Extension
  • Skill Manager

Company

  • About
  • Community
  • Blog
  • API Docs
  • Advertise

2026 Skills Directory. All rights reserved.

ProTermsPrivacyRefunds
Back to skills

Modal Logic

ASecurity

Extending propositional and predicate logic with modal operators -- necessity and possibility, and their relatives (obligation, knowledge, belief, time). Covers Kripke possible-worlds semantics, accessibility relations, the main modal systems (K, T, S4, S5), translation from natural language, and applications in epistemic, deontic, and temporal reasoning. Use when ordinary logic is insufficient to capture distinctions like "must" vs "might," "knows" vs "believes," "always" vs "sometimes."

69 stars
0 votes
0 copies
0 views
Added 5/30/2026
ai-agentsgo

Security Analysis

A100/100

Scanned 5/30/2026

$npx -y skills add Tibsfox/gsd-skill-creator --skill modal-logic --agent claude-code

Installs into .claude/skills of the current project.

Are you the author of Modal Logic?

Add the live security badge to your README — it updates automatically with every re-scan.

Security grade badge for Modal Logic
[![Security: A — Skills Directory](https://www.skillsdirectory.com/api/skills/tibsfox-modal-logic/badge)](https://www.skillsdirectory.com/skills/tibsfox-modal-logic)

More formats (shields.io, HTML) on the badges page. Keep it an A: scan every change in CI with Pro.

Download with Pro
Files
SKILL.md
---
name: modal-logic
description: Extending propositional and predicate logic with modal operators -- necessity and possibility, and their relatives (obligation, knowledge, belief, time). Covers Kripke possible-worlds semantics, accessibility relations, the main modal systems (K, T, S4, S5), translation from natural language, and applications in epistemic, deontic, and temporal reasoning. Use when ordinary logic is insufficient to capture distinctions like "must" vs "might," "knows" vs "believes," "always" vs "sometimes."
type: skill
category: logic
status: stable
origin: tibsfox
modified: false
first_seen: 2026-04-12
first_path: examples/skills/logic/modal-logic/SKILL.md
superseded_by: null
---
# Modal Logic

Modal logic extends standard logic with operators for modes of truth -- most centrally necessity (□, "box") and possibility (◇, "diamond"). "It is possible that it will rain" is not the same claim as "it will rain," and ordinary propositional logic cannot distinguish them. Modal logic can. The framework also generalizes: the same machinery handles obligation and permission (deontic logic), knowledge and belief (epistemic logic), past and future (temporal logic), and provability (provability logic). The common semantic foundation is Saul Kripke's possible-worlds model. This skill covers the syntax, semantics, proof theory, and applications of modal logic at the level of an upper-undergraduate or early-graduate logic course.

**Agent affinity:** frege (foundational framing), quine (resistance and critique), tarski (semantic discipline)

**Concept IDs:** log-propositional-logic, log-predicate-logic, log-proof-techniques, log-logic-in-law

## The Modal Operators

The basic modal operators are:

- **□φ** -- "It is necessary that φ" (necessarily φ)
- **◇φ** -- "It is possible that φ" (possibly φ)

They are interdefinable:

- ◇φ ≡ ¬□¬φ -- "possibly φ" means "not necessarily not φ"
- □φ ≡ ¬◇¬φ -- "necessarily φ" means "not possibly not φ"

These duality relations are the modal counterparts of the quantifier dualities in predicate logic, and in Kripke semantics they will turn out to be exactly that.

## Possible Worlds: Kripke Semantics

Saul Kripke's 1959 paper "A Completeness Theorem in Modal Logic" gave the semantic foundation that made modal logic rigorous. The idea:

A **Kripke frame** is a pair ⟨W, R⟩:

- W is a nonempty set of **possible worlds**
- R ⊆ W × W is an **accessibility relation** between worlds

A **Kripke model** adds a valuation V that assigns a truth value to each atomic proposition at each world.

Truth at a world w in a model:

- Atomic p is true at w iff V(w, p) = T
- ¬φ is true at w iff φ is not true at w
- φ ∧ ψ (and other connectives) work as in propositional logic, evaluated locally at w
- **□φ is true at w iff φ is true at every world v such that wRv**
- **◇φ is true at w iff φ is true at some world v such that wRv**

So □ quantifies universally and ◇ quantifies existentially over *accessible* worlds.

**The intuition.** A "possible world" is a complete alternative way things might be. The actual world is one such alternative. The accessibility relation encodes which alternatives are "live" from a given standpoint. Different modal notions (necessity, obligation, knowledge, time) correspond to different accessibility relations.

## The Main Modal Systems

Different modal logics result from different constraints on the accessibility relation R. Each extra constraint validates additional axioms.

### System K

The minimal normal modal logic. Axioms:

- All propositional tautologies
- **K axiom**: □(φ → ψ) → (□φ → □ψ) (necessitation distributes over implication)
- **Necessitation rule**: from ⊢ φ, infer ⊢ □φ

K imposes no constraints on R. It is sound and complete for the class of all Kripke frames.

### System T (Reflexivity)

Add **T axiom**: □φ → φ. "Whatever is necessary is actually true."

Valid iff R is **reflexive**: every world accesses itself.

### System S4 (Reflexive + Transitive)

T plus **4 axiom**: □φ → □□φ. "What is necessary is necessarily necessary."

Valid iff R is reflexive and **transitive**: if wRv and vRu, then wRu.

### System S5 (Equivalence Relation)

S4 plus **5 axiom**: ◇φ → □◇φ. "What is possible is necessarily possible."

Valid iff R is an **equivalence relation**: reflexive, symmetric, and transitive.

S5 is the strongest commonly studied modal system. In S5, the accessibility structure collapses -- every world accesses every other world in its equivalence class. This matches our intuition about logical (or metaphysical) necessity: something is necessary if it holds in every possible world, period, without the filtering that weaker accessibility relations provide.

## Translation from Natural Language

Translating English modal sentences requires care.

### Necessity and possibility

"It is necessary that it is raining" → □R.

"It is possible that it is raining" → ◇R.

### Ambiguous scope

"A bachelor is necessarily unmarried." Two readings:

- **De dicto** (about the sentence): □∀x (Bachelor(x) → Unmarried(x)) -- "necessarily, all bachelors are unmarried"
- **De re** (about the thing): ∀x (Bachelor(x) → □Unmarried(x)) -- "for every bachelor, he is necessarily unmarried"

These are not equivalent. De dicto says the sentence is necessarily true; de re says each bachelor has a necessary property. The de re reading is much stronger and more contentious.

### "Must" is ambiguous

"It must be raining" can be epistemic (I conclude from the wet ground) or deontic (it is obligatory that it rain -- strange in English but possible in other contexts). Modal logics distinguish these with different operators.

## Epistemic Logic

In epistemic logic, the modal operator is interpreted as knowledge:

- **Kᵢφ** -- "Agent i knows that φ"

The accessibility relation connects worlds that are epistemically indistinguishable for agent i. If w and v are indistinguishable to agent i from w's standpoint, then agent i cannot rule out v as the actual world, so Kᵢφ requires φ to hold in both.

### Standard axioms

- **K**: Kᵢ(φ → ψ) → (Kᵢφ → Kᵢψ). Logical omniscience: agents know all logical consequences of what they know. (This is an idealization.)
- **T**: Kᵢφ → φ. Knowledge implies truth. Agents cannot "know" falsehoods.
- **4**: Kᵢφ → KᵢKᵢφ. Positive introspection: if you know something, you know that you know it.
- **5**: ¬Kᵢφ → Kᵢ¬Kᵢφ. Negative introspection: if you don't know something, you know that you don't.

Systems vary on which introspection axioms to accept. Most uncontroversial is T.

### Distinguishing knowledge and belief

Belief is sometimes formalized with a separate operator **Bᵢφ** that satisfies K and 4 but not T -- you can believe falsehoods.

## Deontic Logic

In deontic logic, the modal operator represents obligation:

- **Oφ** -- "It ought to be the case that φ"
- **Pφ** -- "It is permitted that φ"
- **Fφ** -- "It is forbidden that φ" = O¬φ

### Standard axioms

- **K**: O(φ → ψ) → (Oφ → Oψ)
- **D**: Oφ → ¬O¬φ. "Ought implies consistency" -- you cannot be obligated to do contradictory things. (Though real moral systems sometimes produce genuine dilemmas, which is one reason deontic logic is philosophically contested.)

The T axiom (Oφ → φ) is NOT adopted in deontic logic -- what ought to be is not always the case.

## Temporal Logic

Temporal logic replaces necessity and possibility with operators about time:

- **Gφ** -- "Always in the future, φ"
- **Fφ** -- "Sometime in the future, φ"
- **Hφ** -- "Always in the past, φ"
- **Pφ** -- "Sometime in the past, φ"

The accessibility relation is an earlier-later ordering. Different temporal logics model linear vs branching time, discrete vs continuous, etc. Temporal logic is critical in verification of concurrent systems (LTL, CTL, CTL*).

## Philosophical Issues

### Quine's skepticism

W. V. O. Quine was a famous skeptic of modal logic, especially quantified modal logic (QML). His central worry was about de re modality: quantifying into modal contexts raises questions about whether modal properties attach to objects themselves or only to descriptions. "The number of planets is necessarily greater than 7" -- what is the "number of planets" as a referent, independent of the actual astronomical fact?

This debate drove a great deal of 20th-century philosophical logic and is why the logic department's Quine agent carries a skeptical stance as a matter of role.

### Kripke's response

Kripke argued that de re modality was coherent and that rigid designators (terms that refer to the same object in every possible world) resolved Quine's puzzles. Kripke's *Naming and Necessity* (1980) is the landmark text.

### The necessity of origin

Kripke also argued for striking metaphysical claims like "a human being could not have had different parents" (necessity of origin). These claims are modal metaphysics, not modal logic per se, but they motivate much of the field.

## Worked Example: A Modal Proof

**Claim:** In system K, the formula □φ ∧ □ψ → □(φ ∧ ψ) is valid.

**Proof sketch:** Suppose □φ and □ψ are true at world w. By the semantics, φ is true at every world v with wRv, and ψ is true at every world v with wRv. Therefore at every such v, both φ and ψ are true, so φ ∧ ψ is true at v. Since this holds for every accessible v, □(φ ∧ ψ) is true at w.

This is a typical modal-semantic argument: chase the semantics across worlds.

## When NOT to Use This Skill

- **Arguments with no modal content.** Use `propositional-logic` or `predicate-logic`.
- **Arguments that are actually about informal persuasion.** Use `informal-fallacies` or `critical-argumentation`.
- **Mathematical proofs that happen to mention "necessarily."** Use `mathematical-proof-logic` -- "necessarily" in math usually means "in every model," which is first-order.

## Decision Guidance

When you encounter an argument involving modality:

1. **Identify the modal operators.** Is the key word "must," "could," "ought," "knows," "sometime"?
2. **Choose the system.** Alethic (necessity/possibility)? Epistemic? Deontic? Temporal?
3. **Pick the right strength.** K, T, S4, or S5? The choice depends on what introspection or reflexivity properties are intended.
4. **Check de dicto vs de re.** Where is the quantifier with respect to the modal operator?
5. **Evaluate in a Kripke model.** If you want to show validity, prove it for arbitrary accessibility relations in the system. If you want to show invalidity, construct a countermodel.

## Cross-References

- **frege agent:** Invention of quantifiers, foundational role
- **quine agent:** Skeptical framing, critique of QML
- **tarski agent:** Semantic discipline, model theory
- **propositional-logic skill:** The base system modal logic extends
- **predicate-logic skill:** Combined with modal to give quantified modal logic

## References

- Hughes, G. E., & Cresswell, M. J. (1996). *A New Introduction to Modal Logic*. Routledge.
- Kripke, S. (1959). "A Completeness Theorem in Modal Logic." *Journal of Symbolic Logic* 24(1), 1-14.
- Kripke, S. (1980). *Naming and Necessity*. Harvard University Press.
- Blackburn, P., de Rijke, M., & Venema, Y. (2001). *Modal Logic*. Cambridge University Press.
- Fagin, R., Halpern, J. Y., Moses, Y., & Vardi, M. Y. (2003). *Reasoning About Knowledge*. MIT Press.
- Quine, W. V. O. (1953). "Reference and Modality," in *From a Logical Point of View*. Harvard University Press.

Attribution

TibsfoxTibsfox
View sourceSee grades on GitHubMore from Tibsfox →
SSkills DirectorySkills Directory

Ship a skill? Prove it's safe.

Free 120-pattern security scan, letter grade, and an embeddable README badge.

Submit a skill

Is this your skill, or is something wrong with this listing? Request removal or report an issue. Author removals are honored within 72 hours.

Comments (0)

No comments yet. Be the first to comment!

SSkills DirectorySkills Directory

Ship a skill? Prove it's safe.

Free 120-pattern security scan, letter grade, and an embeddable README badge.

Submit a skill

Related Skills

Caveman

Terse caveman voice: answer first, fluff gone, every technical fact kept. Use for /caveman, "caveman mode", "talk like caveman", "be brief", "less tokens". Stays on until "stop caveman" or "normal mode".

1100021 votes

Hyperplan

Adversarial multi-agent planning skill. Self-orchestrates 5 hostile category members (unspecified-low, unspecified-high, deep, ultrabrain, artistry) via team-mode for ruthless cross-critique debate, distills only the defensible insights, then MANDATORILY hands the distilled insight bundle to the `plan` agent for executable plan formalization. Use when planning needs maximum rigor and surfacing of weak assumptions, blind spots, and over-engineering. Triggers: 'hyperplan', 'hpp', '/hyperplan', ...

698461 votes

Writing Skills

Create and manage Claude Code skills in HASH repository following Anthropic best practices. Use when creating new skills, modifying skill-rules.json, understanding trigger patterns, working with hooks, debugging skill activation, or implementing progressive disclosure. Covers skill structure, YAML frontmatter, trigger types (keywords, intent patterns), UserPromptSubmit hook, and the 500-line rule. Includes validation and debugging with SKILL_DEBUG. Examples include rust-error-stack, cargo-dep...

3931 votes

Mcp Code Execution

Routes multi-tool workflows through MCP servers for large datasets and pipelines. Use when Bash tool overhead is limiting throughput on data-heavy tasks.

3421 votes

catchup

Recovers the conversation and failed tool calls of a previous Codex, Amp, Claude Code, Antigravity, Cline, Copilot CLI, Cursor, DeepSeek Harness, Grok Build, Kimi, OpenCode, Pi Agent, or ZCode session. Use when the user says "catch up", "what did the last session do", "get me up to speed", "I switched agents", asks to recover/summarize a previous session before continuing, or asks to diagnose or report a catchup failure. Do NOT use for the current conversation, git history, or any non-agent log.

741 votes
View all in ai-agents →