Phase 5: sort checking and the argument library

CMakeLists.txt

@@ -38,6 +38,7 @@ add_library(theos_core STATIC
     src/core/proof_checker.cpp
     src/core/site.cpp
     src/core/truth_table.cpp
+    src/core/types.cpp
     src/core/validator.cpp
 )
 target_include_directories(theos_core PUBLIC include)

README.md

@@ -79,12 +79,13 @@ See [web/README.md](web/README.md) to build them locally.
 ## CLI Usage
 
 ```sh
-theosc check   examples/aquinas_first_way.theo
-theosc export  examples/resurrection.theo --format mermaid -o resurrection.mmd
-theosc build   examples/resurrection.theo -o resurrection.theos
+theosc check   library/arguments/aquinas_first_way.theo
+theosc check   examples/affirming_the_consequent.theo     # rejected, with a counterexample
+theosc export  library/arguments/resurrection.theo --format mermaid -o resurrection.mmd
+theosc build   library/arguments/resurrection.theo -o resurrection.theos
 theosc inspect resurrection.theos            # decoded argument
 theosc inspect resurrection.theos --chunks   # chunk table and hex view
-theosc site    examples -o site/gallery      # static gallery pages
+theosc site    library/arguments -o site/gallery   # static gallery pages
 ```
 
 Diagnostics go to stderr as `file:line:col: error: message` with the source line underneath;
@@ -102,7 +103,8 @@ theos-engine/
 ├── src/wasm/        # WebAssembly entry point for the playground
 ├── web/             # Playground, gallery styles, site assembly
 ├── docs/spec/       # Language, proof rules and binary format specifications
-├── examples/        # Sample .theo arguments
+├── examples/        # Small teaching examples
+├── library/         # Formalized arguments (the gallery)
 ├── fuzz/            # libFuzzer targets and seed corpora
 └── tests/           # Catch2 unit tests and golden files
 ```

ROADMAP.md

@@ -263,3 +263,4 @@ Answers to the original open questions (2026-10-24) and decisions made while bui
 | 2 Binary v2 | done — formulas, proofs and objections are serialized here (M3.4 folded in, since the AST already carries them); padding must be zero so every single-byte corruption is detected (verified by flipping every byte); nesting depth is capped in parser (256) and decoder (512) |
 | 3 Propositional logic | done — the natural-deduction checker already implements the full rule set (quantifiers, identity, S5, definitions, property variables) because the substitution machinery is shared and the Aquinas example needs first-order proofs to pass; formulas are immutable shared trees rather than hash-consed (structural sharing happens in the binary encoder); 39 exercises plus misuse tests; recursive definitions are rejected so expansion terminates |
 | 4 Web | done — Emscripten 3.1.74 build with wasm exceptions (embind `check` returning JSON); playground with live verdict, graph, glosses keyed to lines, shareable `#src=` links; `theosc site` gallery with Fitch-style proof rendering; Node and Playwright smoke tests; Pages deployment needs Pages enabled ("GitHub Actions" source) in repository settings |
+| 5 First-order logic | done — sort checker (docs/spec/language.md §6) infers one type per free name across nodes, proofs, objections and definitions, and runs before proof checking; `library/arguments/` holds the gallery set (Aquinas, kalam, resurrection) and `examples/` holds teaching examples, including one invalid on purpose |

docs/spec/language.md

@@ -237,3 +237,28 @@ Warnings:
 Diagnostics are printed as `file:line:col: error: message`, followed by the
 source line and a caret under the offending token. Syntax errors stop parsing at
 the first error; static-rule errors are all reported.
+
+---
+
+## 6. Sorts
+
+Every name that is not bound by a quantifier or λ has exactly one type across
+the whole file (node formulas, proof lines, objections and definitions):
+
+| Type | How it arises |
+|------|---------------|
+| individual | used only as an argument, or in an identity |
+| proposition | applied to no arguments: `Rain` |
+| predicate | applied to arguments: `Moves(y, x)`; argument sorts are individual or property |
+| property | a one-place predicate over individuals, which may also appear as an argument: `G(x)` and `Positive(G)` |
+
+Bound variables have the sort their binder declares (`ind` by default,
+`prop` for properties). Errors:
+
+- a name used with different arities or argument sorts (`P(a)` and `P(a, b)`);
+- an individual variable applied as a predicate, or a property variable applied to anything but one individual;
+- a predicate of more than one place, or over properties, used as an argument;
+- an identity between properties;
+- a λ abstracting over anything but an individual.
+
+A defined name has the type given by its parameters.

examples/affirming_the_consequent.theo

@@ -0,0 +1,21 @@
+// Deliberately invalid: `theosc check` rejects it and shows a counterexample
+// (Rain = false, Wet = true: the street can be wet without rain).
+
+argument "Affirming the Consequent"
+
+axiom Obs = source("Field notes", "p. 4")
+
+premise P1 grounded_by [Obs] {
+    text:    "If it rains, the street is wet."
+    formula: Rain -> Wet
+}
+
+premise P2 grounded_by [Obs] {
+    text:    "The street is wet."
+    formula: Wet
+}
+
+conclusion C1 from [P1, P2] {
+    text:    "It rains."
+    formula: Rain
+}

examples/modus_ponens.theo

@@ -0,0 +1,20 @@
+// The smallest complete argument: two premises and a single rule.
+
+argument "Modus Ponens"
+
+axiom Obs = source("Field notes", "p. 4")
+
+premise P1 grounded_by [Obs] {
+    text:    "If it rains, the street is wet."
+    formula: Rain -> Wet
+}
+
+premise P2 grounded_by [Obs] {
+    text:    "It rains."
+    formula: Rain
+}
+
+conclusion C1 from [P1, P2] by imp_e {
+    text:    "The street is wet."
+    formula: Wet
+}

include/theos/types.hpp

@@ -0,0 +1,30 @@
+#pragma once
+
+#include "theos/ast.hpp"
+#include <map>
+#include <string>
+#include <vector>
+
+// Sort checking (docs/spec/language.md §6): every free symbol gets one consistent type
+namespace Theos::Types {
+
+// A free symbol is an individual constant, or a predicate over individuals and properties.
+// A property constant is a predicate with one individual argument.
+struct Type {
+    bool predicate = false;
+    std::vector<Sort> args;   // predicate argument sorts
+};
+
+using Signature = std::map<std::string, Type>;
+
+std::string describe(const Type& t);
+
+struct Result {
+    Signature signature;
+    Diagnostics diagnostics;
+};
+
+// Checks every formula in the document: nodes, objections, definitions and proof lines
+Result check(const AST::Document& doc);
+
+} // namespace Theos::Types

library/arguments/kalam.theo

@@ -0,0 +1,68 @@
+// The kalam cosmological argument in its modern form. The step from "has a
+// cause" to "has a transcendent cause" is made explicit as premise P3.
+
+argument "The Kalam Cosmological Argument" by "William Lane Craig, after al-Ghazali"
+
+axiom Ghazali  = source("al-Ghazali, The Incoherence of the Philosophers", "First Discussion")
+axiom Craig    = source("William Lane Craig, The Kalam Cosmological Argument", "Part II")
+axiom ExNihilo = principle("Nothing comes from nothing.")
+axiom Gen1     = scripture(protestant, "Genesis 1:1")
+
+premise P1 grounded_by [ExNihilo] {
+    text:    "Whatever begins to exist has a cause."
+    formula: forall x. Began(x) -> exists y. Causes(y, x)
+}
+
+premise P2 grounded_by [Ghazali, Craig, Gen1] {
+    text:    "The universe began to exist."
+    formula: Began(universe)
+}
+
+deduction D1 from [P1, P2] {
+    text:    "Therefore the universe has a cause."
+    formula: exists y. Causes(y, universe)
+    proof {
+        1. forall x. Began(x) -> exists y. Causes(y, x)          premise P1
+        2. Began(universe)                                        premise P2
+        3. Began(universe) -> exists y. Causes(y, universe)       forall_e 1
+        4. exists y. Causes(y, universe)                          imp_e 3, 2
+    }
+}
+
+premise P3 grounded_by [Craig] {
+    text:    "A cause of all of space and time is itself beyond space and time."
+    formula: forall y. Causes(y, universe) -> Transcendent(y)
+}
+
+conclusion C1 from [D1, P3] {
+    text:    "Therefore the universe has a transcendent cause."
+    formula: exists y. (Causes(y, universe) & Transcendent(y))
+    proof {
+        1. exists y. Causes(y, universe)                          premise D1
+        2. forall y. Causes(y, universe) -> Transcendent(y)       premise P3
+        { [c]
+            3. Causes(c, universe)                                assume
+            4. Causes(c, universe) -> Transcendent(c)             forall_e 2
+            5. Transcendent(c)                                    imp_e 4, 3
+            6. Causes(c, universe) & Transcendent(c)              and_i 3, 5
+            7. exists y. (Causes(y, universe) & Transcendent(y))  exists_i 6
+        }
+        8. exists y. (Causes(y, universe) & Transcendent(y))      exists_e 1, 3-7
+    }
+}
+
+objection O1 against P1 {
+    text: "Quantum events, such as radioactive decay, seem to begin without a cause."
+}
+
+reply R1 to O1 {
+    text: "Quantum events arise within a vacuum governed by physical law, which is not nothing; P1 concerns coming into being from nothing."
+}
+
+objection O2 against P2 {
+    text: "The universe might have an infinite past, so it never began."
+}
+
+reply R2 to O2 {
+    text: "A series of past events formed by successive addition cannot be actually infinite, since an infinite cannot be traversed one step at a time."
+}

src/core/driver.cpp

@@ -1,5 +1,6 @@
 #include "theos/driver.hpp"
 #include "theos/checker.hpp"
+#include "theos/types.hpp"
 #include "theos/parser.hpp"
 #include "theos/validator.hpp"
 #include <fstream>
@@ -19,7 +20,10 @@ Result check_source(std::string text, const std::string& path) {
     result.doc = std::move(*parsed);
     auto diags = Validator::validate(*result.doc);
     result.diagnostics.insert(result.diagnostics.end(), diags.begin(), diags.end());
-    if (has_errors(result.diagnostics)) return result;   // logic checking assumes a well-formed document
+    if (has_errors(result.diagnostics)) return result;   // later stages assume a well-formed document
+    auto types = Types::check(*result.doc).diagnostics;
+    result.diagnostics.insert(result.diagnostics.end(), types.begin(), types.end());
+    if (has_errors(result.diagnostics)) return result;   // logic checking assumes well-sorted formulas
     auto logic = Checker::check(*result.doc);
     result.diagnostics.insert(result.diagnostics.end(), logic.begin(), logic.end());
     return result;

src/core/types.cpp

@@ -0,0 +1,158 @@
+#include "theos/types.hpp"
+#include <optional>
+
+namespace Theos::Types {
+
+std::string describe(const Type& t) {
+    if (!t.predicate) return "an individual";
+    if (t.args.empty()) return "a proposition";
+    if (t.args.size() == 1 && t.args[0] == Sort::Ind) return "a property";
+    std::string out = "a predicate of (";
+    for (size_t i = 0; i < t.args.size(); ++i) out += std::string(i ? ", " : "") + (t.args[i] == Sort::Ind ? "individual" : "property");
+    return out + ")";
+}
+
+namespace {
+
+bool same(const Type& a, const Type& b) { return a.predicate == b.predicate && a.args == b.args; }
+
+const Type property{true, {Sort::Ind}};
+const Type individual{false, {}};
+
+class Checker {
+public:
+    explicit Checker(const AST::Document& doc) : doc_(doc) {}
+
+    Result run() {
+        // Definitions fix the type of the symbol they define
+        for (const auto& d : doc_.definitions) {
+            Type t{true, {}};
+            for (const auto& p : d.params) t.args.push_back(p.sort);
+            declare(d.id, t, d.span);
+        }
+        // Heads first: a symbol applied anywhere is a predicate, which decides how bare uses are read
+        for (const auto* f : formulas()) collect_heads(*f, {});
+        for (const auto& d : doc_.definitions) {
+            Env env;
+            for (const auto& p : d.params) env.push_back({p.name, p.sort});
+            formula(*d.body, env);
+        }
+        for (const auto* f : formulas()) formula(*f, {});
+        return {std::move(sig_), std::move(diags_)};
+    }
+
+private:
+    using Env = std::vector<std::pair<std::string, Sort>>;
+
+    std::vector<const Expr*> formulas() const {
+        std::vector<const Expr*> out;
+        for (const auto& n : doc_.nodes) {
+            out.push_back(n.formula.get());
+            if (n.proof) proof_lines(n.proof->items, out);
+        }
+        for (const auto& d : doc_.dialectics) {
+            if (d.formula) out.push_back(d.formula.get());
+        }
+        return out;
+    }
+
+    static void proof_lines(const std::vector<AST::ProofItem>& items, std::vector<const Expr*>& out) {
+        for (const auto& item : items) {
+            if (const auto* line = std::get_if<AST::ProofLine>(&item)) out.push_back(line->formula.get());
+            else proof_lines(std::get<AST::Subproof>(item).items, out);
+        }
+    }
+
+    static std::optional<Sort> lookup(const Env& env, const std::string& name) {
+        for (auto it = env.rbegin(); it != env.rend(); ++it) {
+            if (it->first == name) return it->second;
+        }
+        return std::nullopt;
+    }
+
+    void error(const Span& span, std::string message) {
+        diags_.push_back({Severity::Error, doc_.file, span, std::move(message)});
+    }
+
+    void declare(const std::string& name, const Type& t, const Span& span) {
+        auto [it, inserted] = sig_.emplace(name, t);
+        if (!inserted && !same(it->second, t)) {
+            error(span, "'" + name + "' is used as " + describe(t) + " here but as " + describe(it->second) + " elsewhere");
+        }
+    }
+
+    void collect_heads(const Expr& e, Env env) {
+        if (e.kind == ExprKind::Atom && !lookup(env, e.name)) heads_.emplace(e.name, e.args.size());
+        if (is_binder(e.kind)) env.push_back({e.name, e.sort});
+        for (const auto& a : e.args) collect_heads(*a, env);
+    }
+
+    // Sort of a term in argument position
+    Sort term(const Expr& t, const Env& env) {
+        if (t.kind == ExprKind::Lambda) {
+            if (t.sort != Sort::Ind) error(t.span, "a lambda must abstract over an individual variable");
+            Env inner = env;
+            inner.push_back({t.name, t.sort});
+            formula(*t.args[0], inner);
+            return Sort::Prop;
+        }
+        if (auto bound = lookup(env, t.name)) return *bound;
+        // A free name that is applied somewhere is a property; otherwise an individual
+        auto head = heads_.find(t.name);
+        auto def = sig_.find(t.name);
+        if ((def != sig_.end() && def->second.predicate) || head != heads_.end()) {
+            const Type expected = def != sig_.end() ? def->second : property;
+            if (!same(expected, property)) {
+                error(t.span, "'" + t.name + "' is " + describe(expected) + " and cannot be used as a term");
+                return Sort::Prop;
+            }
+            declare(t.name, property, t.span);
+            return Sort::Prop;
+        }
+        declare(t.name, individual, t.span);
+        return Sort::Ind;
+    }
+
+    void formula(const Expr& e, Env env) {
+        switch (e.kind) {
+            case ExprKind::Atom: {
+                std::vector<Sort> args;
+                for (const auto& a : e.args) args.push_back(term(*a, env));
+                if (auto bound = lookup(env, e.name)) {
+                    if (*bound != Sort::Prop) error(e.span, "'" + e.name + "' is an individual variable and cannot be applied");
+                    else if (args != std::vector<Sort>{Sort::Ind}) error(e.span, "property variable '" + e.name + "' takes one individual");
+                    return;
+                }
+                declare(e.name, Type{true, args}, e.span);
+                return;
+            }
+            case ExprKind::Eq:
+                for (const auto& a : e.args) {
+                    if (term(*a, env) != Sort::Ind) error(a->span, "identity relates individuals; '" + a->name + "' is a property");
+                }
+                return;
+            case ExprKind::Symbol:
+            case ExprKind::Lambda:
+                error(e.span, "expected a formula, found a term");
+                return;
+            case ExprKind::Forall:
+            case ExprKind::Exists:
+                env.push_back({e.name, e.sort});
+                formula(*e.args[0], env);
+                return;
+            default:
+                for (const auto& a : e.args) formula(*a, env);
+        }
+    }
+
+    const AST::Document& doc_;
+    Signature sig_;
+    std::map<std::string, size_t> heads_;
+    Diagnostics diags_;
+};
+
+} // namespace
+
+Result check(const AST::Document& doc) { return Checker(doc).run(); }
+
+} // namespace Theos::Types

tests/CMakeLists.txt

@@ -13,6 +13,7 @@ add_executable(theos_tests
     test_lexer.cpp
     test_parser.cpp
     test_proofs.cpp
+    test_types.cpp
     test_validator.cpp
 )
 target_link_libraries(theos_tests PRIVATE theos_core theos_warnings Catch2::Catch2WithMain)