T|-HALT(Prog1) = Prog1|-H1() ^ Prog1|-H2() ^ .. ^ Prog1|-Hn()

[Graham Cooper]

No need for all of that "It can't be programmed!" "un-doable"
OMEGA_LEVEL_2_INFINITY Maths!

The HALT() Function could be programmed by placing PROGRAM STUBS in
the main loops of the software to test.

Similar to the way Godel PROVED "this is not provable"
in one Theory T1 and it works (TRUE) in another T2!

T|-HALT(Prog1) = Prog1|-H1() ^ Prog1|-H2() ^ .. ^ Prog1|-Hn()

If all the program stubs H1() H2() ... Hn() return TRUE then
HALT(program)=TRUE

******
PROGRAM T
USES: program1

10 IF HALT(program1) PRINT "HALTS"
******

The HALT Proof would not work using a concurrent programming meta-
syntax like:

CONCURRENCY RULE
ALL(m) ALL(n) NOT( P_m|-HALT() ^ P_m|-Hn())

PROGRAM SPECIFICATION HALT()
IF NOT(EXIST-FUNCTION( Hm() ) THEN DIE

i.e. a Halt function can only run if 1 or more Test Harnesses are
within the program to test

which_is_not_the_program_doing_the_testing.

Herc
--
COMPUTER MATHS
http://tinyurl.com/BiggestNumber
http://tinyurl.com/AntiDiagonals
http://tinyurl.com/CountableReals
http://tinyurl.com/ComputableReals
http://tinyurl.com/CountPermutations
http://tinyurl.com/GodelStatement

SET THEORY
http://tinyurl.com/SetAxioms
http://tinyurl.com/ConcreteSetTheory
http://tinyurl.com/FormalProof
http://tinyurl.com/AppliedLogic
http://tinyurl.com/SetOfEverything

POWERSETS MISUSE
http://tinyurl.com/MissingSet
http://tinyurl.com/PureSetTheory
http://tinyurl.com/AxiomOfRegularity
http://tinyurl.com/c-o-n-t-i-n-u-o-u-s-l-o-g-i-c

[Petra]

I have a few letters from ancient Egyptian that are extant....and have
to be rplaced by modern universals\tough

San, Quoppa & Digamma were part f the ancient 'hearing' or
calculations, and we have 48 days before a hearing


actually I agree that Einstein is ' a two op' I read that and its like
its a miscalculation in revers ( thesis or antithesis but 'hyped')

Say


ps do you think chat bot intellignece 'COULD' be used as legal
representations? (so on)

[Graham Cooper]

> > COMPUTER MATHShttp://tinyurl.com/BiggestNumberhttp://tinyurl.com/AntiDiagonalshttp:...
>
> > SET THEORYhttp://tinyurl.com/SetAxiomshttp://tinyurl.com/ConcreteSetTheoryhttp:...
>
> > POWERSETS MISUSEhttp://tinyurl.com/MissingSethttp://tinyurl.com/PureSetTheoryhttp://t...

>
> I have a few letters from ancient Egyptian that are extant....and have
> to be rplaced by modern universals\tough
>
> San, Quoppa & Digamma were part f the ancient 'hearing' or
> calculations, and we have 48 days before a hearing
>
> actually I agree that Einstein is ' a two op' I read that and its like
> its a miscalculation in revers ( thesis or antithesis but 'hyped')
>
> Say
>
> ps do you think chat bot intellignece 'COULD' be used as legal
> representations? (so on)

Exactly! I've already made an offer on the domain LAWBOT.com

There is a definite parallel between LEGAL PROTOCOL and FORMAL
PROVABILITY.

e.g. numerical affidavits, citing the source of the facts,
using a JP is just axiom instantiation you "swear the truth" to!

an excellent domain to extend Winograd's work, and lessen the burden
on the clogged up legal system.

But zooming around this Turing Machine in 3D is more fun!
http://wn.com/Universal_Turing_Machine_implemented_in_Minecraft_redstone_logic

Remember just 20 years ago translating from English to Russian then
back to English again was the hallmark of AI?

ENGLISH: THE SPIRIT IS STRONG BUT THE FLESH IS WEAK
RUSSIAN: Дух сильный, но плоть слаба
ENGLISH: THE WINE TASTES NICE BUT THE MEAT IS TENDER

Now look at how many Russian Brides I have lined up!
(live chat translators)

Herc
--

COMPUTER MATHS
http://tinyurl.com/BiggestNumber
http://tinyurl.com/AntiDiagonals

http://tinyurl.com/CountPermutations
http://tinyurl.com/GodelStatement
http://tinyurl.com/HaltFunction
http://tinyurl.com/ComputableReals