Axiomatizing logics of finite G\"odel-Kripke models

Amanda Vidal; Ricardo O. Rodriguez

arxiv: 2605.15810 · v1 · pith:YYYSENF7new · submitted 2026-05-15 · 🧮 math.LO

Axiomatizing logics of finite G\"odel-Kripke models

Amanda Vidal , Ricardo O. Rodriguez This is my paper

Pith reviewed 2026-05-19 19:46 UTC · model grok-4.3

classification 🧮 math.LO

keywords modal Gödel logicfinite Kripke modelscompletenessaxiomatizationwitnessing conditionsintermediate logics

0 comments

The pith

Natural axiomatic extensions fail to restore completeness for modal Gödel logics over finite Gödel-Kripke models.

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

The paper investigates completeness for modal Gödel logics with respect to finite Gödel-Kripke models. It shows that the logics studied in earlier works are incomplete for these finite structures and that the natural candidate axiomatic extensions do not fix the problem. This resolves a fifteen-year open problem. The authors then introduce new axiomatizations that achieve completeness for finite models while also characterizing certain intermediate witnessing conditions satisfied by the basic logics.

Core claim

The logics studied in prior works fail to be complete with respect to finite Gödel-Kripke models, and the natural candidate axiomatic extensions do not restore this completeness. New axiomatizations are provided that achieve completeness for finite models and characterize intermediate witnessing conditions that hold for the basic logics.

What carries the argument

New axiomatizations for modal Gödel logics that ensure completeness over finite Gödel-Kripke models by enforcing appropriate witnessing conditions.

Load-bearing premise

The modal Gödel logics from the referenced earlier studies form the right base systems and finite Gödel-Kripke models are the intended class of structures for seeking completeness.

What would settle it

A proof that any one of the natural candidate axiomatic extensions is actually complete with respect to all finite Gödel-Kripke models, or an explicit finite counter-model showing that one of the new axiomatizations is still incomplete.

read the original abstract

We investigate completeness for modal G\"odel logics with respect to finite G\"odel-Kripke models, along with related aspects. It is well known that the logics studied in [4, 11] fail to be complete with respect to finite G\"odel-Kripke models. We show that the natural candidate axiomatic extensions do not restore completeness, thereby resolving a 15 year open problem posed in the aforementioned works. We then provide new axiomatizations that are complete for finite models and characterize intermediate witnessing conditions that hold for the basic logics.

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.

Desk Editor's Note private letter to a colleague

Natural extensions fail to restore completeness for finite Gödel-Kripke models, resolving the open problem, while new axiomatizations succeed.

read the letter

Hey, I took a look at this arXiv paper on axiomatizing logics of finite Gödel-Kripke models by Vidal and Rodriguez. The punchline is that the natural candidate axiomatic extensions of the modal Gödel logics don't restore completeness with respect to finite models, which resolves the 15-year open problem mentioned in the earlier works. On the positive side, they introduce new axiomatizations that are complete for those finite models and that characterize some intermediate witnessing conditions for the basic logics. What the paper does well is deliver a clear negative result through counterexamples to the obvious extensions, plus constructive new systems with soundness and completeness. This isn't just incremental; it actively rules out a path that had been open and provides workable alternatives. The citation to the original papers is spot on, and the focus on finite models seems deliberate given the context of the open question. Where it might be soft is in the narrow scope. Everything is anchored to the specific logics studied in references [4,11], so if the field has moved on to other variants or cares more about general or infinite cases, this might not have wide ripple effects. The proofs are likely technical with specific model constructions, and while the abstract presents them cleanly, one would want to verify the details in the full text for any hidden assumptions about the model class. But overall, no load-bearing flaws jump out. This paper is for researchers working in modal many-valued logics and related areas of non-classical logic. A reader interested in completeness results, axiomatizations for restricted model classes, or finite-model reasoning in Gödel logics would get real value from the new systems and the settled open problem. It has enough original content and evidential support to deserve a serious referee rather than a desk reject. My recommendation is to send it out for peer review.

Referee Report

1 major / 2 minor

Summary. The manuscript investigates completeness for modal Gödel logics with respect to finite Gödel-Kripke models. It establishes that the logics studied in [4,11] fail to be complete for this class, shows that natural candidate axiomatic extensions likewise fail to restore completeness (resolving a 15-year open problem), and supplies new axiomatizations that are complete for finite models while characterizing intermediate witnessing conditions satisfied by the base logics.

Significance. If the counterexamples and soundness/completeness arguments hold, the work supplies a definitive negative answer to the natural extensions and positive axiomatizations for the finite-model semantics. This resolves a concrete open question in modal extensions of Gödel logic and provides explicit characterizations of witnessing conditions, which are likely to be useful for further investigations of finite-model properties in fuzzy modal logics.

major comments (1)

The counterexamples to completeness for the natural extensions (presumably in the section following the preliminaries) must be checked for explicitness: each finite Gödel-Kripke model should be given with its underlying Gödel algebra, accessibility relation, and a direct verification that the model satisfies the candidate axioms yet falsifies the target formula.

minor comments (2)

Abstract: the phrase 'the aforementioned works' should be replaced by explicit citations to [4] and [11] for immediate clarity.
Notation for the new axioms and witnessing conditions should be introduced with a short table or list that cross-references the corresponding semantic clauses.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful reading of the manuscript and the positive recommendation for minor revision. The suggestion to enhance the explicitness of the counterexamples is well taken, and we will revise the manuscript accordingly.

read point-by-point responses

Referee: The counterexamples to completeness for the natural extensions (presumably in the section following the preliminaries) must be checked for explicitness: each finite Godel-Kripke model should be given with its underlying Godel algebra, accessibility relation, and a direct verification that the model satisfies the candidate axioms yet falsifies the target formula.

Authors: We agree that greater explicitness will improve readability and verifiability. In the revised manuscript we will expand the relevant section (immediately following the preliminaries) to present each finite Godel-Kripke model in full detail: the underlying Godel algebra will be specified by its carrier set and operations, the accessibility relation will be given explicitly as a binary relation on the set of worlds, and we will supply a direct, step-by-step verification that the model satisfies the candidate axioms while falsifying the target formula. These additions will make the counterexamples self-contained. revision: yes

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper establishes its central results through explicit counterexamples showing incompleteness of natural axiomatic extensions for finite Gödel-Kripke models and through direct soundness and completeness proofs for the newly proposed axiomatizations. These steps rely on standard logical constructions and semantic arguments that do not reduce by definition or construction to fitted parameters, self-referential definitions, or load-bearing self-citations whose validity depends on the present work. The starting logics from prior references are treated as given inputs, and the resolution of the open problem is achieved via independent verification against the target finite model class.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The work rests on standard background assumptions of modal logic and Gödel semantics; no free parameters or invented entities are mentioned in the abstract.

axioms (1)

domain assumption The logics under study are modal extensions of Gödel logic as defined in the cited references.
Taken as given from the prior literature referenced in the abstract.

pith-pipeline@v0.9.0 · 5611 in / 1116 out tokens · 44921 ms · 2026-05-19T19:46:42.267359+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/AbsoluteFloorClosure.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

We show that the natural candidate axiomatic extensions do not restore completeness... new axiomatizations that are complete for finite models and characterize intermediate witnessing conditions
IndisputableMonolith/Foundation/ArithmeticFromLogic.lean LogicNat unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

Definition 2.1. A Gödel-Kripke model... witnessed whenever for each 2φ,3φ, e(v,2φ) := ... for some v2φ,v3φ

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

15 extracted references · 15 canonical work pages · 1 internal anchor

[1]

Baaz and R

M. Baaz and R. Iemhoff. Skolemization in intermediate logics with the finite model property.Logic Journal of the IGPL, 24(3):224–237, 2016

work page 2016
[2]

F. Bou, F. Esteva, L. Godo, and R.O. Rodriguez. Possibilistic semantics for a modal KD45 extension of G¨ odel fuzzy logic. In J. P. et. at. Carvalho, editor,IPMU, pages 123–135, Cham, 2016. Springer International Publishing

work page 2016
[3]

Caicedo, G

X. Caicedo, G. Metcalfe, R.O. Rodriguez, and J. Rogger. Decidability of order-based modal logics. Journal of Computer and System Sciences, 88:53 – 74, 2017

work page 2017
[4]

Caicedo and R.O

X. Caicedo and R.O. Rodriguez. Standard G¨ odel modal logics.Studia Logica, 94(2):189–214, 2010

work page 2010
[5]

Caicedo and R.O

X. Caicedo and R.O. Rodriguez. Bi-modal G¨ odel logic over [0, 1]-valued Kripke frames.Journal of Logic and Computation, 25(1):37–55, 2015

work page 2015
[6]

Ferrari, C

M. Ferrari, C. Fiorentini, P. Giardini, and R.O. Rodriguez. G¨ odel modal logic over witnessed models. InAdvances in Modal Logic 2026, page 0, Amsterdam, 2026. Springer Nature Switzerland

work page 2026
[7]

Ferrari, C

M. Ferrari, C. Fiorentini, and R.O. Rodriguez. A g¨ odel modal logic over witnessed crisp models. In Gian Luca Pozzato and Tarmo Uustalu, editors,Automated Reasoning with Analytic Tableaux and Related Methods, pages 141–160, Cham, 2026. Springer Nature Switzerland

work page 2026
[8]

Fischer-Servi

G. Fischer-Servi. Axiomatizations for some intuitionistic modal logics.Rend. Sem. Mat. Univ. Politec. Torino, 42:179–194, 1984

work page 1984
[9]

A. Horn. FreeL-algebras.Journal of Symbolic Logic, 34:475–480, 1969

work page 1969
[10]

R. Iemhoff. The eskolemization of universal quantifiers.Annals of Pure and Applied Logic, 162(3):201–212, 2010. Special Issue: Dedicated to Nikolai Alexandrovich Shanin on the occasion of his 90th birthday

work page 2010
[11]

Metcalfe and N

G. Metcalfe and N. Olivetti. Proof systems for a G¨ odel modal logic. In M. Giese and A. Waaler, editors,Proceedings of TABLEAUX 2009, volume 5607 ofLNAI. Springer, 2009

work page 2009
[12]

Metcalfe and N

G. Metcalfe and N. Olivetti. Towards a proof theory of G¨ odel modal logics.Logical Methods in Computer Science, 7(2):27, 2011

work page 2011
[13]

Rodriguez and A

R.O. Rodriguez and A. Vidal. Axiomatization of Crisp G¨ odel Modal Logic.Studia Logica, 109:367–395, 2021

work page 2021
[14]

A. Vidal. On the local consequence of modal product logic: standard completeness and decidability. (To appear in) Annals of Pure and Applied Logic, 2026.https://arxiv.org/abs/2306.13903

work page internal anchor Pith review Pith/arXiv arXiv 2026
[15]

Zhang and M

H. Zhang and M. Zhang. Model-characterizing formulas and normal forms in godel logics. In37th International Symposium on Multiple-Valued Logic (ISMVL’07), pages 3–3, 2007. 17

work page 2007

[1] [1]

Baaz and R

M. Baaz and R. Iemhoff. Skolemization in intermediate logics with the finite model property.Logic Journal of the IGPL, 24(3):224–237, 2016

work page 2016

[2] [2]

F. Bou, F. Esteva, L. Godo, and R.O. Rodriguez. Possibilistic semantics for a modal KD45 extension of G¨ odel fuzzy logic. In J. P. et. at. Carvalho, editor,IPMU, pages 123–135, Cham, 2016. Springer International Publishing

work page 2016

[3] [3]

Caicedo, G

X. Caicedo, G. Metcalfe, R.O. Rodriguez, and J. Rogger. Decidability of order-based modal logics. Journal of Computer and System Sciences, 88:53 – 74, 2017

work page 2017

[4] [4]

Caicedo and R.O

X. Caicedo and R.O. Rodriguez. Standard G¨ odel modal logics.Studia Logica, 94(2):189–214, 2010

work page 2010

[5] [5]

Caicedo and R.O

X. Caicedo and R.O. Rodriguez. Bi-modal G¨ odel logic over [0, 1]-valued Kripke frames.Journal of Logic and Computation, 25(1):37–55, 2015

work page 2015

[6] [6]

Ferrari, C

M. Ferrari, C. Fiorentini, P. Giardini, and R.O. Rodriguez. G¨ odel modal logic over witnessed models. InAdvances in Modal Logic 2026, page 0, Amsterdam, 2026. Springer Nature Switzerland

work page 2026

[7] [7]

Ferrari, C

M. Ferrari, C. Fiorentini, and R.O. Rodriguez. A g¨ odel modal logic over witnessed crisp models. In Gian Luca Pozzato and Tarmo Uustalu, editors,Automated Reasoning with Analytic Tableaux and Related Methods, pages 141–160, Cham, 2026. Springer Nature Switzerland

work page 2026

[8] [8]

Fischer-Servi

G. Fischer-Servi. Axiomatizations for some intuitionistic modal logics.Rend. Sem. Mat. Univ. Politec. Torino, 42:179–194, 1984

work page 1984

[9] [9]

A. Horn. FreeL-algebras.Journal of Symbolic Logic, 34:475–480, 1969

work page 1969

[10] [10]

R. Iemhoff. The eskolemization of universal quantifiers.Annals of Pure and Applied Logic, 162(3):201–212, 2010. Special Issue: Dedicated to Nikolai Alexandrovich Shanin on the occasion of his 90th birthday

work page 2010

[11] [11]

Metcalfe and N

G. Metcalfe and N. Olivetti. Proof systems for a G¨ odel modal logic. In M. Giese and A. Waaler, editors,Proceedings of TABLEAUX 2009, volume 5607 ofLNAI. Springer, 2009

work page 2009

[12] [12]

Metcalfe and N

G. Metcalfe and N. Olivetti. Towards a proof theory of G¨ odel modal logics.Logical Methods in Computer Science, 7(2):27, 2011

work page 2011

[13] [13]

Rodriguez and A

R.O. Rodriguez and A. Vidal. Axiomatization of Crisp G¨ odel Modal Logic.Studia Logica, 109:367–395, 2021

work page 2021

[14] [14]

A. Vidal. On the local consequence of modal product logic: standard completeness and decidability. (To appear in) Annals of Pure and Applied Logic, 2026.https://arxiv.org/abs/2306.13903

work page internal anchor Pith review Pith/arXiv arXiv 2026

[15] [15]

Zhang and M

H. Zhang and M. Zhang. Model-characterizing formulas and normal forms in godel logics. In37th International Symposium on Multiple-Valued Logic (ISMVL’07), pages 3–3, 2007. 17

work page 2007