Pith. sign in

REVIEW 2 major objections 5 minor 22 references

Swap Kripke models for deontic LFIs

T0 review · 2 major / 5 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read This paper establishes the first sound-and-complete swap Kripke semantics for the C^D_n hierarchy of deontic paraconsistent logics, including da Costa and Carnielli's 1986 system C^D_1.

desk verdict The paper delivers the first complete semantics for C^D_n, with a fixable seriality gap in the canonical model proof. read the letter →

arxiv 2506.06181 v1 pith:XJN2THET submitted 2025-06-06 cs.LO math.LO

Mahan Vaz , Marcelo E. Coniglio This is my paper
classification cs.LOmath.LO MSC 03B4503B53
keywords deonticlogicparaconsistentlogicsofformalinconsistencynondeterministicsemanticsswapstructuresKripkemodelsC^D_nhierarchyRNmatrices
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper argues that deontic paraconsistent logics built on Logics of Formal Inconsistency can be given a nondeterministic possible-worlds semantics by fusing swap structures with Kripke frames. Its target is the C^D_n hierarchy, the deontic extensions of da Costa's C_n logics, for which it presents, for the first time, a full axiomatization and a complete semantics, including the historical 1986 system C^D_1 of da Costa and Carnielli. The semantics is graded: plain Nmatrices handle systems without the da Costa axiom (cl), while restricted Nmatrices (RNmatrices) are needed once (cl) is present. If the argument is right, the oldest deontic paraconsistent systems finally have a model theory on which their proof theory and semantics provably coincide.

What carries the argument

The central object is the swap Kripke model, a Kripke frame whose worlds are evaluated not by ordinary valuations but by swap valuations into a multialgebra of snapshots. A snapshot is an (n+1)-tuple of bits recording the formula together with its successive paraconsistent negations; the admissible snapshots form the set $A_n=\{z\in 2^{n+1}: (\bigwedge_{i\le k} z_i)\vee z_{k+1}=1 \text{ for }1\le k\le n\}$, whose n+2 values are $T_n$, $t^n_0,\dots,t^n_{n-1}$, $F_n$. The obligation operator is nondeterministic: $v_w(O\alpha)\in\widetilde{O}(\{v_{w'}(\alpha): wRw'\})$, where $\widetilde{O}$ collects snapshots whose first coordinate is the meet of the first coordinates of the accessible values. The load-bearing mechanism is a set of restrictions on valuations that reproduces the restricted Nmatrix for C_n: if $v_w(\alpha)=t^n_0$ then $v_w(\alpha\wedge\neg\alpha)=T_n$; if $v_w(\alpha)=t^n_k$ then $v_w(\alpha\wedge\neg\alpha)\in I_n$ and $v_w(\alpha^1)=t^n_{k-1}$; and if $v_w(\alpha)\in\mathrm{Boo}_n$ then $v_w(O\alpha)\in\mathrm{Boo}_n$. These restrictions validate (cl), the consistency-propagation axioms, and the strong deontic axiom (D_n), while the unrestrained swap Kripke models already characterize the base system DmbC.

What would settle it

Check seriality of the canonical relation R^(n)_can in C^D_n: take any ψ-saturated set Δ and ask whether Den(Δ)={φ:Oφ∈Δ} can be extended to a saturated set. If for some n there is a saturated Δ with Den(Δ)⊢ψ for every ψ, then Δ has no successor, R^(n)_can is not serial, and the canonical model of Proposition 7.16 is not a swap Kripke model in the paper's own sense. A proof from axioms (D_n) and (bcn) would close the gap; a counterexample would overturn Theorem 7.17.

Watch

Extended reading notes

Core claim

On the paper's own terms, the discovery is a swap Kripke semantics for deontic LFIs: each world carries a nondeterministic valuation into a multialgebra of snapshots over the two-element Boolean algebra, and the obligation operator reads the meet of a formula's first coordinate across all accessible worlds. For the C^D_n hierarchy the paper proves, in Theorems 7.12 and 7.17, that for every set of formulas Γ and formula φ, $\Gamma\vdash_{C^D_n}\varphi$ iff $\Gamma\vDash_{C^D_n}\varphi$. This is the first complete semantic characterization of C^D_n for every n≥1; the case n=1 recovers da Costa and Carnielli's C^D_1, whose earlier bivaluation sketch is now replaced by a fully worked-out canonical model.

Load-bearing premise

The load-bearing premise is that every saturated set Δ in C^D_n has a successor under the canonical relation, i.e. that Den(Δ)={φ:Oφ∈Δ} can always be extended to a non-trivial saturated set; Proposition 7.16 asserts this seriality without proving it, and without it the canonical model is not a model in the paper's own definition.

Editorial extensions

If this is right

  • For every n≥1, the deducibility relation of C^D_n coincides exactly with semantic consequence over swap Kripke models, by Theorems 7.12 and 7.17.
  • The original da Costa-Carnielli system C^D_1, previously given only a sketch of bivaluation semantics, receives a full sound and complete model theory.
  • For DCila, the paper explicitly derives decidability from the RNmatrix decision procedure together with decidability of standard deontic logic; the same machinery is in place for the C^D_n models.
  • In strict swap Kripke models, the schema $O\alpha\to\neg O\neg\alpha$ is valid, so the two distinct notions of permission available in the non-strict systems collapse into one.
  • The C^D_n systems formalize moral dilemmas with conflicting obligations of increasing strength without trivialization, using the hierarchy's multiple negations to distinguish weak from strong prohibitions.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The paper's construction is modular: the swap-structure layer fixes the propositional base, and the valuation restrictions are added per axiom, so the same recipe should yield semantics for other LFI hierarchies and for non-deontic modal expansions, a step the authors do not take.
  • The moral-dilemma discussion suggests a quantitative reading the paper leaves implicit: as n grows, C^D_n tolerates deeper layers of contradiction before deontic explosion, so the hierarchy can be read as grading dilemma severity rather than merely offering stronger systems.
  • A direct testable extension would be to extract labelled or tableaux rules from the canonical swap Kripke model to obtain a proof system for C^D_n suitable for implementation, since the completeness proof is constructive.
  • If the missing seriality proof cannot be supplied, the completeness theorem would still hold for the class of swap Kripke models with a non-emptiness condition on the canonical relation, at the cost of a slightly weaker claim.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 5 minor

Summary. The paper introduces 'swap Kripke models', a combination of swap structures (nondeterministic matrices) with Kripke frames, and uses them to give sound and complete semantics for a family of deontic LFIs. It treats DmbC, several extensions (DmbCciw, DmbCci, DbC, DCi), the systems with the da Costa axiom (DmbCcl, DCila), the original da Costa–Carnielli system C^D_1, and the C^D_n hierarchy. For C^D_n the paper claims, for the first time, a full axiomatization and a complete semantics. The technical development is based on ψ-saturated sets, canonical models, and restricted valuations that emulate RNmatrices. The DmbC section is worked out in full detail; later sections rely increasingly on adaptations of that construction.

Significance. If the results are correct, this is a substantial contribution: it provides the first complete semantics for the C^D_n hierarchy, including the historical C^D_1, and it extends the RNmatrix program for da Costa's C_n logics to a modal deontic setting. The paper gives explicit soundness and completeness arguments for DmbC, and it identifies precisely which valuation restrictions are needed to validate (cl), (ca#), (POn), and the several forms of the deontic axiom. The discussion of why the standard (D) axiom fails for n≥2 without extra restrictions is illuminating. The reliance on [11] for the propositional base is acceptable because that work is published and includes decision procedures; I see no circularity in that transfer.

major comments (2)
  1. [Section 7, Proposition 7.16 and Theorem 7.17] The proof that M_n is a swap Kripke model for C^D_n verifies the truth lemma, the valuation clauses, and the extra restrictions, but it never proves that R_can^(n) is serial. Seriality is part of the definition of a swap Kripke pre-model (Definition 7.3) and is inherited by Definition 7.9; without seriality, the set {v^n_{Δ'}(α) : Δ R_can^(n) Δ'} may be empty and the multioperator Õ in Definition 7.2 is undefined. In the DmbC case the corresponding fact is proved explicitly in Proposition 2.17; for C^D_n the analogous argument is absent. A repair should show that Den(Δ) is consistent, using (D_n) and (bcn), and then extend Den(Δ) to a saturated set; this is likely to work, but it must be supplied before Theorem 7.17 can be accepted as proved.
  2. [Section 7, opening paragraphs] The paper claims a full axiomatization of the C^D_n hierarchy, yet it never states in a single place the axiom system for C^D_n when n≥2. The reader must assemble it from the C_n axioms cited from [11], the schemas (D_n) and (PO_n), and the rules Modus Ponens and O-necessitation. Please add an explicit definition of the logic C^D_n (including the case n=1) before the soundness theorem, so that the derivability relation ⊢_{C^D_n} is unambiguous.
minor comments (5)
  1. [Abstract] The abstract contains the typo 'swap Kripe models'; it should read 'swap Kripke models'.
  2. [Definition 7.3, item 2] The set '#∈{∧,→ ¬}' appears to be a typo; it should be '#∈{∧,∨,→}'. A related typo occurs in the proof of Proposition 7.16, where the clause for α#β writes 'v^n_Δ(α#β)∈v^n_Δ(α) ˜# v^n_Δ(α)' instead of using v^n_Δ(β) as the second argument.
  3. [Section 7, hierarchy definition] Please state explicitly how C^D_1 from Section 6 fits the uniform definition for n≥2; the sentence 'the case where n=1 was already studied' does not clarify whether the axiom schemas (D_1) and (PO_1) coincide with the system used in Section 6, which is formulated with (O−E) and (caO)'.
  4. [Theorems 4.8 and 5.6] The completeness proofs for DmbCcl and DCila are one-sentence references to the canonical model propositions. Since Propositions 4.7 and 5.5 carry the main technical burden, this is acceptable, but a brief explanation of how the additional restricted-valuation conditions are verified in those canonical models would improve readability.
  5. [Lemma 7.13, item 10] The proof of item 10 says 'proven as in the previous cases,' but the seriality of the canonical relation is not a consequence of that item alone; it must be proved separately (see the first major comment).

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the C^D_n derivation is a standard soundness/completeness construction; the only author-overlapping citation [11] is independent published work, and the seriality gap in Proposition 7.16 is a proof omission, not a circular reduction.

full rationale

The paper's central claims are proven by the usual route: a non-deterministic semantics is defined from swap structures (Definitions 2.3–2.6, 7.2–7.5) and completeness is obtained from ψ-saturated canonical models (Definitions 2.11–2.15, 7.13–7.14). No step equates a predicted consequence with a fitted input: the valuations v_n^Δ are fixed by membership in saturated sets, and the semantic clauses are not defined in terms of the derivability relation. The only author-overlapping citation is [11] (Coniglio and Toledo), invoked for the RNmatrix characterization of the non-modal C_n fragment, including the truth values A_n, the restricted valuation table, and validity of the propositional axioms (Theorem 7.12, Remark 11, Definition 7.5). This is a published, peer-reviewed result with decision procedures, and its assumptions do not include the modal completeness theorem or the swap Kripke models; it therefore counts as independent support rather than load-bearing self-citation. A genuine gap exists, but it is a correctness gap, not a circularity: Proposition 7.16 asserts that the canonical structure M_n is a swap Kripke model, yet it never proves the seriality of R_can^(n), which Definition 7.3 requires for the multioperator Õ to be defined; the DmbC analogue (Proposition 2.17) contains an explicit seriality argument that is absent here. This omission does not reduce a conclusion to its premise, and the missing argument is plausibly recoverable from (D_n) and (bcn), as the reader's analysis notes. Accordingly, no circular step is exhibited and the circularity score is 0.

Assumptions & free parameters 0 free parameters · 4 assumptions · 2 invented entities

No numerical constants are fitted. The paper's central claims rest on standard saturation lemmas, on the published RNmatrix results in [11] (partly self-cited), and on the unstated but likely provable seriality of the canonical relation for C^D_n. The new formal entities are precisely defined and supported by the paper's own theorems, so they do not resemble unexplained physical postulates.

assumptions (4)
  • standard math Classical metatheory (ZFC) and Lindenbaum-style saturation: every non-derivable pair can be extended to a ψ-saturated set.
    Used throughout the canonical model constructions; stated as Remark 7.
  • domain assumption The RNmatrix characterization of C_n from Coniglio and Toledo [11] is correct, including the restricted valuations of Definitions 7.5.
    Soundness of the non-modal axioms of C^D_n is delegated to [11] in Theorem 7.12 and Remark 11; one of the authors of [11] is a co-author of this paper.
  • domain assumption The deduction metatheorem and proof-by-cases hold for DmbC and its extensions.
    Used to manipulate derivations from premises (Definition 2.2) and cited from Coniglio [12].
  • domain assumption Seriality of the canonical relation R^(n)_can for C^D_n.
    Required by Definition 7.3 but never proved; asserted in Proposition 7.16.
invented entities (2)
  • Swap Kripke model
    purpose: Semantic framework combining swap structures (snapshots) with Kripke frames, one nondeterministic valuation per world.
    The notion is defined in Definition 2.6 and used throughout; its only evidence is the soundness and completeness theorems proved in the paper, so it has no independent external confirmation.
  • Restricted valuation conditions for C^D_n (Definitions 7.5 and 7.9)
    purpose: Simulate the restricted Nmatrix for C_n at the level of world valuations, needed to validate axioms (cl) and (PO_n).
    The restrictions are justified by appeal to the RNmatrix characterization in [11], which is prior published work by one of the authors.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Swap Kripke models for deontic LFIs." pith.science (2026). https://pith.science/paper/XJN2THET

@misc{pith2026250606181,
  author       = {Pith},
  title        = {Pith review of: Swap Kripke models for deontic LFIs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/XJN2THET}},
  note         = {Machine review of arXiv:2506.06181}
}
abstract

We present a construction of nondeterministic semantics for some deontic logics based on the class of paraconsistent logics known as Logics of Formal Inconsistency (LFIs), for the first time combining swap structures and Kripke models through the novel notion of swap Kripe models. We start by making use of Nmatrices to characterize systems based on LFIs that do not satisfy axiom (cl), while turning to RNmatrices when the latter is considered in the underlying LFIs. This paper also presents, for the first time, a full axiomatization and a semantics for the $C^{D}_n$ hierarchy, by use of the aforementioned mixed semantics with RNmatrices. This includes the historical system $C^{D}_1$ of da Costa-Carnielli (1986), the first deontic paraconsistent system proposed in the literature.

Figures

Figures reproduced from arXiv: 2506.06181 by the authors.

Figure 1
Figure 1. A representation of a counterexample to (caO)’, when not adding the suitable restrictions to the models. According to this model, (α ◦ )(1,w) = 1. But this does not say anything about any of the worlds w ′ accessible to w. Notice that v DC1 w ((Oα) ◦ ) ∈ D/ if and only if v DC1 w (Oα) ∈ D and v DC1 w (¬Oα) ∈ D. But this is perfectly possible, since when assigning a truth value for Oα, only the first coordinate of th… view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

22 extracted references · 21 canonical work pages

  1. [11]

    Coniglio and Guilherme V

    Marcelo E. Coniglio and Guilherme V . Toledo. Two decision procedures for da Costa’sC n logics based on restricted nmatrix semantics.Studia Logica, 110(3):601–642, 2022

    work page 2022

  2. [1]

    Non-deterministic semantics for logics with a consistency operator.International Journal of Approximate Reasoning, 45:271–287, 07 2007

    Arnon Avron. Non-deterministic semantics for logics with a consistency operator.International Journal of Approximate Reasoning, 45:271–287, 07 2007

    work page 2007

  3. [2]

    A completeness-proof method for extensions of the implica- tional fragment of the propositional calculus.Notre Dame Journal of Formal Logic, 21(3):509 – 517, 1980

    Diderik Batens. A completeness-proof method for extensions of the implica- tional fragment of the propositional calculus.Notre Dame Journal of Formal Logic, 21(3):509 – 517, 1980

    work page 1980

  4. [3]

    Paraconsistent extensional propositional logics.Logique et Analyse, 23(90/91):195–234, 1980

    Diderik Batens. Paraconsistent extensional propositional logics.Logique et Analyse, 23(90/91):195–234, 1980. 33

    work page 1980

  5. [4]

    A paraconsistent multi-agent frame- work for dealing with normative conflicts

    Mathieu Beirlaen and Christian Straßer. A paraconsistent multi-agent frame- work for dealing with normative conflicts. In João Leite, Paolo Torroni, Thomas Ågotnes, Guido Boella, and Leon van der Torre, editors,Compu- tational Logic in Multi-Agent Systems, pages 312–329, Berlin, Heidelberg,

    work page

  6. [5]

    Two semantical approaches to paraconsistent modali- ties.Logica Universalis, 4(1):137–160, 03 2010

    Juliana Bueno-Soler. Two semantical approaches to paraconsistent modali- ties.Logica Universalis, 4(1):137–160, 03 2010

    work page 2010

  7. [6]

    Coniglio.Paraconsistent Logic: Consis- tency, Contradiction and Negation

    Walter Carnielli and Marcelo E. Coniglio.Paraconsistent Logic: Consis- tency, Contradiction and Negation. Logic, Epistemology, and the Unity of Science. Springer Cham, 1 edition, 2016

    work page 2016

  8. [7]

    Coniglio, and João Marcos

    Walter Carnielli, Marcelo E. Coniglio, and João Marcos. Logics of formal in- consistency. In D.M. Gabbay and F. Guenthner, editors,Handbook of Philo- sophical Logic, pages 1–93. Springer Netherlands, Dordrecht, 2007

    work page 2007

Show all 22 references
  1. [8]

    Coniglio, Luis Fariñas del Cerro, and Newton M

    Marcelo E. Coniglio, Luis Fariñas del Cerro, and Newton M. Peron. Finite non-deterministic semantics for some modal systems.Journal of Applied Non-Classical Logics, 25(1):20–45, 2015

    2015

  2. [9]

    Coniglio and Ana Claudia Golzio

    Marcelo E. Coniglio and Ana Claudia Golzio. Swap structures semantics for Ivlev-like modal logics.Soft Computing, 23(7):2243–2254, 2019

    2019

  3. [10]

    Coniglio, Paweł Pawłowski, and Daniel Skurt

    Marcelo E. Coniglio, Paweł Pawłowski, and Daniel Skurt. Modal logics - RNmatrices vs. Nmatrices.Electronic Proceedings in Theoretical Computer Science, 415:138–149, December 2024

    2024

  4. [12]

    Logics of deontic inconsistency.Revista Brasileira de Filosofia, 233:162–186, 2009

    Marcelo Esteban Coniglio. Logics of deontic inconsistency.Revista Brasileira de Filosofia, 233:162–186, 2009. Preprint available for download athttps://www.cle.unicamp.br/eprints/index.php/CLE_ e-Prints/article/view/886

    2009

  5. [13]

    A paraconsistentist approach to Chisholm’s Paradox.Principia: An International Journal of Epistemology, 13(3):299–326, 2009

    Marcelo Esteban Coniglio and Newton Marques Peron. A paraconsistentist approach to Chisholm’s Paradox.Principia: An International Journal of Epistemology, 13(3):299–326, 2009

    2009

  6. [14]

    Newton C. A. da Costa and Walter A. Carnielli. On paraconsistent deontic logic.Philosophia, 16(3-4):293–305, 1986

    1986

  7. [15]

    Truth tables for modal logics T and S4, by using three- valued non-deterministic level semantics.Journal of Logic and Computation, 32(1):129–157, 12 2021

    Lukas Grätz. Truth tables for modal logics T and S4, by using three- valued non-deterministic level semantics.Journal of Logic and Computation, 32(1):129–157, 12 2021. 34

    2021

  8. [16]

    Coniglio

    Renato Leme, Carlos Olarte, Elaine Pimentel, and Marcelo E. Coniglio. The modal cube revisited: Semantics without worlds, 2025

    2025

  9. [17]

    Phd thesis, University of Minnesota, De- cember 2007

    Casey McGinnis.Paraconsistency and deontic logic: Formal systems for reasoning with normative conflicts. Phd thesis, University of Minnesota, De- cember 2007

    2007

  10. [18]

    More modal semantics without possible worlds.IFCoLog Journal of Logic and its Applications, 3(5), October 2016

    Hitoshi Omori and Daniel Skurt. More modal semantics without possible worlds.IFCoLog Journal of Logic and its Applications, 3(5), October 2016

    2016

  11. [19]

    Pawel Pawlowski and Daniel Skurt.□and♢in Eight-Valued Non- Deterministic Semantics for Modal Logics.Journal of Logic and Compu- tation, page exae010, 03 2024

    2024

  12. [20]

    Peron and Marcelo Esteban Coniglio

    Newton M. Peron and Marcelo Esteban Coniglio. Logics of deontic incon- sistencies and paradoxes.CLE e-prints, 8(6):10, 2008

    2008

  13. [21]

    Modeling deontic inconsistencies in moral dilemmas.Perspectiva Filosófica, forthcoming

    Mahan Vaz and Gabriel Maruchi. Modeling deontic inconsistencies in moral dilemmas.Perspectiva Filosófica, forthcoming. MAHANVAZ Instituto de Filosofia e Ciências Humanas (IFCH), and Institut für Philosophie I, Logik und Erkenntnistheorie Universidade Estadual de Campinas (UNIC...

  14. [2011]

    Springer Berlin Heidelberg

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.