Open research library
Papers you can read, cite and question
611 papers from the QNFO program, filed on nine shelves by the reader each one is written for: energy per answer, error correction, physics, numbers and p-adics, logic and formalism, AI and knowledge, autonomous systems, assessments, and cross-cutting essays. Every page renders its mathematics and can be questioned in place. How a living paper works.
Looking for an answer rather than a paper? Ask the whole corpus: answers cite the papers they come from.
Logic & formalism papers 5 papers
Logicians, formal-methods and foundations readers. Formal systems and what they cannot say: Laws of Form and the calculus of indications, distinction and re-entry, self-reference, category theory, coalgebra and bisimulation, proof assistants, computability, formal ontology.
Formal verification. Contracts, assertions and verified implementations Tagged papers: 16.
Re-Entry as a Binary Prohibition Law: Enumeration, Impossibility, and the Three-Outcome Completion
Self-referential constraints arise in hardware security, programmable logic, and symbolic execution tools, where a system must forbid a state while generating the very operation that enforces the prohibition. The open question is whether a re-entering form of the calculus of indications — a…
Degree Bounds as a First Exercise in Isabelle/ML Metaprogramming: A Reconciled Study of the poly_degree Command
Metaprogramming—writing programs that manipulate the objects, proofs, and tactics of a proof assistant itself—is a notorious barrier to entry for formal-methods newcomers, particularly mathematicians trained in classical rather than computational thinking. This paper presents a structured,…
Distinction-Lattice Framework: Eigenforms, Bisimulation, and the Realizability Boundary of Self-Reference
A conservative formal version of DLF: stable entities are bisimulation classes of observational behaviour, certified coinductively, with realizability separated from fixed-point existence. v0.2.0 narrows novelty claims and corrects the JPCUB/Landauer bridge. Published at papers.qnfo.org…
Formal Ontology of Distinction and Invariance
This document presents the complete, self-compliant synthesis of the Ontic Relational Patternism framework. Starting from a single primitive syntactic token—the mark—and three context-closed reduction rules (Calling, Crossing, Void), we derive a purely relational universe where the cross-ratio is…
Automated Formal Verification and Combinatorial Reduction of Distinction-Based Calculus
The foundation of modern formal mathematics has historically rested upon Zermelo-Fraenkel set theory with the Axiom of Choice (ZFC), a container-based ontology that often conflates zero with the empty set and necessitates arbitrary constraints to prevent self-reference. To systematically evaluate…
New papers by email
One short weekly digest: titles and links. No tracking; unsubscribe any time.