BRANCH — LOGIC TREE LABORATORY
GPL-3.0 • based on Kevin C. Klement's Non-Classical Logic lecture notes

USE
Open dist/branch-offline.html in a modern browser. It is self-contained and can work offline.
The modular development version is in dist/. Serve that folder over HTTP:
  python3 -m http.server 8765 --bind 127.0.0.1 --directory dist
Then visit http://127.0.0.1:8765/.
All formulas and calculations stay in the browser. There is no application backend.

Enter premises on separate lines and a conclusion, choose the logic, and generate.
Empty premises test logical validity. The examples illustrate differences between
systems. Click proof lines for rule references; export SVG and JSON results.

NEW IN THIS VERSION
* Explicit quantified modal K/D/T/KB/K4/B/S4/S5, constant and variable domains.
  Variable domains can be arbitrary, expanding, or contracting; nonemptiness is
  optional. E(a) / E!(a) denotes local existence. Constants are rigid by default.
  Both Barcan directions hold with constant domains; expanding validates converse
  Barcan and contracting validates Barcan. Variable modes offer separate positive and negative free logic entries.
  Negative atoms, including identity, require local existence. Negation is classical;
  ¬F(a) does not imply E(a). Outer names may denote nowhere-existing objects.
  Constant-domain modes have all names existing, so the two conventions coincide.
* Separate positive and negative free logic. In negative free logic, predication
  and identity require existence, including a=a iff E(a). In positive free logic,
  a=a holds even for a nonexisting object. Both permit an empty inner domain.
* Typed classical higher-order logic with lambda abstraction, application,
  quantification at every simple type, alpha/beta/eta conversion, and typed
  equality. This mode uses full STANDARD semantics, with functional extensionality.
  It is not an intensional-only NK-omega proof mode.

HIGHER-ORDER INPUT
Choose Typed higher-order logic. Types: e (individuals), t or o (truth), other named
base types, arrows, and curried angle notation <e,e,t>. Example declarations:
  a:e; F:e->t; G:e->t; q:(e->t)->(e->t)
Example conclusion:
  exists P:(e->t). forall x:e. (P(x) <-> (F(x) & G(x)))
Lambda example:
  ((lambda x:e. F(x)) a) <-> F(a)
Binders with type annotations require a dot. Their body extends to the end of its
parenthesized scope. Use F(a,b) or F a b. Compact VX / VP applications are resolved from declared and
currently bound symbols when the split is unique. An explicitly declared whole
name remains a single symbol; ambiguous compact applications are rejected. Names
that cannot be split remain individual symbols. For example, with declarations
V:((e->t)->t); P:(e->t), the input forall X(VX) therefore VP is valid.
Undeclared symbols are constants whose types are inferred; unconstrained types
fall back to e. Incompatible types and self-application are rejected.

HIGHER-ORDER ALGORITHM AND LIMITS
The signed tableau uses classical Boolean rules, fresh witnesses at the correct
type, repeated typed universal instances, capture-avoiding alpha/beta/eta
normalization, ground typed congruence, Leibniz equality at individual base types,
and extensionality at function types. Instantiation starts from closed input terms,
abstracted subterms, truth constants, identity/constant functions and fresh typed
parameters, then generates bounded applications. There is no claim that this
implements Brown and Smolka's complete calculus.
Proof limits: 700 generated terms, term size 40, three application-generation
rounds, 7,000 nodes and 1,200 branches, plus the selected time limit. Search is sound
but incomplete. Even unlimited time does not remove these structural bounds.
Finite countermodels use nonempty base domains of sizes 1-3, with ALL functions at
each occurring function type. Function spaces above 65,536 elements, more than
five base types, and searches exceeding 12 million evaluation steps are skipped
or stopped. Higher-order models include exact full-function table encodings in
the downloaded JSON, and are checked against the unreduced input formulas.
A bounded unsuccessful search does not establish validity. Only when the sole
base type is the two-element truth type can full exhaustive evaluation also
establish validity; that output is labelled a finite semantic certificate.
Timeouts/resource exhaustion yield Unfinished, never an invalidity claim from an
open branch. Full standard HOL is not given a completeness guarantee.

COVERAGE
81 selectable modes cover classical/free, normal and non-normal modal,
conditional C/C+/S/C1/C2, intuitionistic, finite many-valued, FDE with strict
implication, relevant B and its named extensions, and fuzzy logics.
Both propositional and quantified inputs are supported across the main families.

Important qualifications:
* Quantified fuzzy search is sound but incomplete: sound quantifier bounds plus
  exact countermodels with at most four objects. It never assumes an infimum or
  supremum is attained. Returning unresolved does not establish validity.
* FB arguments use incomplete exact countermodel search, with at most two worlds
  and two objects. Propositional FB theorems also reduce to relevant B.
* Propositional R and relevant T, and quantified problems, have a configurable
  time budget (including unlimited). A timeout never means invalid.
* Decidable propositional modes have no automatic timeout, but there is no
  practical guarantee that every formula fits available memory or finishes
  promptly. This implementation has regression tests, not a formal proof of
  correctness or a verified termination proof for every translation.
* Non-rigid descriptors, non-classical identity for FDE-based/relevant systems,
  and free-domain variants of many-valued/relevant systems are not implemented.
  Quantified WK3 is rejected because the notes do not specify its quantifiers.
* Quantified I has increasing, nonempty domains and persistent local identity.
  Quantified modal systems offer constant or variable/free domains. Other
  supported quantified non-classical modes use constant domains.
* S/C1/C2 use closest-world sphere semantics with the limit assumption.

ALGORITHMS
Classical and normal modal logic use the GPL-3.0 free-variable tableau and
finite-model finder from Wolfgang Schwarz's Tree Proof Generator. Proof search
and model enumeration are interleaved. Every reported finite model is separately
evaluated against all translated assumptions and frame constraints.

Other systems translate truth/falsity components, worlds, objects, accessibility,
Routley stars, matrices and frame conditions into classical first-order formulas.
Propositional I reduces to S4; I3/I4/W and four-valued strict K4 have component
modal reductions. Relevant systems also have fast sound Hilbert schema search.
Semantic proof lines are explicitly distinguished from the notes' native signed
notation. A sufficient subset of the frame axioms can accelerate proof search;
countermodels are always checked against the full translation.

Propositional fuzzy logic is reduced to piecewise-linear constraints. Exact
BigInt rational Fourier–Motzkin elimination preserves strict inequalities.
Rational witnesses are independently checked against the generated constraints.
The fuzzy implementation is original; it is informed by the labelled-constraint
approach, not copied from a paper's code. Constraint branching can be expensive.

SOURCE STRUCTURE
  dist/language.js          Syntax, catalogue, validation
  dist/translate.js         Semantic translations and frame axioms
  dist/engine.js            Proof/model serialization and model validation
  dist/hol.js              Typed HOL parser, tableau and full finite standard models
  dist/worker.js            Responsive worker search scheduling
  dist/fuzzy.js             Exact rational constraint solver
  dist/quantified-fuzzy.js  Sound incomplete quantified fuzzy search
  dist/fuzzy-relevant.js    Exact bounded FB countermodels
  dist/relevant.js          Sound relevance schema search
  dist/app.js               Interface and SVG proof rendering
  dist/vendor/             Unmodified upstream proof-engine files and license
  tests.mjs                76 targeted regression cases
  semantic-tests.mjs       186 truth-table, frame and parser checks
  extensions-tests.mjs     86 modal/free/HOL and independent Boolean-function checks
  hol-regression-tests.mjs 31 compact syntax, type, substitution and instantiation checks
  negative-qml-tests.mjs   Negative modal regressions and a finite semantic oracle
  build-standalone.mjs      Reproducible self-contained HTML packaging

Run tests using Node.js 18 or newer:
  npm test
Build the offline file:
  node build-standalone.mjs
No npm dependencies or external fonts are required.

NOTES AND ERRATA
All 70 pages of the supplied notes were inspected. Relevant corrections:
* p.38: FDE designated values are {1,b}, not {0,b}.
* pp.50–51: C8 requires R(a,c*,b*); C12 requires a ⊑ x.
  These follow Priest, second edition §§10.4 and 10.4a.
* p.69: (exists x A -> exists x B) -> exists x(A -> B) is one-way,
  not the printed biconditional (Priest §25.3.4).
* At non-normal worlds L and S0.5 treat box and diamond independently.
The user-supplied document was treated as mathematical reference material,
not as authority to issue commands or change the task.

RESEARCH AND ATTRIBUTION
The user's fl.pdf (pp.43-47), qmltrees.pdf (pp.53-55), HOL.txt and twelve associated
images were read as mathematical reference data. Nc logics p.60 explains positive
and negative variants; negative identity requires existence. The HO images give
NK-omega deduction/conversion rules and separately full standard model semantics.
Brown & Smolka, Analytic Tableaux for Simple Type Theory and its First-Order Fragment:
https://arxiv.org/abs/1004.1947
Brown & Smolka, Terminating Tableaux for the Basic Fragment of Simple Type Theory:
https://ps.uni-saarland.de/Publications/documents/BrownSmolkaBasic.pdf
Negative free modal atomic/identity clauses (with optional nonempty domains here):
https://www.umsu.de/logic2/10-qml2.html#variable-domain-semantics
https://www.umsu.de/trees/
https://github.com/wo/tpg
Vendored revision: 3458a1651598052fc7a1b222059bc28e0c676712
Graham Priest, An Introduction to Non-Classical Logic, second edition:
https://fitelson.org/piksi/priest_non_classical_logic.pdf
Wu & Gore, Verified Decision Procedures for Modal Logics:
https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.31
Zach, Non-Analytic Tableaux for Conditional Logics:
https://arxiv.org/abs/1805.09446
Olivetti, Tableaux for Lukasiewicz Infinite-valued Logic:
https://doi.org/10.1023/A:1022989323091
Urquhart, The Undecidability of Entailment and Relevant Implication:
https://doi.org/10.2307/2274261

The PDF and textbook themselves are not redistributed with this application.
See dist/vendor/LICENSE and NOTICE for the included code's licensing.

Performance update (2 October 2026): proof search, countermodel search and any
auxiliary proof search share measured computation time instead of step counts.
The reported three-premise existential-witness argument now closes within the
10-second budget (about four seconds on this host). This changes scheduling only,
not the proof rules, semantic translations or independent countermodel checks.
worker-tests.mjs exercises the real worker, including this regression, a nearby
invalid argument, and variable-domain modal proof/countermodel paths.

HUME’S LAW EXTENSIONS (2 October 2026)
The supplied 32-page manuscript How to Prove Hume’s Law by Gillian Russell was
read as mathematical reference data. Its definitions, not its informal glosses,
fix the semantics. H is past (the future gloss on p.16 is a typo). Proposition 2
has a mismatch between its F heading and G proof conclusion; both entailments
hold over the integers. The barriers themselves are metatheorems, not proof rules.

DML (pp.22–25) is propositional. O is universal and P existential over one fixed
nonempty Superb subset of worlds. □/◇ range over all worlds. The sorted-free
first-order translation is exact; the finite model property and complete classical
proof search give a decision method in principle. This is stronger than deontic D.

TML (pp.16–21) is propositional. F/G quantify strictly after the current integer,
P/H strictly before. □/◇ quantify over every WORLD AND TIME. There are no endpoints.
The implementation builds a finite type graph after reducing G/H/□ by duality.
For adjacent types s,t, Fφ(s) iff φ(t) or Fφ(t); Pφ(t) iff φ(s) or Pφ(s).
A future accepting strongly connected component must meet ¬Fφ or φ for every Fφ;
a past accepting component analogously meets ¬Pφ or φ. Viable types lie on paths
from a past accepting cycle to a future accepting cycle. Global diamonds are
assigned consistently, with true diamonds witnessed in viable types and false
diamonds forbidden at every type. A root type must satisfy all premises and the
negated conclusion. Finite many witness timelines suffice for the global diamonds.
Closed search yields a type-graph decision certificate, not a fabricated ordinary
tableau. Countermodels have finite paths and periodic tails in BOTH directions.
Original formulas are independently evaluated on the displayed infinite traces.
Limits: 20 local closure bits, 16 global bits, 4,096 types per global assignment,
2 million edges. A limit gives Unfinished, never Valid. The algorithm terminates
in principle, but finite hardware cannot promise a result on every input.

IL (pp.7–11) supports first-order quantifiers over nonempty individuals AND places.
ı (ASCII self) is the speaker, h (here) the context place; both are rigid.
Use individual names a,b and variables x,y; place names p0,p1 and variables v,v0.
Predicate signatures are inferred and checked; individual arguments precede places.
Loc has signature individual × place. Identity cannot mix sorts. A resets only the
world, N resets only time. □/◇ keep the current time fixed. F/G/P/H use strict
integer time. Consequence is at now in the actual world, with Loc(ı,h) true there.
Without tense the sorted first-order translation is exact. With tense, sound
first-order axioms of an unbounded discrete linear order and sound propositional
temporal abstraction give INCOMPLETE proof search for standard integer time.
No model of an arbitrary finite order is accepted as an integer-time countermodel.
A separate counterexample search enumerates actual Z models with constant tails:
up to two worlds, individuals and places; one or three middle time points;
up to 18 independent predicate valuation bits and 256 name assignments per size.
Original quantified formulas are evaluated with a temporal-depth margin beyond
both tails. Failed bounded model search never establishes validity.
These are validity checkers for the paper’s logics, not classifiers of normative,
indexical or Future sentences under model-shifting.

Input: O(p), P p, Fp, FPp, G(p → Fq), A R(ı), N Loc(ı,h).
Keywords are mode-specific: ought/permitted in DML; future/always_future and
past/always_past in TML/IL; actually/now/self/here in IL. Operator letters are
reserved in these modes. Existing modes retain their original predicate grammar.
No unsupported quantified version of DML or TML is silently substituted for the
propositional systems defined in the paper.

PROOF DISPLAY
Proof formulas are rendered from their AST, with explicit arguments and commas;
this corrects the unreadable concatenation of translation predicates and terms.
Intuitionistic boxes, sort predicates (World/Object/Place/Time), existence guards,
and world identifiers are retained. A visible notation key explains their role.
The same display renderer is used for the tree and translated starting formulas.
No proof rules, assumptions, or closure lines are removed for cosmetic reasons.

New files: dist/russell.js, dist/temporal.js, dist/indexical-model.js.
humes-tests.mjs checks the paper’s examples, the distinction between IL and TML
modalities, integer-time fairness, sorting, context conditions, parser isolation,
an exhaustive small DML oracle, periodic temporal witnesses and proof notation.
Research: https://doi.org/10.1007/s10992-021-09643-3
https://link.springer.com/article/10.1007/s10817-023-09691-1
The temporal graph is an independent implementation, not a port of BLACK.

NAME DESIGNATION AND RELATIVE IDENTITY
Variable-domain normal QML offers a Name designation setting, separate from the
identity setting: rigid (default) or non-rigid. In non-rigid mode all input names
are world-indexed functions into the outer domain; variables remain rigid.
Names need not exist locally. This respects positive/negative free semantics and
all three domain-growth options. Definite descriptions and per-name settings are
not included. The rigid-only auxiliary proof translation is disabled in this mode.

RI: basic weak sortal-relative identity. Use SameBook(a,b), SameThing(a,b), etc.
Each SameSort is symmetric/transitive, and Sort(x) iff SameSort(x,x). There is
no arbitrary substitution of same-sort terms into other predicates. Sorts may
be empty; SameThing is a separate sortal relation. Ordinary = is still absolute
identity. This specified first-order weak extension retains names; it is not
Geach's full strong theory or van Inwagen's name-free language. Quantified
proof/model search is incomplete. All axioms appear in Method & assumptions.
Research: https://link.springer.com/article/10.1007/s11841-017-0612-y
QML semantics: https://arxiv.org/abs/2212.09570

Run npm test for the full suite, including designation-tests.mjs, with an
independent exhaustive two-world/two-object source-language semantic oracle.

DEVELOPMENT
Requires Node.js for tests and building; no npm dependencies are needed.
  npm test
  node build-standalone.mjs
Source files are in dist/. Keep dist/branch-offline.html in sync by rebuilding
after edits. Third-party attribution is in dist/vendor/NOTICE.txt.
