
Re: If ZFC is a FORMAL THEORY ... then what is THEOREM 1 ?
Posted:
Oct 6, 2012 5:09 PM


On Oct 7, 12:11 am, "Mike Terry" <news.dead.person.sto...@darjeeling.plus.com> wrote: > "Curt Welch" <c...@kcwc.com> wrote in message > > > "Mike Delanis" <inva...@invalid.com> wrote: > > > "Graham Cooper" <grahamcoop...@gmail.com> wrote in message > > >news:f76717dae1064b58829bb8531bff5faa@q9g2000pbo.googlegroups.com... > > > > > 20 goto 10 > > > > interpreter BASIC ............. you must be 60 years old. > > > My first access to computers was with an interpreted basic system in the > > early 1970's. Odd that when I first read your comment about being 60 it > > seemed way too high. But them I remembered I'm 56 soon, so 60 really is > > about right. Odd that I don't feel anything like "60". I think that's > > because I started to ignore my age once I hit 50 so I still feel like I'm > > in my 40's. :) > > The question shouldn't be "When did you *first* use interpreted basic?". It > should be "When might someone reasonably *last* have used it?" I recall > using linenumbered basic at work in the late 1980s, so 60 is way to high as > you first thought. > > Mike.
A THEORY *should* have line numbers.
A Syntactic Formula Enumeration
F0001 X F0002 X=X F0003 E(X) X=X F0004 A(x) X=X F0005 X^Y F0006 X^Y>X
A subset of which is sifted into Theoremhood!
F0001  X F0002  X=X F0003 T0001 E(X) X=X F0004 T0002 A(X) X=X F0005  X^Y F0006  X^Y>X F0007 T0003 A(X) X^Y>X ...
Herc  LOGIC E(Y) Y={xP(x)} <> DERIVE( E(Y) Y={xP(x)} ) DERIVE(T) <> DERIVE(a) ^ DERIVE(b) ^ (a^b)>T
MATHEMATICS E(Y) Y={xP(x)} <> PRVBLE( E(Y) Y={xP(x)} ) PRVBLE(T) <> NOT(DERIVE(NOT(T)))

