The paper develops a new logical system that combines two recent ideas in non-classical logic. The first idea, "fundamental logic," is a weak logical framework that avoids some of the standard assumptions built into classical or intuitionistic logic, relying only on basic rules for "and," "or," and "not." The second idea, a "preconditional," is a generalized version of the familiar "if-then" connective that is flexible enough to capture several different notions of implication used across mathematics, physics, and philosophy, including standard constructive implication, a version used in quantum logic, and conditional logics in the style of David Lewis. The paper combines these two ingredients into a single formal system and studies two natural strengthenings of it.
The main technical results establish that these logical systems are well-behaved in several important senses. The authors prove "strong completeness," meaning that the logical systems are powerful enough to capture exactly the truths that hold in their intended mathematical models, even when reasoning involves infinitely many premises. They also prove the "finite model property," which means that whenever a statement fails to be a logical truth, this failure can already be witnessed by a small, finite structure. A practical consequence of this is that the logics are decidable: there is, in principle, an algorithm that can determine whether any given statement is logically valid.
Finally, the paper shows how these new logics relate to better-known and more classical logical systems through precise translation mappings. Specifically, the authors adapt existing translation techniques to show that their logic embeds faithfully into two familiar modal logics, one built on ortho-modal logic and one on intuitionistic modal logic. These embeddings are "full and faithful," meaning the translation perfectly preserves logical relationships in both directions. The key technical novelty is figuring out where the new preconditional connective maps to under each translation, which turns out to correspond to natural but previously unstudied constructions in those better-known systems.