Fracterm Calculus for Partial Meadows

Alban Ponse; Jan A. Bergstra

arxiv: 2502.13812 · v2 · pith:F53TTTCKnew · submitted 2025-02-19 · 💻 cs.LO

Fracterm Calculus for Partial Meadows

Jan A. Bergstra , Alban Ponse This is my paper

Pith reviewed 2026-05-23 02:20 UTC · model grok-4.3

classification 💻 cs.LO

keywords partial meadowsfracterm calculusthree-valued logicpartial algebrasdivision operatorsemi-computabilitybot-enlargementcommon meadows

0 comments

The pith

Axioms for fracterm calculus formalize fields with a division operator using partial meadows in three-valued logic.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper supplies axioms for the fracterm calculus of partial meadows within a three-valued short-circuit first-order logic. This setup yields a natural formalization of fields equipped with a division operator that treats the operation as partial. An interpretation maps the logic into bot-enlargements of partial algebras, from which semi-computability of the consequence relation follows. The bot-enlargement of any partial meadow is shown to be a common meadow. A sympathetic reader would care because the work addresses how algebraic structures can accommodate undefined operations like division by zero without forcing total functions.

Core claim

Axioms for the fracterm calculus of partial meadows are given. In this way a rather natural formalisation of fields with division operator is obtained. It is noticed that the logic thus obtained cannot express that division by zero must be undefined. An interpretation of the three-valued sequential logic into bot-enlargements of partial algebras is given, for which it is concluded that the consequence relation of the former logic is semi-computable, and that the bot-enlargement of a partial meadow is a common meadow.

What carries the argument

The fracterm calculus, consisting of axioms for partial meadows that treat division as a partial function inside three-valued sequential logic.

If this is right

The consequence relation of the three-valued sequential logic is semi-computable.
The bot-enlargement of a partial meadow is a common meadow.
Fields with a division operator receive a natural formalization as partial algebras.
The obtained logic cannot express that division by zero must be undefined.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The method may extend to formalizing other partial operations beyond division in algebraic datatypes used in programming languages.
Semi-computability of the consequence relation could support automated checking of algebraic identities in systems that allow partial functions.
Common meadows obtained via bot-enlargement might provide a uniform way to totalize other classes of partial algebras.

Load-bearing premise

The supplied axioms correctly capture the intended partial meadow structure and the interpretation into bot-enlargements preserves the properties needed to conclude semi-computability.

What would settle it

A concrete model of a partial meadow whose bot-enlargement fails to be a common meadow, or an explicit computation demonstrating that the consequence relation of the three-valued logic is not semi-computable.

read the original abstract

Partial algebras and datatypes are discussed with the use of signatures that allow partial functions, and a three-valued short-circuit (sequential) first order logic with a Tarski semantics. The propositional part of this logic is also known as McCarthy calculus and has been studied extensively. Axioms for the fracterm calculus of partial meadows are given. The case is made that in this way a rather natural formalisation of fields with division operator is obtained. It is noticed that the logic thus obtained cannot express that division by zero must be undefined. An interpretation of the three-valued sequential logic into $\bot$-enlargements of partial algebras is given, for which it is concluded that the consequence relation of the former logic is semi-computable, and that the $\bot$-enlargement of a partial meadow is a common meadow.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper gives axioms for fracterm calculus on partial meadows and an interpretation into bot-enlargements that yields semi-computability of the consequence relation.

read the letter

The paper supplies axioms for the fracterm calculus of partial meadows and shows that an interpretation of the three-valued sequential logic into bot-enlargements makes the consequence relation semi-computable, while also establishing that the bot-enlargement of a partial meadow is a common meadow. This extends the authors' earlier meadow work by handling partial functions through a short-circuit logic that aligns with McCarthy calculus at the propositional level. The setup is presented as a natural way to formalize fields that include a division operator, though the logic cannot express that division by zero must be undefined. The interpretation step is the main new element, as it directly supports the semi-computability claim. The work is coherent on its own terms and stays within the axiomatic style the authors have used before. The connection between partial algebras, three-valued logic, and meadow structures is drawn without obvious internal contradictions in the abstract. The soft spot is that the provided text states the axioms and conclusions but contains no derivations, examples, or proof sketches, so it is not possible to check whether the axioms capture the intended partial structures or whether the bot-enlargement preserves the properties needed for the semi-computability result. That gap is real but typical for an abstract; it does not indicate a flaw in the approach itself. The paper is aimed at researchers already working on algebraic logic, partial datatypes, or meadow theory in theoretical computer science. A reader following that specific literature would see the value in the new axioms and the interpretation result. It deserves peer review because the claims are stated clearly enough for referees in the area to assess the details and because the topic fits established lines of work without relying on unfalsifiable or circular moves.

Referee Report

1 major / 1 minor

Summary. The paper introduces signatures allowing partial functions and a three-valued short-circuit first-order logic (McCarthy calculus) with Tarski semantics for partial algebras and datatypes. It supplies axioms for the fracterm calculus of partial meadows as a natural formalization of fields equipped with a division operator, notes that the resulting logic cannot express that division by zero is undefined, and provides an interpretation of the three-valued logic into bot-enlargements of partial algebras. From this interpretation the paper concludes that the consequence relation is semi-computable and that the bot-enlargement of a partial meadow is a common meadow.

Significance. If the supplied axioms are sound and the interpretation into bot-enlargements is shown to preserve the required properties, the work would contribute a concrete axiomatic treatment of partial division in meadow algebras and link it to semi-computability results useful for automated reasoning. The explicit connection to existing McCarthy calculus and common meadows provides a clear point of contact with prior literature on algebraic logic.

major comments (1)

[Abstract] Abstract (paragraphs on axioms and interpretation): the central claims that the supplied axioms correctly capture partial meadow structure and that the bot-enlargement interpretation yields semi-computability rest on derivations and preservation arguments that are not supplied in the text; without these the soundness of the conclusions cannot be verified.

minor comments (1)

[Abstract] The abstract refers to 'fracterm calculus' and 'bot-enlargements' without a preliminary definition or reference to the section where these notions are introduced.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their report and for highlighting the need for explicit verification of the central claims. We respond to the single major comment below.

read point-by-point responses

Referee: [Abstract] Abstract (paragraphs on axioms and interpretation): the central claims that the supplied axioms correctly capture partial meadow structure and that the bot-enlargement interpretation yields semi-computability rest on derivations and preservation arguments that are not supplied in the text; without these the soundness of the conclusions cannot be verified.

Authors: The manuscript states the axioms for fracterm calculus of partial meadows and supplies an interpretation of the three-valued logic into bot-enlargements, from which semi-computability of the consequence relation and the fact that bot-enlargements are common meadows are concluded. These conclusions are presented as following directly from the given interpretation and the known properties of McCarthy calculus and common meadows. We agree that explicit derivations establishing that the axioms capture the intended partial-meadow structure and that the interpretation preserves the required semantic properties would strengthen the paper; we will add a dedicated section containing these arguments in the revised version. revision: yes

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper supplies axioms for fracterm calculus of partial meadows and gives an interpretation of the three-valued logic into bot-enlargements, from which it concludes semi-computability of the consequence relation and that the bot-enlargement of a partial meadow is a common meadow. No load-bearing steps reduce by the paper's own equations or self-citations to inputs by construction. The development is a standard axiomatic presentation with an external semantic interpretation; no self-definitional equivalences, fitted inputs renamed as predictions, or uniqueness claims imported solely via author-overlapping citations are present in the abstract or described content.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claims rest on the introduction of the fracterm calculus axioms and the bot-enlargement interpretation; no free parameters, invented entities, or additional axioms are visible in the abstract.

axioms (1)

domain assumption Axioms for the fracterm calculus of partial meadows
These axioms are the load-bearing formalization step stated in the abstract.

pith-pipeline@v0.9.0 · 5661 in / 1162 out tokens · 39274 ms · 2026-05-23T02:20:46.949034+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/AbsoluteFloorClosure.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

Axioms for the fracterm calculus of partial meadows are given... bot-enlargement of a partial meadow is a common meadow.
IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

short-circuit implication... McCarthy calculus

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

21 extracted references · 21 canonical work pages · 2 internal anchors

[1]

Anderson, J.A.D.W., V¨ olker, N., and Adams, A.A. (2007). Perspex Machine VIII, axioms of transreal arithmetic. In: Latecki, J., Mount, D.M., and Wu, A.Y. (Eds.), Proc. SPIE 6499, Vision Geometry XV, 649902 (29 January 2007).doi:10.1117/12.698153

work page doi:10.1117/12.698153 2007
[2]

Bergstra, J.A., Bethke, I., and Rodenburg, P.H. (1995). A propositional logic with 4 values: true, false, divergent and meaningless,Journal of Applied Non-Classical Logics, 5(2):199-217. doi:10.1080/11663081.1995.10510855

work page doi:10.1080/11663081.1995.10510855 1995
[3]

Bergstra, J.A., Broy, M., Tucker, J.V., and Wirsing, M. (1981). On the power of algebraic specifications. In: J. Gruska and M. Chytil (eds)Mathematical Foundations of Computer Science 1981(MFCS 1981). LNCS 118, pages 193-204, Springer, Berlin, Heidelberg.doi: 10.1007/3-540-10856-4_85

work page doi:10.1007/3-540-10856-4_85 1981
[4]

and Ponse, A

Bergstra, J.A. and Ponse, A. (2015). Division by zero in common meadows. In R. de Nicola and R. Hennicker (eds.),Software, Services, and Systems(Wirsing Festschrift). LNCS 8950, pages 46-61, Springer, Berlin, Heidelberg.doi:10.1007/978-3-319-15545-6_6. Also avail- able, in improved form, as arXiv:1406.6878v4 [math.RA] (22 Mar 2021).doi:10.48550/ arXiv.1406.6878

work page doi:10.1007/978-3-319-15545-6_6 2015
[5]

Fracpairs and fractions over a reduced commutative ring

Bergstra, J.A. and Ponse, A. (2016). Fracpairs and fractions over a reduced commutative ring.Indigationes Mathematicae, 27(3):727-748.doi:10.1016/j.indag.2016.01.007. Also available as arXiv:1411.4410v2 [math.RA] (22 Jan 2016).doi:10.48550/arXiv.1411.4410

work page internal anchor Pith review Pith/arXiv arXiv doi:10.1016/j.indag.2016.01.007 2016
[6]

and Ponse, A

Bergstra, J.A. and Ponse, A. (2025). Conditional logic as a short-circuit logic.Scientific Annals of Computer Science, 35(2):161-196.doi:10.47743/SACS.2025.2.161

work page doi:10.47743/sacs.2025.2.161 2025
[7]

Bergstra, J.A., Ponse, A., and Staudt, D.J.C. (2013). Short-circuit logic. arXiv:1010.3674v4 [cs.LO] (12 Mar 2013).doi:10.48550/arXiv.1010.3674

work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.1010.3674 2013
[8]

Bergstra, J.A., Ponse, A., and Staudt, D.J.C. (2021). Non-commutative propositional logic with short-circuit evaluation.Journal of Applied Non-Classical Logics, 31(3-4):234-278 (on- line available).doi:10.1080/11663081.2021.2010954

work page doi:10.1080/11663081.2021.2010954 2021
[9]

Deciding equivalances among conjunctive aggregate queries

Bergstra, J.A. and Tucker, J.V. (2007). The rational numbers as an abstract data type. Journal of the ACM, 54 (2), Article 7 (25 pages).doi:10.1145/1219092.1219095

work page doi:10.1145/1219092.1219095 2007
[10]

and Tucker, J.V

Bergstra, J.A. and Tucker, J.V. (2022). Partial arithmetical data types of rational numbers and their equational specification.Journal of Logical and Algebraic Methods in Programming, 128 (15 pages).doi:10.1016/j.jlamp.2022.100797

work page doi:10.1016/j.jlamp.2022.100797 2022
[11]

and Tucker, J.V

Bergstra, J.A. and Tucker, J.V. (2022). On the axioms of common meadows: Fracterm calculus, flattening and incompleteness.The Computer Journal, 66(7):1565-1572.doi:10. 1093/comjnl/bxac026

work page 2022
[12]

and Tucker, J.V

Bergstra, J.A. and Tucker, J.V. (2025). On Defining Expressions for Entropy and Cross- Entropy: The Entropic Transreals and Their Fracterm Calculus.Entropy2025, 27(1), 31. doi:10.3390/e27010031

work page doi:10.3390/e27010031 2025
[13]

Wheels – on division by zero.Mathematical Structures in Computer Science, 14(1):143-184.doi:10.1017/S0960129503004110

Carlstr¨ om, J (2004). Wheels – on division by zero.Mathematical Structures in Computer Science, 14(1):143-184.doi:10.1017/S0960129503004110

work page doi:10.1017/s0960129503004110 2004
[14]

and Dinis B

Dias J. and Dinis B. (2024). Towards an enumeration of finite common mead- ows.International Journal of Algebra and Computation, 24(06):837-855.doi:10.1142/ S0218196724500310. Also available atdoi:10.48550/arXiv.2401.10631. 26

work page doi:10.48550/arxiv.2401.10631 2024
[15]

Dietzel, S

Dias J. and Dinis B. (2024). Strolling through common meadows.Communications in Algebra, 52(12):5015-5042,doi:10.1080/00927872.2024.2362932. Also available atdoi: 10.48550/arXiv.2311.05460

work page doi:10.1080/00927872.2024.2362932 2024
[16]

Guzm´ an, F., Squier, C.C. (1990). The algebra of conditional logic.Algebra Universalis27:88- 110.doi:10.1007/BF01190256

work page doi:10.1007/bf01190256 1990
[17]

and Middelburg, C.A

Jones, C.B. and Middelburg, C.A. (1994). A typed logic of partial functions, reconstructed classically.Acta Informatica, 31:399-430.doi:10.1007/BF01178666

work page doi:10.1007/bf01178666 1994
[18]

Konikowska, B., Tarlecki, A., and Blikle, A. (1988). A three-valued logic for software spec- ification and validation: Tertium tamen datur. In: Bloomfield, R.E., Marshall, L.S., Jones, R.B. (eds),VDM ’88 VDM — The Way Ahead(VDM 1988). LNCS 328, pages 218–242. Springer, Berlin, Heidelberg.doi:10.1007/3-540-50214-9_19

work page doi:10.1007/3-540-50214-9_19 1988
[19]

McCune W. (2008). The GUI: Prover9 and Mace4 with a graphical user interface. Prover9- Mace4 Version 0.5B. (Prover9-Mace4-v05B.zip, March 14, 2008).https://www.cs.unm.edu/ ~mccune/prover9/gui/v05.html

work page 2008
[20]

and Staudt, D.J.C

Ponse, A. and Staudt, D.J.C. (2018): An independent axiomatisation for free short-circuit logic,Journal of Applied Non-Classical Logics, 28(1):35-71.doi:10.1080/11663081.2018. 1448637

work page doi:10.1080/11663081.2018 2018
[21]

seconds = 0

Reis, T.S. dos, Gomide, W., and Anderson, J.A.D.W. (2016). Construction of the transreal numbers and algebraic transfields.IAENG International Journal of Applied Mathematics, 46(1): 11-23.https://www.iaeng.org/IJAM/issues_v46/issue_1/IJAM_46_1_03.pdf. A Prover9 and Mace4 results The axioms of EqCL imply the following consequences, all of which follow easi...

work page 2016

[1] [1]

Anderson, J.A.D.W., V¨ olker, N., and Adams, A.A. (2007). Perspex Machine VIII, axioms of transreal arithmetic. In: Latecki, J., Mount, D.M., and Wu, A.Y. (Eds.), Proc. SPIE 6499, Vision Geometry XV, 649902 (29 January 2007).doi:10.1117/12.698153

work page doi:10.1117/12.698153 2007

[2] [2]

Bergstra, J.A., Bethke, I., and Rodenburg, P.H. (1995). A propositional logic with 4 values: true, false, divergent and meaningless,Journal of Applied Non-Classical Logics, 5(2):199-217. doi:10.1080/11663081.1995.10510855

work page doi:10.1080/11663081.1995.10510855 1995

[3] [3]

Bergstra, J.A., Broy, M., Tucker, J.V., and Wirsing, M. (1981). On the power of algebraic specifications. In: J. Gruska and M. Chytil (eds)Mathematical Foundations of Computer Science 1981(MFCS 1981). LNCS 118, pages 193-204, Springer, Berlin, Heidelberg.doi: 10.1007/3-540-10856-4_85

work page doi:10.1007/3-540-10856-4_85 1981

[4] [4]

and Ponse, A

Bergstra, J.A. and Ponse, A. (2015). Division by zero in common meadows. In R. de Nicola and R. Hennicker (eds.),Software, Services, and Systems(Wirsing Festschrift). LNCS 8950, pages 46-61, Springer, Berlin, Heidelberg.doi:10.1007/978-3-319-15545-6_6. Also avail- able, in improved form, as arXiv:1406.6878v4 [math.RA] (22 Mar 2021).doi:10.48550/ arXiv.1406.6878

work page doi:10.1007/978-3-319-15545-6_6 2015

[5] [5]

Fracpairs and fractions over a reduced commutative ring

Bergstra, J.A. and Ponse, A. (2016). Fracpairs and fractions over a reduced commutative ring.Indigationes Mathematicae, 27(3):727-748.doi:10.1016/j.indag.2016.01.007. Also available as arXiv:1411.4410v2 [math.RA] (22 Jan 2016).doi:10.48550/arXiv.1411.4410

work page internal anchor Pith review Pith/arXiv arXiv doi:10.1016/j.indag.2016.01.007 2016

[6] [6]

and Ponse, A

Bergstra, J.A. and Ponse, A. (2025). Conditional logic as a short-circuit logic.Scientific Annals of Computer Science, 35(2):161-196.doi:10.47743/SACS.2025.2.161

work page doi:10.47743/sacs.2025.2.161 2025

[7] [7]

Bergstra, J.A., Ponse, A., and Staudt, D.J.C. (2013). Short-circuit logic. arXiv:1010.3674v4 [cs.LO] (12 Mar 2013).doi:10.48550/arXiv.1010.3674

work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.1010.3674 2013

[8] [8]

Bergstra, J.A., Ponse, A., and Staudt, D.J.C. (2021). Non-commutative propositional logic with short-circuit evaluation.Journal of Applied Non-Classical Logics, 31(3-4):234-278 (on- line available).doi:10.1080/11663081.2021.2010954

work page doi:10.1080/11663081.2021.2010954 2021

[9] [9]

Deciding equivalances among conjunctive aggregate queries

Bergstra, J.A. and Tucker, J.V. (2007). The rational numbers as an abstract data type. Journal of the ACM, 54 (2), Article 7 (25 pages).doi:10.1145/1219092.1219095

work page doi:10.1145/1219092.1219095 2007

[10] [10]

and Tucker, J.V

Bergstra, J.A. and Tucker, J.V. (2022). Partial arithmetical data types of rational numbers and their equational specification.Journal of Logical and Algebraic Methods in Programming, 128 (15 pages).doi:10.1016/j.jlamp.2022.100797

work page doi:10.1016/j.jlamp.2022.100797 2022

[11] [11]

and Tucker, J.V

Bergstra, J.A. and Tucker, J.V. (2022). On the axioms of common meadows: Fracterm calculus, flattening and incompleteness.The Computer Journal, 66(7):1565-1572.doi:10. 1093/comjnl/bxac026

work page 2022

[12] [12]

and Tucker, J.V

Bergstra, J.A. and Tucker, J.V. (2025). On Defining Expressions for Entropy and Cross- Entropy: The Entropic Transreals and Their Fracterm Calculus.Entropy2025, 27(1), 31. doi:10.3390/e27010031

work page doi:10.3390/e27010031 2025

[13] [13]

Wheels – on division by zero.Mathematical Structures in Computer Science, 14(1):143-184.doi:10.1017/S0960129503004110

Carlstr¨ om, J (2004). Wheels – on division by zero.Mathematical Structures in Computer Science, 14(1):143-184.doi:10.1017/S0960129503004110

work page doi:10.1017/s0960129503004110 2004

[14] [14]

and Dinis B

Dias J. and Dinis B. (2024). Towards an enumeration of finite common mead- ows.International Journal of Algebra and Computation, 24(06):837-855.doi:10.1142/ S0218196724500310. Also available atdoi:10.48550/arXiv.2401.10631. 26

work page doi:10.48550/arxiv.2401.10631 2024

[15] [15]

Dietzel, S

Dias J. and Dinis B. (2024). Strolling through common meadows.Communications in Algebra, 52(12):5015-5042,doi:10.1080/00927872.2024.2362932. Also available atdoi: 10.48550/arXiv.2311.05460

work page doi:10.1080/00927872.2024.2362932 2024

[16] [16]

Guzm´ an, F., Squier, C.C. (1990). The algebra of conditional logic.Algebra Universalis27:88- 110.doi:10.1007/BF01190256

work page doi:10.1007/bf01190256 1990

[17] [17]

and Middelburg, C.A

Jones, C.B. and Middelburg, C.A. (1994). A typed logic of partial functions, reconstructed classically.Acta Informatica, 31:399-430.doi:10.1007/BF01178666

work page doi:10.1007/bf01178666 1994

[18] [18]

Konikowska, B., Tarlecki, A., and Blikle, A. (1988). A three-valued logic for software spec- ification and validation: Tertium tamen datur. In: Bloomfield, R.E., Marshall, L.S., Jones, R.B. (eds),VDM ’88 VDM — The Way Ahead(VDM 1988). LNCS 328, pages 218–242. Springer, Berlin, Heidelberg.doi:10.1007/3-540-50214-9_19

work page doi:10.1007/3-540-50214-9_19 1988

[19] [19]

McCune W. (2008). The GUI: Prover9 and Mace4 with a graphical user interface. Prover9- Mace4 Version 0.5B. (Prover9-Mace4-v05B.zip, March 14, 2008).https://www.cs.unm.edu/ ~mccune/prover9/gui/v05.html

work page 2008

[20] [20]

and Staudt, D.J.C

Ponse, A. and Staudt, D.J.C. (2018): An independent axiomatisation for free short-circuit logic,Journal of Applied Non-Classical Logics, 28(1):35-71.doi:10.1080/11663081.2018. 1448637

work page doi:10.1080/11663081.2018 2018

[21] [21]

seconds = 0

Reis, T.S. dos, Gomide, W., and Anderson, J.A.D.W. (2016). Construction of the transreal numbers and algebraic transfields.IAENG International Journal of Applied Mathematics, 46(1): 11-23.https://www.iaeng.org/IJAM/issues_v46/issue_1/IJAM_46_1_03.pdf. A Prover9 and Mace4 results The axioms of EqCL imply the following consequences, all of which follow easi...

work page 2016