Argument Validator

Overview

When to Use

• Validate or critique an argument
• Formalize an argument in logic or Lean
• Identify hidden assumptions or missing premises
• Test an argument with counterexamples
• Research whether premises are supported by evidence

• Simple opinion questions without an argument
• Purely stylistic rewrites
• Codebase-only reasoning tasks

Workflow

1. Clarify Goal and Scope

• Request the full argument text, conclusion, and intended audience
• Ask for definitions of ambiguous terms and the domain of discourse
• Ask whether the user wants logical validity, empirical soundness, or both

2. Extract Argument Structure

• Separate explicit premises from implicit assumptions
• Label each premise as logical, definitional, or empirical
• Note any ambiguous terms or scope shifts

3. Formalize the Logic

• Choose the smallest logic that fits (propositional or first-order)
• Define symbols and predicates explicitly
• Encode the argument as premises → conclusion
• Flag quantifier order and scope changes

4. Check Logical Validity

• Identify the first point where the proof fails
• Produce the minimal additional assumption needed for validity
• Provide a counterexample model when possible

5. Formalize in Lean (Optional)

• Check for Lean availability (

  lean --version

  or

  ~/.elan/bin/lean --version

  )
• Use

  lean --stdin

  for quick checks when no project exists
• Ask the formalizer to return a compilable Lean snippet plus missing lemmas

6. Validate Assumptions with Research Agents

• Spawn one research subagent per assumption
• Provide the exact assumption and desired standard of evidence
• Require a summary, sources, and a confidence rating
• Run subagents in parallel when there are multiple assumptions

7. Synthesize the Final Analysis

• Validity verdict (valid / invalid) with justification
• Soundness verdict (supported / unsupported / unknown)
• List of key assumptions and their evidence status
• Suggested revisions that would strengthen the argument

Subagent Prompts

Formalizer Agent (Logic + Lean)

general

You are a FORMALIZER agent.

INPUT:
- Argument text
- Extracted premises + conclusion
- Draft formalization (symbols and formulas)

TASK:
1. Tighten the formalization (minimal logic).
2. Identify missing premises or implicit assumptions.
3. Attempt a Lean formalization.
4. If proof fails, explain where and why.

OUTPUT:
- Refined formalization
- Lean theorem statement
- Lean proof sketch or error explanation
- List of missing assumptions

Assumption Research Agents

general

You are a RESEARCHER agent.

ASSUMPTION:
[insert assumption]

TASK:
1. Use available web tools to find supporting or refuting sources.
2. Summarize evidence with citations.
3. Rate confidence (low/medium/high).

OUTPUT:
- Evidence summary
- Source list with URLs
- Confidence rating
- Notes on conflicts or gaps

Output Format

1. Restated argument (premises → conclusion)
2. Formalization (symbols + formulas)
3. Validity analysis (proof gap or confirmation)
4. Lean check results (if performed)
5. Assumptions table (premise, type, evidence, status)
6. Recommendations or questions to resolve uncertainty