Liste des Groupes | Revenir à s math |
On 8/2/2024 3:55 PM, Ross Finlayson wrote:Geometry, axiomatic geometry or Euclid's,On 08/02/2024 03:39 AM, FromTheRafters wrote:>>[...]>
What I ask,
if that you surpass,
the inductive impasse,
of the infinite super-task.
I don't see what infinite super.task or
what inductive impasse you are asking about.
>
I see transfinite induction being
a consequence of ordinals being
well.ordered.
>
I see cisfinite induction being
a consequence of finite ordinals being
well.ordered and bounding only 2.ended sets.
>
----
In transfinite induction,
{ξ ∈ 𝕆: ¬P(ξ)} holds
no first ordinal β:
¬P(β) ∧ ¬∃α<β: ¬P(α)
>
⎛ Because ordinals are well.ordered,
⎝ the set is no.first only.if {ξ ∈ 𝕆: ¬P(ξ)} = {}.
>
¬∃β ∈ 𝕆:( ¬P(β) ∧ ¬∃α<β: ¬P(α) )
⟹
¬∃ξ ∈ 𝕆: ¬P(ξ)
>
∀β ∈ 𝕆:( P(β) ⇐ ∀α<β: P(α) )
⟹
∀ξ ∈ 𝕆: P(ξ)
>
----
⎛ Because a finite.ordinal bounds only
⎜ 2.ended non.{}.sets
⎜ finite.ordinal β bounds only
⎜ non.{} [0,α)ᴼ with a second.end
⎝ [0,α)ᴼ = [0,α-1]ᴼ for 0 < α ≤ finite β
>
In cisfinite induction,
{ξ ∈ 𝕆ᶠⁱⁿ: ¬P(ξ)} doesn't hold
0 or ordinal β+1: ¬P(β+1) ∧ P(β)
>
...which implies
{ξ ∈ 𝕆ᶠⁱⁿ: ¬P(γ)} holds
no first ordinal β:
¬P(β) ∧ ¬∃α<β: ¬P(α)
and
no.first implies
{ξ ∈ 𝕆ᶠⁱⁿ: ¬P(ξ)} = {}.
>
P(0) ∧ ¬∃β ∈ 𝕆ᶠⁱⁿ: ¬P(β+1) ∧ P(β)
⟹
¬∃β ∈ 𝕆ᶠⁱⁿ:( ¬P(β) ∧ ¬∃α<β: ¬P(α) )
⟹
¬∃ξ ∈ 𝕆: ¬P(ξ)
>
P(0) ∧ ∀β ∈ 𝕆ᶠⁱⁿ: P(β) ⇒ P(β+1)
⟹
∀β ∈ 𝕆ᶠⁱⁿ:( P(β) ⇐ ∀α<β: P(α) )
⟹
∀ξ ∈ 𝕆ᶠⁱⁿ: P(ξ)
>
---->Then what *is* restricted comprehension?>
Usually it's just
the antonym of expansion of comprehension.
I am more familiar with unrestricted comprehension
being the antonym of restricted comprehension.
>
Unrestricted comprehension grants that
{x:P(x)} exists because
description P(x) of its elements exists.
>
Restricted comprehension grants that
{x∈A:P(x)} exists because
description P(x) and set A exist.
>
The existence of set A might have been granted
because of Restricted.Comprehension or Infinity or
Power.Set or Union or Replacement or Pairing,
but A would be logically prior to {x∈A:P(x)}
by some route.
>
>
Les messages affichés proviennent d'usenet.