This draft introduces the technical machinery of a semantic framework for potentialist truthmaking based on our innovation of intentic states, which are structured partial models accounting for our distinction between non-hypothetical and hypothetical reasoning. The framework is developed for first-order logic in a purely relational language and is compatible with both classical and intuitionistic settings. Truthmaking is defined via a recursive construction over intentic states, yielding a semantic consequence relation that is shown to be sound and complete with respect to standard natural deduction. The resulting structure supports two natural extension relations, corresponding to truthmaking growth and hypothetical refinement, which are shown to satisfy the axioms governing Linnebo's bi-modal potentialist semantics. Moreover, we investigate the computational properties of the non-hypothetical fragment of natural deduction. Motivated by proof-theoretic and semantic considerations, we formulate a conjecture that non-hypothetical logic is decidable over Peano Arithmetic in a purely relational axiomatization, and more ambitiously over any fixed Peano Arithmetic theorem taken as an additional axiom. A schematic proof-search procedure is drafted to support this conjecture, identifying structural sources of finiteness. While preliminary, this analysis suggests a strong subformula discipline for normal non-hypothetical proofs and provides a proof-theoretic foundation for future work.
翻译:本草案基于我们创新的意向状态引入了一种用于潜存主义真值制造的语义框架技术体系,该框架通过结构化部分模型来区分非假设性与假设性推理。该框架专为纯关系语言中的一阶逻辑而构建,同时兼容经典逻辑与直觉主义逻辑体系。真值制造通过在意向状态上的递归构造进行定义,由此产生的语义后承关系被证明相对于标准自然演绎系统具有可靠性与完备性。所得结构支持两种自然扩展关系,分别对应真值制造的扩展与假设性精化,这些关系被证明满足Linnebo双模态潜存主义语义学的公理要求。此外,我们研究了自然演绎系统中非假设性片段的计算特性。基于证明论与语义学的双重考量,我们提出一个猜想:在纯关系公理化体系中,非假设性逻辑在皮亚诺算术上是可判定的;更宏大的目标是证明其在任何作为附加公理的固定皮亚诺算术定理上也是可判定的。我们草拟了支持该猜想的结构化证明搜索流程,并确定了有限性的结构来源。尽管是初步研究,该分析揭示了正规非假设性证明的强子公式约束规律,为后续研究奠定了证明论基础。