fom
Posts:
1,968
Registered:
12/4/12


Re: Surprise at my failure to resolve an issue in an elementary paper by Rado
Posted:
Nov 3, 2013 11:54 PM


On 11/3/2013 10:43 PM, fom wrote:
<snip>
With the following definitions, Rado's proof is correct.
It assumes an implicit biconditional as is common with definitions.
It does not assume an exclusive index at which values may vary.
The definition interprets the "whenever ... then" statement as
Ax( P(x) > Q )
Corrected property definition =============================
P(k) <> (
k in { 1, ..., r }
/\
AmAn(
[ ( ( < m > = < a_1, ..., a_r > /\ < n > = < b_1, ..., b_r > )
/\
( m subset B' /\ n subset B' ) )
/\
Ai( ~( i = k) > ( a_i = b_i ) )
/\
( a_k = b_k ) )
<>
f( m ) =/= f( n ) ]
) )
Negation of corrected property definition =============================
~P(k) <> (
~( k in { 1, ..., r } )
\/
EmEn(
[ ( ( ~( < m > = < a_1, ..., a_r > /\ < n > = < b_1, ..., b_r > )
\/
~( m subset B' /\ n subset B' ) )
\/
Ei( ~( i = k) /\ ~( a_i = b_i ) )
\/
~( a_k = b_k ) )
<>
f( m ) =/= f( n ) ]
) )
Defintion at beginning of paper: ================================
Let L subset {1, 2, ..., r} be given.
Let A and f:[A]^r :=> F be given
LCB(x) denotes "x is Lcanonical on B"
===================================================
LCB(x) <> (
B subset A
/\
AmAn(
( ( < m > = < a_1, ..., a_r > /\ < n > = < b_1, ..., b_r > )
/\
( m subset B /\ n subset B ) )
>
( f( m ) = f( n ) <> Ak( k in L /\ a_k = b_k ) )
) )

