info
Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss
Re: Opportunities arising from the refutation of Godel's incompleteness theorem [--it is not that difficult--]
0 views
Skip to first unread message
peteolcott
May 10, 2019, 11:34:47 AM5/10/19
to
On 5/10/2019 4:10 AM, xilog wrote:
> To be specific, a description of a relatively recent proof in a modern proof tool may be found here:
>
> https://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-logic.pdf
>
> Someone in possession of a refutation would be able to extend this work to obtain a derivation of a contradiction in isabelle/HOL, which would be taken seriously by many people.
>
How hard is it to understand the basic model of Sound_Deduction?
True premises combined with valid inference necessitates true consequences.
How hard is it to understand ¬Sound_Deduction as either not true premises
or not valid deduction?
It really should not take any wild stretch of the imagination to realize
that any logic sentences X that cannot possibly be resolved to X or ¬X
are deductively unsound.
All of the undecidable sentences of conventional mathematical logic then
simply become deductively unsound.
--
Copyright 2019 Pete Olcott
All rights reserved
> To be specific, a description of a relatively recent proof in a modern proof tool may be found here:
>
> https://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-logic.pdf
>
> Someone in possession of a refutation would be able to extend this work to obtain a derivation of a contradiction in isabelle/HOL, which would be taken seriously by many people.
>
How hard is it to understand the basic model of Sound_Deduction?
True premises combined with valid inference necessitates true consequences.
How hard is it to understand ¬Sound_Deduction as either not true premises
or not valid deduction?
It really should not take any wild stretch of the imagination to realize
that any logic sentences X that cannot possibly be resolved to X or ¬X
are deductively unsound.
All of the undecidable sentences of conventional mathematical logic then
simply become deductively unsound.
--
Copyright 2019 Pete Olcott
All rights reserved
0 new messages