Pith. sign in

REVIEW 3 major objections 4 minor 30 references

Hardness as an Information Constraint: A Unifying Meta-Complexity Assumption

T0 review · 3 major / 4 minor · reviewed 2026-08-02 · deepseek-v4-flash

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

Pith's one-line read True random facts are unusable by feasible proofs unless a weak base theory already explains them; from that single principle the paper derives conditionally PH noncollapse, SAT not in P/poly, and routes to cryptography and random-refutatio

desk verdict The framework is worth a referee, but the strong PH-noncollapse result currently rests on a formal gap: Lemma 3.8 conflates arithmetic truth with the polynomial hierarchy. read the letter →

arxiv 2606.04257 v2 pith:VLEZMVFQ submitted 2026-06-02 cs.CC

Hunter Monroe This is my paper · ORCID
classification cs.CC MSC 03F3003F2068Q1568Q30
keywords Kolmogorovrandomnessboundedconsistencyproofcomplexitypolynomialhierarchymeta-complexityone-wayfunctionsderandomizationrandom3-SATrefutation
topics P versus NP
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

This paper tries to establish that a single information constraint organizes the major hardness conjectures of complexity theory. The constraint, Kolmogorov Hardness (KH), says that a sound arithmetic theory cannot efficiently prove the consistency of adjoining a true Kolmogorov-random fact—x is random—unless that fact is already provable over a weak base theory (EA plus the theory's consistency). If KH holds, difficult conditional consequences follow: random strings generate dense families of exponentially hard tautologies, a hierarchy-level strengthening separates every adjacent level of the polynomial hierarchy and rules out SAT having polynomial-size circuits, and calibrated variants lead to one-way functions, derandomization, and random 3-SAT refutation hardness. The paper also argues that KH behaves like a reflection principle and may be formally independent of standard metatheories, and it lays out a research program for testing the principle.

What carries the argument

Bounded-consistency simulation and the HRC/Feasible Reflection converse. For theories S⊇S^1_2, S simulates S+φ if S has polynomial-size proofs of Con_{S+φ}(n). The known positive direction is that EA⊢Con_S→Con_{S+φ} implies simulation. The key machinery is the proposed converse—simulation only if that weak-base implication holds—specialized to φ=(x∈R). KH then uses standard incompleteness arguments to supply infinitely many random axioms inaccessible over EA+Con_S. The finite-scale variant SETH-K-Finite and the hierarchy-level variant SETH-K-PH add the algorithmic and circuit-theoretic calibration needed to turn the proof-theoretic obstruction into concrete complexity separations.

What would settle it

Take a fixed sound theory S (say S^1_2 plus its own consistency), pick a true string x that is Kolmogorov-random in the logarithmic-deficiency sense and not provably so over EA+Con_S, and check whether S has proofs of Con_{S+(x∈R)}(n) of length n^c for infinitely many n. A single such proof family, found by any means other than an EA-level relative-consistency proof, would refute KH. More directly, construct a nonstandard model of S with a standard cut containing such polynomial-size proof codes while the weak-base implication fails.

Watch

Extended reading notes

Core claim

The paper's central claim is a proposed exact converse to a known proof-complexity mechanism. It is known that if a weak base theory EA proves Con_S→Con_{S+φ}, then S has polynomial-size proofs of Con_{S+φ}(n), i.e., S simulates S+φ. The paper's Higher Relative Consistency (HRC) / Feasible Reflection principle asserts the converse: no polynomial-size proof family for a true extension exists without such an EA-level explanation. Specializing to φ being a true statement 'x∈R' (x is Kolmogorov-random), this becomes Kolmogorov Hardness (KH): a sound theory cannot efficiently prove consistency of adjoining an inaccessible random fact. The paper then shows that finite-scale and hierarchy-level str

Load-bearing premise

The load-bearing premise is that feasible simulation requires a weak-base relative-consistency explanation—the known sufficient condition (EA proving Con_S → Con_{S+φ}) is also necessary; at higher levels, an analogous level-respecting certification bridge must hold. If a polynomial-size proof family can exist without such an explanation, KH and all its consequences collapse.

Editorial extensions

If this is right

  • If KH holds, for every sound theory S and all but finitely many true random strings x, S lacks polynomial-size proofs of Con_{S+(x∈R)}(n); this yields a density-1 family of polynomial-size tautologies requiring exponential-size proofs.
  • If SETH-K-PH holds, the polynomial hierarchy is infinite: Π^p_i ≠ Π^p_{i+1} for every i≥1, with explicit dense separating predicates; the standard advice-collapse argument then gives SAT∉P/poly.
  • With the average-case boundary reflection and boundary calibration assumptions, KH transfers to one-way functions via the known equivalence with mild average-case hardness of time-bounded Kolmogorov complexity.
  • With sparse Feige hardness and refutation reflection, KH implies the random 3-SAT refutation hypothesis at constant clause density.
  • KH and HRC imply that no sufficiently strong sound theory simulates its own consistency extension, and a self-applicable KH principle implies the theory's own consistency, so it cannot be proved inside that theory.

Reading between the lines

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

  • A concrete way to pressure-test the program is to prove or disprove the HRC converse in weak fragments of bounded arithmetic; a counterexample there would show exactly where the 'no-cheating' principle breaks.
  • If KH is independent of standard metatheories, its role would be closer to a reflection principle than a theorem; the paper's own program treats this as an open target.
  • The framework suggests that meta-complexity problems like time-bounded Kolmogorov complexity are hard because they sit on the boundary between weak-base-accessible randomness and inaccessible randomness; this boundary could be formalized and tested against known hardness results.
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

3 major / 4 minor

Summary. The paper proposes a proof-theoretic meta-complexity assumption package centered on Kolmogorov Hardness (KH): a sound theory S should have polynomial-size proofs of bounded consistency of S+(x∈R) only when EA+Con_S already proves x∈R. From KH and its finite-scale and hierarchy-level strengthenings, the paper derives, conditionally, density-1 families of hard tautologies, no-mutual-help phenomena, PH noncollapse with explicit dense separators, SAT∉P/poly, and conditional routes to one-way functions, derandomization, natural-proofs compatibility, and Feige-style random-refutation hardness. The paper is explicit that HRC, KH, and the bridge principles are conjectural, and it discusses formal independence obstacles.

Significance. If the framework were sound, it would provide a genuinely unifying explanation of several major open problems, and the paper is commendably transparent about which steps are theorems and which are assumptions. The finite-scale consequences (Theorem 3.3, Corollaries 3.4–3.5) follow from SETH-K-Finite in a straightforward way, and Theorem 2.9 on machine invariance is a useful robustness check. However, the hierarchy-level payoff is built on an invalid identification of arithmetical truth oracles with polynomial-hierarchy predicates. Lemma 3.8 is not a minor gap: it is the load-bearing step for SETH-K-PH and therefore for Theorems 3.10 and 3.12. The paper remains a programmatic proposal, but its headline conditional consequences for PH noncollapse and SAT∉P/poly are not established as stated.

major comments (3)
  1. [§3.2.1, Definition 3.7 and Lemma 3.8] The finite predicate Q^t_{i,fin} is not a finite approximation of x∈R^t_i. R^t_i is defined relative to an oracle for the true Π_i sentences (the i-th Turing jump), while Definition 3.7 requires every oracle query to be decidable by a predicate in Π^p_i. For i=1, a single query can be a Π_1 sentence such as ∀s ¬Halt(e,0,s), which is Π_1-complete and is not decidable by any Π^p_1 = coNP predicate. Replacing the oracle by a PH-decidable predicate changes which strings are compressible in t steps, and the paper gives no argument that the two notions agree on the relevant bounded computations. Lemma 3.8 therefore does not place Q^t_{i,fin} in Π^p_{i+1}; it defines a different arithmetical predicate. Since Theorem 3.10 and Corollary 3.11 depend directly on Lemma 3.8, the PH noncollapse conclusion is unsupported even assuming SETH-K-PH.
  2. [§3.2.4, Theorem 3.15] The theories T_i := S + Π^{true}_i are not recursively (or computably) axiomatizable for i≥1, since the set of true Π_i sentences is not c.e. for i≥1. The proof invokes 'relativized Chaitin-style incompleteness' to assert that T_i proves only finitely many true level-i randomness assertions. Chaitin's incompleteness theorem applies to effectively axiomatized sound theories; no formalization or proof is supplied for an oracle axiomatized theory. This is not a technicality: the contradiction in Theorem 3.15 depends exactly on this finiteness. Without a valid relativized Chaitin theorem for T_i, the derivation of SETH-K-PH from Certified Feasible Reflection and the Level-Respecting Certification Bridge is not established.
  3. [§3.2.4, Assumption 3.14] The Level-Respecting Certification Bridge asserts that if a polynomial-time Π^p_i-oracle machine correctly decides Q^t_i, then T_i certifies its accepting correctness on every sufficiently long true random input. This is not a bridge derived from any property of polynomial-time computation; it is a strong formal provability assumption, essentially as strong as the conclusion it is used to prove. Combined with the non-effectivity of T_i, the assumption is not backed by any supporting example, consistency check, or counterexample analysis. Consequently Theorem 3.15 is a derivation of SETH-K-PH from an assumption that already contains the key certificate existence claim, rather than an explanation of why a level-i decider must have such a certificate. This makes the hierarchy-level argument circular in a way that is not acknowledged in the text.
minor comments (4)
  1. [§3.2.2] The names SETH-K-Finite and SETH-K-PH are misleading: the assumptions have no evident relation to the Strong Exponential Time Hypothesis, and the acronym invites confusion.
  2. [§4.2, Theorem 4.2 and surrounding text] Theorem 4.2 states Liu–Pass as an equivalence for the value problem of time-bounded Kolmogorov complexity, but the paragraph immediately after warns that the decision/MINKT variant should be cited instead. This ambiguity matters because Theorem 4.6 relies on the formulation; the statement and the caveat should be reconciled.
  3. [§4.3] The notation 'R tt_t' appears malformed; it should likely be R^{tt}_t or a similar typographically distinct symbol. Please fix the notation to avoid confusion with R^t_i.
  4. [§6] The internal/external reading distinction is useful, but the claim that the ∀x closure of KH is Π^0_2 should be displayed explicitly with the formalized quantifier structure, since the exact complexity depends on the arithmetization of 'S has poly-size proofs' and of 'x∈R'.

Circularity Check

0 steps flagged · score 0.0 of 10

No construction-level circularity: the paper's payoffs are explicitly conditional on stated conjectures and bridge assumptions rather than on re-labeled fits or self-justifying definitions.

full rationale

This is a framework/conditional paper. The load-bearing principles—HRC (Conjecture 2.3), KH (Definition 2.7), SETH-K-Finite (Conjecture 3.1), SETH-K-PH (Assumption 3.9), Certified Feasible Reflection at Level i (Assumption 3.13), and Level-Respecting Certification Bridge (Assumption 3.14)—are all stated as assumptions, not derived results. The main technical payoffs are explicitly conditional: Theorem 3.10 and Corollary 3.11 follow from SETH-K-PH plus Lemma 3.8, and the paper does not claim SETH-K-PH follows from KH alone. Similarly, the one-way-function route (Theorem 4.6) is explicitly conditional on Average-Case Boundary Reflection and Boundary Calibration, and the Feige-style route on Sparse Feige Hardness and Refutation Reflection. These are calibrated bridge hypotheses, not fitted parameters renamed as predictions. The self-citations to Monroe [21] (Theorems 2.2 and 2.6; HRC) are not used as external proof of the new conclusions: HRC is labeled a conjecture, and the hierarchy-level and calibration assumptions are introduced in the present paper. The most serious concern is a formal-gap/correctness issue, not circularity: Lemma 3.8's claim that Q^t_{i,fin} lies in Π^p_{i+1} depends on Definition 3.7's replacement of arithmetic-truth oracle queries by Π^p_i-decidable finite approximations, and the paper does not prove this approximation agrees with R^t_i on the relevant computations. That is an unproven coding claim, but it is not a circular reduction; the assumption SETH-K-PH is not being used to prove itself. No step meets the required standard of exhibiting a specific reduction of a claimed prediction to its own input by construction.

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

The paper's load-bearing inputs are (i) standard proof-theoretic background (Chaitin, Pudlak, Visser, Liu-Pass), and (ii) a stack of new conjectures and bridge assumptions. The relation between the unconditional positive mechanism and the conjectural converse HRC is the crux: the program is only as strong as its willingness to assert that converse plus a separate calibration bridge for each frontier consequence.

free parameters (4)
  • d (randomness deficiency constant) = d >= 3
    Chosen by hand in Definition 2.7 to define the randomness predicate R. The invariance theorem shows changing d only shifts thresholds, so it is not load-bearing.
  • epsilon in SETH-K-Finite
    An existential exponent asserted by Conjecture 3.1. No explicit value is given, and the finite-scale lower bound depends on its existence.
  • t_i in SETH-K-PH
    An existential polynomial time bound per level i in Assumption 3.9. The PH-separating predicate Q_i^{t_i} is defined through this unspecified time bound.
  • N^S_R threshold
    Defined in Section 3.1 as the maximum of vacuity, Chaitin, and mentionability thresholds. Its existence follows from incompleteness, but the scale is not computed.
assumptions (9)
  • domain assumption S is a sound theory extending S^1_2 with polynomial-time decidable axioms
    Standing setup in Section 2.1; all simulation and hardness statements are relative to such an S.
  • standard math Positive simulation theorem: if EA proves Con_S -> Con_{S+phi}, then S simulates S+phi
    Theorem 2.2, repackaging Jerabek/Pudlak proof translation and Visser's interpretability lemma; cited from Monroe [21].
  • ad hoc to paper HRC / Feasible Reflection: if S has poly-size proofs of Con_{S+phi}(n), then EA proves Con_S -> Con_{S+phi}
    Conjecture 2.3 / Assumption 2.4. This is the unproved converse that KH and all downstream consequences depend on.
  • ad hoc to paper SETH-K-Finite: finite-scale exponential lower bound for bounded consistency of random-axiom extensions
    Conjecture 3.1. This is the engine behind the density and no-mutual-help theorems.
  • ad hoc to paper Certified Feasible Reflection at level i
    Assumption 3.13: if T_i certifies the accepting correctness of a level-i machine on true random inputs, then T_i proves x in R_i. Used in Theorem 3.15.
  • ad hoc to paper Level-Respecting Certification Bridge
    Assumption 3.14: any actual level-i decider for Q_i^t has a T_i certificate. This is effectively the no-cheating conclusion being argued, making Theorem 3.15 highly assumption-driven.
  • ad hoc to paper Average-Case Boundary Reflection and Boundary Calibration
    Assumptions 4.3 and 4.5: tailored bridges connecting the boundary-exposure predicate to time-bounded Kolmogorov complexity. They are needed for the one-way-function theorem.
  • ad hoc to paper Sparse Feige Hardness and Refutation Reflection
    Assumptions 4.13 and 4.14: bridges needed to derive Feige's random-3-SAT hypothesis. Theorem 4.15 is just the conjunction of these two assumptions.
  • ad hoc to paper Disjoint-Pair Feasible Reflection
    Assumption 5.1: needed to make the random-axiom disjoint NP pair P-inseparable under SETH-K-Finite.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Hardness as an Information Constraint: A Unifying Meta-Complexity Assumption." pith.science (2026). https://pith.science/paper/VLEZMVFQ

@misc{pith2026260604257,
  author       = {Pith},
  title        = {Pith review of: Hardness as an Information Constraint: A Unifying Meta-Complexity Assumption},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/VLEZMVFQ}},
  note         = {Machine review of arXiv:2606.04257}
}
read the original abstract

Monroe (2026) shows that, if no optimal proof system exists, then every sound arithmetic theory S extending S^1_2 with polynomial-time decidable axioms fails, for all sufficiently large k, to simulate S^1_2+phi_BB(k), where phi_BB(k) asserts the exact k-state Busy Beaver value. This gives the nonexistence hypothesis an information-constraint interpretation through canonical hard instances. If the best-known route to simulation is also necessary--namely, if simulation requires a relative-consistency explanation over a weak base--then the same constraint applies to inaccessible Kolmogorov-randomness facts. We call this conjecture Kolmogorov Hardness (KH). Finite-scale and hierarchy-level forms of KH yield, conditionally, dense families of small hard tautologies, PH noncollapse with explicit dense separators, and SAT notin P/poly. Under separately stated assumptions, variants yield P-inseparability of a disjoint NP pair, no mutual help between mutually conditionally random axioms, one-way functions via Liu--Pass, derandomization, and Feige-style random-refutation hardness. Allender et al. provide a complementary calibration: full access to conventional random-string oracles supports every PSPACE computation, whereas any fixed sound computably axiomatized theory can certify only finitely many positive randomness instances. The framework organizes complexity conjectures around canonical information constraints. It seems self-evident that efficient proofs should not leverage true randomness facts unavailable to the proving theory. Yet KH may be independent of standard metatheories: it resembles reflection, can fail internally in nonstandard models even when externally true, and may constrain the metatheories themselves. We propose a research program on extensions, self-evidence, formal independence, and possible new axioms.

Review history (2 revisions) →

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

30 extracted references

  1. [1]

    Scott Aaronson,Is P versus NP formally independent?, Bulletin of the European Association for Theoretical Computer Science81(2003), 109–136

    2003

  2. [2]

    1, 2:1–2:54

    Scott Aaronson and Avi Wigderson,Algebrization: A new barrier in complexity theory, ACM Transactions on Computation Theory1(2009), no. 1, 2:1–2:54

    2009

  3. [3]

    Comput.35(2006), no

    Eric Allender, Harry Buhrman, Michal Kouck´ y, Dieter van Melkebeek, and Detlef Ronneburger,Power from random strings, SIAM J. Comput.35(2006), no. 6, 1467–1493

    2006

  4. [4]

    Oliveira,Consistency of circuit lower bounds with bounded theories, Logical Methods in Computer Science16(2020), no

    Jan Bydˇ zovsk´ y, Jan Kraj ´ ıˇ cek, and Igor C. Oliveira,Consistency of circuit lower bounds with bounded theories, Logical Methods in Computer Science16(2020), no. 2, 12:1–12:16

    2020

  5. [5]

    Chaitin,Information-theoretic limitations of formal systems, JACM 21(1974), no

    Gregory J. Chaitin,Information-theoretic limitations of formal systems, JACM 21(1974), no. 3, 403–424

    1974

  6. [6]

    Oliveira,Reverse mathematics of complexity lower bounds, SIAM Journal on Computing (2024), To appear; preprint 2024

    Lijie Chen, Jiatu Li, and Igor C. Oliveira,Reverse mathematics of complexity lower bounds, SIAM Journal on Computing (2024), To appear; preprint 2024

    2024

  7. [7]

    Cook and Jan Kraj ´ ıˇ cek,Consequences of the provability of NP⊆P/poly, Journal of Symbolic Logic72(2007), no

    Stephen A. Cook and Jan Kraj ´ ıˇ cek,Consequences of the provability of NP⊆P/poly, Journal of Symbolic Logic72(2007), no. 4, 1353–1371. 34

    2007

  8. [8]

    Shuichi Hirahara,Non-black-box worst-case to average-case reductions within NP, 2018 IEEE 59th Annual Symposium on Foundations of Computer Science (FOCS), 2018, pp. 247–258

    2018

Show all 30 references
  1. [9]

    264, 2023, pp

    Shuichi Hirahara, Zhenjian Lu, and Hanlin Ren,Bounded relativization, 38th Com- putational Complexity Conference (CCC), LIPIcs, vol. 264, 2023, pp. 6:1–6:46

    2023

  2. [10]

    Russell Impagliazzo and Avi Wigderson, P=BPPifErequires exponential circuits: Derandomizing the XOR lemma, STOC, ACM, 1997, pp. 220–229

    1997

  3. [11]

    Math.28(1982), 191–209

    Richard Karp and Richard Lipton,Turing machines that take advice, Enseign. Math.28(1982), 191–209

    1982

  4. [12]

    Erfan Khaniki,Jump operators, interactive proofs and proof complexity generators, 2024 IEEE 65th Annual Symposium on Foundations of Computer Science (FOCS), 2024, pp. 573–593

    2024

  5. [13]

    1, 20–40

    Jan Kraj ´ ıˇ cek,On the existence of strong proof complexity generators, Bulletin of Symbolic Logic30(2024), no. 1, 20–40

    2024

  6. [14]

    3, To appear

    ,A proof complexity conjecture and the incompleteness theorem, Journal of Symbolic Logic90(2025), no. 3, To appear

    2025

  7. [15]

    497, Cambridge University Press, 2025

    ,Proof complexity generators, London Mathematical Society Lecture Note Series, no. 497, Cambridge University Press, 2025

    2025

  8. [16]

    Jan Kraj ´ ıˇ cek,Proof complexity, Cambridge University Press, New York, NY, 2019

    2019

  9. [17]

    Jan Kraj ´ ıˇ cek and Pavel Pudl´ ak,Propositional proof systems, the consistency of first order theories and the complexity of computations, J. Symb. Log.54(1989), 1063–79

    1989

  10. [18]

    Oliveira,Unprovability of strong complexity lower bounds in bounded arithmetic, Proceedings of the 55th Annual ACM Symposium on Theory of Computing (STOC), 2023, pp

    Jiatu Li and Igor C. Oliveira,Unprovability of strong complexity lower bounds in bounded arithmetic, Proceedings of the 55th Annual ACM Symposium on Theory of Computing (STOC), 2023, pp. 1051–1064

    2023

  11. [19]

    Ming Li and Paul M. B. Vit´ anyi,An introduction to Kolmogorov complexity and its applications, Texts in Computer Science, Springer, 2008

    2008

  12. [20]

    1243–1254

    Yanyi Liu and Rafael Pass,On one-way functions and Kolmogorov complexity, 2020 IEEE 61st Annual Symposium on Foundations of Computer Science (FOCS), 2020, pp. 1243–1254

    2020

  13. [21]

    Colloquium Comput

    Hunter Monroe,Toward a characterization of simulation between arithmetic theo- ries, Electron. Colloquium Comput. Complex.TR26-062(2026), Preprint

    2026

  14. [22]

    2, 102735

    Moritz M¨ uller and J´ an Pich,Feasibly constructive proofs of succinct weak circuit lower bounds, Annals of Pure and Applied Logic171(2020), no. 2, 102735. 35

    2020

  15. [23]

    J´ an Pich and Rahul Santhanam,Strong co-nondeterministic lower bounds for NP cannot be proved feasibly, Proceedings of the 53rd Annual ACM SIGACT Sympo- sium on Theory of Computing (STOC), 2021, pp. 223–233

    2021

  16. [24]

    120, Elsevier, 1986, pp

    Pavel Pudl´ ak,On the length of proofs of finitistic consistency statements in first order theories, Studies in Logic and the Foundations of Mathematics, vol. 120, Elsevier, 1986, pp. 165–196

    1986

  17. [25]

    Buss, ed.), Elsevier, 1998

    ,The lengths of proofs, Handbook of Proof Theory (Samuel R. Buss, ed.), Elsevier, 1998

    1998

  18. [26]

    ,Incompleteness in the finite domain, Bull. Symb. Log.23(2017), no. 4, 405–441

    2017

  19. [27]

    Razborov,Unprovability of lower bounds on circuit size in certain fragments of bounded arithmetic, Izvestiya: Mathematics59(1995), no

    Alexander A. Razborov,Unprovability of lower bounds on circuit size in certain fragments of bounded arithmetic, Izvestiya: Mathematics59(1995), no. 1, 205– 227

    1995

  20. [28]

    Razborov and Steven Rudich,Natural proofs, STOC ’94: Proceed- ings of the Twenty-Sixth Annual ACM Symposium on Theory of Computing,, (New York, NY: ACM Press), 1994, pp

    Alexander A. Razborov and Steven Rudich,Natural proofs, STOC ’94: Proceed- ings of the Twenty-Sixth Annual ACM Symposium on Theory of Computing,, (New York, NY: ACM Press), 1994, pp. 204–13

    1994

  21. [29]

    219, 2022, pp

    Hanlin Ren and Rahul Santhanam,A relativization perspective on meta-complexity, 39th International Symposium on Theoretical Aspects of Computer Science (STACS), LIPIcs, vol. 219, 2022, pp. 54:1–54:13

    2022

  22. [30]

    Albert Visser,The interpretation existence lemma, Feferman on Foundations: Logic, Mathematics, Philosophy (Gerhard J¨ ager and Wilfried Sieg, eds.), Springer International Publishing, Cham, 2017, pp. 101–144. 36

    2017

Pith tools

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