Noetherian sets without LEM

Question

A noetherian ring can be defined as a ring in which any nonempty set of ideals has a maximal element. They're pretty nice objects. One can obviously generalize this to a bunch of different algebraic structures : what happens if we take our structures to have no operations, i.e. to be sets ?

Then the question becomes : which sets are noetherian, i.e. any nonempty subset of $\mathcal{P}(X)$ has a maximal element ? Of course in ZFC the answer is trivial : these are precisely the finite sets.

What happens if we remove choice ? Well it's still easy, just take the subset of finite sets: it's never empty ($\emptyset$) so it has a maximal element. If this maximal element is $X$, we are done, otherwise take so $x$ not in it, add it to the set, contradiction: $X$ is finite (this works with any notion of finite, so we may as well take the strongest one which - I think- is "be in bijection with a finite ordinal")

But things start to look more interesting if we remove the law of excluded middle (LEM) and work intuitionistically. Indeed in my proof without choice I still used the LEM, and it seems to be complicated to get out of using it. Without LEM I'm not even sure that finite sets are noetherian in this sense. By the way, I should add that without the LEM my definition of noetherian set becomes "any inhabited set of subsets has a maximal element".

Now I have a lot of questions about these, but just to start to get an intuition I have the following ones :

Is any finite set noetherian ?

I tried using induction to prove it, but it's not clear how that would work. I'm sure $\emptyset$ is noetherian, but not even that $1$ is...

I don't know enough about topos semantics, but if I take (pre)sheaves on a topological space like $\mathbb R$, then it seems like by defining $X_n(U):= 1$ if $U\subset (-n,n)$, $\emptyset$ otherwise, then I have an increasing family of subsheaves of $1$, so $1$ is not externally noetherian in this topos of sheaves, but I don't know how that relates to internal noetherianity.

If the answer to the first question is "not in general" (or "it's not provable"), is it provable that there exists some noetherian sets? What are some examples of noetherian sets?

If the answer to the first question is "yes", are there examples of not-finite noetherian sets ? Is it provable that there is none ? Same question with infinite ?

EDIT before posting the question : I realized that my ZF proof used the LEM earlier than was wise; and so I have another question, which would answer the last question :

If $Y\subset X$ is finite, and $x\in X$, is it the case that $Y\cup \{x\}$ is finite ?

Answer 1

I originally wrote this proof in constructive type theory, but it should translate well enough to constructive set theory.

Theorem If A is an inhabited and noetherian set, then the law of excluded middle (LEM) holds.

This means that if any finite set (for some sufficiently nice definition of finite) other than the empty set can't be proven to be noetherian without LEM.

Before I begin, I'll settle some definitions.

A set $A$ is inhabited if there exists $a \in A$. This is a better constructive notion of nonempty.

In a poset $P$, an element $x \in P$ is maximal if for all $y \in P$, $x \leq y \rightarrow x = y$. In particular, in a subposet $P$ of the poset of subsets of a set $A$, $X$ is maximal if for all $Y \in P$, $X \subseteq Y \rightarrow X = Y$.

A set $A$ is noetherian if for all $P \subseteq \mathcal{P}(A)$, if $P$ is inhabited, then $P$ has a maximal element.

Alright, let's begin.

Proof.

Suppose A is inhabited and noetherian. Let $Q$ be some proposition. We'll be proving that $Q \lor \lnot Q$ holds. Let $P = \{B \subseteq A \vert Q \lor (B = \emptyset) \}$. $P$ is inhabited since $\emptyset \in P$. So by hypothesis, $P$ has a maximal element $M$.

Since $M$ is in $P$, $M$ satisfies $Q \lor (M = \emptyset)$. We'll do case analysis on this disjunction.

1. $Q$ holds. Then $Q \lor \lnot Q$ holds.

2. $M = \emptyset$. We'll prove that $\lnot Q$ holds. Assume that $Q$ is true. Since A is inhabited, there exists an $a \in A$. Since $Q$ is true by assumption, $Q \lor (\{a\} = \emptyset)$, so $\{a\} \in P$. But this means that $M = \emptyset$ isn't maximal in $P$, so we have a contradiction. Thus, $\lnot Q$ is true, so $Q \lor \lnot Q$ is true.

Since $Q \lor \lnot Q$ is true in both cases, it holds. $Q$ was arbitrary, so LEM is true.

---

Just a side note. The proof in the second branch is a proof of negation, not a proof by contradiction (see this article for some discussion of the distinction). $\lnot Q$ is usually defined to be $Q \rightarrow \bot$ in intuitionistic settings, so this kind of proof is how you prove negation.

---

Here's my proof in Coq of the above theorem. Since type theory is not set theory, I had to use some different conventions. First and foremost, I identified the type A -> Prop with the powerset of A. This means that a subset is determined by some predicate on the set. It also means that a subset of the powerset of A is some map P: (A -> Prop) -> Prop.

Secondly, in the definition of a maximal element, I used the alternative formulation $\forall y \in P, x \leq y \rightarrow y \leq x$. In a poset, this is equivalent, but A -> Prop doesn't generally form a poset, merely a preorder. That means that we can have two propositions P and Q together with P -> Q and Q -> P, but still not have P = Q. We could add this as an axiom (the axiom of propositional extensionality), but it's simpler to just weaken the definition of maximal element.

(* The subsets of A are the predicates on A *)
Definition subsets (A: Type) := A -> Prop.

(* M is maximal if whenever it's less than another element, it's also greater than that element *)
Definition IsMaximal {A: Type} (P: subsets (subsets A)) (M: subsets A) :=
  P M /\ forall B: subsets A, P B ->
    (forall a: A, M a -> B a) ->
    (forall a: A, B a -> M a).

Definition Noetherian (A: Type) :=
  forall P: subsets (subsets A),
    (exists B: subsets A, P B) -> (* This means that P is inhabited *)
      (exists M: subsets A, IsMaximal P M).

Definition LEM := forall P: Prop, P \/ ~P.

Theorem Noetherian_LEM {A: Type} {A_inhab: inhabited A}
{A_noetherian: Noetherian A}: LEM.
Proof.
  (* We'll prove LEM for a proposition Q *)
  intro Q.

  (* The subset of the powerset of A that we'll be considering *)
  (* In set theory, this would be {B subset A | Q or (B = emptyset)} *)
  set (P := fun X => Q \/ forall a: A, ~(X a)).

  assert (P_inhab: exists B: subsets A, P B). {
    (* We can prove that a type is inhabited by producing a term
       of that type. *)
    unshelve econstructor.

    (* The empty set is in P *)
    exact (fun _ => False).

    (* unfold the definition of P *)
    unfold P; cbn.

    (* We have the empty set, so use the right branch of the
       disjunction *)
    right; unfold not; trivial.
  }

  (* Hence, P satisfies the hypothesis for the existence of a maximal
     element *)
  set (H := A_noetherian P P_inhab).

  (* So we get a maximal element in P *)
  destruct H as [M [M_in_P M_maximal]]; cbn in *.

  (* Unfold the definition of P in M_in_P *)
  unfold P in M_in_P.

  (* Do case analysis on Q \/ (forall a : A, ~ M a) *)
  destruct M_in_P as [Q_true | M_always_false].
  - (* We have Q, so use the left branch *)
    left; exact Q_true.
  - (* For this branch, we have M_always_false: forall a: A, ~M a *)

    (* In this branch, we'll prove ~Q *)
    right.

    (* So assume that Q is true *)
    intro Q_true.

    (* A itself as a predicate *)
    set (A_itself := (fun _: A => True)).

    (* Then A itself is in P *)
    assert (A_in_P: P A_itself). {
      (* This holds trivially, since Q is true *)
      unfold P; left; exact Q_true.
    }

    (* A itself is greater than M *)
    assert (A_greater_than_M: forall a: A, M a -> A_itself a). {
      (* But this is trivial since A_itself a is always True *)
      intros ? _; unfold A_itself.

      (* I is the unique witness of type True *)
      exact I.
    }

    (* But since M is maximal, that means that M is greater than A *)
    assert (M_greater_than_A: forall a: A, A_itself a -> M a). {
      exact (M_maximal A_itself A_in_P A_greater_than_M).
    }

    (* That means that M must always be true too *)
    assert (M_always_true: forall a: A, M a). {
      intro a.
      exact (M_greater_than_A a I).
    }

    (* But now we have both M_always_false and M_always_true *)
    (* This is fine as long as A isn't inhabited,
       but we also have A_inhab *)

    (* This extracts a witness of A being inhabited *)
    destruct A_inhab as [a0].

    (* Now we have a contradiction: M a0 is true, but also false *)
    (* Remember that ~(M a0) is a function (M a0) -> False,
       So we can apply it like a function to produce False *)
    exact (M_always_false a0 (M_always_true a0)).
Qed.