Și dacă v-am plictisit

cu argumentul ontologic al lui Gödel, să notăm că el a fost recent formalizat și demonstrat pe calculator cu ajutorul demonstratoarelor automate de teoreme.

Nu in sine acest lucru este interesant la anunțul respectiv (despre demonstrarea automată a argumentului ontologic original, cel al lui Anselm, am mai adus vorba). Ci (cu rezerva că nu sunt specialist in logica modală și s-ar putea să mă inșel) faptul că potrivit anunțului de două pagini pe care l-am citat mai sus logica modală K5 nu este necesară in demonstrație. In locul acesteia este suficient să folosim logica mai slabă KB.

Putem spune, până la urmă, că și problema  existenței lui Dumnezeu e bună la ceva: ca benchmark pentru Isabelle sau Coq.

Anunțuri
Acest articol a fost publicat în filosofie, haios, informaticã teoreticã. Pune un semn de carte cu legătura permanentă.

Lasă un răspuns

Completează mai jos detaliile tale sau dă clic pe un icon pentru a te autentifica:

Logo WordPress.com

Comentezi folosind contul tău WordPress.com. Dezautentificare / Schimbă )

Poză Twitter

Comentezi folosind contul tău Twitter. Dezautentificare / Schimbă )

Fotografie Facebook

Comentezi folosind contul tău Facebook. Dezautentificare / Schimbă )

Fotografie Google+

Comentezi folosind contul tău Google+. Dezautentificare / Schimbă )

Conectare la %s