Writing formulas
Use p, q, r or names such as rain for propositions; F(a), R(a,b) (or Fa, Rab) for predicates. Quantify variables: ∀x (F(x) → G(x)). Quantifiers bind the next formula; use parentheses for a larger scope. Premises can be separated by newlines or semicolons. You can also paste a full p → q, p |= q inference into the conclusion.
Keep the conditionals distinct. → / -> is the selected system’s main implication. ⊃ is its material or truth-functional conditional; in FDE-based systems it abbreviates ¬A ∨ B. > is the ceteris paribus conditional. ⥽ / strict abbreviates □(A ⊃ B). ↦ is the restricted relevant implication from p.69. In three-valued systems □ and ◇ are the quasi-modal operators on p.35.
Higher-order formulas
Choose Typed higher-order logic. Types are e, t (alias o), other named base types, and right-associative arrows, such as e→e→t. Angle notation <e,e,t> also works. Declare constants in the types field; omitted types are inferred, with unconstrained types defaulting to e. A bare unbound symbol is a constant. Application is F(a,b) or F a b; compact applications such as VX and VP are split into declared or bound symbols when there is a unique reading. An explicitly declared whole name stays one symbol. Ambiguous compact applications require spaces or parentheses; unknown names remain single symbols. Parenthesize lambda arguments.
Examples: ∀P:(e→t). (P(a) → P(a)), (λx:e. F(x)) a, ∀D:(t→t). ∀p:t. (D(p) ∨ ¬D(p)). A typed binder requires a dot and its scope extends to the end of the enclosing parentheses. ∀(λx:e. F(x)) is also accepted. Equality is typed; α, β and η conversion avoid variable capture.
Standard semantics: base domains are nonempty, t has exactly two elements, and function domains contain every function. The supplied NKω natural-deduction rules motivate the typed quantifier and conversion steps. The prover additionally uses functional extensionality for standard semantics; it is not an intensional-only NKω mode. This implementation is sound but incomplete and is not the complete Brown–Smolka tableau calculus. It does not treat a Henkin model as a countermodel to standard validity.
HOL proof search bounds generated terms (700 terms, 7,000 tree nodes, three rounds of application generation). Model search tries base sizes 1–3 and complete function spaces up to 65,536 elements, with an evaluation budget. Exhausting these bounds yields Unfinished. Finite sizes alone never prove validity over an unrestricted individual base. A truth-only type hierarchy is finite; exhaustive enumeration can instead issue an exact finite semantic certificate.
Free and quantified modal logic
Positive free logic permits true predication about nonexisting objects and validates a=a. Negative free logic makes every atomic formula with a nonexisting argument false, including identity; a=a is equivalent to E(a). Both have a nonempty outer domain and a possibly empty inner domain. Negated predication does not imply existence.
The Quantified modal menu gives explicit constant- and variable-domain K, D, T, KB, K4, B, S4 and S5. Variable-domain settings include arbitrary, expanding and contracting domains, and an optional nonemptiness condition. Constants are rigid by default. Constant-domain modes validate both Barcan directions; expanding domains validate converse Barcan, and contracting domains validate Barcan. The E predicate is reserved for existence in these modes. Each variable-domain system has positive and negative free logic versions. Positive versions follow the supplied handout. In negative versions, true predication and identity require every argument to exist at that world; negated predication does not. With rigid identity, a=b may cease to be true where either name does not exist, although the names keep their referents. Local domains may be empty unless Nonempty is selected. Names may denote outer-domain objects that exist at no world. The constant-domain entries use one nonempty domain with every name denoting in it, so positive and negative semantics coincide.
Logics from How to Prove Hume’s Law
DML is the paper’s propositional deontic-modal logic: O p means obligatory, P p permitted. Both range over one fixed nonempty Superb subset of worlds. □ and ◇ range over all worlds. It is stronger than ordinary deontic D.
TML is propositional tense-modal logic on the integers, with no first or last time. F/G mean some/all strictly future times; P/H some/all strictly past times. Here □/◇ quantify over all worlds and all times. A finite temporal type graph checks successor equations and eventuality fairness in both directions. It is an exhaustive decision method within memory limits (4,096 states, 2 million edges, 20 local bits, 16 global bits). Exhausting a resource limit gives Unfinished, never a verdict.
IL is the paper’s quantified indexical logic. ı (ASCII self) is the speaker; h (here) the place. Individuals use constants a,b and variables x,y; places use constants p0,p1 and variables v,v0. Loc(ı,h) says I am here. Predicate argument order is individuals, then places. Identity compares like sorts. A resets the world to actually; N resets time to now. □/◇ keep time fixed. Consequence is evaluated at the context world and time, with Loc(ı,h) true there. Tense is strict integer time.
IL’s first-order translation is exact without tense operators. With tense, proofs use sound discrete linear-order axioms or sound propositional temporal abstractions; this search is incomplete for the integers. Counterexamples are evaluated on genuine infinite integer timelines with constant tails, not finite timelines with endpoints. This witness search is bounded (up to two worlds/individuals/places, five time slots with infinite tails, 18 free valuation bits), so failure to find one means Unfinished.
Write O(p), F p, G(p → Fq), A R(ı) or compact FPp. Keywords: ought, permitted, future, always_future, past, always_past, actually, now. Uppercase O/P are operators in DML; F/G/P/H are operators in TML and IL, and A/N also in IL. These letters are reserved in those modes; use R,Q,S for IL predicates. Elsewhere the existing predicate syntax is unchanged. The paper’s barriers are metatheorems, not extra inference rules.
Non-rigid designation in variable-domain QML
Under Quantifiers & search settings, Name designation lets every input name keep one referent (rigid, the default) or denote a potentially different outer-domain object at each world (non-rigid). Variables keep their assignments across modal operators. Names are total on the outer domain; local existence is still tested with E. This works with positive/negative free semantics, domain growth and either identity option. Non-rigid does not force referents to differ. For example, with ordinary equality, a=b ⊨ □(a=b) holds in positive free QML with rigid names and can fail with non-rigid names. In negative free QML, modal identity also depends on local existence. Definite-description operators and per-name rigidity declarations are not provided.
Basic relative identity (RI)
Write SameBook(a,b), SameThing(a,b), or Same followed by any capitalized sort name. These relations obey symmetry and transitivity, with Book(x) ↔ SameBook(x,x). Each is an equivalence relation on its own sort; sorts can be empty. There is no unrestricted substitution from SameBook into arbitrary predicates or other sameness relations. Thus SameBook(a,b) ∧ ¬SameThing(a,b) can be consistent, even if both are Things. Ordinary = still means absolute identity and permits substitution; SameThing is not shorthand for it.
This is an explicitly specified weak first-order system, using the symmetry/transitivity core discussed by van Inwagen and the sortal reflexivity discussed by Routley and Griffin, with membership defined as self-sameness. It retains names and absolute equality for practical use. It is not the full Geach strong theory or van Inwagen’s name-free language. A classical tableau checks the stated axioms; quantified search may remain unfinished. Add any further relationships between sorts as premises.
Reading translated proofs
Intuitionistic propositional proofs use an S4 translation, so their boxes are intentional. World(w), Object(a), Place(p) and Time(t) are sort guards; R(w,v) is accessibility. The @ suffix identifies a world, not a truth degree. Numeric carrier entries in countermodels are element labels. The notation key above each translated proof explains these symbols. Predicate arguments are displayed with parentheses and commas to avoid running names together.
What is implemented
Propositional and quantified formulas are accepted in the listed families. Quantified I uses growing, nonempty domains and persistent local identity. Other quantified non-classical systems use constant domains by default. S, C1 and C2 use closest-world sphere semantics with the limit assumption.
Incomplete searches: quantified fuzzy logic uses sound quantifier bounds and exact finite countermodels (up to four objects). FB arguments use a bounded exact countermodel search (up to two worlds and two objects); propositional FB theorems additionally reduce to B. These modes may return unresolved for valid inputs. R and relevant T are undecidable. Quantified searches can also remain unresolved.
Not implemented: definite-description operators, non-classical identity in FDE-based/relevant systems, and free-domain variants of many-valued/relevant systems. The notes do not fix a weak-Kleene quantifier semantics, so quantified WK3 is rejected. Unsupported inputs receive an explanation, never a result from a substitute logic.
What a result means
Valid requires a closed tableau, an exact arithmetic certificate, a typed higher-order proof or exhaustive truth-only type certificate, or a derivation in the selected relevant system. Invalid requires a finite model checked against every translated input and frame condition, an exact fuzzy witness, or a sound RM3 refutation of a weaker relevant system. An unfinished tree never counts as a countermodel.
Classical and normal-modal trees use textbook-style sentence tableaux from Wolfgang Schwarz’s prover. Other systems use explicit truth/falsity or world translations followed by classical tableaux; these are labelled as translated proofs. Intuitionistic propositional formulas use the McKinsey–Tarski S4 translation. Fuzzy proofs use linear-constraint branches with exact rational arithmetic. Relevant systems first try their own axiom schemata, then use translated semantic tableaux. A Hilbert derivation is labelled as such.
Proof search and finite-model search run together. For the supported propositional systems with the finite-model property this provides a terminating decision method in principle. This does not promise a fast answer for every input: finite hardware still limits memory. Search errors or user cancellation produce no verdict. Quantified searches and propositional R/relevant T have a configurable budget. You can choose no time limit. Decidable propositional modes have no automatic timeout. Completeness of every implementation is not formally verified; regression tests cannot establish it.
Reading the models
In translated models, World and Object specify the two sorts (their carriers may overlap). @ is the evaluation world; R is accessibility; R₃ is ternary relevance accessibility. A predicate with ⁻ denotes falsity support, not lack of truth. An omitted tuple is false in that predicate. For modal reductions, p⁺ and p⁻ are component predicates; read them together with the displayed translation.
Source notes and corrections
The uploaded notes were reviewed across all 70 pages. The implementation uses FDE designated values {1,b}, agreeing with the truth-preservation definition on p.36; the {0,b} printed on p.38 is a typo. “−0” on p.28 means value 0 at world 0. The free-logic existential rule on p.60 uses the same fresh constant for E(c) and A(c). The C8 frame rule uses R(a,c*,b*) and C12 uses a ⊑ x, following Priest §§10.4 and 10.4a, correcting the notes pp.50–51. On p.69 the last quantified fuzzy biconditional is only a one-way implication (Priest §25.3.4). L and S0.5 follow Priest’s independent □/◇ treatment at non-normal worlds (p.19).
Research & source code
- Daniel Molto (2017), The Logical Problem of the Trinity and the Strong Theory of Relative Identity — formal RI symmetry/transitivity, sortal reflexivity, and distinctions between weak and strong theories. Our RI mode specifies its own basic weak extension above.
- Steen et al., Solving Quantified Modal Logic Problems by Translation to Classical Logics — semantic translations of quantified modal logic. Our non-rigid names translate as world-indexed functions.
- Gillian Russell, How to Prove Hume’s Law — the supplied 32-page manuscript defines IL, TML and DML. We follow its semantic definitions; H is past (the “future” gloss on p.16 is a typo), and the conclusion printed in Proposition 2’s proof differs from its heading; both stated inferences hold over integer time.
- Geatti et al., SAT Meets Tableaux for LTL Satisfiability — temporal tableaux and eventuality checking. Our implementation is an independent finite type-graph construction for this paper’s strict F/P fragment over bi-infinite time, not the BLACK implementation.
- The supplied qmltrees.pdf (pp.53–55), fl.pdf (pp.43–47), HOL.txt and accompanying typed NKω / standard-semantics images inform these extensions.
- Brown & Smolka · Analytic Tableaux for Simple Type Theory — typed tableau methods and the distinction between Henkin and standard completeness. This app implements its own bounded sound search, not their complete calculus.
- Brown & Smolka · Terminating Tableaux for the Basic Fragment — standard models and finite truth-only type hierarchies.
- Graham Priest · An Introduction to Non-Classical Logic, second edition — sphere semantics, relevance frame rules, and quantified semantics.
- Schwarz · Modal Predicate Logic, §10.3 — negative free atomic and identity clauses. Here nonempty local domains are optional and outer names may be nowhere existing.
- Wolfgang Schwarz · Tree Proof Generator and GPL-3.0 source. Vendored revision
3458a16. - Wu & Goré · Verified Decision Procedures for Modal Logics — termination and the care needed for loop checks.
- Zach · Non-Analytic Tableaux for Conditional Logics — why stronger conditional systems need additional machinery.
- Olivetti · Tableaux for Łukasiewicz Infinite-valued Logic — labelled constraints and linear feasibility.
This app and its included prover are GPL-3.0. License · Download all source and tests. The tests are regression checks, not a formal correctness proof.