Reader's guide · Terminology legend
Reading a result
A status belongs to a question, not to an argument in isolation.
“sat” can be a successful consistency check. “unsat” can be a successful proof-by-contradiction check. Always read the input and the question beside the reported status.
Solver and prover terms
Plain-language legend- sat · satisfiable
- The supplied conditions have a model: at least one assignment makes them all hold. For a consistency test this is a positive result. For a negated-conclusion test it supplies a counterexample within the encoding.
- unsat · unsatisfiable
- No assignment satisfies all supplied conditions. When the input is the premises together with the negation of the conclusion, this supports that conclusion under those premises and within that encoding. If the premises alone are unsatisfiable, they are inconsistent instead.
- Theorem / SZS status Theorem
- The automated prover reports a derivation of the conjecture from the supplied axioms. SZS is a standardized result vocabulary. A theorem status does not independently establish the axioms' truth.
- unknown / timeout
- The tool did not settle this input, or exhausted its allotted resources. Neither is a proof, a countermodel, nor a finding of impossibility.
- exit code 0
- The program finished successfully. Its significance depends on the command: for a proof compiler it means the submitted proof was accepted; for a solver, read its status as well.
- Model / countermodel
- A model is an interpretation satisfying the input conditions. A countermodel satisfies the premises but falsifies the requested conclusion.
- Axiom / premise / hypothesis
- A starting condition supplied to the proof. A hypothesis remains a condition of a theorem even when the theorem is machine-checked.
- Conjecture / negated conclusion
- The proposition requested for proof, or its denial. Adding the denial to the premises is a standard way to test whether they allow a counterexample.
- Inference step
- One application of a formal reasoning rule. “51 inference steps” describes one archived machine derivation, not 51 experiments or 51 independent confirmations.
- Kernel-checked / assumption audit
- A small trusted checker verifies proof objects. An audit reports logical dependencies. “Closed under the global context” means no undeclared global axioms remain; quantified hypotheses inside the theorem are still present.
- Finite check / unbounded theorem
- A finite check restricts a test to the declared number of objects or rounds. An unbounded theorem quantifies over its stated domain without that finite test bound. Do not extrapolate a bounded search to all possible domains.
- Formal validity / soundness
- Validity means the conclusion follows from the premises. Soundness additionally requires the premises to be true under the intended interpretation. Machine checking establishes the formal derivation, not physical fidelity by itself.
- SMT-LIB / TPTP / HOL
- SMT-LIB and TPTP are machine-readable problem formats. HOL means higher-order logic, which can quantify over functions or predicates. The filenames link to the exact submitted problems.
- Source hash / JSON / JSONL / training corpus
- A source hash identifies an exact file version. JSON stores structured data; JSONL stores one record per line. The corpus contains checked examples for future training; collecting it does not mean a neural model has been trained.
Terms in the argument
Dalīl al-imkān- Necessary in itself · wājib al-wujūd bi-dhātihi
- An existent whose existence is necessary in itself, rather than supplied by another. The abstract proof uses this predicate explicitly; the primitive configuration models use their declared invariant-existence definitions.
- Possible in itself · mumkin al-wujūd bi-dhātihi
- An existent whose existence is not necessary in itself and requires determination. Here “possible” means contingent, not merely “not logically impossible.”
- Necessary through another · wājib li-ghayrihi
- Necessitated by its sufficient cause while still possible in itself. This is not a third category in the division by status in itself.
- Murajjiḥ / equipoise
- A determining or preponderating cause. Equipoise expresses that the possible's essence alone does not select existence rather than non-existence; it is not a claim of a 50% statistical probability.
- Aggregate / exhaustive totality / outside
- The collection covers all existing possibles, including every possible cause. “Outside” means not among those members, not outside a place or earlier in time.
- Sufficient cause / whole-to-constituents
- An explanation sufficient for existence. The whole-to-constituents principle says a sufficient explanation of the aggregate accounts for its members. Its collective-subset extension is stated explicitly in the proof.
- Base case / configuration / primitive proof
- A base case ends a recursive evaluation. A configuration is an admitted setting or run of a model. A primitive proof checks a premise in a small, explicitly defined computer model. The base represents the necessary foundation; the non-base outputs represent possibles. Applying the result to reality requires accepting that this mapping accurately represents the relevant features, just as human reasoning requires an adequate representation of its subject.
- Logical premise L1 / non-contradiction / same respect
- A claim and its logical negation cannot both hold of the same subject in the same respect. A base cannot be both a base and not a base. The P3 causal interpretation treats sufficient self-causation as requiring both dependence upon and independence from oneself in that same respect.
- Circularity / infinite regress / well-foundedness
- Circularity returns dependence to an earlier participant; infinite regress continues indefinitely. Well-foundedness rules out endless descent. P6 concerns an ungrounded regress of mandatory dependencies: each requested result awaits another, with no foundation. The Fibonacci proof checks this under completed-result rules. The aggregate proof uses P1–P5 and does not assume P6 or well-foundedness.