[alexpglez]

Muchas gracias por la respuesta, con esa demostración,

\( x\leq y\land x\neq y\rightarrow x'\leq y \), ya sale todo.
Sin embargo veo un fallo: 

En el primer caso, por la transitividad ya probada, \( y\leq y'\leq x \) implica que \( y\leq x \), luego por hipótesis de inducción \( x=y \). (En realidad este caso no puede darse, pero eso no importa para la prueba.)[/li][/list]

Y es que se quería probar [texx] x=y' [/texx]

Sin embargo:
[texx] x'\leq y' \rightarrow x \leq y [/texx]
Por inducción: [texx] x' \leq 0' \rightarrow x' \leq 0 \vee x'=0' \rightarrow x=0 \rightarrow x \leq 0 [/texx]
Para [texx] y' [/texx], [texx] x' \leq y'' \rightarrow x'\leq y' \vee x'=y'' [/texx]. En el primer caso, por hipótesis de inducción y transitividad [texx]  x \leq y \leq y'[/texx]. En el segundo por el 4 axioma de Peano, [texx] x=y' \rightarrow x \leq y' [/texx].

Luego: [texx] \neg x'\leq x [/texx]
Para [texx] 0'\leq 0 \rightarrow 0'=0 [/texx] contradicción. Suponiendo para [texx] x [/texx], para el siguiente, [texx] x''\leq x' \rightarrow x' \leq x [/texx] contradicción.

Luego la demostración de la antisimétrica: [texx] x\leq y \wedge y \leq x \rightarrow x=y [/texx]
[texx] y=0 \rightarrow x=0=y [/texx]
[texx] y\not=0 \rightarrow \exists r y=r' \rightarrow x\leq r \vee x=r'=y [/texx], en el segundo caso está demostrado. En el primero, por transitividad [texx] r' \leq x \leq r [/texx], contradicción.

Gracias otra vez y saludos.

[Carlos Ivorra]

Sin embargo veo un fallo: 

En el primer caso, por la transitividad ya probada, \( y\leq y'\leq x \) implica que \( y\leq x \), luego por hipótesis de inducción \( x=y \). (En realidad este caso no puede darse, pero eso no importa para la prueba.)[/li][/list]

Y es que se quería probar [texx] x=y' [/texx]

Cierto. Ya lo he corregido.

[alexpglez]

Perdonad que siga preguntando, se me ha ocurrido intentar demostrar si la relación es un buen orden en N. Pero no lo veo claro.
Para estas demostraciones entiendo que lo más sencillo es por reducción al absurdo.
[texx] \neg \forall A \subset N (A\not=\emptyset \rightarrow \exists m \; minimo \; de \; A) [/texx]
[texx] \exists A \subset N (A\not=\emptyset \wedge \forall m \in A \;\; \exists x \in A \; x \leq m \wedge x\not=m) [/texx]
Supongo tal conjunto A [texx] A \subset N \wedge A \not= \emptyset [/texx].
Y ver que:
[texx]\forall m \in A \;\; \exists x \in A \; x \leq m \wedge x\not=m [/texx]
Lleva a una contradicción. Pero no encuentro como formalizar alguna.

Gracias, saludos.

Edito: si el 0 está en el subconjunto, es claro que es mínimo, si no lo está tendría que haber otro que fuera mínimo. Y si se quiere, se debería poder demostrar que un subconjunto sin mínimo es el vacío, pero no sé como formalizar alguna de éstas contradicciones.

[Carlos Ivorra]

No uses reducción al absurdo. Toma un \( A\subset \mathbb N \) y demuestra por inducción sobre \( n \) que si existe un \( m\in A \) tal que \( m\leq n \), entonces \( A \) tiene un mínimo elemento.

[alexpglez]

No uses reducción al absurdo. Toma un \( A\subset \mathbb N \) y demuestra por inducción sobre \( n \) que si existe un \( m\in A \) tal que \( m\leq n \), entonces \( A \) tiene un mínimo elemento.

¿Inducción sobre el número de elementos?

¿No habría otra forma sin dar por demostrado y no utilizar nada acerca de los cardinales?

Edito: Perdona, leyendo otra vez entiendo que no has dicho número de elementos, sin embargo no entiendo qué es el [texx] n [/texx] que indicas.

[Carlos Ivorra]

\( n \) es un número natural. Por ejemplo, para \( n=0 \) se trata de probar que si existe un \( m\in A \) tal que \( m\leq 0 \) entonces \( A \) tiene mínimo elemento. Y esto es cierto, porque en tal caso tiene que ser \( m=0\in A \), luego \( 0 \) es el mínimo de \( A \).

[alexpglez]

\( n \) es un número natural. Por ejemplo, para \( n=0 \) se trata de probar que si existe un \( m\in A \) tal que \( m\leq 0 \) entonces \( A \) tiene mínimo elemento. Y esto es cierto, porque en tal caso tiene que ser \( m=0\in A \), luego \( 0 \) es el mínimo de \( A \).

Entiendo.
[texx] m \leq n' \rightarrow  m \leq n \vee m =n' [/texx], por HI en el primer caso A tiene mínimo elemento, y en el segundo caso: [texx] n' [/texx] es mínimo de A (en tal caso ya está demostrado), o existe otro menor [texx] r \leq n' \wedge r \not=n' \rightarrow r \leq n [/texx] que por la hipótesis A tendría mínimo elemento.
Luego:
[texx] \forall n \in N \; (\exists m \in A \; m \leq n \rightarrow A \; tiene \; minimo) [/texx]
Como [texx] A\not=\emptyset [/texx], [texx] \exists x \in A [/texx], como [texx] x \in N [/texx] y [texx] x \leq x [/texx], entonces [texx] A [/texx] tiene mínimo.


La idea detrás de esta inducción supongo que sería:
"Existe un [texx] x [/texx] que pertenece a [texx] A [/texx], si es el mínimo hemos acabado, en caso contrario existe un [texx] x_2<x [/texx] en [texx] A [/texx], si no es el mínimo existe un [texx] x_3<x_2<x[/texx].... Así hasta que encontremos un [texx] x_N \not=0 [/texx] que sea mínimo, y en caso de no haberlo necesariamente llegamos al valor [texx] 0 \in A [/texx]"
¿Es así?

[Carlos Ivorra]

Eso es.