pith. sign in

arxiv: 2606.29954 · v1 · pith:SHHW5JQ2new · submitted 2026-06-29 · 🧮 math.LO · cs.LO

Fundamental Logic Through the Lens of Modality

Wesley H. Holliday , Guillaume Massas This is my paper

Pith reviewed 2026-06-30 03:42 UTC · model grok-4.3

classification 🧮 math.LO cs.LO
keywords fundamental logicmodal logicGMT translationGoldblatt translationorthologicintuitionistic logicembeddingsnatural deduction
0
0 comments X

The pith

Modal translations provide full and faithful embeddings of fundamental logic into orthological S4 and an intuitionistic version of KTB.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Fundamental logic is built from introduction and elimination rules for conjunction, disjunction, negation, and quantifiers in a Fitch-style natural deduction system. The paper shows that two standard modal translations connect this system to other non-classical logics without loss or gain of theorems. The GMT translation embeds fundamental logic fully into the orthological version of S4, while the Goldblatt translation does the same for an intuitionistic version of KTB. A third result embeds intuitionistic logic fully into a modal extension of fundamental logic. These embeddings give a precise way for fundamental logicians, orthologicians, and intuitionistic logicians to translate their systems into one another via modality.

Core claim

The GMT translation of intuitionistic logic into S4 is a full and faithful embedding of fundamental logic into the orthological version of S4; the Goldblatt translation of orthologic into KTB is a full and faithful embedding of fundamental logic into an intuitionistic version of KTB; and the GMT translation is a full and faithful embedding of intuitionistic logic into a modal extension of fundamental logic.

What carries the argument

The GMT translation and the Goldblatt translation, each acting as a full and faithful embedding that preserves and reflects provability between fundamental logic and the target modal systems.

If this is right

  • Fundamental logic sits inside orthological S4 and inside intuitionistic KTB as a common fragment preserved exactly by the translations.
  • Intuitionistic logic embeds into a modal extension of fundamental logic, showing that the latter can serve as a base for recovering intuitionistic theorems via modality.
  • Orthologic and intuitionistic logic become comparable through their respective modal embeddings of the same fundamental core.
  • Natural deduction derivations in fundamental logic correspond exactly to derivations in the image logics under the translations.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The results suggest that modality can act as a neutral bridge for comparing non-classical logics that otherwise lack a shared semantics.
  • If the embeddings hold, then completeness or decidability results for one system might transfer to fundamental logic via the translations.
  • The approach leaves open whether similar embeddings exist for other modal bases or for first-order extensions beyond the quantifier rules already included.

Load-bearing premise

The natural deduction rules for fundamental logic and the definitions of the orthological and intuitionistic modal logics are set up so that the translations preserve and reflect logical structure in both directions.

What would settle it

A formula provable in fundamental logic whose image under the GMT translation is not provable in the orthological version of S4, or vice versa.

Figures

Figures reproduced from arXiv: 2606.29954 by Guillaume Massas, Wesley H. Holliday.

Figure 1
Figure 1. Figure 1: Fitch-style introduction and elimination rules for fundamental logic, where [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: The Reductio ad Absurdum (RAA) rule of orthologic. [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: The Reiteration rule of intuitionistic logic. [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: The “fundamental diamond” relating fundamental logic, orthologic, [PITH_FULL_IMAGE:figures/full_fig_p005_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Introduction and elimination rules for □. . . . . . . i □φ . . . . . . . . . φ T Rule, i . . . . . . i □φ . . . . . . . . . □□φ 4 Rule, i [PITH_FULL_IMAGE:figures/full_fig_p006_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: S4 principles for □. 2.2 Algebras We now introduce classes of algebras corresponding to the logics of the previous section. Given a bounded lattice L, we denote its meet and join operations by ∧ and ∨, trusting that no confusion will arise between lattice operations and logical connectives; we denote its minimum and maximum by 0 and 1, respectively, and we assume throughout that 0 ̸= 1. Algebraic semantics… view at source ↗
Figure 7
Figure 7. Figure 7: Illustration of the modal frame condition in Definition 2.16. A solid line from [PITH_FULL_IMAGE:figures/full_fig_p009_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: An OS4-lattice in which □♢□a ∧ □♢□b = 1 and □♢□(a ∧ b) = 0. Solid edges give the Hasse diagram of the ortholattice, and dashed arrows represent the □ operation. Let us now consider a particular class of modal frames. Whenever (X, ◁|, L9) is a modal frame such that ◁| is symmetric, we will call it an orthomodal frame, and we use the symbol ⊤ to denote the relation ◁| in a way that emphasizes its symmetry. D… view at source ↗
Figure 9
Figure 9. Figure 9: An OS4-frame (left) and its fundamental reduct (right). A solid line from w to v indicates v⊤w on the left and v ◁| w on the right; a dashed line from w to v on the left indicates v ≤ w. The dual algebra of the OS4-frame is the OS4-lattice in [PITH_FULL_IMAGE:figures/full_fig_p012_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: The skeletal condition of Definition 3.10.1. [PITH_FULL_IMAGE:figures/full_fig_p013_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: A balanced fundamental frame (left) and its orthomodal companion (right). Note that the [PITH_FULL_IMAGE:figures/full_fig_p015_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: Fitch-style rules for the logic with quantifiers. [PITH_FULL_IMAGE:figures/full_fig_p018_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: An FSTB-frame (left) and its fundamental reduct (right). On the left, a dashed (resp. solid) line from v to u indicates that u ≤ v (resp. u⊤v). On the right, a solid line from v to u indicates that u ◁| v. see that the dual algebra of (X, ◁|) coincides with the fixpoints of the □⊤♢⊤ operation, note first that ≤ is a subrelation of the prerefinement relation ≤◁| . Consequently, since any element in the dua… view at source ↗
Figure 14
Figure 14. Figure 14: A strongly factoring fundamental frame (left) and its [PITH_FULL_IMAGE:figures/full_fig_p024_14.png] view at source ↗
Figure 15
Figure 15. Figure 15: The □-Reiteration rule of FN4. The corresponding class of algebras is the following. Definition 5.1. An FN4-algebra is an algebra (L, ¬, □) where (L, ¬) is a fundamental lattice and for all a, b, c ∈ L: 1. □1 = 1, □(a ∧ b) = □a ∧ □b, □a ≤ a, and □a ≤ □□a; 2. (a ∨ b) ∧ □c ≤ (a ∧ □c) ∨ (b ∧ □c); 3. if a ∧ □c ≤ ¬b, then b ∧ □c ≤ ¬a. The second item corresponds to the use of □-Reiteration into subproofs for ∨… view at source ↗
Figure 16
Figure 16. Figure 16: FN4 proofs of principles corresponding to Definition 5.1.2-3. 28 [PITH_FULL_IMAGE:figures/full_fig_p028_16.png] view at source ↗
Figure 17
Figure 17. Figure 17: Introduction and elimination rules for →. The class of algebras corresponding to FC4∼= is the following. Definition 5.10. An FC4-algebra is an algebra (L, ¬, □, →) where (L,¬, □) is an FN4-algebra and for all a, b, c ∈ L: 1. if □c ∧ a ≤ b, then □c ≤ a → b; 2. a ∧ (a → b) ≤ b. The first principle corresponds to →I, allowing □-Reiteration into →I-subproofs, while the second corre￾sponds to →E. The soundness… view at source ↗
Figure 18
Figure 18. Figure 18: Congruence rules for → in FC4∼=. The subproofs must be proofs given ∅ (see Appendix A.4), so □-Reiteration cannot be used to bring formulas outside of these subproofs into the subproofs. Proposition 5.12. For all φ, ψ ∈ L(∧,∨, ¬), if φ ⊢FC4∼= ψ, then φ ⊢F ψ. Proof. The proof is the same as that of Proposition 5.3 except that we further expand (L, ¬, □) to the algebra (L, ¬, □, →) where a → b = ( 1 if a ≤ … view at source ↗
Figure 19
Figure 19. Figure 19: The ♢-RAA rule of FM4∗ . We can now define the desired orthomodal logic. Let OMR (where R suggests regular, as in Proposi￾tion 5.24 below) be the orthomodal logic with □-Reiteration, the 4 Rule, and the following rules: • from □♢□φ, infer □φ; • from □□φ, infer □φ; • from □⊥, infer ψ. Thus, by Theorem 5.22, µ + is a full and faithful embedding of CPC into OMR. Let OMR algebras be defined just like FM4 alge… view at source ↗
Figure 20
Figure 20. Figure 20: The “reversed fundamental diamond”, reversing the arrows from Figure 4. Dashed arrows [PITH_FULL_IMAGE:figures/full_fig_p036_20.png] view at source ↗
Figure 21
Figure 21. Figure 21: A fundamental lattice, where dashed arrows represent the [PITH_FULL_IMAGE:figures/full_fig_p040_21.png] view at source ↗
Figure 22
Figure 22. Figure 22: Two OS4-lattices, where dashed arrows represent the □ operation, into which F4 OS4-embeds. The shaded nodes are the □-fixpoints. Clearly, neither of the ortholattices in [PITH_FULL_IMAGE:figures/full_fig_p040_22.png] view at source ↗
Figure 23
Figure 23. Figure 23: To apply □-Case, the α and β subproofs must be subproofs for an application of ∨E. Definition 6.9. An FN4+-frame is a fundamental modal frame (X, ◁|, L9) in which L9 is reflexive and transitive and the following conditions hold: 1. direct enrichment: if x |▷ y, then there is a prerefinement y + of y such that x |▷ y+ L9 x; 2. indirect enrichment: if x |▷ z ◁| y, then there is a prerefinement y + of y such… view at source ↗
Figure 24
Figure 24. Figure 24: Illustration of the frame conditions in Definition 6.9. [PITH_FULL_IMAGE:figures/full_fig_p042_24.png] view at source ↗
Figure 25
Figure 25. Figure 25: The “fundamental lotus”, connecting fundamental logic to various propositional and modal logics. [PITH_FULL_IMAGE:figures/full_fig_p043_25.png] view at source ↗
Figure 26
Figure 26. Figure 26: FN4 proof for Lemma A.9.1. Officially a □-subproof begins with ⊤ (see Appendix A.3), but we suppress this step in proof diagrams. 48 [PITH_FULL_IMAGE:figures/full_fig_p048_26.png] view at source ↗
Figure 27
Figure 27. Figure 27: Proof of □∃xµ+(φ) from ∃xµ+(φ) in QFC4. In the first-order case, we must slightly revise the second part of Lemma A.5 in the presence of ∀I. Lemma A.17. For L ∈ {IQC, IQC, QFC4}: 1. If ⟨σ1, . . . , σn⟩ is an L-proof given R and σi is a formula, then ⟨σ1, . . . , σi⟩ is an L-proof given R. 2. If ⟨σ1, . . . , σn⟩ and ⟨τ1, . . . , τm⟩ are L-proofs given R such that σn = τ1, then there is an L-proof ⟨π1, . . … view at source ↗
Figure 28
Figure 28. Figure 28: Turning an FN4+ proof with □-Case (left) into an intuitionistic proof with Reiteration (right). Definition A.21. An FN4+-algebra is an FN4-algebra (L, ¬, □) such that for all a, b, c ∈ L, we have (a ∨ b) ∧ (a ∨ □c) ≤ a ∨ (b ∧ □c). To prove the additional form of distributivity in FN4+, we use the □-Case rule, as shown in [PITH_FULL_IMAGE:figures/full_fig_p053_28.png] view at source ↗
Figure 29
Figure 29. Figure 29: Proof of α ∨ (β ∧ □φ) from (α ∨ β) ∧ (α ∨ □φ). For the soundness of FN4+ with respect to FN4+-algebras, note that we can bring multiple □φ formulas into the β case using the □-Case rule. The key algebraic fact for the soundness of ∨E allowing □-Cases is the following. Lemma A.22. In an FN4+ algebra (L, ¬, □), we have (a ∨ b) ∧ V 1≤i≤n (a ∨ □ci) ≤ a ∨ (b ∧ V 1≤i≤n □ci). Proof. We prove the claim by inducti… view at source ↗
read the original abstract

Fundamental logic is a non-classical logic based only on the introduction and elimination rules for conjunction, disjunction, negation, and the quantifiers in a Fitch-style natural deduction system. In this paper, we attempt to obtain a better understanding of fundamental logic and its semantics through the lens of modality. Using modal logic, we develop means of mutual understanding between the fundamental logician, on the one hand, and the orthologician and intuitionistic logician, on the other: we prove that the G\"odel-McKinsey-Tarski (GMT) translation of intuitionistic logic into the classical modal logic $\mathsf{S4}$ is a full and faithful embedding of fundamental logic into the orthological version of $\mathsf{S4}$; that the Goldblatt translation of orthologic into the classical modal logic $\mathsf{KTB}$ is a full and faithful embedding of fundamental logic into an intuitionistic version of $\mathsf{KTB}$; and that the GMT translation is a full and faithful embedding of intuitionistic logic into a modal extension of fundamental logic.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 1 minor

Summary. The manuscript defines fundamental logic via a Fitch-style natural deduction system consisting solely of the introduction and elimination rules for conjunction, disjunction, negation, and the quantifiers. It then establishes three embedding results: the Gödel-McKinsey-Tarski (GMT) translation yields a full and faithful embedding of fundamental logic into the orthological variant of S4; the Goldblatt translation yields a full and faithful embedding of fundamental logic into an intuitionistic variant of KTB; and the GMT translation yields a full and faithful embedding of intuitionistic logic into a modal extension of fundamental logic. All results are proved from the natural-deduction presentation.

Significance. If the embeddings are indeed full and faithful, the work supplies a precise modal bridge between fundamental logic and both orthologic and intuitionistic logic, allowing direct comparison of their deductive structures. The use of natural-deduction presentations rather than axiomatic ones strengthens the claims by making the preservation of rules explicit and verifiable.

minor comments (1)
  1. [Abstract] The abstract and introduction would benefit from a brief, self-contained statement of the precise natural-deduction rules that constitute fundamental logic before the embedding theorems are stated.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary, significance assessment, and recommendation to accept the manuscript. There are no major comments requiring response.

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper defines fundamental logic via its Fitch-style natural deduction rules for the standard connectives and quantifiers, then proves three embedding theorems using the standard GMT translation (into orthological S4) and Goldblatt translation (into intuitionistic KTB). These are syntactic preservation/reflection results between independently presented systems; no step reduces a claimed prediction or embedding to a fitted parameter, self-citation chain, or definitional renaming. The derivations rest on the explicit rule sets and translation clauses rather than on any prior result by the same authors that would render the central claims tautological.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

No free parameters or invented entities; the work rests on standard logical definitions and axioms for natural deduction and modal logics.

axioms (2)
  • domain assumption Introduction and elimination rules for conjunction, disjunction, negation, and quantifiers define fundamental logic in Fitch-style natural deduction.
    This is the base definition of fundamental logic invoked in the abstract.
  • standard math Standard semantics and properties of classical modal logics S4 and KTB.
    These are the target systems for the translations and embeddings.

pith-pipeline@v0.9.1-grok · 5702 in / 1188 out tokens · 49629 ms · 2026-06-30T03:42:51.277070+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

16 extracted references · 13 canonical work pages

  1. [1]

    Aguilera & G

    doi: 10.1098/rspa.2025.0628. Agostinho Almeida. Canonical extensions and relational representations of lattices with negation.Studia Logica, 91(2):171–199,

    work page doi:10.1098/rspa.2025.0628 2025

  2. [2]

    Rodrigo Nicolau Almeida

    doi: 10.1007/s11225-009-9171-8. Rodrigo Nicolau Almeida. Polyatomic logics and generalized Blok-Esakia theory.Journal of Logic and Computation, 34(5):887–935,

    work page doi:10.1007/s11225-009-9171-8

  3. [3]

    doi: 10.1007/978-94-017-0460-1

    work page doi:10.1007/978-94-017-0460-1

  4. [4]

    URLhttps: //prooftheory.blog/2022/08/19/brouwer-meets-kripke-constructivising-modal-logic/. A. G. Dragalin.Mathematical Intuitionism: Introduction to Proof Theory. Translations of Mathematical Monographs. American Mathematical Society, Providence, Rhode Island,

    2022

  5. [5]

    Relational representation theorems for general lattices with negations

    Wojciech Dzik, Ewa Orlowska, and Clint van Alten. Relational representation theorems for general lattices with negations. InRelations and Kleene Algebra in Computer Science. RelMiCS 2006, volume 4136 of Lecture Notes in Computer Science, pages 162–176. Springer, 2006a. doi: 10.1007/11828563

    work page doi:10.1007/11828563 2006

  6. [6]

    Relational representation theorems for lattices with negations: A survey.Lecture Notes in Artificial Intelligence, 4342:245–266, 2006b

    Wojciech Dzik, Ewa Orlowska, and Clint van Alten. Relational representation theorems for lattices with negations: A survey.Lecture Notes in Artificial Intelligence, 4342:245–266, 2006b. doi: 10.1007/11964810

    work page doi:10.1007/11964810

  7. [7]

    doi: 10.1007/978-3-030-12096-2

    ISBN 978-3-030- 12096-2. doi: 10.1007/978-3-030-12096-2. Gis` ele Fischer Servi. Axiomatizations for some intuitionistic modal logics.Rendiconti del Seminario Matem- atico Universit` a e Politecnico di Torino, 42(3):179–194,

    work page doi:10.1007/978-3-030-12096-2

  8. [8]

    English translation in Szabo 1969, pp. 132-213. K. G¨ odel. Eine Interpretation des intuitionistischen Aussagenkalk¨ uls.Ergebnisse eines Mathematischen Kolloquiums, 4:39–40,

    1969

  9. [9]

    English translation in G¨ odel 1986, pp. 301-303. K. G¨ odel.Collected Works. Oxford University Press, New York,

    1986

  10. [10]

    Wesley H

    doi: 10.1007/BF00652069. Wesley H. Holliday. Compatibility and accessibility: lattice representations for semantics of non-classical and modal logics. In David Fern´ andez Duque and Alessandra Palmigiano, editors,Advances in Modal Logic, Vol. 14, pages 507–529. College Publications, London,

    work page doi:10.1007/bf00652069

  11. [11]

    Wesley H

    arXiv:2201.07098 [math.LO]. Wesley H. Holliday. A fundamental non-classical logic.Logics, 1(1):36–79,

    work page arXiv

  12. [12]

    Wesley H

    doi: 10.3390/logics1010004. Wesley H. Holliday. Modal logic, fundamentally. In Agata Ciabattoni, David Gabelaia, and Igor Sedl´ ar, editors,Advances in Modal Logic, Vol. 15, pages 423–446. College Publications, London,

    work page doi:10.3390/logics1010004

  13. [13]

    Wesley H

    arXiv:2403.14043 [math.LO]. Wesley H. Holliday. Preconditionals. In Igor Sedl´ ar, editor,The Logica Yearbook 2023, pages 59–77. College Publications, 2025a. arXiv:2402.02296 [math.LO]. 57 Wesley H. Holliday. Vagueness and the connectives. In Jialiang Yan, Mingming Liu, Dag Westerst˚ ahl, and Xiaolu Yang, editors,The Connectives in Logic and Language, vol...

    work page doi:10.1007/978-3-031-86054-6 2023

  14. [14]

    Bjarni J´ onsson and Alfred Tarski

    doi: 10.1007/s10992-024-09746-7. Bjarni J´ onsson and Alfred Tarski. Boolean Algebras with Operators. Part I.American Journal of Mathe- matics, 73:891–939,

    work page doi:10.1007/s10992-024-09746-7

  15. [15]

    arXiv:2406.10182 [math.LO]. J. C. C. McKinsey and A. Tarski. Some theorems about the sentential calculi of Lewis and Heyting.The Journal of Symbolic Logic, 13:1–15,

    work page arXiv

  16. [16]

    John Stuart Mill.A System of Logic, Ratiocinative and Inductive: Being a Connected View of the Principles of Evidence, and the Methods of Scientific Investigation

    doi: 10.2307/2268135. John Stuart Mill.A System of Logic, Ratiocinative and Inductive: Being a Connected View of the Principles of Evidence, and the Methods of Scientific Investigation. John W. Parker, London,

    work page doi:10.2307/2268135