Lawrence Paulson
2018-10-31 16:31:58 UTC
Formalisation and Evaluation of Alan Gewirth's Proof for the Principle of Generic Consistency in Isabelle/HOL
An ambitious ethical theory ---Alan Gewirth's "Principle of Generic Consistency"--- is encoded and analysed in Isabelle/HOL. Gewirth's theory has stirred much attention in philosophy and ethics and has been proposed as a potential means to bound the impact of artificial general intelligence.
The proof document is a full paper describing the work.An ambitious ethical theory ---Alan Gewirth's "Principle of Generic Consistency"--- is encoded and analysed in Isabelle/HOL. Gewirth's theory has stirred much attention in philosophy and ethics and has been proposed as a potential means to bound the impact of artificial general intelligence.
This is one of a number of entries concerned with the formalisation of philosophical theories. We have a new topic, Logic/Philosophy, and I've taken the liberty of moving some existing entries to this topic. These include a number of proofs of the existence of God.
The new entry is at https://www.isa-afp.org/entries/GewirthPGCProof.html.
Larry Paulson