Pith. sign in

REVIEW 4 major objections 5 minor 42 references

An Intuitionistic Glance at Primes

T0 review · 4 major / 5 minor · reviewed 2026-08-03 · deepseek-v4-flash

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

Pith's one-line read No total constructive functional can uniformly turn primality into explicit prime-sum witnesses in Heyting arithmetic.

desk verdict A load-bearing misclassification of bounded primality as unbounded Π1 makes the paper's central realizability barrier false, and the paper contradicts its own abstract. read the letter →

arxiv 2511.07774 v3 pith:KFTG52XV submitted 2025-11-11 math.LO cs.LO

Milan Rosko This is my paper · ORCID
classification math.LOcs.LO MSC 03F5003F5511A4111P32
keywords HeytingarithmeticrealizabilityGoldbachconjectureprimalityΠ1predicatesBHKsemanticsconstructiveprooftheorynon-uniformization
topics Goldbach's Conjecture
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 the constructive status of prime conjectures is determined by realizability, not by the distribution of primes. Working in Heyting arithmetic under the BHK interpretation, it claims that no total functional can uniformly convert a Π1 primality judgment into explicit Σ1 witnesses, because such a conversion would violate strong normalization. Applied to a constructive Goldbach principle — every even number is a sum of two primes, with primality expressed by the bounded universal formula PrimeΠ — the conclusion is that even if the principle holds in the standard natural numbers, HA cannot supply a uniform constructor for the prime summands. If this is right, the difficulty of Goldbach's conjecture is a logical boundary of constructive definability, and HA, PA, and true arithmetic separate into three distinct layers.

What carries the argument

The load-bearing object is the bounded primality predicate PrimeΠ(n) ≡ n>1 ∧ ∀a,b≤n[a·b=n ⇒ a=1∨b=1], treated as a Π1 condition, together with the BHK reading of implication as a total functional. The argument's work is done by the thesis that any uniform realizer of Π1 ⇒ ∃yΣ1 would be a global Skolem function, and that such a function would contradict normalization in HA. The paper also builds a geometric packing semantics — composites are finite rectangles, primes are the universal absence of such rectangles — to make the local/global asymmetry vivid and to connect the logical barrier to bounded divisor schemata that can always miss composites with large factors.

What would settle it

Formalize trial division in HA: for a given numeral n, a primitive-recursive program checks every a from 2 to ⌊√n⌋ and decides whether a divides n; this is a finite, terminating computation over a bounded range. Since bounded quantification over numerals is provably decidable by induction in HA, the procedure decides the paper's own formula PrimeΠ(n) constructively, contradicting the claim that primality is a constructively undecidable Π1 predicate and thus removing the premise on which the barrier theorems rest.

Watch

Extended reading notes

Core claim

In the paper's own terms, the discovery is a realizability barrier: a proof in HA of statements of the form ∀x(φ(x)⇒∃yψ(x,y)) must yield a total, closed realizer t such that for every x, ψ(x,t(x)) holds. For primality, φ(n)=PrimeΠ(n) is classified as Π1 and compositeness as ∃ with Σ1 witness; the paper asserts there is no total primitive-recursive functional, and no closed term in any strongly normalizing typed λ-calculus adequate for HA, that uniformly transforms PrimeΠ evidence into such witnesses. Consequently the constructive Goldbach principle GC*Π has no total Σ1 constructor in HA, so even a classical proof of Goldbach would not give a constructive proof. The paper translates this into

Load-bearing premise

The load-bearing premise is that the paper's own primality formula — no factorization with factors up to n — is a genuinely undecidable universal claim; because the search is bounded, intuitionistic arithmetic can decide it by finite checking, and the barrier results stand or fall with that classification.

Editorial extensions

If this is right

  • A classical proof of the strong Goldbach conjecture would not yield a constructive proof; the constructive Goldbach principle GC*Π would remain unprovable in HA even if arithmetically true.
  • Any prime conjecture whose conclusion requires witnesses for a truly Π1 premise and has no primitive-recursive bound on the witnesses is predicted to be constructively unprovable, regardless of its truth in N.
  • PA proves that no total recursive index uniformly realizes the Σ1 witnesses for GC*Π; any alleged uniform extractor would create constant-length proofs for infinitely many instances, colliding with proof-length speedup.
  • Goldbach's constructive form sits in the gap between HA and true arithmetic: true in N (if the classical conjecture is true) but not HA-provable.

Reading between the lines

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

  • Editorial inference: The paper's own final section concedes that every modern system implements primality as a bounded, decidable Δ0₀ predicate; if that is the right formalization, the claimed barrier would have to be restated for an unbounded universal predicate and would no longer concern the primality used in ordinary arithmetic.
  • Editorial inference: The same uniformization argument, if sound, would generalize to any Π1-premised existential statement about primes, such as twin-prime or prime-k-tuple conjectures, predicting they too are constructively unprovable in HA for realizability reasons rather than arithmetical ones.
  • Editorial inference: The bounded-search criterion in the paper suggests a constructive repair: replace an unbounded prime conjecture by a bounded version that assumes an explicit search bound B(n) for witnesses; such bounded approximations should fall into the constructively provable case, giving finite Goldbach certificates for each n.
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

4 major / 5 minor

Summary. The paper claims to establish a proof-theoretic barrier: no total functional in Heyting Arithmetic (HA) can uniformly transform Π₁ primality predicates into explicit Σ₁ witnesses, so that the constructive Goldbach principle, even if true in ℕ, has no uniform realizer in HA. The argument is built on a classification of primality as a genuinely unbounded Π₁ predicate (Definition 2.7, Remark after Definition 2.7, Thesis 2.5/2.6) and on several non-uniformization and diagonalization principles. The paper also includes geometric, forcing, and analytic interpretations of this claimed barrier.

Significance. If the central claim were correct, it would describe a fundamental logical obstruction to constructive proofs of prime conjectures, with consequences for proof theory and the philosophy of mathematics. However, the paper's own definition of primality is a bounded (Δ₀) formula, and the paper itself acknowledges this in the abstract and in Section 8 (8.110). Since HA proves decidability of every bounded formula, the central classification premise is false, and the claimed realizability barrier does not apply to primality as defined. Consequently, the paper's main result does not stand. The paper does contain useful reminders about boundedness of standardized primality tests, but these points are already standard and do not support the claimed barrier.

major comments (4)
  1. [Def. 2.7 and Remark; abstract; §8 (8.110)] The load-bearing premise is that PrimeΠ(n) = n>1 ∧ ∀a,b≤n [a·b=n ⇒ a=1∨b=1] is a genuinely unbounded Π₁ predicate that is 'not constructively decidable' (Remark after Def. 2.7). This is false: all quantifiers in the displayed formula are bounded, so the formula is Δ₀. In HA every bounded formula is decidable by induction on the bound; hence HA proves PrimeΠ(n) ∨ ¬PrimeΠ(n) for each n. The paper itself contradicts this in the abstract ('both searches are bounded, both predicates are decidable') and in §8, (8.110), where primality is correctly described as Δ₀. Since Theses 2.5/2.6, Proposition 4.7, Theorem 6.5, and §7.1 all reach the primes only through this misclassification, the central claim collapses.
  2. [Thesis 2.5/2.6; Prop. 4.5] Prop. 4.5 asserts a non-uniform extraction theorem 'by [Friedman, 1975; Beeson, 1985]' to the effect that no total primitive recursive F can satisfy HA⊢∀n(∃y R(n,y) ⇒ R(n,F(n))) for Σ₁ R with Π₁ parameters. This is not a theorem of the cited works in the form used. More importantly, for a decidable (Δ₀) relation R, such an F does exist by bounded search. Thus the proposition is either misstated or vacuous. The same problem infects Theorem 4.10 and Corollary 6.4, which transfer the alleged constructive barrier to PA.
  3. [Lemma 4.6; §8, (8.111)] Lemma 4.6 attempts a diagonal argument against a Σ₁ predicate Dec(e,n,m) 'deciding' PrimeΠ(m). The step 'by the diagonal lemma there exists n_e such that PrimeΠ(n_e) ↔ ¬Dec(e,n_e,n_e)' conflates a formula with its Gödel number and presumes that primality is an undecidable semantic property. Since PrimeΠ is Δ₀ and decidable in HA, no such contradiction arises. The Rice-style analogy is also unsound: Rice's theorem concerns semantics of partial computable functions, not decidable arithmetical predicates. The same issue appears in §8, (8.111), where a non-uniformization theorem is invoked to assert the existence of primes beyond any machine's 'operational horizon'.
  4. [Thm. 5.9; §5.4–5.5] Theorem 5.9 claims that forcing over models of HA yields generic extensions M[G1] and M[G2] with M[G1]⊨GC*Π and M[G2]⊨¬GC*Π. This is not a legitimate use of forcing: forcing is a technique for set theory, not for Heyting Arithmetic, and the paper provides no formal definition of the forcing relation for HA or proof that the generic extensions preserve HA. Moreover, the later 'derivation' of the Euler product from Bekić's lemma (Logic 5.11, Theorem 5.18) is not a derivation within HA: it uses analytic convergence, classical manipulations, and an unproved fixed-point schema (Thesis 5.13). These sections are speculative and do not provide a rigorous alternative proof of the paper's central thesis.
minor comments (5)
  1. [Throughout] The notation is inconsistent: PrimeΠ is sometimes described as Π₁, sometimes as Π⁰₁, and sometimes as Δ₀ (e.g., Def. 2.7 vs. Def. 4.2 vs. §8, 8.110). This inconsistency is not merely cosmetic; it drives the central confusion.
  2. [Def. 2.7, Remark] The Remark after Def. 2.7 invokes Markov's Principle and claims ¬¬Comp(n)→Comp(n) is not derivable in HA. For a bounded predicate Comp(n), HA does prove Comp(n) ∨ ¬Comp(n), independently of Markov's Principle. The remark should be corrected or removed.
  3. [§3, Def. 3.4/3.5] The geometric translation is informal: 'Rect(a,b;n)' is asserted to be Δ₀ and locally decidable, but the intended relationship between the geometric configuration Γ(n) and the arithmetic equality A(PQRS)=n is never formally specified. Figures 2–6 are illustrative and do not constitute a proof.
  4. [§5.3, Heuristic 5.7] The claim that a Cantor-style diagonal argument on rational aspect ratios yields an 'irrational slope' corresponding to a prime is mathematically incoherent: the enumeration is countable and there is no uncountable space of 'potential divisive configurations' in arithmetic.
  5. [§7.4–7.6] The entropy–packing and 'cost of knowledge' heuristics introduce constants Φ and k without any derivation from the stated formalism. Equations (7.102)–(7.109) are heuristic analogies, not theorems, and should be clearly labeled as such if the paper is revised.

Circularity Check

3 steps flagged · score 7.0 of 10

Central barrier is stipulated: bounded primality is labeled undecidable Π1, non-uniformization is asserted as Thesis then cited, and the Euler product assumes unique factorization.

  1. other [Definition 2.7; Remark after Def 2.7; Abstract]
    "PrimeΠ(n) ⇐⇒ n>1∧∀a,b≤n[a·b=n⇒a=1∨b=1] ... Consequently, PrimeΠ(n) is not constructively decidable, even though it is arithmetically Π0_1 in PA."

    The whole barrier (Theses 2.5/2.6, Prop 4.7, Thm 6.5, §7.1) reaches primes only through the classification of PrimeΠ as an undecidable Π1 predicate. But the displayed definition has only bounded quantifiers; in HA every bounded formula is decidable by induction on the bound, so HA proves PrimeΠ(n)∨¬PrimeΠ(n). The paper's own Abstract says 'both searches are bounded, both predicates are decidable,' and §8 (8.110) calls such predicates 'Δ0 because all quantifiers range over explicit finite domains.' Thus the load-bearing 'undecidable Π1' premise is asserted in the Remark against the paper's own definition and abstract, so the barrier is an input, not a derived result.

  2. other [Ansatz 2.3; Thesis 2.5; Proposition 4.5; Observation after Def 2.9]
    "Ansatz 2.3 ... a proof in HA of such a sentence is taken to determine a total functional t ... Thesis 2.5: No total primitive recursive functional E can uniformly transform Π1 predicates—i.e., elements of PrimeΠ—into explicit Σ1 witnesses within HA."

    The paper's conclusion that GC*Π has no total Σ1 constructor is derived from the non-uniformization claim of Thesis 2.5. But Thesis 2.5 is not proved; it is stipulated as an Ansatz/Thesis, and Proposition 4.5 then restates the same claim as 'By [Friedman, 1975; Beeson, 1985] ... No total primitive-recursive function F satisfies ...' with no derivation. The Observation after Def 2.9 and Logic 6.3 then use this restatement as the reason GC*Π cannot be realized. The 'prediction' is therefore the assumption itself, merely renamed as a theorem.

1 more flagged steps
  1. renaming known result [§5.4; Logic 5.11; Propositions 5.15, 5.17; Theorem 5.18]
    "the Euler Product arises not as an analytic artifact but as the diagonal solution of a purely logical recursion, derived in fixed-point logic without arithmetic premises ... Every n∈N corresponds uniquely to a finitely supported function νp:P→N with n=∏p p^{νp}, so that ζ(s)=∏p 1/(1-p^{-s})."

    The Euler product identity is equivalent to unique prime factorization. The fixed-point operator Comp(n)=µX∃a,b[...∨X(a)∨X(b)] only closes under multiplicative decomposition; it does not produce uniqueness. The paper obtains the product only by assuming the free commutative monoid structure on primes (Prop 5.15: 'Let (N,·) be the free commutative monoid on the prime generators P') and then asserting unique decompositions in Prop 5.17. Thus the 'derivation without arithmetic premises' builds the target theorem, unique factorization / the Euler product, into its starting data under the new name 'Bekić decomposition'.

full rationale

The paper is not circular in the usual self-citation sense: the citations are to Friedman, Beeson, and Kleene, not to the author's own prior work. However, the central claim that no total Σ1 constructor exists for GC*Π is not derived from an independent mathematical fact. It is built from two stipulated inputs: (1) PrimeΠ, although defined with bounded quantifiers and declared decidable in the paper's own Abstract and §8, is asserted in the Remark after Def 2.7 to be a constructively undecidable Π1 predicate; and (2) the impossibility of uniform extraction for such predicates is introduced as Ansatz 2.3/Thesis 2.5 and then re-cited as Proposition 4.5. Every later barrier result inherits these two premises, so the conclusion is forced by the chosen definitions rather than by a derivation. Additionally, the Euler-product section claims to derive a classical theorem 'without arithmetic premises' while assuming unique factorization, the very content of that theorem. The score is high because the paper's main advertised result—a uniform realizability barrier to prime conjectures—reduces to its own stipulated classification and Thesis. The honest mathematical content that remains (bounded primality is decidable, HA has decidable bounded formulas, etc.) is standard and not circular, but it contradicts rather than supports the paper's central barrier.

Assumptions & free parameters 2 free parameters · 6 assumptions · 3 invented entities

The central claim rests on four unestablished inputs: (1) Ansatz 2.3's uniformity demand, (2) Thesis 2.5/2.6 stated as a thesis and cited back as a theorem, (3) the classification of a bounded decidable predicate as an unbounded constructively-undecidable Π₁ predicate, and (4) invented machinery (Prime Beaver, forcing extensions, Cert, Φ) whose properties are asserted rather than derived. The only standard-mathematics inputs (UFD for the Euler product; trial division for the sieve machine) are textbook content. Net: the paper adds postulates and relabelings, not supported consequences.

free parameters (2)
  • Φ (golden-ratio constant) = (1+√5)/2 ≈ 1.618
    Prop 5.12 posits the ratio recurrence φ_{n+2}/φ_{n+1} = 1 + 1/(φ_{n+1}/φ_n) with no derivation; its fixed point is the golden ratio, named 'the constant Φ,' then used in Prop 5.14 (k(n) ~ log_Φ n) and Heuristic 7.4. The recurrence is chosen by hand to produce Φ; it is not forced by the problem.
  • k (cost/entropy normalizing constant) = unspecified
    Heuristic 7.6 asserts CostF(p) ∝ −∂S_n/∂n|_{n=p} ≈ k/ln p and Heuristic 7.4 defines S_n = k log W_n; k is a free normalizing constant that makes the desired '∼1/ln p' and '→Φ' conclusions read off the definitions.
assumptions (6)
  • domain assumption Ansatz 2.3: existence in HA is evaluated only via uniform total realizers (BHK witnessability); 'existence in principle' is not a semantic resource.
    This semantic postulate is the frame for the entire barrier: once witness extraction must be uniform and total, any failure to Skolemize is read as a logical obstruction. Standard for full BHK, but the paper relies on it to convert open arithmetic questions into claimed impossibilities (§2.2).
  • ad hoc to paper Thesis 2.5/2.6: 'No total primitive recursive functional E can uniformly transform Π₁ predicates into explicit Σ₁ witnesses within HA' — stated as a thesis before proof.
    The conclusion of the paper is assumed at the outset and later 'proved' by citing [Friedman 1975; Beeson 1985] (Prop 4.5, Lemma 4.6). Those works contain no such theorem for predicates with decidable matrices; the thesis is false for decidable P (e.g., P(n):=0=0 is trivially uniformizable).
  • ad hoc to paper Classification of PrimeΠ(n) (Def 2.7: n>1 ∧ ∀a,b≤n[a·b=n ⇒ a=1∨b=1]) as a constructively undecidable unbounded Π₁ predicate.
    Bounded formulas are decidable in HA; the paper's own abstract and §8 (8.110) concede primality is ∆⁰₀. The barrier for primes exists only under this false classification.
  • standard math Unique factorization / N as free commutative monoid on primes, used as input to the Euler-product 'derivation' (Prop 5.15-5.18, §5.4).
    FTA is standard, but Logic 5.11 claims the Euler product is 'derived in fixed-point logic without arithmetic premises' — the premises include exactly the factorization structure that constitutes the identity.
  • ad hoc to paper Speedup premise: 'no arithmetical theory extending PA can have uniformly bounded proofs for an infinite family of true sentences' (Thm 6.11).
    False in general (n=n has constant-length proofs for all n). Gödel's speedup theorem compares theories, not uniform proof lengths within one theory; the oracle-violation result depends on this invented premise.
  • ad hoc to paper Rice's theorem / diagonal lemma applied to arithmetical primality (Lemma 4.6).
    Primeness is a decidable arithmetical predicate, not a semantic property of programs; the diagonal construction as written does not yield a fixed-point numeral with the asserted property, so the contradiction HA ⊢ ⊥ does not follow.
invented entities (3)
  • Prime Beaver PB and packing machines PM
    purpose: To assert deg(PB) = 0′ and that PB dominates every total recursive function, transferring Busy-Beaver results to a 'prime number machine' whose halting encodes compositeness.
    Definitions 5.1-5.2 restate the Busy Beaver on trial-division machines; the lower-bound Lemma 5.5 is an incoherent sketch, so the claimed Turing degree is not established and the entity has no falsifiable handle.
  • Generic filters/extensions M[G1], M[G2] for HA (Thm 5.9)
    purpose: To claim GC*Π is independence-style undecided over HA, by analogy with Cohen forcing for ZFC.
    Σ₁ facts about numerals are absolute across models of arithmetic; one cannot force new factors into a prime or remove them from a composite in a model of HA/PA. The construction is not coherent.
  • Σ₁ certificate predicate Cert(p,w) (Def 6.1)
    purpose: To define the witnessing form WGC and conclude that constructive provability would require a uniform Skolem function, 'the very operation prohibited.'
    For the decidable predicate PrimeΠ as defined, certificates are bounded search witnesses; the claim that WGC presupposes a prohibited uniform extractor presupposes the barrier thesis.

how reviews work

0 comments
Cite this review

Pith. "Pith review of An Intuitionistic Glance at Primes." pith.science (2026). https://pith.science/paper/KFTG52XV

@misc{pith2026251107774,
  author       = {Pith},
  title        = {Pith review of: An Intuitionistic Glance at Primes},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/KFTG52XV}},
  note         = {Machine review of arXiv:2511.07774}
}
abstract

This paper gives a proof-theoretic account of how positive integers must be classified as $1$, prime, or composite in intuitionistic logic. Compositehood is expressed in $\Sigma^0_0$ by exhibiting a factorization; primality is expressed in $\Pi^0_0$ by exhibiting a lack of interior factorization. Because both searches are bounded, both predicates are decidable. Organizing the checks in stages yields a recursive sieve for the primes, a characterization of modular cancellation, and finite arithmetic certificates. The final sections distinguish what Heyting Arithmetic ($\mathsf{HA}$) proves internally from what depends on the standard interpretation of $\mathbb{N}$.

Figures

Figures reproduced from arXiv: 2511.07774 by the authors.

Figure 1
Figure 1. Predicting the decomposition of cuboids would effectively provide an oracle . Can the semantics of primality (gold) be syntactically separated from the “combinatorial entropy” of decompositions (right)? This question frames the present investigation. Let mathematics correspond to the greatest rigor after assumption; then logic will be the rigor before assumption. In this spirit, we examine the boundary where the two… view at source ↗
Figure 2
Figure 2. A 2 × 2 rectangular packing realizing Comp(4). The configuration makes the multiplicative structure of 4 explicit (blue) within the grid semantics of G. In particular, taking E = Set gives soundness and completeness with respect to ordinary (set-based) models. Lemma 3.2 (Geometric Reduction Principle). For any geometric theory G and geometric sequent σ, |=G σ ⇐⇒ |=L σ (3.13) for every logic L whose semantics are red… view at source ↗
Figure 3
Figure 3. The number 6 and 8 admit consistent rectangular decompositions, while 5 and 7 yield none. This illustrates the asymmetry of verification: composites produce explicit local witnesses (blue), whereas primality is detected only through the global (Π1) absence of such configurations. Observation. Given an explicit rectangular packing, compositeness is decid￾able by a bounded constructive procedure. Let Turn3(γ) denote a… view at source ↗
Figures from the paper (3 more)
Figure 4
Figure 4. Figure 4: Primality as a logical Farey sequence problem, connecting to [Franel, 1924], on xy = n. Factor pairs within the finite bound a, b ≤ D (solid points) are detected by the bounded verifier, while those beyond the window remain invisible. Composites with large factors thus…
Figure 5
Figure 5. Figure 5: Combinatorial growth in n = 9. The sequence of structural configurations (gray) follows a fractal pattern until a composite witness appears (blue). As combinatorial complexity increases, local configurations become compressible. Proof. For any fixed divisor bound D, th…
Figure 6
Figure 6. Figure 6: Illustration of a bounded divisor lattice classifying primes (gold) while restricted to factors {2, 3}. 25 (purple) is not recognized as composite by the local rule Comp2 (n)≡ ∃a, b∈ {2, 3} [a·b = n, a, b > 1]: The factors (5, 5) lie outside the enumerated lattice. Thi…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

42 extracted references · 9 canonical work pages

  1. [1]

    High-Level Methods for Quantum Computation and Information

    Samson Abramsky. High-Level Methods for Quantum Computation and Information . In Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 410--414. IEEE Computer Society, 2004. doi:10.1109/LICS.2004.1319630

    arXiv 2004

  2. [2]

    Tom M. Apostol. Introduction to Analytic Number Theory . Springer, 1976. doi:10.1007/978-1-4757-5579-4

    doi:10.1007/978-1-4757-5579-4 1976

  3. [3]

    Michael J. Beeson. Foundations of Constructive Mathematics . Springer, 1985. doi:10.1007/978-3-642-68952-9

    doi:10.1007/978-3-642-68952-9 1985

  4. [4]

    A machine-independent theory of the complexity of recursive functions

    Manuel Blum. A machine-independent theory of the complexity of recursive functions . Journal of the ACM, 14 0 (2): 0 322--336, 1967. doi:10.1145/321386.32139

    arXiv 1967

  5. [5]

    L. E. J. Brouwer. Historical Background, Principles and Methods of Intuitionism . North-Holland, 1975. doi:10.1016/B978-0-7204-2076-0.50062-3

    work page doi:10.1016/b978-0-7204-2076-0.50062-3 1975

  6. [6]

    Samuel R. Buss. Handbook of Proof Theory . Elsevier, 1998. ISBN 9780444551375

    1998

  7. [7]

    Über eine elementare Frage der Mannigfaltigkeitslehre

    Georg Cantor. Über eine elementare Frage der Mannigfaltigkeitslehre . Jahresbericht der Deutschen Mathematiker-Vereinigung, 1: 0 75--78, 1891

  8. [8]

    Contributions to the Founding of the Theory of Transfinite Numbers

    Georg Cantor. Contributions to the Founding of the Theory of Transfinite Numbers . Dover Publications, New York, 1955

    1955

Show all 42 references
  1. [9]

    Paul J. Cohen. The Independence of the Continuum Hypothesis . Proceedings of the National Academy of Sciences of the United States of America, 50 0 (6): 0 1143--1148, 1963. doi:10.1073/pnas.50.6.1143

    1963 doi

  2. [10]

    Paul J. Cohen. The Independence of the Continuum Hypothesis, II . Proceedings of the National Academy of Sciences of the United States of America, 51 0 (1): 0 105--110, 1964. doi:10.1073/pnas.51.1.105

    1964 doi

  3. [11]

    Nigel J. Cutland. Computability: An Introduction to Recursive Function Theory . Cambridge University Press, 1980. ISBN 9780521294652

    1980

  4. [12]

    Ekert and Richard Jozsa

    Artur K. Ekert and Richard Jozsa. Quantum Computation and Shor's Factoring Algorithm . Reviews of Modern Physics, 68 0 (3): 0 733--753, 1996. doi:10.1103/RevModPhys.68.733

    1996 doi

  5. [13]

    Systems of predicative analysis

    Solomon Feferman. Systems of predicative analysis . Journal of Symbolic Logic, 29 0 (1): 0 1--30, 1964. doi:10.2307/2269764

    1964 doi

  6. [14]

    Fourman and Dana S

    Michael P. Fourman and Dana S. Scott. Sheaves and Logic . In Michael P. Fourman, Christopher J. Mulvey, and Dana S. Scott, editors, Applications of Sheaves, volume 753 of Lecture Notes in Mathematics, pages 302--401. Springer, 1979. doi:10.1007/BFb0061824

    1979 doi

  7. [15]

    Les suites de Farey et le problème des nombres premiers

    Jérôme Franel. Les suites de Farey et le problème des nombres premiers . Mathematische Annalen, 83 0 (1--2): 0 8--29, 1924. purl: PPN252457811\_1924

    1924

  8. [16]

    Some Systems of Second Order Arithmetic and Their Use

    Harvey Friedman. Some Systems of Second Order Arithmetic and Their Use . Proceedings of the International Congress of Mathematicians, pages 235--242, 1975

    1975

  9. [17]

    Systems of Second Order Arithmetic with Restricted Induction, I

    Harvey Friedman. Systems of Second Order Arithmetic with Restricted Induction, I . Journal of Symbolic Logic, 41 0 (2): 0 557--558, 1976

    1976

  10. [18]

    Letter to Leonhard Euler, June 7, 1742

    Christian Goldbach. Letter to Leonhard Euler, June 7, 1742 . Opera Omnia Leonhardi Euleri, Series IV A, 1: 0 43--47, 1742

  11. [19]

    Über die Vollständigkeit des Logikkalküls

    Kurt Gödel. Über die Vollständigkeit des Logikkalküls . Monatshefte für Mathematik und Physik, 37 0 (1): 0 349--360, 1930. doi:10.1007/BF01700692

    1930 doi

  12. [20]

    On the length of proofs

    Kurt Gödel. On the length of proofs . In Collected Works, Vol. I: Publications 1929–1936, pages 396--399. Oxford University Press, Oxford, 1986. (Published posthumously)

    1929

  13. [21]

    H. A. Helfgott. Minor arcs for Goldbach's problem . Preprint, 114, 2013. doi:10.48550/arXiv.1205.5252

    2013 doi arXiv

  14. [22]

    Die formalen Regeln der intuitionistischen Logik

    Arend Heyting. Die formalen Regeln der intuitionistischen Logik. I, II, III . Sitzungsber. Preu . Akad. Wiss., Phys.-Math. Kl. , 1930: 0 42--56, 57--71, 158--169, 1930

    1930

  15. [23]

    William A. Howard. The Formulae-as-Types Notion of Construction . To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 479--490, 1980

    1980

  16. [24]

    Über die angenäherte Darstellung der Irrationalzahlen durch rationale Brüche

    Adolf Hurwitz. Über die angenäherte Darstellung der Irrationalzahlen durch rationale Brüche . Mathematische Annalen, 39: 0 279--284, 1891

  17. [25]

    Metamathematics of First-Order Arithmetic

    Petr Hájek and Pavel Pudlák. Metamathematics of First-Order Arithmetic . Springer, 1998. ISBN 978-3-540-63648-9

    1998

  18. [26]

    E. T. Jaynes. Information Theory and Statistical Mechanics . Physical Review, 106 0 (4): 0 620--630, 1957. doi:10.1103/PhysRev.106.620

    1957 doi

  19. [27]

    Jones and Hans Beki ć

    Cliff B. Jones and Hans Beki ć . Programming Languages and Their Definition , 1984. (Published posthumously)

    1984

  20. [28]

    Stephen C. Kleene. Introduction to Metamathematics . North-Holland, 1952. ISBN 9780444896230

    1952

  21. [29]

    On the Arithmetical Hierarchy

    Stephen Cole Kleene. On the Arithmetical Hierarchy . Journal of Symbolic Logic, 8 0 (2): 0 109--124, 1943. doi:10.2307/2267551

    1943 doi

  22. [30]

    Kolmogorov

    Andrei N. Kolmogorov. On the Principle of the Excluded Middle . Matematicheskii Sbornik, 1925

    1925

  23. [31]

    Interpretation of Non-Finitist Proofs, Part I

    Georg Kreisel. Interpretation of Non-Finitist Proofs, Part I . Journal of Symbolic Logic, 16 0 (4): 0 241--267, 1951. doi:10.1017/S0022481200100581

    1951 doi

  24. [32]

    Irreversibility and Heat Generation in the Computing Process

    Rolf Landauer. Irreversibility and Heat Generation in the Computing Process . IBM Journal of Research and Development, 5 0 (3): 0 183--191, 1961. doi:10.1147/rd.53.0183

    1961 doi

  25. [33]

    On Non-Computable Functions

    Tibor Radó. On Non-Computable Functions . Bell System Technical Journal, 41 0 (3): 0 877--884, 1962. doi:10.1002/j.1538-7305.1962.tb00480.x

    1962

  26. [34]

    Henry G. Rice. Classes of Recursively Enumerable Sets and Their Decision Problems . Transactions of the American Mathematical Society, 74 0 (2): 0 358--366, 1953. doi:10.2307/1990888

    1953 doi

  27. [35]

    The Fractal Logic of Phi-adic Recursion

    Milan Rosko. The Fractal Logic of Phi-adic Recursion . Preprint, 2025. doi:10.48550/arXiv.2510.08934

    2025 doi arXiv

  28. [36]

    Peter W. Shor. Algorithms for Quantum Computation: Discrete Logarithms and Factoring . In Proceedings of the 35th Annual Symposium on Foundations of Computer Science (FOCS), pages 124--134. IEEE, 1994. doi:10.1109/SFCS.1994.365700

    1994

  29. [37]

    Solomonoff

    Ray J. Solomonoff. A Formal Theory of Inductive Inference. Part I . Information and Control, 7 0 (1): 0 1--22, 1964 a . doi:10.1016/S0019-9958(64)90223-2

    1964 doi

  30. [38]

    Solomonoff

    Ray J. Solomonoff. A Formal Theory of Inductive Inference. Part II . Information and Control, 7 0 (2): 0 224--254, 1964 b . doi:10.1016/S0019-9958(64)90131-7

    1964 doi

  31. [39]

    Contributions to the Theory of Models, I

    Alfred Tarski. Contributions to the Theory of Models, I . Indagationes Mathematicae, 16 0 (3): 0 572--581, 1954. doi:10.2307/2268420

    1954 doi

  32. [40]

    Troelstra

    Anne S. Troelstra. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis . Springer, 1973. doi:10.1007/BFb0066739

    1973 doi

  33. [41]

    Troelstra and Dirk van Dalen

    Anne S. Troelstra and Dirk van Dalen. Constructivism in Mathematics: An Introduction . North-Holland, 1988. ISBN 9780444703699

    1988

  34. [42]

    Uber die Anzahl der Primzahlen unter einer gegebenen Gr\

    Hans von Mangoldt. Zu Riemanns Abhandlung: \"Uber die Anzahl der Primzahlen unter einer gegebenen Gr\"osse . Journal f\"ur die reine und angewandte Mathematik, 114: 0 255--305, 1895

Pith tools

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