{"id":"327bf8ba-7c1c-4f12-911d-bfb6d3cadbb2","arxiv_id":"2607.20221","paper_version":1,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Fundamental logic with a preconditional is strongly complete, has the finite model property, and embeds fully and faithfully into ortho-S4 and intuitionistic KTB.","lead":"This paper adds a conditional connective—Holliday's 'preconditional'—to fundamental logic, and proves the resulting logics are strongly complete, decidable, and faithfully translatable into two modal logics. It thereby unifies intuitionistic implication, the Sasaki hook, and conditional-logic conditionals inside one framework.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Faithfulness of the modal translations is conditional on unproved [HM26] completeness and companion-frame lemmas; the internal canonical-model and FMP arguments are sound.","rationale":"The reader's weakest assumption is exactly the one I would flag: the modal faithfulness chain inherits unproved results from [HM26]. I checked the internal canonical-model construction, the truth and existence lemmas, the finite-model argument, and the factoring-condition proof in Section 7; they appear coherent and complete within the paper. The only real risk is external: Theorems 8.14 and 9.14 depend on target-logic completeness and on the companion-frame lemmas being applicable to the paper's balanced/strongly-factoring frames. Since [HM26] is itself a preprint and these results are not reproduced, the central modal claim is conditional on their correctness. This does not amount to an internal inconsistency, but it does mean the full/faithful translations are not self-contained. I therefore recommend accepting the paper only on condition that the cited lemmas and completeness theorems are verified against the definitions used here.","tokens_in":33966,"tokens_out":24396,"duration_ms":221123,"concrete_test":"Independently re-derive [HM26, Lem. 3.14, 3.16(1), 4.14] in the notation of this paper, checking the two specific applications: (i) for a balanced F-model, G1(N) satisfies the OS4 condition (int) and FP(c◁)⊆FP(c◁▷); (ii) for a strongly factoring F-model, G2(N) satisfies the FSTB condition (fs). In the same pass, verify Theorems 8.4 and 9.4 from the axiomatizations in §§8.1 and 9.1. If all four derivations go through, the concern is resolved.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"Theorems 8.14 and 9.14 are the central modal claims, but their faithfulness directions are not self-contained. Theorem 8.14(⇐) uses Theorem 8.13, which cites [HM26, Lem. 3.14 and 3.16] to turn the balanced canonical F-model of Corollary 7.11 into an OS4-model; Theorem 9.14(⇐) uses [HM26, Lem. 4.14] to turn the strongly factoring canonical model into an FSTB-model. The paper proves the needed factoring conditions (Theorem 7.9) and the semantic transfer calculations, but it does not prove that these cited lemmas apply with exactly Definitions 8.2/9.2, nor does it reproduce the OS4/ITB completeness theorems (8.4 and 9.4). If any cited lemma requires an extra frame condition beyond prefactoring+postfactoring (resp. strong factoring), or if the target completeness theorems use a different notion of frame or validity, the round-trip constructions and therefore the full/faithful conclusions would fail. This is a dependency on an external preprint rather than an internal gap, but it is load-bearing for the modal half of the central claim.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces and studies a family of propositional consequence systems K ⊆ T ⊆ F obtained by adding Holliday's preconditional axioms to a basic ∧,∨,⊥,⊤ consequence relation, with negation defined as φ→⊥. K is shown to be algebraically complete for bounded lattices with a preconditional; T adds conditional identity and semicomplementation of the defined negation; F adds double-negation introduction and is a conservative extension of fundamental logic. The paper proves strong completeness of T and F with respect to purely relational frames — reflexive, and reflexive-plus-pseudo-symmetric, respectively — using a canonical model whose points are pairs (theory, counter-theory), and proves the finite model property with an explicit 4^|Σ| bound. In the second half, the paper adapts the Holliday–Massas modal-embedding framework: the GMT-style translation with clause (α→β)^I = □(α^I →_s β^I) is claimed to be a full and faithful embedding of F into ortho-S4, and the Goldblatt-style translation with clause (α→β)^O = □(α^O → ♢(α^O ∧ β^O)) is claimed to embed F fully and faithfully into intuitionistic KTB. The frame-level technical core is the reduct-and-companion construction, with the preconditional-specific semantic transfer calculations carried out in Sections 8 and 9.","tokens_in":34232,"tokens_out":34775,"duration_ms":329275,"significance":"If the cited [HM26] results hold, this is a substantial contribution. It gives a syntactic presentation of Holliday's preconditional base, a clean relational completeness proof for two natural extensions, an explicit FMP bound, and two nontrivial modal embeddings that connect fundamental logic with a conditional to well-studied modal targets. A particular strength is that the canonical-model and FMP arguments are explicit and rule-by-rule; the closure conditions on counter-theories, the Σ-restricted existence lemmas, and the truth lemmas are carefully checked. The semantic transfer calculations for the preconditional clauses are the genuinely new technical work and are internally coherent. The algebraic completeness proof for K, T, and F is clean and parameter-free. I found no internal gap in Sections 2–7 or in the frame-level calculations of Sections 8–9.","major_comments":[{"comment":"The faithfulness directions of the two main modal theorems are load-bearing and are not self-contained. Theorem 8.14(⇐) uses Theorem 8.13, which delegates the construction of the OS4-model to [HM26, Lem. 3.14, 3.16(1)]; Theorem 9.14(⇐) similarly delegates the FSTB-model construction to [HM26, Lem. 4.14]. In addition, the completeness of the target logics — Theorems 8.4 and 9.4 — is cited from [HM26, Thm. 3.3 and Lem. 4.21]. Since [HM26] is an arXiv preprint and these lemmas carry the target-side frame conditions, the full/faithful conclusions are conditional on external results. Please either state and prove the needed companion lemmas in the present notation, or cite a published version of [HM26] and explicitly confirm that the definitions of frame, validity, and companion coincide with Definitions 8.2 and 9.2.","section":"§8.5, §9.5 (Theorems 8.14 and 9.14)"},{"comment":"The paper verifies that the canonical F-model satisfies the factoring conditions (Theorem 7.9), but it does not verify that these conditions are exactly what the cited [HM26] companion lemmas require. Definition 8.2 uses the interaction condition (int) in the algebraic form '□_≤ sends ≬-propositions to ≬-propositions', while Definition 9.2 uses (fs). The proof of Theorem 8.13(1) says only that '[HM26, Lem. 3.14] shows' the frame is an OS4-frame, and Theorem 9.12(1) does the same with [HM26, Lem. 4.14]. If a cited lemma carries an extra frame condition not implied by balancedness or strong factoring, the equalities F1(G1(N))=N and F2(G2(N))=N would no longer suffice for the modal-frame conclusion. Please spell out the alignment step in the notation of this paper, or include proofs of the companion lemmas.","section":"Definitions 8.2/9.2 and Theorems 8.13/9.12"}],"minor_comments":[{"comment":"The notation is confusing because the same letter F is used for fundamental logic and for the system F in Proposition 2.6 and Corollary 4.8. Please distinguish the two, for example by using a different symbol for fundamental logic.","section":"§2.5"},{"comment":"The predecessor-style conventions for ◁ and the modal operators are explained, but the reader must constantly translate between y◁x and forward accessibility. A small table displaying the forward-relation reading of each operator identity would improve readability.","section":"§4.1/Notation 4.2"},{"comment":"The references to [HM26] are precise as to lemma numbers, but for resilience the paper should state the exact inclusion FP(c◁) ⊆ FP(c◁▷) used for OS4-valuations and the exact FSTB-frame condition used in Theorem 9.12, even if the proofs are cited. This would also make it easier for a reader to check the definitional alignment raised in the major comments.","section":"§8–9"}],"recommendation":"major_revision","confidential_remarks":"The internal Sections 2–7 are strong: the canonical-model construction, the Σ-restricted existence lemmas, and the FMP proof appear correct. My only substantive reservation is the modal half of the paper, where the two headline faithfulness theorems depend on unproved companion lemmas and completeness theorems from an external preprint. If the author can supply those lemmas in an appendix or cite a published version of [HM26] with verified definitional alignment, I would be willing to accept."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The paper is worth a serious referee. It gives the first consequence-relation presentation K/T/F of fundamental logic with Holliday's preconditional, proves strong completeness and FMP for T and F, and extends Holliday-Massas's modal embeddings. What is genuinely new: the pair-of-theories canonical model in §5, the filtration-style finite countermodels in §6, and the two preconditional translation clauses in §8–9. I checked the rule-by-rule derivations in the completeness proofs; they are coherent and I found no gap. The conservativity result over fundamental logic (Cor 4.8) is handled cleanly.\n\nThe soft spot is the modal half. Theorems 8.14 and 9.14 are only as strong as the external results cited from [HM26]: OS4 and ITB completeness, plus the companion-frame lemmas that turn balanced (resp. strongly factoring) fundamental frames into the target modal frames. The paper proves the needed factoring conditions for its canonical model (Thm 7.9) and does the semantic transfer calculations, but it does not reproduce the cited lemmas nor verify that their exact frame definitions match Definitions 8.2/9.2. That is a normal citation pattern in this literature, but it means the full-and-faithful claims are conditional on an unpublished companion. If those [HM26] results carry additional frame conditions, the round-trip would need repair. The stress-test note makes exactly this point, and I think it lands.\n\nThe base systems look sound. Algebraic completeness for K matches Holliday's preconditional algebras; T and F are natural. The FMP bound is coarse but adequate. The proof of W_e ⊆ W_d is a bit dense but checks out. The open-complexity remark is honest.\n\nWho this is for: people working on fundamental logic, orthologic, lattice representations, or intuitionistic modal embeddings. It is not a paradigm shift; it is a solid extension of a known framework. It deserves peer review, not desk rejection. If the referee can access [HM26] and verify the companion lemmas apply, the paper can be accepted.","headline":"Solid extension of fundamental logic with a preconditional; internal completeness proofs are sound, but the modal full-and-faithful claims inherit load-bearing unproved results from [HM26].","tokens_in":34693,"tokens_out":2683,"would_cite":true,"duration_ms":30990,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B45","03B20","03G10","03F03"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper claims that adding Holliday's preconditional to fundamental logic yields a consequence relation F that is strongly complete over reflexive, pseudo-symmetric frames, has the finite model property (with countermodels of at most 4^{|","keywords":["fundamental logic","preconditional","relational semantics","strong completeness","finite model property","ortho-S4","intuitionistic KTB","modal translation"],"falsifier":"Consult the cited results [HM26, Lemmas 3.14, 3.16, 4.14] and check whether the balanced/strongly-factoring conditions they assume match exactly the conditions proved for the canonical model in Theorem 7.9; any discrepancy (e.g., a hidden normality or totality requirement) would break the faithfulness direction of Theorems 8.14 and 9.14.","tokens_in":33844,"feed_emoji":"🧩","tokens_out":8337,"duration_ms":69190,"temperature":0.7,"pith_summary":"This paper claims that a single operation—Holliday's preconditional—can be added to fundamental logic to produce a logic F that is exactly the logic of reflexive, pseudo-symmetric openness frames with a specific relational clause for the conditional. It proves strong completeness for F (and its weaker companion T) by constructing a canonical model whose points are pairs of theories and counter-theories, and it shows every non-derivable consequence has a finite countermodel with at most 4^{|Σ|} states, making F decidable. The paper further claims that F embeds fully and faithfully into two well-studied modal logics—ortho-S4 and intuitionistic KTB—via translations whose conditional clauses are a boxed Sasaki hook and a strict intuitionistic conditional. If these claims are right, fundamental logic with a preconditional occupies the same mediating role among conditional logics that fundamental logic occupies among negation-based logics.","feed_headline":"Fundamental logic plus a conditional is decidable","feed_subtitle":"Strong completeness over reflexive pseudo-symmetric frames and faithful embeddings into ortho-S4 and intuitionistic KTB.","key_machinery":"The key mechanism is the relational preconditional operation on propositions, A →◁ B = □◁(−A ∪ ♢▷(A∩B)), together with the canonical model built from (theory, counter-theory) pairs where y◁x iff Γ_x ∩ Δ_y = ∅ and the counter-theory is →-closed relative to the theory. The further ingredient is the factoring-condition framework: frames that are balanced (prefactoring and postfactoring) or strongly factoring give rise to same-carrier modal companions G1 and G2, and the canonical model is proven to satisfy these conditions, enabling the round-trip constructions with no extra conditions. The translations use a boxed Sasaki hook on the ortho side and a strict conditional on the intuitionistic side","core_discovery":"The central discovery is that the consequence relation ⊢_F—fundamental logic augmented by Holliday's preconditional—is both strongly complete and finite-model-definable over the class of reflexive, pseudo-symmetric frames, with the preconditional interpreted as A →◁ B = {x | ∀y◁x (y ∈ A ⇒ ∃z (y◁z ∧ z ∈ A ∩ B))}. This clause simultaneously generalizes Heyting implication and the Sasaki hook. Moreover, the logic is exactly what is obtained by translating into ortho-S4 with a boxed Sasaki hook, or into intuitionistic KTB with a strict clause classically equivalent to the Goldblatt translation of that hook: φ ⊢_F ψ iff φ^I ⊢_{OS4} ψ^I iff φ^O ⊢_{ITB} ψ^O. The proof of these embeddings rests on a","pith_inferences":["The 4^{|Σ|} bound is likely not tight; a cut-free sequent calculus in the spirit of the decidability proof for fundamental logic could give a much better complexity bound.","The factoring conditions may carve out exactly the class of frames that are reducts of OS4 and FSTB frames, so the same technique could be reused for other extended languages (e.g., quantifiers, strict implication).","The two modal readings of the preconditional—boxed Sasaki hook vs. strict intuitionistic conditional—could correspond to two natural-language readings of conditionals (strict vs. variably strict), giving a precise modal map between them."],"forward_implications":["F is decidable: a non-derivable consequence φ ⊬ ψ has a countermodel with at most 4^{|Σ|} states, where |Σ| grows linearly with the subformulas of φ and ψ.","A single conditional covers a wide range of existing conditionals: Heyting implication and the Sasaki hook are both instances of the preconditional clause, so theorems proved for F apply to both.","Reasoning about preconditionals can be systematically translated into ortho-S4 and intuitionistic KTB, and conversely; the two modal logics become conservative computational mirrors of F.","Strong completeness holds for arbitrary premise sets, not just finite ones, because the canonical model is built from infinite theories and counter-theories."],"fun_headline_variants":["Preconditional logic: strongly complete, decidable, translatable","Sasaki hook meets Heyting: decidable preconditional logic","Reflexive pseudo-symmetric frames yield strong completeness","Two modal embeddings for decidable preconditional logic"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The faithfulness of the two modal embeddings (Theorems 8.14 and 9.14) inherits unproved-in-this-paper results of Holliday and Massas—OS4 completeness for ortho-S4 frames, ITB completeness for FSTB frames, and the companion-frame lemmas that balanced or strongly-factoring fundamental frames produce the needed modal companions; if any of those cited results carries an additional frame condition not covered by the factoring conditions proved here, the round-trip constructions wo","fun_headline_variants_meta":{"raw":{"variants":["Preconditional logic: strongly complete, decidable, translatable","Sasaki hook meets Heyting: decidable preconditional logic","Reflexive pseudo-symmetric frames yield strong completeness","Two modal embeddings for decidable preconditional logic"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001269,"raw_usage":{"total_tokens":5099,"prompt_tokens":881,"completion_tokens":4218,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":625,"completion_tokens_details":{"reasoning_tokens":4152}},"tokens_in":625,"tokens_out":4218,"duration_ms":30191,"temperature":1.0,"reasoning_tokens":4152,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-01T10:26:36.134243+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Consult the cited results [HM26, Lemmas 3.14, 3.16, 4.14] and check whether the balanced/strongly-factoring conditions they assume match exactly the conditions proved for the canonical model in Theorem 7.9; any discrepancy (e.g., a hidden normality or totality requirement) would break the faithfulness direction of Theorems 8.14 and 9.14.","supporting_citations":[],"review_version":1}