AI 中文总结
研究带前提条件的基本命题逻辑,通过给出后承关系表示结合基本逻辑与前提条件,研究其扩展$\mathsf{T}$和$\mathsf{F}$,证明强完备性与有限模型性质,适配模态嵌入到正交$\mathsf{S4}$和直觉主义$\mathsf{KTB}$,给出新条件从句及框架构造。
AI 中文摘要
基本逻辑(Holliday 2023)是一种仅基于菲奇式自然演绎系统中合取、析取和否定的引入与消去规则的非经典逻辑,而前提条件(Holliday 2025)是有界格上满足五条自然公理且包含海廷蕴涵、正交格上的佐々木钩以及满足扁平化的刘易斯 - 施塔尔纳克式条件句的二元运算。我们通过给出一个其代数恰好是带有前提条件的Holliday有界格的后承关系表示$\mathsf{K}$来结合二者,然后研究两个自然扩展$\mathsf{T}$和$\mathsf{F}$,后者是带前提条件的基本命题逻辑。对于$\mathsf{T}$和$\mathsf{F}$,我们使用点为理论对的典范模型证明相对于纯关系语义的强完备性,并建立有限模型性质及可判定性。最后,遵循Holliday和Massas(2026),我们将他们的GMT - 和戈德布拉特式嵌入适配到带前提条件的基本逻辑。所得翻译分别完全且忠实地嵌入到正交$\mathsf{S4}$和直觉主义$\mathsf{KTB}$中。新的条件从句在前一种情况下将前提条件发送到盒装佐々木钩,在后一种情况下发送到严格直觉主义条件句,其经典的$\mathsf{KTB}$解读等同于佐々木钩的戈德布拉特翻译。框架构造遵循Holliday和Massas的归约与伴随模式;关键的额外要素是前提条件的语义转移计算。
英文摘要
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.