Fundamental Propositional Logic with Preconditional: Strong Completeness, Finite Model Property, and Modal Translations

Fundamental logic (Holliday 2023) is a non-classical logic based only on the introduction and elimination rules for conjunction, disjunction, and negation in a Fitch-style natural deduction system, while a preconditional (Holliday 2025) is a binary operation on a bounded lattice satisfying five natural axioms and subsuming Heyting implication, the Sasaki hook on ortholattices, and Lewis-Stalnaker-style conditionals satisfying flattening.

We combine the two by giving a consequence-relation presentation $\mathsf{K}$ whose algebras are exactly Holliday's bounded lattices with a preconditional, and then studying two natural extensions, $\mathsf{T}$ and $\mathsf{F}$, the latter being fundamental propositional logic with a preconditional.

For $\mathsf{T}$ and $\mathsf{F}$, we prove strong completeness with respect to a purely relational semantics, using a canonical model whose points are pairs of theories, and establish the finite model property and hence decidability.

Finally, following Holliday and Massas (2026), we adapt their GMT- and Goldblatt-style embeddings to fundamental logic with a preconditional.

The resulting translations are full and faithful into ortho-$\mathsf{S4}$ and intuitionistic $\mathsf{KTB}$, respectively.

The new conditional clauses send the preconditional to a boxed Sasaki hook on the former side and to a strict intuitionistic conditional on the latter whose classical $\mathsf{KTB}$ reading is equivalent to the Goldblatt translation of the Sasaki hook.

The frame constructions follow the reduct-and-companion pattern of Holliday and Massas; the essential additional ingredient is the semantic transfer calculation for the preconditional.