5 ms·

Given the recent push towards formally verifying mathematics, it's surprising how comparatively little effort's been put into formalising ethics. Fundamentally

Given the recent push towards formally verifying mathematics, it's surprising how comparatively little effort's been put into formalising ethics. Fundamentally an ethical system is not that different from a mathematical one: there are some assumptions, some deductive rules, and a potentially infinite set of conclusions that result from applying those deductive rules to those assumptions. One particularly important property to verify about such a system is consistency: if it can prove conclusion "X", it should not also be able to prove conclusion "not X". An inconsistent system can prove anything, so is essentially useless for reasoning.

m12k 6y ago
Philosophers have been trying and failing for millennia to come up with hard rules for ethics. A rule that is essential in one context invariably leads to absurdity in others (there are many examples involving people strapped to train tracks). So an attempt at formalizing this will not just be ambiguous, but likely unsound and contradictory. While mathematics seem to be this perfect structure encoded in the fabric of the universe, just waiting for us to discover and describe it, ethics in contrast seems to be a very fuzzy, imperfect, ad-hoc creation of mankind.
- logicchains 6y ago
  >Philosophers have been trying and failing for millennia to come up with hard rules for ethics. They've been trying to find one true/correct system of ethics, which is doomed to fail due to https://en.wikipedia.org/wiki/Regress_argument https://en.wikipedia.org/wiki/Regress_argument. What I'm talking about is not trying to find new systems, rather just formalising existing systems, so that they can be analysed more rigorously and checked for consistency. Much as for instance one can formalise and compare homotopy type theory and set theory as foundations for real analysis.
  - dfabulich 6y ago
    Rudolf Carnap worked hard on formalizing ethics (and everything else) in the 20th century; the project was a total flop. It turns out you can't formalize anything that doesn't have proofs -- in other words, it basically only works for what we'd call "mathematics" or "pure logic". You can't formalize literally anything else in philosophy, at all. The regress argument has nothing to do with ethics in particular. It applies just as much to any non-proof area of study, including all of science, history, and even ordinary observations and recollections.
    - logicchains 6y ago
      >It turns out you can't formalize anything that doesn't have proofs -- in other words, it basically only works for what we'd call "mathematics" or "pure logic". You can't formalize literally anything else in philosophy, at all. What do you mean by "doesn't have proofs" here? It's demonstrably possible to develop a formalised philosophy: see Spinoza's Ethics for an example. It's impossible to prove that one formalisation is more "correct", but the same applies to mathematics, via Gödel's second incompleteness theorem. >The regress argument has nothing to do with ethics in particular. It applies just as much to any non-proof area of study, including all of science, history, and even ordinary observations and recollections. It also applies to maths in the form that a system cannot prove its own consistency. Yet that doesn't stop us formally analysing, comparing and making use of different mathematical systems.
    - tr352 6y ago
      > It turns out you can't formalize anything that doesn't have proofs -- in other words, it basically only works for what we'd call "mathematics" or "pure logic". You can't formalize literally anything else in philosophy, at all. This couldn’t be further from the truth. There is a wealth of logics that have been developed and studied within philosophy, that aim to formalize various philosophical concepts. See modal logics, deontic logics, logics about knowledge and belief, and so on.
      - ukj 6y ago
        The notion of a "proof" is only meaningful in a formal context. Logic, mathematics, computer science, proof theory... same thing. https://en.wikipedia.org/wiki/Proof_theory https://en.wikipedia.org/wiki/Proof_theory We are eternally stuck interpreting all of our theories in the context of their meta-theoretic assumptions.
        tr352 6y ago
        Not sure we’re talking about the same thing here. I was replying to your claim that nothing in philosophy (apart from mathematics) can be formalized. The role of logic is not to solve the metaphysical problem of infinite regress.
- RivieraKid 6y ago
  Yeah, ethics is subjective and it's fascinating that many smart people don't realize this. Ultimately it always boils down to "I feel this is right". Of course, you can have objective claims such as "if all people followed this principle, it would have this outcome".
  - animationwill 6y ago
    There is a tension between relative/subjective ethics and absolute/objective ethics. Philosophers seek to discover the absolute, but they cannot shake the human condition
  - coldtea 6y ago
    >Of course, you can have objective claims such as "if all people followed this principle, it would have this outcome". Good luck proving the outcome for anything less than very trivial cases...
    - RivieraKid 6y ago
      Well obviously you can't prove the outcome of making a change in a complex physical system with many biological components. We can barely model a protein.
tr352 6y ago
There has actually been quite some work since the 50ies up to the present day on deontic logic, which is reasoning about ethical concepts such as obligation and permission.
netcan 6y ago
There has always been a ton of effort at formalising ethics, political theories and philosophy generally in a mathematical-like way. The whole of modern philosophy, especially political philosophy , is a product of that effort. That's basically what the enlightenment was. The problem, IMO, is that formalistic, math-like approach produces "an inconsistent system can prove anything, so is essentially useless for reasoning." Going for fundamental, objective truths with a mathematical standard as an ideal can go one of three ways: delusion, nihilism or sociopathy. Peter Singer, Jeremy Bentham and other utilitarians came up with a "moral math" system that (a) sounded morally reasonable at first pass and (b) are theoretical applicable widely. The problem they encounter is extreme conclusions. Bentham was responsible for some horrific prison/reformatory systems. Singer ends up with some sociopathic conclusions like morally good infanticide. Ayn Rand went down a philosophical worm-whole trying to tie her philosophical system into one "theory-of-everything" bow where pure (Aristotelian) logic yields conclusive answers to all epistemological, moral, political & economic questions. This certainty, rather than just the extreme or counterintuitive (selfishness as a virtue) elements of objectivism is what gives it that cult-like flavour. Ayn Rand was simply following the frame created by Marxism, and Trotsky particularly. Marxism of that era was all about airtight rationality. Communism wasn't a choice, but a dictate of pure reason. Marxists got this idea from French revolutionary philosophers, who started with the idea of "rationalising" everything with math-like systems of thought. What all these have in common is a desire to create irreproachable systems. Like math, like physics. In practice, they created religions. Religions are irreproachable too. The way religions become irreproachable is by banishing heretics. That's what the "secular" rationalist philosophers did to. Rand was famous for her banishments. If you are after scientifically valid, reductive, Popperian insights only... you might just have to accept that this is an amoral viewpoint. Morals just don't exist in the mathematical realm.
- logicchains 6y ago
  >What all these have in common is a desire to create irreproachable systems. Like math, like physics. In practice, they created religions. Religions are irreproachable too. The way religions become irreproachable is by banishing heretics. That's what the "secular" rationalist philosophers did to. Rand was famous for her banishments. I'm not talking about using mathematical, logical approach to find the "most correct" philosophy. As Wittegenstein noted in Tractatus, the "most correct" approach is: "To say nothing except what can be said, i.e. the propositions of natural science, i.e. something that has nothing to do with philosophy: and then always, when someone else wished to say something metaphysical, to demonstrate to him that he had given no meaning to certain signs in his propositions". Rather I'm talking about using formal methods to analyse existing systems. Identify their axioms, identify the deductive rules they permit, and determine how consistent they are. Maybe even formally verify this in a proof assistant. Then it'd be also possible to e.g. explore what different systems can and cannot prove (somewhat akin to https://en.wikipedia.org/wiki/Reverse_mathematics https://en.wikipedia.org/wiki/Reverse_mathematics). An example kinda along these lines is Lawvere's work on modelling Hegelian philosophy as modal type theory: https://ncatlab.org/nlab/show/Hegel%27s+%22Logic%22+as+Modal+Type+Theory https://ncatlab.org/nlab/show/Hegel%27s+%22Logic%22+as+Modal....
ahelwer 6y ago
If we want to be very reductive about it there is not a great reason to believe we can use formal logic to inform the chosen(?) actions of huge aggregates of molecules jiggling around. All ethical systems that have withstood the test of time (the gold & silver rules) use subjectivity. Everything else falls prey to absurdity. I recall an objection was raised (possibly by Alasdair MacIntyre? it's been a while since I got wrapped up in all this) that any system of ethics must be inherently self-contradictory. The reason for this is something like any time we spend in pursuit of correcting or preventing some moral wrong is time not given doing the same for another. And there are certainly a great many moral wrongs going on according to any given system of ethics - probably all of equal importance. Separately we might also ask whether we even want to solve the problem of ethics. Imagine tomorrow we develop an ironclad formal moral system - everyone is forced to agree it is correct through sheer reason alone, and it meaningfully informs our every action. Would you really want to live in such a world? It seems a world without freedom, or one which would quickly become that way. All-encompassing totalitarianism. [0] In other threads you say you aren't interested in proving which system of ethics is most applicable to human endeavours or anything like that. At this point we get into "higher order truths about chmess" territory, as in - why bother? [1] [0] https://www.existentialcomics.com/comic/139 https://www.existentialcomics.com/comic/139 [1] https://ase.tufts.edu/cogstud/dennett/papers/chmess.pdf https://ase.tufts.edu/cogstud/dennett/papers/chmess.pdf
- logicchains 6y ago
  >Separately we might also ask whether we even want to solve the problem of ethics. The article's author presents a good example: for AI ethics. If we want to prove "an AI following this system won't kill all humans (or has e.g. less than 0.1% chance of killing all humans)", we need to be able to formally reason about that system. >In other threads you say you aren't interested in proving which system of ethics is most applicable to human endeavours or anything like that. At this point we get into "higher order truths about chmess" territory, as in - why bother? [1] By that logic, why bother with any of the higher, more abstract fields of mathematics?
  - RivieraKid 6y ago
pron 6y ago
Have you heard of paraconsistent logic? Ethics does not aim to practically tell us what we should do at all times, but to give us the tools to think about such question. A system of ethics where two opposing conclusions can be reach could be perfectly fine.
- logicchains 6y ago
  In paraconsistent logics one cannot use a proof of "X" and "not X" to prove any arbitrary statement, so it can indeed still be useful. However we still need to formally reason about the system to be able to establish that it is indeed a paraconsistent logic (that the principle of explosion doesn't apply).
asdasdasdas5453 6y ago
There has been at least since 1951 since the famous publication of Arrow's impossibility theorem. Extract from Wikipedia : "The framework for Arrow's theorem assumes that we need to extract a preference order on a given set of options (outcomes). Each individual in the society (or equivalently, each decision criterion) gives a particular order of preferences on the set of outcomes. We are searching for a ranked voting electoral system, called a social welfare function (preference aggregation rule), which transforms the set of preferences (profile of preferences) into a single global societal preference order. Arrow's theorem says that if the decision-making body has at least two members and at least three options to decide among, then it is impossible to design a social welfare function that satisfies all these conditions (assumed to be a reasonable requirement of a fair electoral system) at once: [...]" https://en.wikipedia.org/wiki/Arrow%27s_impossibility_theorem https://en.wikipedia.org/wiki/Arrow%27s_impossibility_theore...
coldtea 6y ago
>Fundamentally an ethical system is not that different from a mathematical one: there are some assumptions, some deductive rules, and a potentially infinite set of conclusions that result from applying those deductive rules to those assumptions. Even simple enough math starting from formal axioms are incomplete (Godel) [1]. Real world ethics, starting by ethical assumptions will be 1000 times as full of holes and inconsistencies. And that's before we even consider language ambiguities in the much more complex "ethical assumptions". [1] "The first incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an effective procedure (i.e., an algorithm) is capable of proving all truths about the arithmetic of natural numbers. For any such consistent formal system, there will always be statements about natural numbers that are true, but that are unprovable within the system. The second incompleteness theorem, an extension of the first, shows that the system cannot demonstrate its own consistency".
- logicchains 6y ago
  >Even simple enough math starting from formal axioms are incomplete (Godel) [1]. Real world ethics, starting by ethical assumptions will be 1000 times as full of holes and inconsistencies. Just because a mathematical system like set theory is incomplete (can't prove its own consistency), that doesn't mean it's "full of holes and inconsistencies". And just because a system cannot prove itself consistent, doesn't mean it can't be proven consistent in some larger system (for instance how we can use ZFC to prove that Peano arithmetic is consistent).

m12k 6y ago

Philosophers have been trying and failing for millennia to come up with hard rules for ethics. A rule that is essential in one context invariably leads to absurdity in others (there are many examples involving people strapped to train tracks). So an attempt at formalizing this will not just be ambiguous, but likely unsound and contradictory. While mathematics seem to be this perfect structure encoded in the fabric of the universe, just waiting for us to discover and describe it, ethics in contrast seems to be a very fuzzy, imperfect, ad-hoc creation of mankind.

logicchains 6y ago
>Philosophers have been trying and failing for millennia to come up with hard rules for ethics. They've been trying to find one true/correct system of ethics, which is doomed to fail due to https://en.wikipedia.org/wiki/Regress_argument https://en.wikipedia.org/wiki/Regress_argument. What I'm talking about is not trying to find new systems, rather just formalising existing systems, so that they can be analysed more rigorously and checked for consistency. Much as for instance one can formalise and compare homotopy type theory and set theory as foundations for real analysis.
- dfabulich 6y ago
  Rudolf Carnap worked hard on formalizing ethics (and everything else) in the 20th century; the project was a total flop. It turns out you can't formalize anything that doesn't have proofs -- in other words, it basically only works for what we'd call "mathematics" or "pure logic". You can't formalize literally anything else in philosophy, at all. The regress argument has nothing to do with ethics in particular. It applies just as much to any non-proof area of study, including all of science, history, and even ordinary observations and recollections.
  - logicchains 6y ago
    >It turns out you can't formalize anything that doesn't have proofs -- in other words, it basically only works for what we'd call "mathematics" or "pure logic". You can't formalize literally anything else in philosophy, at all. What do you mean by "doesn't have proofs" here? It's demonstrably possible to develop a formalised philosophy: see Spinoza's Ethics for an example. It's impossible to prove that one formalisation is more "correct", but the same applies to mathematics, via Gödel's second incompleteness theorem. >The regress argument has nothing to do with ethics in particular. It applies just as much to any non-proof area of study, including all of science, history, and even ordinary observations and recollections. It also applies to maths in the form that a system cannot prove its own consistency. Yet that doesn't stop us formally analysing, comparing and making use of different mathematical systems.
  - tr352 6y ago
    > It turns out you can't formalize anything that doesn't have proofs -- in other words, it basically only works for what we'd call "mathematics" or "pure logic". You can't formalize literally anything else in philosophy, at all. This couldn’t be further from the truth. There is a wealth of logics that have been developed and studied within philosophy, that aim to formalize various philosophical concepts. See modal logics, deontic logics, logics about knowledge and belief, and so on.
    - ukj 6y ago
      The notion of a "proof" is only meaningful in a formal context. Logic, mathematics, computer science, proof theory... same thing. https://en.wikipedia.org/wiki/Proof_theory https://en.wikipedia.org/wiki/Proof_theory We are eternally stuck interpreting all of our theories in the context of their meta-theoretic assumptions.
      - tr352 6y ago
        Not sure we’re talking about the same thing here. I was replying to your claim that nothing in philosophy (apart from mathematics) can be formalized. The role of logic is not to solve the metaphysical problem of infinite regress.
RivieraKid 6y ago
Yeah, ethics is subjective and it's fascinating that many smart people don't realize this. Ultimately it always boils down to "I feel this is right". Of course, you can have objective claims such as "if all people followed this principle, it would have this outcome".
- animationwill 6y ago
  There is a tension between relative/subjective ethics and absolute/objective ethics. Philosophers seek to discover the absolute, but they cannot shake the human condition
- coldtea 6y ago
  >Of course, you can have objective claims such as "if all people followed this principle, it would have this outcome". Good luck proving the outcome for anything less than very trivial cases...
  - RivieraKid 6y ago
    Well obviously you can't prove the outcome of making a change in a complex physical system with many biological components. We can barely model a protein.

tr352 6y ago

There has actually been quite some work since the 50ies up to the present day on deontic logic, which is reasoning about ethical concepts such as obligation and permission.

netcan 6y ago

There has always been a ton of effort at formalising ethics, political theories and philosophy generally in a mathematical-like way. The whole of modern philosophy, especially political philosophy , is a product of that effort. That's basically what the enlightenment was. The problem, IMO, is that formalistic, math-like approach produces "an inconsistent system can prove anything, so is essentially useless for reasoning." Going for fundamental, objective truths with a mathematical standard as an ideal can go one of three ways: delusion, nihilism or sociopathy. Peter Singer, Jeremy Bentham and other utilitarians came up with a "moral math" system that (a) sounded morally reasonable at first pass and (b) are theoretical applicable widely. The problem they encounter is extreme conclusions. Bentham was responsible for some horrific prison/reformatory systems. Singer ends up with some sociopathic conclusions like morally good infanticide. Ayn Rand went down a philosophical worm-whole trying to tie her philosophical system into one "theory-of-everything" bow where pure (Aristotelian) logic yields conclusive answers to all epistemological, moral, political & economic questions. This certainty, rather than just the extreme or counterintuitive (selfishness as a virtue) elements of objectivism is what gives it that cult-like flavour. Ayn Rand was simply following the frame created by Marxism, and Trotsky particularly. Marxism of that era was all about airtight rationality. Communism wasn't a choice, but a dictate of pure reason. Marxists got this idea from French revolutionary philosophers, who started with the idea of "rationalising" everything with math-like systems of thought. What all these have in common is a desire to create irreproachable systems. Like math, like physics. In practice, they created religions. Religions are irreproachable too. The way religions become irreproachable is by banishing heretics. That's what the "secular" rationalist philosophers did to. Rand was famous for her banishments. If you are after scientifically valid, reductive, Popperian insights only... you might just have to accept that this is an amoral viewpoint. Morals just don't exist in the mathematical realm.

logicchains 6y ago
>What all these have in common is a desire to create irreproachable systems. Like math, like physics. In practice, they created religions. Religions are irreproachable too. The way religions become irreproachable is by banishing heretics. That's what the "secular" rationalist philosophers did to. Rand was famous for her banishments. I'm not talking about using mathematical, logical approach to find the "most correct" philosophy. As Wittegenstein noted in Tractatus, the "most correct" approach is: "To say nothing except what can be said, i.e. the propositions of natural science, i.e. something that has nothing to do with philosophy: and then always, when someone else wished to say something metaphysical, to demonstrate to him that he had given no meaning to certain signs in his propositions". Rather I'm talking about using formal methods to analyse existing systems. Identify their axioms, identify the deductive rules they permit, and determine how consistent they are. Maybe even formally verify this in a proof assistant. Then it'd be also possible to e.g. explore what different systems can and cannot prove (somewhat akin to https://en.wikipedia.org/wiki/Reverse_mathematics https://en.wikipedia.org/wiki/Reverse_mathematics). An example kinda along these lines is Lawvere's work on modelling Hegelian philosophy as modal type theory: https://ncatlab.org/nlab/show/Hegel%27s+%22Logic%22+as+Modal+Type+Theory https://ncatlab.org/nlab/show/Hegel%27s+%22Logic%22+as+Modal....

ahelwer 6y ago

If we want to be very reductive about it there is not a great reason to believe we can use formal logic to inform the chosen(?) actions of huge aggregates of molecules jiggling around. All ethical systems that have withstood the test of time (the gold & silver rules) use subjectivity. Everything else falls prey to absurdity. I recall an objection was raised (possibly by Alasdair MacIntyre? it's been a while since I got wrapped up in all this) that any system of ethics must be inherently self-contradictory. The reason for this is something like any time we spend in pursuit of correcting or preventing some moral wrong is time not given doing the same for another. And there are certainly a great many moral wrongs going on according to any given system of ethics - probably all of equal importance. Separately we might also ask whether we even want to solve the problem of ethics. Imagine tomorrow we develop an ironclad formal moral system - everyone is forced to agree it is correct through sheer reason alone, and it meaningfully informs our every action. Would you really want to live in such a world? It seems a world without freedom, or one which would quickly become that way. All-encompassing totalitarianism. [0] In other threads you say you aren't interested in proving which system of ethics is most applicable to human endeavours or anything like that. At this point we get into "higher order truths about chmess" territory, as in - why bother? [1] [0] https://www.existentialcomics.com/comic/139 https://www.existentialcomics.com/comic/139 [1] https://ase.tufts.edu/cogstud/dennett/papers/chmess.pdf https://ase.tufts.edu/cogstud/dennett/papers/chmess.pdf

logicchains 6y ago
>Separately we might also ask whether we even want to solve the problem of ethics. The article's author presents a good example: for AI ethics. If we want to prove "an AI following this system won't kill all humans (or has e.g. less than 0.1% chance of killing all humans)", we need to be able to formally reason about that system. >In other threads you say you aren't interested in proving which system of ethics is most applicable to human endeavours or anything like that. At this point we get into "higher order truths about chmess" territory, as in - why bother? [1] By that logic, why bother with any of the higher, more abstract fields of mathematics?
- RivieraKid 6y ago

pron 6y ago

Have you heard of paraconsistent logic? Ethics does not aim to practically tell us what we should do at all times, but to give us the tools to think about such question. A system of ethics where two opposing conclusions can be reach could be perfectly fine.

logicchains 6y ago
In paraconsistent logics one cannot use a proof of "X" and "not X" to prove any arbitrary statement, so it can indeed still be useful. However we still need to formally reason about the system to be able to establish that it is indeed a paraconsistent logic (that the principle of explosion doesn't apply).

asdasdasdas5453 6y ago

There has been at least since 1951 since the famous publication of Arrow's impossibility theorem. Extract from Wikipedia : "The framework for Arrow's theorem assumes that we need to extract a preference order on a given set of options (outcomes). Each individual in the society (or equivalently, each decision criterion) gives a particular order of preferences on the set of outcomes. We are searching for a ranked voting electoral system, called a social welfare function (preference aggregation rule), which transforms the set of preferences (profile of preferences) into a single global societal preference order. Arrow's theorem says that if the decision-making body has at least two members and at least three options to decide among, then it is impossible to design a social welfare function that satisfies all these conditions (assumed to be a reasonable requirement of a fair electoral system) at once: [...]" https://en.wikipedia.org/wiki/Arrow%27s_impossibility_theorem https://en.wikipedia.org/wiki/Arrow%27s_impossibility_theore...

coldtea 6y ago

>Fundamentally an ethical system is not that different from a mathematical one: there are some assumptions, some deductive rules, and a potentially infinite set of conclusions that result from applying those deductive rules to those assumptions. Even simple enough math starting from formal axioms are incomplete (Godel) [1]. Real world ethics, starting by ethical assumptions will be 1000 times as full of holes and inconsistencies. And that's before we even consider language ambiguities in the much more complex "ethical assumptions". [1] "The first incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an effective procedure (i.e., an algorithm) is capable of proving all truths about the arithmetic of natural numbers. For any such consistent formal system, there will always be statements about natural numbers that are true, but that are unprovable within the system. The second incompleteness theorem, an extension of the first, shows that the system cannot demonstrate its own consistency".

logicchains 6y ago
>Even simple enough math starting from formal axioms are incomplete (Godel) [1]. Real world ethics, starting by ethical assumptions will be 1000 times as full of holes and inconsistencies. Just because a mathematical system like set theory is incomplete (can't prove its own consistency), that doesn't mean it's "full of holes and inconsistencies". And just because a system cannot prove itself consistent, doesn't mean it can't be proven consistent in some larger system (for instance how we can use ZFC to prove that Peano arithmetic is consistent).