Orthocomplemented subspaces and partial projections on a Hilbert space

Iosif Petrakis

REVIEW 3 major objections 3 minor 63 references

Orthocomplemented subspaces and partial projections on a Hilbert space

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

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

Pith's one-line read Orthocomplemented subspaces of a Hilbert space are in bijection with partial projections on it, giving a constructive version of the classical subspace–projection correspondence that avoids locatedness.

desk verdict A genuinely useful constructive two-dimensional treatment of subspaces and projections, but the main bijection silently inherits an AC! dependency that should be stated up front. read the letter →

arxiv 2508.15906 v1 pith:EFAY37UN submitted 2025-08-21 quant-ph

Iosif Petrakis This is my paper · ORCID

classification quant-ph MSC 03F6046C0581P10

keywords constructivemathematicsHilbertspacesorthocomplementedsubspacespartialprojectionsquantumlogiclocatednessBishopsettheoryuniquechoice

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 a fully constructive counterpart to the classical correspondence between closed subspaces of a Hilbert space and projection operators. It does so by replacing a single subspace with an orthocomplemented pair of orthogonal closed subspaces, and by replacing total projections with partial projections defined on the sum of the two subspaces. The main claim is that these two objects stand in a bijection that preserves order, strictness, and totality, so that every closed-subspace question can be reformulated as a pair of orthogonal subspaces equipped with a partial projection. If correct, this removes the standing restriction of locatedness from much of constructive Hilbert space theory and yields a constructive quantum logic closer to classical orthomodular logic than earlier intuitionistic versions.

What carries the argument

The central object is the orthocomplemented subspace L = (L1, L0), a pair of orthogonal closed subspaces that acts as a 'two-dimensional' substitute for a single closed subspace. The key theorem is the construction (Theorem 4.3) of the partial projection P_L^1 : L1 + L0 → L1, defined by the unique orthogonal decomposition x = l1 + l0, which exists without assuming locatedness. This partial projection is self-adjoint, idempotent, bounded, and satisfies the orthogonality condition (x − P_L^1(x)) ⊥ L1. The bijection theorem (Theorem 6.4) then shows that the maps L ↦ P_L^1 and P ↦ (range(P), kernel(P)) invert each other and respect order, strictness, and totality. The machinery depends on Myhill

What would settle it

Find two distinct orthocomplemented subspaces (L1, L0) and (M1, M0) that give the same partial projection under the map L ↦ P_L^1; or find an orthogonal pair of closed subspaces whose sum is not the domain of any self-adjoint idempotent bounded partial operator. Theorem 6.4 says both are impossible.

Watch

Extended reading notes

Core claim

The paper's central claim is Theorem 6.4: for every Hilbert space H there is a bijection between the totality of orthocomplemented subspaces of H and the totality of partial projections on H. An orthocomplemented subspace is a pair L = (L1, L0) of closed subspaces that are orthogonal to each other; its domain is the closed sum L1 + L0. To each such pair the paper assigns the partial projection P_L^1 that sends x = l1 + l0 to l1. Conversely, to a partial projection P (a self-adjoint, idempotent, bounded partial operator) it assigns the pair formed by the range of P and the kernel of P. The paper proves that these two assignments are inverse, strongly extensional functions, and that they prese

Load-bearing premise

The proof needs Myhill's axiom of unique choice to turn the unique decomposition x = l1 + l0 into a function; if unique choice is not available, the stated bijection is not derived, and the paper notes that avoiding it would require adding closure and completeness witnessing data to the framework.

Editorial extensions

If this is right

Every orthocomplemented subspace of H yields a partial projection operator without any locatedness assumption, so projection theory can be developed for all pairs of orthogonal closed subspaces.
Located subspaces of H are exactly the total orthocomplemented subspaces, giving a lattice-theoretic characterisation of locatedness and unifying it with totality.
The quotient Hilbert space can be defined for any orthocomplemented subspace, not just for located ones, with the classical quotient of a located subspace appearing as the total case.
The bijection transfers the lattice operations on orthocomplemented subspaces to operations on partial projections, yielding a complemented quantum lattice that satisfies the classical negation laws.
Partial projections become first-class objects in constructive Hilbert space theory, in parallel to the role of partial Boolean-valued functions in Bishop–Cheng measure theory.
Commuting partial projections compose to a partial projection and satisfy the partial analogues of the classical formulas for meet and join, without relying on the classical law (L ∧ M)^⊥ = L^⊥ ∨ M^⊥.

Reading between the lines

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

Going beyond the paper: if the proof's use of AC! is eliminated by adding explicit closure and completeness witnessing data, the same bijection should remain provable in other constructive frameworks, making it a natural target for formalisation in type theory.
Going beyond the paper: the pair (range, kernel) of a partial projection suggests a constructive treatment of unbounded self-adjoint operators as partial operators with dense domain, since the domain is no longer required to be located.
Going beyond the paper: the quotient construction for non-located orthocomplemented subspaces may provide a new route to constructive spectral theory by avoiding the classical detour through locatedness.
Going beyond the paper: because total orthocomplemented subspaces coincide with located subspaces, one could test whether the complemented quantum lattice collapses to the intuitionistic one exactly when totality is imposed, which would make the two constructive quantum logics different only in their treatment of partiality.

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.

Desk Editor's Note

read the letter

The paper does something real: it replaces the one-dimensional located-subspace/projection correspondence with a two-dimensional one between orthocomplemented subspaces (pairs of orthogonal closed subspaces) and partial projections, and proves a bijection between those totalities. That is a natural and useful extension of the author's complemented-subsets program and of Bridges–Svozil quantum logic. The quotient construction without locatedness, the lattice laws of complemented quantum logic, and the partial linear space abstraction are all worth having. The core bijection proof is detailed and mostly self-contained, and I see no sign of fitting or circularity.

The main soft spot is the choice axiom. Theorem 4.3 is explicitly labeled (AC!), and Theorem 6.4 depends on it but is stated without that annotation. A reader reasonably expects a choice-free bijection, and the paper does not supply one. The author acknowledges this after the proof of 4.3, noting that avoiding AC! would require adding closure and completeness witnessing data. That is an honest caveat, but it needs to be moved into the statement of the main theorem. The fix is straightforward: either state the bijection under AC! or build the witnessing data into the definitions of orthocomplemented subspace and partial projection.

Prop 4.5 has a smaller issue: the completeness justification for the quotient says that dompL) is closed in H and therefore complete, but completeness of the quotient is about the quotient norm, not the norm inherited from H. The later isometry with L0 gives the correct argument, so the result stands, but the proof as written is sloppy. Also, Theorem 6.4 asserts without comment that the image and kernel subspaces are closed; that should be stated explicitly or proved in the surrounding text.

These are repairable, not fatal. The mathematics looks coherent, the citation pattern is heavy on the author's own work but not misleading, and the claimed novelty is genuinely present: the bijection itself and the non-located construction of P_L^1 are new. I would send this to a serious referee. The author should be asked to clarify the choice status and patch the completeness argument, but the paper deserves a real review rather than a desk rejection.

Referee Report

3 major / 3 minor

Summary. The paper introduces a constructive, two-dimensional counterpart to closed subspaces of a Hilbert space: an orthocomplemented subspace L=(L1,L0) is a pair of orthogonal closed subspaces. To each such L the author attaches a partial projection P_L^1 defined on the (not necessarily located) domain L1+L0, and conversely each partial self-adjoint idempotent bounded operator P gives a pair (range(P), ker(P)). The central result, Theorem 6.4, asserts a bijection between the totality of orthocomplemented subspaces and the totality of partial projections, preserving order, strictness, and totality. The paper further develops quotient Hilbert spaces without locatedness, introduces partial linear spaces, and uses the bijection to define a 'complemented quantum logic' whose negation is component swapping. The development is carried out in Bishop Set Theory, and the key projection construction is explicitly based on Myhill's unique choice axiom AC!.

Significance. If the technical issues are fixed, the paper gives a genuinely useful constructive reformulation: it replaces the locatedness hypothesis by an explicit pair of orthogonal closed subspaces, so that closed-subspace questions can be studied through partial projections. The connection to Bishop-Cheng complemented subsets is well motivated, and the paper is honest about the use of AC! and about the witnessing data needed to avoid it. The quotient-space construction in Section 4 is a notable conceptual contribution, and the lattice-theoretic characterisation of locatedness in Theorem 3.6 is elegant. The paper is not machine-checked, but the central bijection is proved from definitions with explicit axiom tracking. The main obstacles are a misprinted equality of partial operators and a few places where theorem statements do not carry the assumptions their proofs actually use.

major comments (3)

[Definitions 5.1 and 6.1] The equality of partial bounded operators is misprinted: in both definitions the second conjunct reads 'x∈dom(U) ⇒ x∈dom(U)' instead of the intended 'x∈dom(U) ⇒ x∈dom(T)'. As written, the relation is not symmetric and does not force the domains to coincide. This equality is used in the proof of Theorem 6.4(i) to show that j is a function ('P=Q ... equalities L1_P=L1_Q and L0_P=L0_Q follow immediately'). Please correct the definitions; with the intended clause the argument goes through.
[Theorem 6.4] The theorem is stated without a choice axiom, but the map i(L)=P_L^1 is constructed in Theorem 4.3, whose proof the paper explicitly labels as resting on Myhill's unique choice AC! (see the paragraph after Theorem 4.3, which also says that avoiding AC! requires adding closure and completeness witnessing data). Hence Theorem 6.4, and later results that inherit this construction (e.g., Proposition 7.3, Corollary 7.4, Proposition 7.5), should either be annotated with (AC!) or state the choice assumption explicitly. The bijection itself is not in question, but its stated domain of validity is.
[Proposition 4.5(i)] The proof claims 'dompLq is complete, since it is closed in H'. Completeness is claimed for the quotient norm ||x||=||P0_L(x)||_H, not for the inherited H-norm; closedness in H does not imply completeness in this new norm. The gap is repairable from part (iii): T_L: dompLq → L0 is a linear isometry onto L0, and L0 is closed in H and therefore complete. Since the quotient equality identifies exactly the kernel of P0_L, this isometry supplies the missing completeness. Please reorder the proof or add this argument.

minor comments (3)

[Throughout] There are numerous typographical slips: 'correpsondence', 'biljection', 'existence' spelled as 'existsence', 'Moroever' in the proof of Proposition 7.3, and duplicated pIntQL2 in Proposition 3.4. These should be corrected in a final pass.
[Proposition 4.5] The notation 'dompLq/L' is potentially confusing because L is a pair (L1,L0), not a subspace. The intended quotient is by the kernel of P0_L (which in the total case reduces to H/L1). Please clarify the notation.
[Definition 5.1] The inequality on BpX,Yq contains an ill-formed disjunct in the displayed formula ('x∈dom(T) & x∈dom(U)^‰' appears garbled). Please check the typesetting of the inequality relation.

Circularity Check

1 steps flagged · score 2.0 of 10

Central bijection in Theorem 6.4 is independently proved; the only definitional/conventional part is the transported order and inequality used to state (ii)-(iii), and the proof inherits the explicitly stated AC! dependence from Theorem 4.3.

self definitional [Theorem 6.4, Section 6 (definitions of the order on PpHq and inequality on SpHq, clauses (ii)-(iii))]
"If we define the partial order on PpHq by the rule: P ≤ Q :⇔ j(P) ≤ j(Q) :⇔ L_P ≤ L_Q, and if we define the inequality on SpHq by the rule: L ≠_SpHq M :⇔ i(L) ≠_PpHq i(M) :⇔ P^1_L ≠_PpHq P^1_M, then ... (iii) i and j preserve the corresponding partial orders."

The order on PpHq is stipulated as the pullback of the SpHq-order along j, and the inequality on SpHq is stipulated as the pullback of the PpHq-inequality along i. Hence clause (iii), and the injectivity/strong-extensionality part of (ii), are not independent results: i(L) ≤ i(M) holds iff j(i(L)) ≤ j(i(M)) iff L ≤ M (using (i)), and L ≠ M is defined to mean i(L) ≠ i(M). These clauses are true by construction. They do not affect the substantive bijection in (i), which is proved from Theorem 4.3 and the range/kernel construction.

full rationale

The paper's central result, Theorem 6.4(i), is a genuine derivation: i(L)=P_L^1 is constructed in Theorem 4.3 from the unique orthogonal decomposition of elements of L1+L0 (using AC!, explicitly stated), and j(P)=(range P, ker P) is built directly from idempotence and self-adjointness; the inverse equalities L = L_{P_L^1} and P = P^1_{L_P} are proved by direct computation. No data are fitted and no external 'prediction' is renamed. The frequent self-citations ([31], [32], [48], [49], etc.) are analogical or background; the Hilbert-space bijection is not imported from them. The only reduction-by-construction found is in Theorem 6.4's structure-transport definitions: the order on PpHq is defined as j(P)≤j(Q) and the inequality on SpHq as i(L)≠i(M), so the stated order/inequality preservation and injectivity/strong-extensionality clauses are immediate from those definitions. This is a presentational tautology, not a load-bearing circularity. The proof also depends on AC! via Theorem 4.3; the paper states this for Theorem 4.3 ('The proof of Theorem 4.3(ii) rests on Myhill's axiom unique choice (AC!)') and even sketches how to avoid it with witnessing data, but Theorem 6.4's statement does not repeat the annotation. That is an assumption-transparency issue, not circularity. Overall score 2.

Assumptions & free parameters 0 free parameters · 5 assumptions · 3 invented entities

There are no fitted parameters and no data-driven inputs. The central claim rests on the inherited BISH/BST framework, the explicitly flagged unique choice axiom AC!, and standard facts about closed subspaces and locatedness. The new objects are mathematical definitions, not empirically postulated entities.

assumptions (5)

domain assumption Bishop Set Theory (BST) and BISH constructive foundations, including extensional inequalities and partial functions
The entire paper is formalized in BST/BISH (Sections 1-2). These are inherited commitments, not proved here.
domain assumption Myhill's axiom of unique choice AC!
Used in Theorem 4.3(ii) and in the proof of ComplQL8 to turn unique existence of decompositions into functions. Explicitly flagged after Theorem 4.3.
standard math A closed subspace of a complete Hilbert space is complete
Needed in Theorem 4.3(i) to take limits of Cauchy sequences in L1 and L0. Standard in constructive metric theory.
domain assumption Locatedness of L is equivalent to L or LK equals H, following Bishop-Bridges results
Theorem 3.6 cites Exercise 37 of [5] and [11]; it underpins the identification of total orthocomplemented subspaces with located subspaces. Not reproved.
standard math The range and kernel of a self-adjoint idempotent bounded partial operator are closed subspaces
Used in Theorem 6.4 to place L1_P and L0_P in SpH; follows from kernels of bounded operators, but left implicit.

invented entities (3)

orthocomplemented subspace (pair (L1,L0) of orthogonal closed subspaces)
purpose: Two-dimensional constructive surrogate for a closed subspace; its domain L1 or L0 supports a partial projection without locatedness.
A definitional notion, not an empirical entity; its mathematical handle is the bijection proved in the paper, not an external falsifiable prediction.
partial projection (self-adjoint idempotent bounded partial operator)
purpose: Computational two-dimensional counterpart to a projection, defined only on the domain of an orthocomplemented subspace.
Definition introduced here; no independent empirical evidence, but it is a defined mathematical object rather than an ad hoc physical entity.
partial linear space
purpose: Abstract algebraic structure motivated by the operations on bounded partial operators.
Auxiliary mathematical definition introduced in Section 5; no empirical handle, and its role is organizational.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Orthocomplemented subspaces and partial projections on a Hilbert space." pith.science (2026). https://pith.science/paper/EFAY37UN

@misc{pith2026250815906,
  author       = {Pith},
  title        = {Pith review of: Orthocomplemented subspaces and partial projections on a Hilbert space},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/EFAY37UN}},
  note         = {Machine review of arXiv:2508.15906}
}

read the original abstract

We introduce the notion of an orthocomplemented subspace of a Hilbert space H, that is, a pair of orthogonal closed subspaces of H, as a two-dimensional counterpart to the one-dimensional notion of a closed subspace of H. Orthocomplemented subspaces are the Hilbert space-analogue to Bishop's complemented subsets. To complemented subsets correspond their characteristic functions, which are partial, Boolean-valued functions. Similarly, to orthocomplemented subspaces of H correspond partial projections on H. Previous work of Bridges and Svozil on constructive quantum logic is an one-dimensional approach to the subject. The lattice-properties of the orthocomplemented subspaces of a Hilbert space is a two-dimensional approach to constructive quantum logic, that we call complemented quantum logic. Since the negation of an orthocomplemented subspace is formed by swapping its components, complemented quantum logic, although constructive, is closer to classical quantum logic than the constructive quantum logic of Bridges and Svozil. The introduction of orthocomplemented subspaces and their corresponding partial projections allows a new approach to the constructive theory of Hilbert spaces. For example, the partial projection operator of an orthocomplemented subspace and the construction of the quotient Hilbert space bypass the standard restrictive hypothesis of locatedness on a subspace. Located subspaces correspond to total orthocomplemented subspaces.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

63 extracted references · 58 canonical work pages

[1]

Aczel, M

P. Aczel, M. Rathjen:Notes on Constructive Set Theory, Report No. 40, 2000/2001, ISSN 1103- 467X. Institut Mittag-Leffler

work page 2000
[2]

Birkhoff, J

G. Birkhoff, J. von Neumann: The Logic of Quantum Mechanics, Annals of Mathematics, Vol. 37, No. 4 (Oct., 1936), pp. 823–843

work page 1936
[3]

Bishop: Foundations of Constructive Analysis, McGraw-Hill, 1967

E. Bishop: Foundations of Constructive Analysis, McGraw-Hill, 1967

work page 1967
[4]

Bishop, H

E. Bishop, H. Cheng:Constructive Measure Theory, Mem. Amer. Math. Soc. 116, 1972

work page 1972
[5]

Bishop, D

E. Bishop, D. S. Bridges: Constructive Analysis, Grundlehren der math. Wissenschaften 279, Springer-Verlag, Heidelberg-Berlin-New York, 1985

work page 1985
[6]

D. S. Bridges: Constructive Functional Analysis, Research Notes in Mathematics, 28, Pitman, London, 1979

work page 1979
[7]

Bridges: Towards a constructive foundation for quantum mechanics

D. Bridges: Towards a constructive foundation for quantum mechanics. In: F. Richman (Ed.) Constructive Mathematics, Proceedings of the New Mexico State University Conference Held at Las Cruces, New Mexico, August 11–15, 1980, Lecture Notes in Mathematics 873, Springer-Verlag, Berlin, 1981, 260–273

work page 1980
[8]

D. S. Bridges: Can constructive mathematics be applied in physics? Journal of Philosphical Logic, 28, 1999, 439–453

work page 1999

Show all 63 references

[9]

D. S. Bridges, F. Richman:Varieties of Constructive Mathematics, Cambridge University Press, 1987

1987
[10]

D. S. Bridges, K. Svozil: Constructive Mathematics and Quantum Physics, International Journal of Theoretical Physics, Vol. 39, No. 3, 2000, 503–515

2000
[11]

D. S. Bridges, L. S. Vîţă:Techniques of Constructive Analysis, in: Universitext, Springer, New York, 2006

2006
[12]

Chan: Foundations of Constructive Probability Theory, Cambridge University Press, 2021

2021
[13]

Ciraulo and G

F. Ciraulo and G. Sambin: The overlap algebra of regular opens, J. Pure Appl. Algebra 214(11), 2010, 1988–1995

2010
[14]

D. W. Cohen:An Introduction to Hilbert Space and Quantum Logic, Springer-Verlag, 1989

1989
[15]

Coquand, H

T. Coquand, H. Lombardi: Hidden constructions in abstract algebra, Krull Dimension, Going Up, Going Down, arXiv.1712.04725v1, 2017

2017 arXiv
[16]

P. J. Daniell: A general form of integral, Annals of mathematics, Second Series, 19 (4), 1918, 279–294

1918
[17]

Engesser, D

K. Engesser, D. M. Gabbay, D. Lehmann (Eds.)Handbook of Quantum Logic and Quantum Struc- tures: Quantum Logic, Elsevier, 2009

2009
[18]

Diener: Constructive Reverse Mathematics, arXiv:1804.05495, 2020

H. Diener: Constructive Reverse Mathematics, arXiv:1804.05495, 2020. 33

2020 arXiv
[19]

Feferman: Constructive Theories of Functions and Classes, in Boffa et

S. Feferman: Constructive Theories of Functions and Classes, in Boffa et. al (Eds.)Logic Collo- quium ’78, Elsevier, 1979, 159–224

1979
[20]

A. M. Gleason: Measures on the Closed Subspaces of a Hilbert Space, J. Math. Mechanics 6(4), 1957, 885–893

1957
[21]

Goldberg: Unbounded Linear Operators: Theory and Applications, McGraw-Hill, 1966

S. Goldberg: Unbounded Linear Operators: Theory and Applications, McGraw-Hill, 1966

1966
[22]

F. L. Grubmüller, I. Petrakis: A Predicative Approach to the Constructive Integration The- ory of Locally Compact Metric Spaces, Journal of Logic and Analysis 17 FDS4, 2025, 1–24, https://doi.org/10.4115/jla.2025.17.FDS4

2025 doi
[23]

P. R. Halmos:Introduction to Hilbert Space and the Theory of Spectral Multiplicity, Second Edi- tion, Chelsea Publishing Company, 1957

1957
[24]

P. R. Halmos:A Hilbert Space Problem Book, Second Edition, Revised and Enlarged, Springer- Verlag, 1982

1982
[25]

R. V. Kadison, J. R. Ringrose:Fundamentals of the theory of operator algebras, Volume 1, Aca- demic Press, 1983

1983
[27]

Landsman: Foundations of Quantum Theory, From Classical Concepts to Operator Algebras, Springer, 2017

K. Landsman: Foundations of Quantum Theory, From Classical Concepts to Operator Algebras, Springer, 2017

2017
[28]

Leinster: A categorical derivation of Lebesgue integration, arXiv:2011.00412, 2023

T. Leinster: A categorical derivation of Lebesgue integration, arXiv:2011.00412, 2023

2011 arXiv
[29]

B. V. Limaye:Functional Analysis, Wiley Eastern Limited, 1981

1981
[30]

Mines, F

R. Mines, F. Richman, W. Ruitenburg:A course in constructive algebra, Springer Science` Busi- ness Media New York, 1988

1988
[31]

Misselbeck-Wessel, I

D. Misselbeck-Wessel, I. Petrakis: Complemented subsets and Boolean-valued, partial functions, Computability, vol. 13, no. 3-4, 2024, pp. 399–431

2024
[32]

Misselbeck-Wessel, I

D. Misselbeck-Wessel, I. Petrakis: Constructive Stone representations for separated swap and Boolean algebras, submitted, 2025

2025
[33]

Misselbeck-Wessel, I

D. Misselbeck-Wessel, I. Petrakis: Boolean Rigs, Algebra Universalis, to appear, 2025

2025
[34]

Misselbeck-Wessel, I

D. Misselbeck-Wessel, I. Petrakis: Richman Rigs Revisited, submitted, 2025

2025
[35]

Myhill: Constructive Set Theory, J

J. Myhill: Constructive Set Theory, J. Symbolic Logic 40, 1975, 347–382

1975
[36]

Palmgren: Constructivist and structuralist foundations: Bishop’s and Lawvere’s theories of sets, Annals of Pure and Applied Logic 163, 2012, 1384–1399

E. Palmgren: Constructivist and structuralist foundations: Bishop’s and Lawvere’s theories of sets, Annals of Pure and Applied Logic 163, 2012, 1384–1399

2012
[37]

Palmgren: Bishop-style constructive mathematics in type theory - A tutorial, Slides, 2013

E. Palmgren: Bishop-style constructive mathematics in type theory - A tutorial, Slides, 2013. http://staff.math.su.se/palmgren/

2013
[38]

Palmgren: Lecture Notes on Type Theory, manuscript, 2014

E. Palmgren: Lecture Notes on Type Theory, manuscript, 2014

2014
[39]

Palmgren, O

E. Palmgren, O. Wilander: Constructing categories and setoids of setoids in type theory, Logical Methods in Computer Science. 10 (2014), Issue 3, paper 25

2014
[40]

Palmgren: Constructions of categories of setoids from proof-irrelevant families, Archive for Mathematical Logic 56, 2017, 51–66

E. Palmgren: Constructions of categories of setoids from proof-irrelevant families, Archive for Mathematical Logic 56, 2017, 51–66

2017
[41]

Palmgren: From type theory to setoids and back, preprint, 2019

E. Palmgren: From type theory to setoids and back, preprint, 2019. 34

2019
[42]

Pavicic, N

M. Pavicic, N. D. Megill: Is Quantum Logic a Logic?, in [17], pp. 23–47
[43]

Petrakis: Borel and Baire sets in Bishop Spaces, in F

I. Petrakis: Borel and Baire sets in Bishop Spaces, in F. Manea et. al. (Eds): Computing with Foresight and Industry, CiE 2019, LNCS 11558, Springer, 2019, 240–252

2019
[44]

Petrakis: Families of Sets in Bishop Set Theory, Habilitationsschrift, LMU, Munich, 2020, available athttps://www.mathematik.uni-muenchen.de/~petrakis/content/Theses.php

I. Petrakis: Families of Sets in Bishop Set Theory, Habilitationsschrift, LMU, Munich, 2020, available athttps://www.mathematik.uni-muenchen.de/~petrakis/content/Theses.php

2020
[45]

Petrakis: Proof-relevance in Bishop-style constructive mathematics, Mathematical Structures in Computer Science, Volume 32, Issue 1, 2022, 1–43

I. Petrakis: Proof-relevance in Bishop-style constructive mathematics, Mathematical Structures in Computer Science, Volume 32, Issue 1, 2022, 1–43. doi:10.1017/S0960129522000159

2022 doi
[46]

Petrakis: Sets Completely Separated by Functions in Bishop Set Theory, Notre Dame Journal of Formal Logic, 65(2): 151-180 (May 2024) DOI: 10.1215/00294527-2024-0010

I. Petrakis: Sets Completely Separated by Functions in Bishop Set Theory, Notre Dame Journal of Formal Logic, 65(2): 151-180 (May 2024) DOI: 10.1215/00294527-2024-0010

2024 doi
[47]

Petrakis: The apart algebra of regular closed sets, in preparation, 2025

I. Petrakis: The apart algebra of regular closed sets, in preparation, 2025

2025
[48]

Constructive Mathematics: Foundation and Practice

I. Petrakis: Topologies of open complemented subsets, in “Constructive Mathematics: Foundation and Practice”, M. Mitrović, M. N. Hounkonnou (Eds.), “Mathematics in Mind" series, Springer, 2026, forthcoming. Also available at arXiv:2312.17095v1, 2023

2026 arXiv
[49]

Petrakis, D

I. Petrakis, D. Wessel: Algebras of complemented subsets, in U. Berger et.al. (Eds):Revolutions and Revelations in Computability, CiE 2022, Lecture Notes in Computer Science 13359, Springer, 2022, 246–258

2022
[50]

Petrakis, M

I. Petrakis, M. Zeuner: Pre-measure spaces and pre-integration spaces in predicative Bishop-Cheng measure theory, Logical Methods in Compter Science, Volume 21, Issue 2 - https://doi.org/10.46298/lmcs-21(2:1)2025

2025 doi
[51]

Piron: Foundations of Quantum Physics, W.A

C. Piron: Foundations of Quantum Physics, W.A. Benjamin, Inc., 1976

1976
[52]

Richman: Gleason’s theorem has a constructive proof

F. Richman: Gleason’s theorem has a constructive proof. J. Philos. Logic 29, 2000, 425–431

2000
[53]

Richman: Constructive mathematics without choice, in P

F. Richman: Constructive mathematics without choice, in P. Schuster et. al. (Eds.)Reuniting the Antipodes Constructive and Nonstandard Views of the Continuum, Dordrecht: Kluwer, 2001, 199–205

2001
[54]

Richman: Algebraic Functions, Calculus Style, Communications in Algebra, 40, 2012, 2671– 2683

F. Richman: Algebraic Functions, Calculus Style, Communications in Algebra, 40, 2012, 2671– 2683

2012
[55]

Richman, D

F. Richman, D. S. Bridges, A constructive proof of Gleason’s Theorem, Journal of Functional Analysis 162, 1999, 287–312

1999
[56]

Rijke: Introduction to Homotopy Type Theory, https://arxiv.org/abs/2212.11082, 2022, pre- publication version, which will be published by Cambridge University Press

E. Rijke: Introduction to Homotopy Type Theory, https://arxiv.org/abs/2212.11082, 2022, pre- publication version, which will be published by Cambridge University Press

2022 arXiv
[57]

Shulman: Affine logic for constructive mathematics, The Bulletin of Symbolic Logic, Volume 28, Number 3, 2022, 327–386

M. Shulman: Affine logic for constructive mathematics, The Bulletin of Symbolic Logic, Volume 28, Number 3, 2022, 327–386

2022
[58]

B.Spitters: Constructiveandintuitionisticintegrationtheoryandfunctionalanalysis, PhDThesis, University of Nijmegen, 2002

2002
[59]

Spitters: Constructive results on operator algebras, Journal of Universal Computer Science, 12, 2005, 2096–2113

B. Spitters: Constructive results on operator algebras, Journal of Universal Computer Science, 12, 2005, 2096–2113

2005
[60]

A. S. Troelstra, D. van Dalen: Constructivisim in Mathematics, An Introduction, Volume 1, North-Holland, 1988

1988
[61]

The Univalent Foundations Program:Homotopy Type Theory: Univalent Foundations of Mathe- matics, Institute for Advanced Study, Princeton, 2013. 35

2013
[62]

J. von Neumann:Mathematische Grundlagen der Quanten-mechanik, Berlin, 1932, English trans- lation Mathematical Foundations of Quantum Mechanics, Princeton: Princeton University Press, 1955

1932
[63]

Ye: Toward a constructive theory of unbounded linear operators, The Journal of Symbolic Logic, 65 (1), 357–370

F. Ye: Toward a constructive theory of unbounded linear operators, The Journal of Symbolic Logic, 65 (1), 357–370
[64]

Ye:Strict Finitism and the Logic of Mathematical Applications, Synthese Library 355, Springer, 2011

F. Ye:Strict Finitism and the Logic of Mathematical Applications, Synthese Library 355, Springer, 2011. 36

2011

Pith tools

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

[1] [1]

Aczel, M

P. Aczel, M. Rathjen:Notes on Constructive Set Theory, Report No. 40, 2000/2001, ISSN 1103- 467X. Institut Mittag-Leffler

work page 2000

[2] [2]

Birkhoff, J

G. Birkhoff, J. von Neumann: The Logic of Quantum Mechanics, Annals of Mathematics, Vol. 37, No. 4 (Oct., 1936), pp. 823–843

work page 1936

[3] [3]

Bishop: Foundations of Constructive Analysis, McGraw-Hill, 1967

E. Bishop: Foundations of Constructive Analysis, McGraw-Hill, 1967

work page 1967

[4] [4]

Bishop, H

E. Bishop, H. Cheng:Constructive Measure Theory, Mem. Amer. Math. Soc. 116, 1972

work page 1972

[5] [5]

Bishop, D

E. Bishop, D. S. Bridges: Constructive Analysis, Grundlehren der math. Wissenschaften 279, Springer-Verlag, Heidelberg-Berlin-New York, 1985

work page 1985

[6] [6]

D. S. Bridges: Constructive Functional Analysis, Research Notes in Mathematics, 28, Pitman, London, 1979

work page 1979

[7] [7]

Bridges: Towards a constructive foundation for quantum mechanics

D. Bridges: Towards a constructive foundation for quantum mechanics. In: F. Richman (Ed.) Constructive Mathematics, Proceedings of the New Mexico State University Conference Held at Las Cruces, New Mexico, August 11–15, 1980, Lecture Notes in Mathematics 873, Springer-Verlag, Berlin, 1981, 260–273

work page 1980

[8] [8]

D. S. Bridges: Can constructive mathematics be applied in physics? Journal of Philosphical Logic, 28, 1999, 439–453

work page 1999