# created ```dataview LIST WITHOUT ID file.link FROM -"windsurf" WHERE file.cday = date(this.file.name) AND !startswith(file.folder, "windsurf") SORT file.cday ASC ``` # modified ```dataview LIST WITHOUT ID file.link FROM -"windsurf" WHERE file.mday = date(this.file.name) AND !startswith(file.folder, "windsurf") SORT file.mday ASC ``` --- # [[diary and thoughts]] #thought #diary --- # Notes # How to progress with the paper? #llmtext #brainstorm #paper/generatingphilosophy ## 0. Meta-principles that guide the whole strategy • Separate conceptual research (What do **abduction**, **argument**, **virtue** really mean?)  from technical/engineering research (How do we code, reward and test those things?). • For every proposed step keep two verification channels:  – philosophical literature / domain experts  – empirical check with real LLM behaviour. • Adopt an adversarial stance at each milestone (“How could this be wrong / unworkable?”). • Document findings in a shared notebook; tag each item with “confident / plausible / shaky”. --- ## 1. Clarify the core analogy: Proof ↔ Argument 1.1 Literature scan  • Target papers explicitly comparing **mathematical proofs** and **philosophical arguments**   (Leitgeb 2011; Aberdein 2020; MacFarlane on logical consequence; Toulmin model critiques).  • Check AI-sided analyses of proof ↔ argument (e.g. FOL-to-natural-language mapping work). 1.2 Concept mapping exercise  • List [[structural features]] of a Lean proof (axioms, lemmas, verification, binary correctness).  • List [[structural features]] of a philosophical argument (premises, warrants, defeaters, gradated plausibility).  • Highlight homologies **and** ineliminable disanalogies.  • Decide explicitly whether the project keeps [[the analogy]] “as is”, weakens it, or replaces it with a network-dependency picture (the previous Dellsén-style idea). 1.3 Failure mode probe  • Try to cast a notoriously controversial argument (e.g. Gettier counter-example) into the prover template.  • Record where the template breaks (premise contestation, lack of proof checker, etc.). --- ## 2. Nail down what counts as “argument” and “theory” 2.1 Taxonomy of philosophical text types  • Short deductive argument; abductive explanatory sketch; conceptual analysis; thought experiment; dialectical exchange.  • Test which of these can sensibly be the target output of **PhiloSeeker-v1**. 2.2 Boundary experiments  • Prompt an existing LLM: “Give a three-premise argument for X” versus “Give a theory of X”.  • Evaluate with human raters: does the shorter, more controlled prompt yield higher clarity and evaluability? 2.3 Decision checkpoint  • If argument-only route is chosen, write a one-page spec: token budget, required sections (premise list, inference, objection, reply), style constraints.  • If broader “theory” route remains on the table, log extra costs: larger reward model, harder annotation, weaker verification signals. --- ## 3. Operationalise abduction + [[theoretical virtues]] 3.1 Abduction landscape review  • Read: Harman (1965), Lipton (2004), Schupbach (2020), Williamson (2017), Douven (2017).  • Extract minimal set of features that a *machine-friendly* account must encode ([[explanatory power]], simplicity, predictive novelty). 3.2 Virtue taxonomy refinement  • Start from Keas’s four clusters; cross-check with other lists (Kuhn’s values, McMullin, Schindler).  • For each virtue write: (a) informal definition (b) at least one *proxy metric* (e.g. brevity/scope ratio for simplicity; cross-text entailment consistency for coherence). 3.3 Competing perspectives  • Pragmatist view: virtues are context-relative heuristics, not objective; may undermine metric-building.  • Bayesian view: virtues reduce to likelihoods and priors; could simplify rewards but risks triviality. 3.4 Verification paths  • Small pilot: feed 10 classic journal abstracts into crowdsourced raters → collect virtue ratings → train a quick classifier → see which virtues are learnable.  • If ≥ 60 % inter-rater agreement fails on a virtue, mark it “high-subjectivity”, treat with caution in RL. --- ## 4. Replace Lean checker with a multi-signal “Virtue-Evaluator” 4.1 Signal inventory  • Static rule checks: basic logic validity, contradiction detection (off-the-shelf parsers).  • LLM critic chain: a separate model rates clarity, completeness, relevance.  • Human in the loop: expert panel scores high-level virtues monthly; outputs recalibrate virtue-discriminator.  • Adversarial “objection bot”: tries to refute premises; robustness score becomes a reward component. 4.2 Engineering research to schedule  • Study recent RLHF variants that support *vector* rewards rather than scalar (e.g. ParetoRL, Multi-objective PPO).  • Investigate open-source contradiction detectors (GPT-4o style “self-referee”) and argument mining libraries. 4.3 Pitfall watchlist  • Virtue signals may conflict (simplicity vs. [[explanatory depth]]). Need weighting or Pareto front approach.  • Reward hacking: model learns to game readability metrics without substantive improvement. 4.4 Back-up plan  • If virtue evaluator proves too noisy, fall back to a **two-stage** paper idea:   Stage 1 Model generates *argument blueprints* only, scored mainly on internal coherence (easier).   Stage 2 Separate study tackles full virtue portfolio. --- ## 5. Data: collect, annotate, curate 5.1 Source selection  • Open-access philosophy journals, PhilPapers archive, [[Stanford Encyclopedia]] (SEP), structured debate sites.  • Ensure domain diversity: metaphysics, ethics, epistemology, philosophy of science. 5.2 Annotation guidelines draft  • Label spans: premises, conclusion, argumentative move (analogy, reductio, etc.).  • Virtue tags: coherence flag, simplicity rating (1-5), cited evidence quality (yes/no/weak). 5.3 Automated bootstrapping  • Run argument mining models to pre-segment texts; human annotators correct; yields scalable pipeline. 5.4 Ethical/Legal check  • Verify licences; decide on excerpting vs. full texts; respect journal copyrights. --- ## 6. People, timeline, and resource coordination 6.1 Expert outreach  • Set up short interviews with:   – Michelle (epistemic virtues)  – Takuya Nikawa (methodology / cross-cultural reasoning)   – One logician working with Lean or IsaCoq – One argumentation theorist (informal logic community). 6.2 Milestone sketch (subject to change once above clarifications land)  • T + 2 weeks Core analogy white-paper (Work-streams 1–2).  • T + 1 month Virtue-metric spec + annotated pilot dataset (Work-streams 3–5).  • T + 3 months Prototype virtue evaluator + RL sandbox experiments.  • T + 6 months Draft of “Paper 1: Argument-generating LLM”. 6.3 Tooling  • Version-controlled repo for annotations (GitHub + DVC).  • Shared Zotero library for literature; tag each entry with “analogy / virtues / abduction / proof”. --- ## 7. Final self-audit & reflective reset Before locking in the plan, run one more pass asking: • Have we conflated “makes sense to us” with “likely implementable at scale”? • Are we over-committing to Keas’s taxonomy—should we keep a placeholder for alternative virtue lists? • Is the philosophical community likely to accept automated virtue scoring as *meaningful evidence*?  If not, build a subsection explicitly defending the move. • Could the **previous** Dellsén-style “network of dependencies” approach actually be a better near-term path?  Set aside one afternoon to re-evaluate it against the above work-streams. Only after this reflective checkpoint should you green-light resource allocation and begin detailed literature reviews and coding. --- ### Bottom line Your immediate next actions are: 1. Conduct the proof-argument analogy literature sweep (Work-stream 1.1). 2. Draft a one-page definition of “argument” for PhiloSeeker-v1 and circulate it for quick feedback (Work-stream 2.3). 3. Build a small virtue-rating pilot with 5–10 texts to test inter-rater reliability and metric learnability (Work-stream 3.4). These three steps will reveal whether the rest of the plan rests on solid ground or needs a pivot.