REVIEW 1 major objections 6 minor 20 references
Effective Finite-Valued Approximations of General Propositional Logics
T0 review · 1 major / 6 minor · reviewed 2026-08-14 · deepseek-v4-flash
Pith's one-line read For every Hilbert calculus in a natural rule format, the optimal finite-valued approximation is computable.
desk verdict Solid, correct paper on finite-valued approximations of Hilbert calculi; send it to a referee, but fix the abstract's singular 'minimal' and the reversed monotonicity in Prop. 34. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The load-bearing object is the cover of a calculus: a finite-valued logic M for which the calculus is strongly sound, meaning every axiom evaluates to a designated truth value and every rule preserves designation under every valuation. Strong soundness is the right notion because, unlike mere soundness, it is decidable by truth-table checking, and it yields the many-valued closure $\mathrm{MC}(C)$, the intersection of the tautology sets of all covers. The technical tools are the product of two finite-valued logics, whose tautologies are exactly the intersection of the two tautology sets; the formula-as-truth-value finite logics $M_{i,j}(L)$, whose truth values are formula fragments and which separate any non-member of $L$ from $L$; and a depth bound of the form $m^{m^m+1}-1$ showing that if one finite-valued logic is not contained in another, a witness formula of bounded depth exists. These pieces make the optimal-cover search decidable and supply the construction of sequential approximations.
What would settle it
Find a strictly analytic calculus (in the paper's Definition 7) and a formula it does not prove that is nevertheless a tautology of every finite-valued cover; Corollary 41 asserts no such pair exists, and the proof says the cover $M_{\mathrm{dp}(F),j}(\mathrm{Thm}(C))$ should falsify the formula.
Extended reading notes
Core claim
The central claim is that, for any propositional Hilbert-type calculus C of the kind defined in the paper (finitely many axioms and rules of the form A1,...,An / C, with no side conditions), and for any fixed number m of truth values, the best finite-valued approximations of C can actually be computed. A finite-valued logic M is a cover of C when C is strongly sound for M: every axiom is a tautology and every rule instance preserves designated truth values. The paper proves that the m-valued covers that are minimal with respect to tautology inclusion are computable, because it is decidable whether one finite-valued logic has a tautology not shared by another. It defines the many-valued closure MC(C) as the set of formulas true in every cover, shows that MC(C) always has an effective sequential approximation, and proves that for strictly analytic calculi—those whose rules never introduce variables and never increase formula depth under substitution—MC(C) equals the theorem set of C. For undecidable calculi, the paper shows no effective sequential approximation can exist.
Load-bearing premise
All theorems assume a calculus whose rules have the simple shape 'from premises A1,...,An infer C', with no side conditions and with every variable in a premise also present in the conclusion; sequent-style or modal-necessitation rules do not automatically fall under the results.
Editorial extensions
If this is right
- The classic many-valued method of proving non-derivability becomes automatable: for any calculus of the restricted format and any m, the minimal m-valued covers can be computed, so proposed non-theorems can be checked against the best finite-valued approximations.
- Strictly analytic calculi receive a uniform finite-valued semantics: every non-theorem is falsified by some cover, so their theorem set equals their many-valued closure.
- Undecidable propositional calculi cannot be approximated from above by any effective sequence of finite-valued logics; their many-valued closure is always a proper superset of their theorems.
- Every decidable substitution-closed logic has an effective sequence of finite-valued logics whose intersection is exactly the logic, independent of how the logic is presented.
- Modal logics with the finite model property yield sequential approximations by coding finite Kripke models as finite-valued matrices, and this approximation is effective whenever the finite models are effectively enumerable.
Reading between the lines
- The depth bound behind computability is enormous, so the practical route suggested by the paper is to restrict attention to small m or to syntactically special rule classes; the paper leaves the complexity of optimal-cover computation open.
- For modal logics with the finite model property, the Kripke-model translation suggests a recipe for building approximate semantics directly from finite countermodels, then taking products; this may give smaller matrices than the standard chain-valued examples.
- Because the paper measures approximation quality by tautology inclusion, an alternative metric—such as minimizing the number of truth values or number of designated values—could lead to different 'optimal' covers; the paper notes that not every approximable logic is approximable by matrices with a single designated value.
Signed reviews
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper investigates to what extent propositional logics presented as Hilbert calculi in a restricted rule format can be approximated by finite-valued logics. It defines covers (strong soundness) and t-soundness, proves that strong and t-soundness are decidable (Props. 21 and 22) while weak soundness is undecidable (Prop. 20), and shows that the relation "has no more tautologies than" between finite-valued logics is decidable via an explicit depth bound (Thm. 28). It then shows that the minimal m-valued covers of a calculus under the relation ⊳ are computable (Prop. 30), studies effective sequential approximations and the many-valued closure MC(C), and proves that strictly analytic calculi satisfy MC(C) = Thm(C) (Cor. 41). The main theorems are proved in detail with explicit finite bounds.
Significance. The paper's central results are interesting and, apart from the issue in Prop. 15 discussed below, the proofs are largely correct. The decidability of t-soundness (Prop. 22) and the depth bound in Thm. 28 provide useful tools for automating Bernays-style independence proofs; Prop. 30 answers a natural question about optimal covers; Cor. 41 gives a clean sufficient condition for the many-valued closure to coincide with the theorem set. The paper is self-contained and includes explicit constructions, including the M_{i,j}(L) logics and the Kripke-model coding in Thm. 48. A significant limitation is the restrictive rule format of Def. 4; Remarks 5 and 6 explicitly acknowledge that sequent-style rules and side-formula modal rules fall outside the class, and the sketched encodings do not preserve strict analyticity. This scope restriction is honestly stated, but it narrows the generality promised by the title and abstract.
major comments (1)
- [Def. 14, Prop. 15] Proposition 15 is false as stated. The claim "otherwise A ∈ Taut(M_{i,j}(L))" for A ∉ Frm_{i,j}(L) fails when A has depth ≤ i but uses a variable not among X_1,...,X_j. For example, take L = ∅, i = 0, j = 1, and A = X_2. Since Frm_{0,1}(∅) = {X_1} and V^+ = {⊤}, the valuation v with v(X_2) = X_1 gives v(A) = X_1, which is not designated; hence A is not a tautology. The proofs of Prop. 34 and Cor. 41 cite Prop. 15, so this needs repair. The applications remain sound: for A ∈ Frm_{i,j}(L) the stated equivalence is correct, and the inclusion L ⊆ Taut(M_{i,j}(L)) follows from closure of L under substitution; for formulas of depth > i, every substitution instance has depth > i and hence evaluates to ⊤. I recommend either restricting the "otherwise" clause to the case dp(A) > i with variables restricted to X_1,...,X_j, or deleting it and stating the two correct claims separately.
minor comments (6)
- [Abstract] The abstract's phrase "the minimal m-valued logic" should be plural or indefinite, since Prop. 30 guarantees existence but not uniqueness of ⊳-minimal covers; multiple incomparable minima may exist.
- [Proof of Prop. 34] The proof states "Mi ⊴ Mi+1", but for the constructed sequence M_i = M_{i,i}(L) the inclusion goes in the opposite direction: Taut(M_{i+1}) ⊆ Taut(M_i), so M_{i+1} ⊴ M_i. This is consistent with Def. 32, and the intersection argument is unaffected, but the displayed relation should be corrected.
- [Def. 4] The sentence "A formula F is a theorem of L" should read "a theorem of C", since L denotes the language.
- [Proof of Prop. 20] The proof uses the same symbol C for the calculus and for a newly introduced propositional constant; this notational clash is confusing and should be resolved by renaming the constant.
- [Sec. 6] The opening sentence "Our brief discussion unfortunate must leave many interesting questions open" is ungrammatical and should be recast, e.g., "Our brief discussion unfortunately must leave many interesting questions open."
- [Title and abstract] The phrase "General Propositional Logics" overstates the scope established in Def. 4; Remarks 5 and 6 show that sequent-style rules and side-formula modal rules are not covered, and the encodings do not preserve strict analyticity. A prominent scope disclaimer in the abstract or introduction would bring the title in line with the actual results.
Circularity Check
No significant circularity: the paper's central results are derived from explicit constructions and independent decidability arguments, not from its own conclusions.
full rationale
The main derivation chain is self-contained and does not reduce to its inputs. Proposition 30 follows from Proposition 21 and Theorem 28, both of which are independent decidability results: strong soundness is checked by finite truth-table enumeration, and the ordering of many-valued logics is decided by a bounded-depth search using a standard counting argument on truth functions. Neither step presupposes that optimal covers exist or that MC(C)=Thm(C). Corollary 41 is also non-circular: for a non-theorem F it explicitly constructs M_{dp(F),j}(Thm(C)), a Lindenbaum-style finite-valued logic whose truth values are formulas of bounded depth and whose designated values are theorems of C; the proof then verifies directly that this matrix is strongly sound for C and falsifies F. This is an existence construction, not a fitted parameter renamed as a prediction. Proposition 34 and Corollary 35, while immediate from Definition 14, are presented as constructions rather than as independent empirical or mathematical discoveries, and they do not feed back into the central cover-computability or many-valued-closure claims. The Kripke-model approximation result in Theorem 48 is justified by the independent Lemma 46. The only self-citations are [3] and [4]; [4] is merely a pointer to a prior conference version, and [3] supports a side remark about proof lengths, so neither is load-bearing. The acknowledged scope restriction to Hilbert rules of the simple form in Definition 4 is an explicit limitation, not a circular step.
Assumptions & free parameters
assumptions (6)
- domain assumption Thm(C) is recursively enumerable for every Hilbert calculus C as defined in Def. 4.
- standard math Standard finite combinatorics (counting and pigeonhole) is valid.
- domain assumption Gödel logics are covers of IPC, Taut(G_{m+1}) is a subset of Taut(G_m), and the intersection is the infinite-valued Gödel logic G_ℵ.
- domain assumption Intuitionistic propositional logic and relevant modal logics have the finite model property; IPL is characterized by finite trees.
- domain assumption Lindenbaum's theorem: every propositional logic is the tautology set of some infinite-valued logic.
- domain assumption Gödel's double-negation translation: B is a classical tautology iff ¬¬B is an intuitionistic theorem.
Cite this review
Pith. "Pith review of Effective Finite-Valued Approximations of General Propositional Logics." pith.science (2026). https://pith.science/paper/OOATAXNB
@misc{pith2026190801200,
author = {Pith},
title = {Pith review of: Effective Finite-Valued Approximations of General Propositional Logics},
year = {2026},
howpublished = {\url{https://pith.science/paper/OOATAXNB}},
note = {Machine review of arXiv:1908.01200}
}
abstract
Propositional logics in general, considered as a set of sentences, can be undecidable even if they have "nice" representations, e.g., are given by a calculus. Even decidable propositional logics can be computationally complex (e.g., already intuitionistic logic is PSPACE-complete). On the other hand, finite-valued logics are computationally relatively simple - at worst NP. Moreover, finite-valued semantics are simple, and general methods for theorem proving exist. This raises the question to what extent and under what circumstances propositional logics represented in various ways can be approximated by finite-valued logics. It is shown that the minimal $m$-valued logic for which a given calculus is strongly sound can be calculated. It is also investigated under which conditions propositional logics can be characterized as the intersection of (effectively given) sequences of finite-valued logics.
Reference graph
Works this paper leans on
-
[1]
Avron, A.: The semantics and proof theory of linear logic. Theoret. Comput. Sci. 57 (1988) 161–184
work page 1988
-
[2]
Baaz, M., Ferm¨ uller, C.G., Salzer, G., Zach, R.: Labeled calculi and finite-valued logics. Studia Logica 61 (1998) 7–33
work page 1998
-
[3]
Baaz, M., Zach, R.: Short proofs of tautologies using the s chema of equivalence. In E. B¨ orger, et al., eds.: Computer Science Logic. CSL’93, Swansea, Wales. Selected Papers. LNCS 832, Berlin, Springer (1994) 33–35
work page 1994
-
[4]
In: 24th International Symposium on Multiple-valued Logic
Baaz, M., Zach, R.: Approximating propositional calculi by finite-valued logics. In: 24th International Symposium on Multiple-valued Logic . ISMVL’94, Boston. Proceedings. IEEE Press, Los Alamitos (1994) 257–263
work page 1994
-
[5]
Bernays, P.: Axiomatische Untersuchungen des Aussagenk alk¨ uls der “Principia Mathematica”. Math. Z. 25 (1926) 305–320
work page 1926
-
[6]
Carnielli, W.A.: Systematization of finite many-valued l ogics through the method of tableaux. J. Symbolic Logic 52 (1987) 473–493
work page 1987
-
[7]
Cambridge U niversity Press, Cam- bridge (1980)
Chellas, B.F.: Modal Logic: An Introduction. Cambridge U niversity Press, Cam- bridge (1980)
work page 1980
-
[8]
Dummett, M.: A propositional calculus with denumerable m atrix. J. Symbolic Logic 24 (1959) 97–106
work page 1959
Show all 20 references
-
[9]
Syn- these Library, vol
Gabbay, D.M.: Semantical Investigations in Heyting’s In tuitionistic Logic. Syn- these Library, vol. 148. Reidel, Dordrecht (1981)
1981
-
[10]
G¨ odel, K.: Zum intuitionistischen Aussagenkalk¨ ul. A nz. Akad. Wiss. Wien 69 (1932) 65–66
1932
-
[11]
Researc h Studies Press, Baldock (2001)
Gottwald, S.: A Treatise on Many-valued Logics. Researc h Studies Press, Baldock (2001)
2001
-
[12]
Oxford University Press, Oxford (1993)
H¨ ahnle, R.: Automated Deduction in Multiple-Valued Logics. Oxford University Press, Oxford (1993)
1993
-
[13]
In: Actes du Congr` es International de Philosophie Scientifique 1936, vol
Ja´ skowski, S.: Recherches sur la syst` eme de la logiqueintuitioniste. In: Actes du Congr` es International de Philosophie Scientifique 1936, vol. 6, Paris (1936) 58–61 23
1936
-
[14]
In: 31st IEEE Symposium on Foundations of Computer Science
Lincoln, P.D., Mitchell, J., Scedrov, A., Shankar, N.: Decision problems for proposi- tional linear logic. In: 31st IEEE Symposium on Foundations of Computer Science. FOCS’90, St. Louis. Proceedings. IEEE Press, Los Alamitos ( 1990) 662–671
1990
-
[15]
Comptes rendus des s´ eances de la Soci´ et´ e des Sciences et des Lettres de Varsovie Cl
/suppress Lukasiewicz, J., Tarski, A.: Untersuchungen ¨ uber denAussagenkalk¨ ul. Comptes rendus des s´ eances de la Soci´ et´ e des Sciences et des Lettres de Varsovie Cl. III 23 (1930) 30–50. English translation in [18, 38–59]
1930
-
[16]
Mundici, D.: Satisfiability in many-valued sentential logic is NP-complete. Theoret. Comput. Sci. 52 (1987) 145–153
1987
-
[17]
McGraw-Hill, New York ( 1969)
Rescher, N.: Many-valued Logic. McGraw-Hill, New York ( 1969)
1969
-
[18]
Tarski, A.: Logic, Semantics, Metamathematics. 2nd edn . Hackett, Indianapolis (1983)
1983
-
[19]
CSLI Lecture Notes 29
Troelstra, A.S.: Lectures on Linear Logic. CSLI Lecture Notes 29. CSLI, Standford, CA (1992)
1992
-
[20]
Urquhart, A.: Decidability and the finite model property . J. Philos. Logic 10 (1981) 367–370 24
1981
Reviewed August 14, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.