{"id":"72dc37f6-1d53-4f7c-8961-d70d0d527f9d","arxiv_id":"1908.01200","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"Optimal finite-valued covers of Hilbert calculi are computable, and a calculus has an effective sequential finite-valued approximation exactly when its theorem set is decidable.","lead":"This paper studies when a propositional logic given by a proof system can be approximated by finite-valued logics, whose truth tables make reasoning simpler. It shows the best such finite-valued approximation can be calculated, and that undecidable logics cannot be approximated by an effective sequence of finite-valued logics, while decidable ones can.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"No significant objection identified: main theorems hold within the declared calculus class; scope limits and typographical errors are not load-bearing.","rationale":"Proposition 30's proof is almost immediate once Theorem 28 is available: the set of m-valued matrices over a fixed carrier is finite, strong soundness is decidable by Prop. 21, and the poset quotient by identical tautology sets is finite, so all ⊴-minimal covers can be found by exhaustive comparison. I could not locate a gap in Theorem 28: the unification of variables with equal countermodel values preserves the M2-tautology property because Taut(M2) is closed under substitution, and the subformula replacement by equal (function, value) pairs preserves both validity and countermodelhood. The depth bound from the pigeonhole argument is correct. Corollary 41 also checks out: the matrix M_{dp(F),j}(Thm(C)) falsifies F, validates all theorems, and strict analyticity supplies exactly the two facts needed for strong soundness of every rule (premise variables in the conclusion, and premise-depth bounded by conclusion-depth). The main weakness is that Def. 4 excludes many natural rule formats; the paper is transparent about this in Remarks 5/6, and its formal claims are conditional on the definition. If the intended contribution is read as 'general propositional logics' in the title, this scope mismatch is a substantive limitation but not a correctness error. The textual slips (Gödel logic 0/m−1 convention inconsistency, reversed monotonicity in Prop. 34, singular 'minimal' in the abstract) are real but do not affect the proofs once corrected. Hence the reader's CONDITIONAL verdict need not be changed.","tokens_in":18385,"tokens_out":34245,"duration_ms":362597,"concrete_test":"Brute-force verify Theorem 28's depth bound in the smallest nontrivial case: enumerate all pairs of 2-valued logics over a fixed finite language with one binary connective, and for each pair decide whether a separating formula exists; if any difference requires a formula with more than 2 variables or depth greater than 31, the bound underlying Proposition 30 is false. This directly tests the only non-trivial computational step of the central claim.","verdict_should_be":"UNCHANGED","load_bearing_attack":"I find no load-bearing mathematical defect in the paper's central claims. Proposition 30 follows directly from the finiteness of m-valued matrices and Theorem 28's decidable comparison; I rechecked Theorem 28's variable-reduction and depth-bound argument and it is sound. Corollary 41's construction of M_{dp(F),j}(Thm(C)) does establish a falsifying cover for strictly analytic C, and Propositions 34–36 support the approximation characterization. The most serious limitation is the Def. 4 rule format: sequent-style rules and side-formula modal rules are excluded, and Remarks 5–6 concede that the sketched encodings do not preserve strict analyticity. This narrows the advertised 'general' scope and prevents Corollary 41 from automatically transferring to sequent or modal calculi, but it is an explicit stated condition, not an internal inconsistency. The proof of Prop. 34 contains a reversed monotonicity claim ('M_i ⊴ M_{i+1}' should be 'M_{i+1} ⊴ M_i'), yet the intersection argument still works and Def. 32 itself says monotonicity is technically unnecessary. The abstract's singular 'minimal m-valued logic' overstates Prop. 30 when multiple incomparable minima exist, but the proposition is correctly plural. None of these issues changes the correctness of the formal results.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":18608,"tokens_out":24951,"duration_ms":231805,"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":[{"comment":"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.","section":"Def. 14, Prop. 15"}],"minor_comments":[{"comment":"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.","section":"Abstract"},{"comment":"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.","section":"Proof of Prop. 34"},{"comment":"The sentence \"A formula F is a theorem of L\" should read \"a theorem of C\", since L denotes the language.","section":"Def. 4"},{"comment":"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.","section":"Proof of Prop. 20"},{"comment":"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.\"","section":"Sec. 6"},{"comment":"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.","section":"Title and abstract"}],"recommendation":"major_revision","confidential_remarks":"The manuscript is a substantially revised and expanded version of the authors' 1994 conference paper [4], and this relationship is acknowledged in the text. The main theorems are correct in substance, with the exception of the false statement in Prop. 15, which is used in proofs but is repairable locally. The paper fits the journal's scope and makes a genuine contribution to many-valued approximations of calculi; I recommend accepting after the lemma is corrected and the minor issues are fixed."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"First thing you should know: the paper is right, and the reader's conditional verdict is fair. It is a genuinely useful contribution to proof theory and many-valued logic. The new results are real: decidability of t-soundness (Prop. 22), the decidable preorder on finite-valued logics and the resulting computability of optimal m-valued covers (Thm. 28, Prop. 30), and the many-valued closure analysis with Cor. 41. I rechecked the subformula-collapse argument in Thm. 28 and the M_{dp(F),j} construction in Cor. 41; both work. The paper also honestly separates the three notions of soundness, and the undecidability of weak soundness (Prop. 20) is a nice counterpoint.\n\nThe proof that t-soundness is decidable is the most delicate part, and it holds: the finite truth-function bound plus the minimal-depth argument closes. The comparison theorem for finite-valued logics is also sound, and the fact that optimal covers are computable follows cleanly. If you work on Bernays-style underivability proofs, sequential approximations, or the metatheory of Hilbert calculi, this is worth your time.\n\nSoft spots, in proportion to how soft they are. The biggest is scope: despite the title, the results apply only to Hilbert calculi whose rules have the restricted shape A1...An / C with all premise variables in the conclusion and no side conditions. Sequent-style rules and modal rules with side formulas are out. Remarks 5 and 6 say exactly this, and the proposed encodings are sketches that do not preserve strict analyticity. So the advertised \"general\" scope is narrower than it looks. That is a stated condition, not an internal flaw, but it does limit how far Cor. 41 can be pushed.\n\nThe textual issues are minor but real. The abstract says \"the minimal m-valued logic\" when Prop. 30 yields minimal covers, possibly multiple and incomparable. And the proof of Prop. 34 has a reversed monotonicity claim: it says M_i ⊴ M_{i+1}, but the construction gives the opposite inclusion. The intersection argument in the paper still goes through and Def. 32 itself says the monotonicity condition is technically unnecessary, so this is a correction, not a collapse. Some counting bounds in Prop. 22 and Thm. 28 are typeset indistinctly; a referee should ask for cleaner notation.\n\nWho is this for? Proof theorists and many-valued logicians, especially people interested in which calculi can be effectively approximated by finite-valued semantics. It deserves a serious referee. I would send it out, and the required fixes are local.\n\nRecommendation: accept for peer review, with requests for a corrected abstract and the Prop. 34 monotonicity fix.","headline":"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.","tokens_in":19168,"tokens_out":2557,"would_cite":true,"duration_ms":26551,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B50","03B25","03B45"],"pacs":[],"model":"deepseek-v4-flash","headline":"For every Hilbert calculus in a natural rule format, the optimal finite-valued approximation is computable.","keywords":["finite-valued logic","many-valued logic","Hilbert calculus","propositional logic","sequential approximation","many-valued closure","strictly analytic calculi","finite model property"],"falsifier":"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.","tokens_in":18153,"feed_emoji":"🧮","tokens_out":12624,"duration_ms":107967,"temperature":0.7,"pith_summary":"The paper asks when a propositional logic presented as a Hilbert-style calculus can be approximated by a finite-valued logic, whose satisfiability problem is at worst NP-complete. It works with covers: finite-valued matrices for which every axiom of the calculus is a tautology and every rule preserves truth under all valuations. The main structural result is that, for each m, the optimal m-valued covers—those minimal under inclusion of tautology sets—are computable, so the best finite-valued approximation of a given calculus can be found by search. The paper also shows that every decidable propositional logic has an effective sequence of finite-valued logics whose intersection is exactly the logic, that undecidable calculi admit no such sequence, and that strictly analytic calculi are exactly captured by their many-valued closure. A reader should care because this turns the classic many-valued method for proving non-derivability into a general automated tool, and it clarifies when finite-valued semantics completely determine a proof system.","feed_headline":"Best finite-valued approximations of calculi are computable","feed_subtitle":"The smallest finite-valued logic sound for a given calculus can be computed, automating non-derivability proofs.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Supplies the formula-as-truth-value construction, from which the finite approximations $M_{i,j}(L)$ are built.","marker":"[15, Satz 3]"},{"why":"Introduces the many-valued matrix method for proving underivability, the historical root of the paper's covers.","marker":"[5]"},{"why":"Establishes NP-completeness of satisfiability in finite-valued propositional logic, the computational motivation for approximating by finite-valued logics.","marker":"[16]"},{"why":"Gives the first effective strong sequential approximation of intuitionistic logic, the model case for the approximation concept.","marker":"[13]"},{"why":"Points out that the standard chain-valued logics cover intuitionistic logic and get successively better, anchoring the sequential-approximation discussion.","marker":"[10]"},{"why":"Axiomatizes the intersection of the chain-valued logics, showing that sequence is not an approximation of intuitionistic logic.","marker":"[8]"},{"why":"Supplies the finite model property for intuitionistic logic used to obtain sequential approximations from Kripke semantics.","marker":"[9, Ch. 4, Theorem 4(a)]"},{"why":"Provides an undecidable propositional logic used to show undecidable calculi have no effective sequential approximation.","marker":"[14]"},{"why":"Shows a recursively axiomatizable modal logic with the finite model property need not be decidable, delimiting when Kripke-model approximations are effective.","marker":"[20]"}],"fun_headline_variants":["Best finite-valued approximations of calculi are computable","Computing the best finite-valued logic for any calculus","Minimal sound finite-valued logic is computable","Finite-valued covers: computable minimal logic","Automated: find the smallest sound multi-valued logic"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Best finite-valued approximations of calculi are computable","Computing the best finite-valued logic for any calculus","Minimal sound finite-valued logic is computable","Finite-valued covers: computable minimal logic","Automated: find the smallest sound multi-valued logic"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000458,"raw_usage":{"total_tokens":2275,"prompt_tokens":905,"completion_tokens":1370,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":521,"completion_tokens_details":{"reasoning_tokens":1296}},"tokens_in":521,"tokens_out":1370,"duration_ms":11179,"temperature":1.0,"reasoning_tokens":1296,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T15:22:16.537079+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"Principia Mathematica","cited_arxiv_id":null,"evidence_quote":"Introduces the many-valued matrix method for proving underivability, the historical root of the paper's covers."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Establishes NP-completeness of satisfiability in finite-valued propositional logic, the computational motivation for approximating by finite-valued logics."},{"cited_title":"In: Actes du Congr` es International de Philosophie Scientifique 1936, vol","cited_arxiv_id":null,"evidence_quote":"Gives the first effective strong sequential approximation of intuitionistic logic, the model case for the approximation concept."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Points out that the standard chain-valued logics cover intuitionistic logic and get successively better, anchoring the sequential-approximation discussion."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Axiomatizes the intersection of the chain-valued logics, showing that sequence is not an approximation of intuitionistic logic."},{"cited_title":"In: 31st IEEE Symposium on Foundations of Computer Science","cited_arxiv_id":null,"evidence_quote":"Provides an undecidable propositional logic used to show undecidable calculi have no effective sequential approximation."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Shows a recursively axiomatizable modal logic with the finite model property need not be decidable, delimiting when Kripke-model approximations are effective."}],"review_version":1}