Introduction

Noetherianity

Well quasi-orders

Conclusion

A Constructive Picture ofNoetherianity and Well Quasi-Orders
Gabriele Buriola1 , Peter Schuster1 , Ingo Blechschmidt2
1 University of Verona, Italy
2 University of Augsburg, Germany

28/07/2023

dmi.png

Introduction

Noetherianity

Well quasi-orders

Conclusion

Summary

We will see:Constructive Noetherian definitions;
Constructive well quasi-orders and their relations.

dmi.png

Introduction

Noetherianity

Well quasi-orders

Conclusion

Ascending chain condition, classicallyClassical logic := Excluded Middle (LEM) + Axiom of Choice (AC).
Classical Noetherianity for Rings
FBP (Finite Basis Property): every ideal is finitely generated;
ACC: every ascending chain of ideals stabilizes
I0 ⊆ I1 ⊆ I2 ⊆ . . .

⇒ ∃n : In = In+1 = In+2 = . . . ;Classically: FBP ↔ ACC.
Problem:
FBP and ACC are not constructively meaningful!
E.g. the 2 element field F2 is neither constructively FBP nor ACC.

dmi.png

Introduction

Noetherianity

Well quasi-orders

Conclusion

Ascending chain condition, constructively
Toward a constructive ACC
ACC: every ascending chain of ideals stabilizes
I0 ⊆ I1 ⊆ I2 ⊆ . . .

⇒ ∃n : In = In+1 = In+2 = . . . ;ACCfg : every ascending chain of finitely generated ideals stabilizes
I0 ⊆ I1 ⊆ I2 ⊆ . . .

⇒ ∃n : In = In+1 = In+2 = . . . ;ACC0 : every ascending chain of ideals stalls
I0 ⊆ I1 ⊆ I2 ⊆ . . .

⇒ ∃n : In = In+1 ;ACCfg
0 : every ascending chain of finitely generated ideals stalls
I0 ⊆ I1 ⊆ I2 ⊆ . . .

⇒ ∃n : In = In+1 ;ACC: is not constructive, e.g. F2 ;ACCfg : is not constructive, e.g. by Halting problem for Turing machines;
ACC0 : is not constructive, e.g. by topological models of intuitionistic logic;
ACCfg
0 : is constructive! as discovered by Richman and Seidenberg;
Notation: RS-Noetherian:=ACCfg
0(d’après Richman and Seidenberg).

dmi.png

Introduction

Noetherianity

Well quasi-orders

Conclusion

Related Properties
Let (E , ⩽) be a partial order with x < y ≡ x ⩽ y ∧ x ̸= y :Hereditary conditions
H ⊆ E is hereditary if ∀x ({y | y < x } ⊆ H ⇒ x ∈ H);
E is hereditary well-founded, hwf, if H ⊆ E hereditary ⇒ H = E ;E is well ordered if it is hereditary well-founded and linear.
Ascending trees (Richman’03)
An ascending tree in E is a family (xi )i∈I ⊆ E where
I is a tree;
i < j ⇒ xi ⩽ xj .
An ascending tree stalls if ∃ i < j : xi = xj .
Inductive definition of “P bars σ”
For a predicate P on ascending finite lists on E , we define P|σ:if P(σ) then P|σ;if P|σx for all x ⩾ σ, then P|σ.

dmi.png

Introduction

Noetherianity

Well quasi-orders

Conclusion

Intuitionistic Noetherian properties and their relations
A partial order (E , ⩽) is
RS-Noetherian if for e1 ⩽ e2 ⩽ . . . there is n with en = en+1 ;ML-Noetherian if the reverse order (E , ⩾) is hwf;
strongly Noetherian if there is a well-order W and a strictly
descending map φ : E → W , i.e. e < f ⇒ φ(e) > φ(f );tree Noetherian if every ascending tree in E stalls;
inductively Noetherian if Stall | [], whereStall(σ)=“σ is an ascending finite list with repeated terms”.
Def: given a ring R, If (R) is the set of finitely generated ideals of R.
Def: a ring R is * Noetherian if (If (R), ⊆) is * Noetherian.
Constructive implications for a decidable poset (E , ⩽)strongindtreeRSdmi.png

MLIntroduction

Noetherianity

Well quasi-orders

Conclusion

Basic definitions for quasi-orders
Quasi-order
A qo (Q, ⩽) is a set Q with a transitive and reflexive relation ⩽.
Notationp < q ≡ p ⩽ q ∧ q ⩽̸ p;p ⊥ q ≡ p ⩽̸ q ∧ q ⩽̸ p;
p ∼ q ≡ p ⩽ q ∧ q ⩽ p.
Auxiliary definitions
For every qo (Q, ⩽):the closure of B ⊆ Q is ↑B := {q ∈ Q | ∃b ∈ B b ⩽ q};
B is closed if B=↑B and finitely generated if B=↑{b1 , . . . , bn };a sequence (qk )k in Q is a total function from N to Q;
an antichain is a sequence (qk )k such that qi ⊥ qj if i ̸= j;
dmi.png
an extension of (Q, ⩽) is a qo ≼ on Q extending ⩽, i.e.,p ⩽ q ⇒ p ≼ q and p ≼ q ∧ q ≼ p ⇒ p ∼ q.

Introduction

Noetherianity

Well quasi-orders

Conclusion

Well quasi-orders definitions
A qo (Q, ⩽) iswell-founded if for q1 ⩾ q2 ⩾ . . . there is n such that qn = qn+1 ;wqo if for any sequence (qk )k in Q there exist i < j with qi ⩽ qj ;wqo(set) if every sequence (qk )k in Q has an infinite ascending
subsequence: there are k0 < k1 < . . . such that qk0 ⩽ qk1 ⩽ . . . ;wqo(anti) if it is well-founded and every antichain is finite;
wqo(ext) if every linear extension of Q is well-founded;
wqo(fbp) if every closed subset is finitely generated;
wqo(acc) if the set of closed subsets is Noetherian;wqo(*) if the set of finitely generated closed subsets is *Noetherian.
Remark: all the wqo definitions are classically equivalent.
dmi.png

Introduction

Noetherianity

Well quasi-orders

Conclusion

Constructive relations between wqo definitions
Theorem
The conditions wqo(set), wqo(fbp) and wqo(acc) are notconstructively meaningful.
Implications between constructive wqo definitionswqo(anti)
wqo(str)wqo(ML)wqo(RS)

wqo
wqo(ext)

A closure property
Let P any of the properties wqo, wqo(anti), . . . except wqo(ext).
If (Q, ⩽) has property P and P ⊆ Q, then (P, ⩽) has property P.

dmi.png

Introduction

Noetherianity

Well quasi-orders

Conclusion

Future work
Well-founded vs. hereditarily well-foundedClassically equivalent, but not constructively.
Reverse implications
Which of the following implications can be reversed?
strongly Noetherian ⇒ ML-Noetherian;wqo(RS) ⇒ wqo;
wqo ⇒ wqo(anti);...
For now, RS-Noetherian ̸⇒ ML-Noetherian by A. Blass.
Further closure properties
Is wqo(ext) closed under subset?
If P and Q have property P, doesP ∪˙ Q constructively have property P?
P ×Q constructively have property P?

dmi.png

Introduction

Noetherianity

Well quasi-orders

Thank you!

Conclusion

References:

Higman, G.: Ordering by divisibility in abstract algebras. Proc. London Math.
Soc. 3, 2:326-336, (1952).
Richman, F.: Constructive Aspects of Noetherian Rings. Proceedings of theAmerican Mathematical Society 44(2), 436-441, (1974).
Seidenberg, A.: What is Noetherian? Rendiconti del Seminario matematico e
fisico di Milano 44(1), 55-61 (1974).
Jacobsson C., Löfwall C.: Standard bases for general coefficient rings and a new
constructive proof of Hilbert’s basis theorem. J. Symbolic Comput. 12(3),337-371 (1991)
Richman, F.: The ascending tree condition: constructive algebra without
countable choice. Commun. Algebra 31(4), 1993-2002 (2003)
Perdry, H.: Strongly Noetherian rings and constructive ideal theory. Journal ofsymbolic computation 37(4), 511-535 (2004).
Veldman, W.: An Intuitionistic Proof of Kruskal’s Theorem. Archive forMathematical Logic 43(2), 215-264 (2004).
Cholak P., Marcone A., and Solomon R.: Reverse mathematics and theequivalence of definitions for well and better quasi-orders. The Journal ofsymbolic logic, 66(1):683-55, (2004).

dmi.png