refactor: replace Sentence ℒₒᵣ/Sentence ℒₛₑₜ with ArithmeticSentence/SetTheorySentence

[Copilot]

Sentence ℒₒᵣ and Sentence ℒₛₑₜ were used directly throughout the codebase alongside the alias ArithmeticSentence, creating inconsistency. SetTheorySentence did not exist at all.

Changes

• New alias: Added abbrev SetTheorySentence := Sentence ℒₛₑₜ in SetTheory/Basic/Misc.lean, parallel to the existing ArithmeticSentence := Sentence ℒₒᵣ and SetTheory := Theory ℒₛₑₜ
• Arithmetic: Replaced all Sentence ℒₒᵣ occurrences with ArithmeticSentence across Incompleteness/, Bootstrapping/, Arithmetic/, and ProvabilityLogic/
• Set theory: Replaced all Sentence ℒₛₑₜ occurrences with SetTheorySentence in SetTheory/Basic/Misc.lean and SetTheory/Basic/Axioms.lean

Sentence ℒₒᵣ⋆ in TA/Nonstandard.lean is intentionally untouched — it refers to the distinct extended language ℒₒᵣ⋆.

Original prompt

---

This section details on the original issue you should resolve

<issue_title>ℒₒᵣ / ℒₛₑₜ-Sentence to ArithmeticSentence / SetTheorySentence</issue_title>
<issue_description>混在していてよくないと思う．</issue_description>

Comments on the Issue (you are @copilot in this section)

@iehality たしかに．

• Fixes ℒₒᵣ / ℒₛₑₜ-Sentence to ArithmeticSentence / SetTheorySentence #803

---

💬 We'd love your input! Share your thoughts on Copilot coding agent in our 2 minute survey.

[SnO2WMaN]

@copilot Summalize this

[Copilot]

@copilot Summalize this

This PR standardizes how sentences are typed across the codebase:

• New alias: SetTheorySentence := Sentence ℒₛₑₜ added to mirror the existing ArithmeticSentence := Sentence ℒₒᵣ
• 17 files updated: All direct uses of Sentence ℒₒᵣ → ArithmeticSentence and Sentence ℒₛₑₜ → SetTheorySentence

Files touched span Incompleteness/, Bootstrapping/, Arithmetic/, SetTheory/, and ProvabilityLogic/. The Sentence ℒₒᵣ⋆ in TA/Nonstandard.lean was left as-is since ℒₒᵣ⋆ is a distinct extended language.

[SnO2WMaN]

大雑把にリファクタリングしたが #794 と競合している可能性はある．