add(SetTheory): Recursion, ordinal addition and multiplication

[tosiaki]

No description provided.

[iehality]

I added few comments. I haven't finished reviewing Recursion.lean yet, so I may add more comments later.

[iehality]

I added comments. Please request a review when you're done.

[iehality]

This statement should be proved by a general proposition:

@[grind ->] lemma IsFunction.odSubset (f g : V) [hf : IsFunction f] : g ⊆ f → IsFunction g

and

@[simp] lemma restrict_subset (f A : V) : f ↾ A ⊆ f

[iehality]

Since all procedures defining transfinite recursion are similar, it might be good to create a suitable structure to package these procedures.

I did this for primitive recursive definitions while working on arithmetic. See this and its improvement for details. I defined a structure Blueprint for handling definability and its model-theoretic realization Blueprint.Construction, ensuring that once these are constructed, many lemmas for common properties, e.g. definability and structural induction, etc. are automatically generated.

However, since this is somewhat technical, it can be postponed until you (we) actually tackle complicated theorems.

[Convindix]

Is there currently any active work on making this PR ready for merge? If not, maybe I could help shorten proofs (I have heard most LLM-generated Lean proofs are about 10x longer than a concise human-written proof of the same theorem). However, if I do help, I would have to pause work on the Levy hierarchy.

[iehality]

@Convindix

It would be helpful if you could work on it. The Levy hierarchy isn't an urgent issue, so I think it can be postponed.

[Convindix]

(I am still working on this. I currently have that the theorem attempt_function_exists_on) compiles with my changes, which shows that for every ordinal there exists an attempt function of that length. Some of the code is still convoluted in this theorem and optimization is likely still possible. I've only just started on this part, but I'm guessing that much of the code in SuccessorLimitRecursion is unnecessary, since attempt functions were already proven to exist by successor and limit cases beforehand.)

[Convindix]

noncomputable def attemptOrEmpty
    (F : V → V) (α : V) : V := by
  classical
  by_cases hα : ExistsAttempt F α
  · exact Classical.choose hα
  · exact ∅

Since using by in the definition of a def is discouraged, how should I rewrite this?

[iehality]

Since using by in the definition of a def is discouraged, how should I rewrite this?

You should use Classical.epsilon.

noncomputable def attemptOrEmpty
    (F : V → V) (α : V) : V := Classical.epsilon fun f ↦ "description of ExistsAttempt F α"

[Convindix]

Some more info about my progress:

I've unfortunately made very little progress over the last month, I'm having trouble with rewriting the lemma attemptOrDefault_eq_iff. I was thinking for a bit about proving a more general lemma with a type like lemma orDefaultDefinable (φ : V → V → Prop) [ℒₛₑₜ-relation[V] φ] : ℒₛₑₜ-function₁[V] (fun x ↦ (Classical.epsilon (φ x))), but now I realize it wouldn't really help in this specific scenario since attemptOrDefault has a parameter which is a function F : V → V which would need to be required to be an ℒₛₑₜ-function₁[V].

[Convindix]

I don't know if it's true that attemptOrDefault is definable, since I don't think there's an ℒₛₑₜ-predicate[V] φ such that φ x holds iff x = Classical.arbitrary V (I don't know how Classical.arbitrary works internally, so I don't know if the arbitrary element has any special properties.) Maybe I should define a function attemptOrEmpty instead, which returns Ø if an attempt doesn't exist. Is there a way to use Classical to define a function like this? (I could try using dite, and using Classical.dec ExistsAttempt whenever Decidable ExistsAttempt comes up.)

[iehality]

I think it is hard to make those functions definable.

In FirstOrder/Arithmetic, the standard way to handle noncomputable functions defined using choice is to restrict to cases where the value exists uniquely in a definable form. That is, rather than using Classical.epsilon directly, we first show that P x y is definable, then prove ∀ x, ∃! y, P x y, and finally use Classical.choose! to obtain a function. Its graph is then clearly definable.

Thus, making the output unique by returning Ø when no attempt exists is the standard solution. For example, we use this approach to define subtraction in arithmetic.

[Convindix]

@iehality This is an elegant way. However, unfortunately due to definability reasons I need to show that attemptOrEmpty is definable before I can prove ∀ α, ∃! f, IsAttempt F α f. (This is the method that tosiaki's PR follows, and I think that it's the simplest possible way unless I've missed another way.)

So instead of defining attemptOrEmpty F α to be something like Classical.choose! (isAttemptUnique F α), I'll have to define it by a case splitting on whether ExistsAttempt F α is true or not. Usually a case splitting in a definition would use dite, but this might be discouraged here because everything is noncomputable (although I could use Classical.dec ExistsAttempt here whenever dite gives an error that it needs an instance of the typeclass Decidable ExistsAttempt to work)

[tosiaki]

Besides dite, there is also the option to use Classical.byCases directly:

noncomputable def attemptOrEmpty (F : V → V) (α : V) : V :=
  Classical.byCases
    (fun hα : ExistsAttempt F α => Classical.choose hα)
    (fun _ => ∅)

[Convindix]

@tosiaki Thanks, I can try to get this to work. Currently it's not typechecking for me, saying that the value of Classical.byCases needs to be a type which is of sort Prop, instead of a term with type V.

Edit: I think I got it to typecheck by using the similar Decidable.casesOn, but I'll have to see if the behavior is correct.

[tosiaki]

@Convindix right, my suggestion actually won't work because it returns Prop, not V. Perhaps the earlier suggestion to do something similar to subtraction makes the most sense. It doesn't require a large reorganization, just an additional small existence lemma on the "or default" conditional:

/--
Choose a recursion-function graph at input `β` if one exists.
Otherwise, return an arbitrary value.
-/
lemma attemptOrEmpty_exists
    (F : V → V) (β : V) :
    ∃ y : V,
      (IsOrdinal β ∧ ExistsAttempt F β ∧ IsAttempt F β y) ∨
      (¬(IsOrdinal β ∧ ExistsAttempt F β) ∧ y = ∅) := by
  by_cases hβ : IsOrdinal β ∧ ExistsAttempt F β
  · exact ⟨Classical.choose hβ.2, Or.inl ⟨hβ.1, hβ.2, Classical.choose_spec hβ.2⟩⟩
  · exact ⟨∅, Or.inr ⟨hβ, rfl⟩⟩

noncomputable def attemptOrEmpty
    (F : V → V) (β : V) : V :=
  Classical.choose (attemptOrEmpty_exists F β)

The spec and eq_iff theorems would just need minor adjustments:

lemma attemptOrEmpty_spec_on
    (F : V → V) (β : Ordinal V)
    (hex : ExistsAttempt F β) :
    IsAttemptOn F β (attemptOrEmpty F β.val) := by
  have hchosen := Classical.choose_spec (attemptOrEmpty_exists F β.val)
  rcases hchosen with ⟨_, _, hrec⟩ | ⟨hnex, _⟩
  · simpa [attemptOrEmpty] using hrec
  · exact (hnex ⟨β.ordinal, hex⟩).elim

lemma attemptOrEmpty_eq_iff
    (F : V → V) (β y : V) :
    y = attemptOrEmpty F β ↔
      (IsOrdinal β ∧ ExistsAttempt F β ∧
        IsAttempt F β y) ∨
      (¬(IsOrdinal β ∧ ExistsAttempt  F β) ∧
        y = ∅) := by
  constructor
  · intro hy
    rw [hy]
    exact Classical.choose_spec (attemptOrEmpty_exists F β)
  · rintro (⟨hord, hex, hrecf⟩ | ⟨hnex, rfl⟩)
    · have hchosen := Classical.choose_spec (attemptOrEmpty_exists F β)
      rcases hchosen with ⟨_, _, hrecg⟩ | ⟨hnex, _⟩
      · letI : IsOrdinal β := hord
        let βo : Ordinal V := IsOrdinal.toOrdinal β
        exact isAttempt_unique_on (F := F) (α := βo)
          (by simpa [βo] using hrecf) (by simpa [attemptOrEmpty, βo] using hrecg)
      · exact (hnex ⟨hord, hex⟩).elim
    · have hchosen := Classical.choose_spec (attemptOrEmpty_exists F β)
      rcases hchosen with ⟨hord, hex, _⟩ | ⟨_, harb⟩
      · exact (hnex ⟨hord, hex⟩).elim
      · exact harb.symm

[Convindix]

@tosiaki Thank you. I haven't responded in a bit, but I currently believe I might be able to skip attemptOrEmpty altogether by using the lemma replacement_exists_on, which works for a definable relation instead of a function and only requires uniqueness on the domain set X of the application of replacement. I also would like to try merging the zero, successor, and limit cases of the proof of attempt_function_exists into one, which might make the construction more uniform. (My main worry with this last point is that the lemma about the union of a coherent set of functions being a function will get less use, but I guess this isn't much of a problem?)

Also, maybe removing the zero/successor/limit case subdivision will make transfinite recursion in set theory more amenable to being generalized like the blueprints mentioned in this post?

[Convindix]

I'm now starting over with the new commits on FormalizedFormalLogic (e.g. Lean 4.31 version) and see lots of errors. I might post more on Zulip about the errors I'm getting, for example I guess that now the SetStructure is no longer V but V↓[ℒₛₑₜ].

[iehality]

I'm now starting over with the new commits on FormalizedFormalLogic (e.g. Lean 4.31 version) and see lots of errors. I might post more on Zulip about the errors I'm getting, for example I guess that now the SetStructure is no longer V but V↓[ℒₛₑₜ].

Unless I'm missing something, the changes concerning SetTheory are minor, and I think it will work if you rewrite it as follows.

• Replace V ⊧ₘ/V ⊧ₘ* with V↓[ℒₛₑₜ] ⊧/V↓[ℒₛₑₜ] ⊧*.
• Replace Semiformula.Eval s e ε φ/Semiformula.Evalm M e ε φ with Semiformula.Eval e ε φ/Semiformula.Eval (M := M) e ε φ

See https://github.com/FormalizedFormalLogic/Foundation/pull/794/changes for details.