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 4, 2013 12:18 AM


On 11/3/2013 10:54 PM, fom wrote: > 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 ) >
Whoops
Ax( P(x) <> Q )
I had just been thinking of the quantifier issue when I wrote that. This would be the formula with the implied biconditional of definition as well.
> > 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 ) ) > > > ) ) > > > >

