Theory GewirthArgument

(*<*)
theory GewirthArgument
  imports ExtendedDDL
begin
nitpick_params[user_axioms=true, show_all, expect=genuine, format = 3] 
(*>*)

text‹\noindent{Before starting our formalisation in the next section. We show that the axioms defined so far are consistent.
Rather surprisingly, the \emph{nunchaku} model finder states that no model has been found, while \emph{nitpick}
is indeed able to find one:}›
lemma True nunchaku[satisfy] nitpick[satisfy] oops

section ‹Gewith's Argument for the Principle of Generic Consistency (PGC)›

text‹\noindent{Alan Gewirth's meta-ethical position is known as moral (or ethical) rationalism. According to it, moral principles are knowable \emph{a priori},
by reason alone.
Immanuel Kant is perhaps the most famous figure who has defended such a position. He has argued for the existence of upper moral principles
(e.g. his "categorical imperative")
from which we can reason (in a top-down fashion) in order to deduce and evaluate other more concrete maxims and actions.
In contrast to Kant, Gewirth attempts to derive such upper moral principles by starting from non-moral considerations alone, namely from
an agent's self-reflection.
Gewirth's Principle of Generic Consistency (PGC) asserts that any agent (by virtue of its self-understanding as an agent) is rationally committed
to asserting that (i) it has rights to freedom and well-being, and (ii) that all other agents have those same rights. Gewirth claims that, in his informal proof,
the latter generalisation step (from "I" to all individuals) is done on purely logical grounds and does not presuppose any kind of universal moral principle.
Gewirth's result is thus meant to hold with some kind of apodicticity (i.e.~necessity).
Deryck Beyleveld, author of an authoritative book on Gewirth's argument, puts it this way:
"The argument purports to establish the PGC as a rationally necessary proposition with an apodictic status
\emph{for any PPA} equivalent to that enjoyed by the logical principle of noncontradiction itself." (cite‹"Beyleveld"› p. 1) 
If this is correct, then he succeeded in the task that Kant set himself, i.e.~to found certain basic principles of morality in reason alone.}›
text‹\noindent{The argument for the PGC  employs what Gewirth calls "the dialectically necessary method" within the "internal viewpoint" (perspective) of an agent.
Although the drawn inferences are relative to the reasoning agent, Gewirth further argues that
"the dialectically necessary method propounds the contents of this relativity
as necessary ones, since the statements it presents reflect judgements all agents necessarily make on the basis of what is necessarily
involved in their actions ... The statements the method attributes to the agent are set forth as necessary ones in that they reflect what is conceptually
necessary to being an agent who voluntarily or freely acts for purposes he wants to attain." (cite‹"GewirthRM"›).
In other words, the "dialectical necessity" of the assertions and inferences made in the argument comes from the definitional features (conceptual analysis)
of the involved notions of agency, purposeful action, obligation, rights, etc. Hence the alternative notions of logical (i.e.~indexical) validity
and 'a priori necessity', developed in Kaplan's logical framework LD, have been considered by us as appropriate to model this kind of "dialectical necessity".}›

subsection ‹Conceptual Explications›

type_synonym p = "e⇒m" ― ‹ Type for properties (function from individuals to sentence meanings) ›

subsubsection ‹Agency›

text‹\noindent{The type chosen to represent what Gewirth calls "purposes" is not essential for the argument's validity.
We choose to give "purposes" the same type as sentence meanings (type 'm'), so "acting on a purpose" would be
represented in an analogous way to having a certain propositional attitude (e.g. "desiring that some proposition obtains"). }›
consts ActsOnPurpose:: "e⇒m⇒m" ― ‹  ActsOnPurpose(A,E) gives the meaning of the sentence "A is acting on purpose E" ›
consts NeedsForPurpose:: "e⇒p⇒m⇒m" ― ‹  NeedsForPurpose(A,P,E) gives the meaning of "A needs to have property P in order to reach purpose E" ›

text‹\noindent{In Gewirth's argument, an individual with agency (i.e.~capable of purposive action) is said to be a PPA (prospective purposive agent).}›
definition PPA:: "p" where "PPA a ≡ ∃E. ActsOnPurpose a E" ― ‹  Definition of PPA ›

text‹\noindent{We have added the following axiom in order to guarantee the argument's logical correctness. It basically says that being
a PPA is identity-constitutive for an individual (i.e.~it's an essential property).}›
axiomatization where essentialPPA: "⌊∀a. PPA a → □D(PPA a)⌋D" ― ‹ being a PPA is an essential property ›

text‹\noindent{Quite interestingly, the axiom above entails, as a corollary, a kind of ability for a PPA to recognise other PPAs.
For instance, if some individual holds itself as a PPA (i.e.~seen from its own perspective/context 'd') then this individual
(Agent(d)) is considered as a PPA from any other agent's perspective/context 'c'.}›
lemma recognizeOtherPPA: "∀c d. ⌊PPA (Agent d)⌋⇩d ⟶ ⌊PPA (Agent d)⌋⇩c" using essentialPPA by blast


subsubsection ‹Goodness›

text‹\noindent{Gewirth's concept of (subjective) goodness, as employed in his argument, applies to purposes and is relative to some agent.
It is therefore modelled as a binary relation relating an individual (type 'e') with a purpose (type 'm').
Other readings given by Gewirth's for the expression "P is good for A" include among others: "A attaches a positive value to P",
"A values P proactively" and "A is motivated to achieve P".}›
consts Good::"e⇒m⇒m"

text‹\noindent{The following axioms interrelate the concept of goodness with the concept of agency, thus providing
the above concepts with some meaning (by framing their inferential roles). Notice that such meaning-constitutive
axioms (which we call "explications") are given as indexically valid (i.e.~a priori) sentences.}›
axiomatization where explicationGoodness1: "⌊∀a P. ActsOnPurpose a P → Good a P⌋D"
axiomatization where explicationGoodness2: "⌊∀P M a. Good a P ∧ NeedsForPurpose a M P → Good a (M a)⌋D"
axiomatization where explicationGoodness3: "⌊∀φ a. ◇pφ → O⟨φ | □DGood a φ⟩⌋D"

text‹\noindent{Below we show that all axioms defined so far are consistent:}›
lemma True nitpick[satisfy, card c = 1, card e = 1, card w = 1] oops ― ‹ one-world model found (card w=1) ›


text‹\noindent{The first two assertions above have been explicitly provided by Gewirth as premises of his argument.
The third axiom, however, has been added by us as an implicit premise in order to render Gewirth's proof as correct.
This axiom aims at representing the intuitive notion of "seeking the good". In particular, it asserts
that, from the point of view of an agent, necessarily good purposes are not only action motivating,
but also entail an instrumental obligation to their realisation. The notion of necessity here involved 
is not the usual alethic one (which is represented in DDL with the modal box operators ‹□a› and ‹□p›), but the linguistic one
introduced above (‹□D›) derived from indexical validity, signaling that an agent holds some
purpose as being true almost 'by definition' (i.e.~a priori).
This sets quite high standards for the kind of purposes an agent would ever take to be (instrumentally) obligatory and is 
indeed the weakest implicit premise we could come up with so far (taking away the ‹□D› 'a priori necessity' operator
would indeed make this premise much stronger and our proof less credible).}›

subsubsection ‹Freedom and Well-Being›

text‹\noindent{According to Gewirth, enjoying freedom and well-being (which we take together as a predicate: FWB) is the property 
which represents the "necessary conditions" or "generic features" of agency (i.e.~being capable of purposeful action).
Gewirth argues, the property of enjoying freedom and well-being (FWB) is special amongst other action-enabling properties,
in that it is always required in order to act on any purpose (no matter which one).}›

consts FWB::"p" ― ‹ Enjoying freedom and well-being (FWB) is a property (i.e.~has type @{text "e⇒m"}) ›

axiomatization where
explicationFWB1: "⌊∀P a. NeedsForPurpose a FWB P⌋D"

text‹\noindent{We use model finder \emph{nitpick} to verify that all axioms defined so far are consistent.
\emph{Nitpick} can indeed find a 'small' model with cardinality one for the sets of worlds and contexts.}›
lemma True nitpick[satisfy, card c = 1, card e = 1, card w = 1] oops ― ‹ one-world model found  ›

text‹\noindent{At some point in Gewirth's argument we have to show that there exists an (instrumental) obligation to enjoying freedom and well-being (FWB).
Since, according to the so-called "Kant's law" (which is a corollary of DDL), impossible or necessary things cannot be obligatory,
we can reasonably demand that
FWB be (metaphysically) possible for every agent. As before, we take this demand to be an a priori
characteristic of the concept of FWB and therefore axiomatise it as an indexically valid sentence.}›
axiomatization where explicationFWB2: "⌊∀a. ◇p FWB a⌋D"  
axiomatization where explicationFWB3: "⌊∀a. ◇p ¬FWB a⌋D"  

text‹\noindent{As a result of enforcing the contingency of FWB, the models found by \emph{nitpick} now have a cardinality
of two for the set of worlds:}›
lemma True nitpick[satisfy, card c = 1, card e = 1, card w = 1, expect=none] oops ― ‹ no model found for one-world models ›
lemma True nitpick[satisfy, card c = 1, card e = 1, card w = 2] oops ― ‹ models need now at least two worlds ›

subsubsection ‹Obligation and Interference›

text‹\noindent{ Kant's Law ("ought implies can") is derivable directly from DDL: If ‹φ› oughts to obtain then ‹φ› is possible.
Note that we will use for the formalisation of Gewirth's argument the DDL ideal obligation operator (‹Oi›) but
we could have also used (mutatis mutandis) the DDL actual obligation operator (‹Oa›).}›
lemma "⌊Oiφ → ◇pφ⌋" using sem_5ab by simp


text‹\noindent{Furthermore, we have seen the need to postulate the following (implicit) premise in order to validate the argument.
This axiom can be seen as a variation of the so-called Kant's law ("ought implies can"), i.e.~an impossible act cannot be obligatory.
In the same vein, our variation can be read as "ought implies ought to can" and is closer to Gewirth's own description:
that having an obligation to do X implies that "I ought (in the same sense and the same criterion) to be free to do X,
that I ought not to be prevented from doing X, that my capacity to do X ought not to be interfered with." (cite‹"GewirthRM"› p. 91-95)}›
axiomatization where OIOAC: "⌊Oiφ → Oi(◇aφ)⌋D"

text‹\noindent{Concerning the concept of interference, we state that the existence of an individual (successfully) interfering
with some state of affairs S implies that S cannot possibly obtain in any of the actually possible situations (and the other way round).
Note that for this definition we have employed a possibility operator (‹◇a›) which is weaker than metaphysical
possibility (‹◇p›) (see Carmo and Jones DDL framework cite‹"CJDDL"› for details).
Also note that we have also employed the (stronger) classical notion of modal
validity instead of indexical validity. (So far we haven't been able to get theorem provers and model finders to prove/disprove
Gewirth's proof if formalizing this axiom as simply indexically valid.)}›

consts InterferesWith::"e⇒m⇒m" ― ‹ an individual can interfere with some state of affairs (from obtaining) ›
axiomatization where explicationInterference: "⌊(∃b. InterferesWith b φ) ↔ ¬◇aφ⌋"

text‹\noindent{From the previous axiom we can prove following corollaries: If someone (successfully) interferes with agent 'a' having FWB,
then 'a' can no longer possibly enjoy its FWB (and the other way round).}›
lemma "⌊∀a. (∃b. InterferesWith b (FWB a)) ↔ ¬◇a(FWB a)⌋" using explicationInterference by blast
lemma InterferenceWithFWB: "⌊∀a.  ◇a(FWB a) ↔ (∀b. ¬InterferesWith b (FWB a))⌋" using explicationInterference by blast

subsubsection ‹Rights and Other-Directed Obligations›
 
text‹\noindent{Gewirth points out the existence of a correlation between an agent's own claim rights and other-referring obligations (see e.g. cite‹"GewirthRM"›, p. 66).
A claim right is a right which entails duties or obligations on other agents regarding the right-holder
(so-called Hohfeldian claim rights in legal theory).
We model this concept of claim rights in such a way that an individual 'a' has a (claim) right to some property 'P' if and only if
it is obligatory that every
(other) individual 'b' does not interfere with the state of affairs 'P(a)' from obtaining.
Since there is no particular individual to whom this directive is addressed, this obligation has been referred to by Gewirth as being "other-directed"
(aka. "other-referring") in contrast to "other-directing" obligations which entail a moral obligation for some particular subject (cite‹"Beyleveld"› p. 41,51).
This latter distinction is essential to Gewirth's argument.}›
definition RightTo::"e⇒(e⇒m)⇒m" where "RightTo a φ ≡ Oi(∀b. ¬InterferesWith b (φ a))"

text‹\noindent{Now that all needed axioms and definitions are in place, we use model finder \emph{nitpick} to show that
they are consistent:}›
lemma True nitpick[satisfy, card c = 1, card e = 1, card w = 2] oops ― ‹ models with at least two worlds found ›

subsection ‹Formal Proof of Gewirth's Argument for the PGC›

text‹\noindent{Following Beyleveld's summary (cite‹"Beyleveld"›, ch. 2), the main steps of the argument are (with original numbering): }›
text‹\noindent{(1) I act voluntarily for some (freely chosen) purpose E (equivalent --by definition-- to: I am a PPA).}›
text‹\noindent{(2) E is (subjectively) good (i.e.~I value E proactively).}›
text‹\noindent{(3) My freedom and well-being (FWB) are generically necessary conditions of my agency (i.e.~I need them to achieve any purpose whatsoever).}›
text‹\noindent{(4) My FWB are necessary goods (at least for me).}›
text‹\noindent{(5) I (even if no one else) have a claim right to my FWB.}›
text‹\noindent{(13) Every PPA has a claim right to their FWB.}›

subsubsection ‹Weak Variant›
text‹\noindent{In the following we present a formalised proof for a weak variant of the Principle of Generic Consistency (PGC),
which asserts that the following sentence is valid from every PPA's standpoint:
"I (as a PPA) have a claim right to my freedom and well-being".}›
theorem PGC_weak: shows "∀C. ⌊PPA (Agent C) → (RightTo (Agent C) FWB)⌋⇩C"
proof - {
  fix C::c ― ‹ 'C' is some arbitrarily chosen context (agent's perspective) ›
  let ?I = "(Agent C)" ― ‹ 'I' is/am the agent with perspective 'C' ›
  {
    fix E::m ― ‹ 'E' is some arbitrarily chosen purpose ›
    {
      assume P1: "⌊ActsOnPurpose ?I E⌋⇩C" ― ‹ (1) I act voluntarily on purpose E ›
      from P1 have P1a: "⌊PPA ?I⌋⇩C" using PPA_def by auto ― ‹ (1a) I am a PPA ›
      from P1 have C2: "⌊Good ?I E⌋⇩C" using explicationGoodness1 essentialPPA by meson ― ‹ (2) purpose E is good for me ›
      from explicationFWB1 have C3: "⌊∀P. NeedsForPurpose ?I FWB P⌋D" by simp ― ‹ (3) I need FWB for any purpose whatsoever ›
      hence "∃P.⌊Good ?I P ∧ NeedsForPurpose ?I FWB P⌋D" using explicationFWB2 explicationGoodness3 sem_5ab by blast
      hence "⌊Good ?I (FWB ?I)⌋D" using explicationGoodness2 by blast ― ‹ FWB is (a priori) good for me (in a kind of definitional sense) ›
      hence C4: "⌊□D(Good ?I (FWB ?I))⌋⇩C" by simp ― ‹ (4) FWB is an (a priori) necessary good for me › 
      have "⌊O⟨FWB ?I | □D(Good ?I) (FWB ?I)⟩⌋⇩C" using explicationGoodness3 explicationFWB2 by blast ― ‹ I ought to pursue my FWB on the condition that I consider it to be a necessary good ›
      hence "⌊Oi(FWB ?I)⌋⇩C" using explicationFWB2 explicationFWB3 C4 CJ_14p by fastforce ― ‹ There is an (other-directed) obligation to my FWB ›
      hence "⌊Oi(◇a(FWB ?I))⌋⇩C" using OIOAC by simp ― ‹ It must therefore be the case that my FWB is possible ›
      hence "⌊Oi(∀a. ¬InterferesWith a (FWB ?I))⌋⇩C" using InterferenceWithFWB by simp ― ‹ There is an obligation for others not to interfere with my FWB  ›
      hence C5: "⌊RightTo ?I FWB⌋⇩C" using RightTo_def by simp ― ‹ (5) I have a claim right to my freedom and well-being ›
    }
    hence "⌊ActsOnPurpose ?I E → RightTo ?I FWB⌋⇩C" by (rule impI) ― ‹ I have a claim right to my freedom and well-being (since I act on some purpose E) ›
  }
  hence "⌊∀P. ActsOnPurpose ?I P → RightTo ?I FWB⌋⇩C" by (rule allI) ― ‹  "allI" is a logical generalisation rule: "all-quantifier introduction" ›
  hence "⌊PPA ?I → RightTo ?I FWB⌋⇩C" using PPA_def by simp ― ‹ (seen from my perspective C) I have a claim right to my freedom and well-being since I am a PPA ›
  hence "⌊PPA (Agent C) → RightTo (Agent C) FWB⌋⇩C" by simp ― ‹ (seen from the perspective C) C's agent has a claim right to its freedom and well-being since it is a PPA ›
}
  thus C13: "∀C. ⌊PPA (Agent C) → (RightTo (Agent C) FWB)⌋⇩C" by (rule allI) ― ‹ (13) For every perspective C: C's agent has a claim right to its freedom and well-being ›
qed

text‹\noindent{Regarding the last inference step, given that the context (agent's perspective) 'C' has been arbitrarily fixed at the beginning, we can use again the "all-quantifier introduction" rule
to generalise the previous assertion to all possible contexts 'C' (and agents 'Agent(C)').
Note that the generalisation from "I" to all individuals has been done on purely logical grounds and does not involve any kind of universal moral principle.
This is a main requirement Gewirth has set for his argument.}›

subsubsection ‹Strong Variant›
text‹\noindent{This is a proof for a stronger variant of the PGC, which asserts that the following
sentence is valid from every PPA's standpoint: "Every PPA has a claim right to its freedom and well-being (FWB)".}›

theorem PGC_strong: shows "⌊∀x. PPA x → (RightTo x FWB)⌋D"
proof - {
fix C::c  ― ‹ 'C' is some arbitrarily chosen context (agent's perspective) ›
{
  fix I::"e"  ― ‹ 'I' is some arbitrarily chosen individual (agent's perspective) › 
  {
    fix E::m  ― ‹ 'E' is some arbitrarily chosen purpose ›
    {     
     assume P1: "⌊ActsOnPurpose I E⌋⇩C" ― ‹ (1) I act voluntarily on purpose E ›     
     from P1 have P1a: "⌊PPA I⌋⇩C" using PPA_def by auto  ― ‹ (1a) I am a PPA ›     
     from P1 have C2: "⌊Good I E⌋⇩C" using explicationGoodness1 essentialPPA by meson  ― ‹ (2) purpose E is good for me ›
     from explicationFWB1 have C3: "⌊∀P. NeedsForPurpose I FWB P⌋D" by simp  ― ‹ (3) I need FWB for any purpose whatsoever ›
     hence "∃P.⌊Good I P ∧ NeedsForPurpose I FWB P⌋D" using explicationFWB2 explicationGoodness3 sem_5ab by blast     
     hence "⌊Good I (FWB I)⌋D" using explicationGoodness2 by blast  ― ‹ FWB is (a priori) good for me (in a kind of definitional sense) ›   
     hence C4: "⌊□D(Good I (FWB I))⌋⇩C" by simp  ― ‹ (4) FWB is an (a priori) necessary good for me›  
     have "⌊O⟨FWB I | □D(Good I) (FWB I)⟩⌋⇩C" using explicationGoodness3 explicationFWB2 by blast  ― ‹ I ought to pursue my FWB on the condition that I consider it to be a necessary good›            
     hence "⌊Oi(FWB I)⌋⇩C" using explicationFWB2 explicationFWB3 C4 CJ_14p by fastforce  ― ‹ There is an (other-directed) obligation to my FWB›  
     hence "⌊Oi(◇a(FWB I))⌋⇩C" using OIOAC by simp  ― ‹ It must therefore be the case that my FWB is possible›     
     hence "⌊Oi(∀a. ¬InterferesWith a (FWB I))⌋⇩C" using InterferenceWithFWB by simp  ― ‹ There is an obligation for others not to interfere with my FWB›
     hence C5: "⌊RightTo I FWB⌋⇩C" using RightTo_def by simp  ― ‹ (5) I have a claim right to my FWB›
   }   
    hence "⌊ActsOnPurpose I E → RightTo I FWB⌋⇩C" by (rule impI)  ― ‹ I have a claim right to my FWB (since I act on some purpose E)›   
  }  
  hence "⌊∀P. ActsOnPurpose I P → RightTo I FWB⌋⇩C" by (rule allI)  
  hence "⌊PPA I → RightTo I FWB⌋⇩C" using PPA_def by simp  ― ‹ I have a claim right to my FWB since I am a PPA ›
}  
  hence "∀x. ⌊PPA x → RightTo x FWB⌋⇩C" by simp  ― ‹ Every agent has a claim right to its FWB since it is a PPA›  
}
thus C13: "∀C. ⌊∀x. PPA x → (RightTo x FWB)⌋⇩C" by (rule allI)  ― ‹ (13) For every perspective C: every agent has a claim right to its FWB›  
qed

text‹\noindent{We show that the weaker variant of the PGC presented above can be derived 
from the stronger one.}›
lemma PGC_weak2: "∀C. ⌊PPA (Agent C) → (RightTo (Agent C) FWB)⌋⇩C" using PGC_strong by simp

subsubsection ‹Some Exemplary Inferences›

text‹\noindent{In the following, we illustrate how to draw some inferences building upon Gewirth's PGC.}›

consts X::c  ― ‹ Context of use X (to which a certain speaker agent corresponds)›
consts Y::c  ― ‹ Context of use Y (to which another speaker agent corresponds)›

text‹\noindent{The agent (of context) X holds itself as a PPA.}›
axiomatization where AgentX_X_PPA: "⌊PPA (Agent X)⌋⇩X"

text‹\noindent{The agent (of another context) Y holds the agent (of context) X  as a PPA.}›
lemma AgentY_X_PPA: "⌊PPA (Agent X)⌋⇩Y" using AgentX_X_PPA recognizeOtherPPA by simp

text‹\noindent{Now the agent (of context) Y holds itself as a PPA.}›
axiomatization where AgentY_Y_PPA: "⌊PPA (Agent Y)⌋⇩Y"

text‹\noindent{The agent Y claims a right to FWB.}›
lemma AgentY_Y_FWB: "⌊RightTo (Agent Y) FWB⌋⇩Y" using AgentY_Y_PPA PGC_weak by simp

text‹\noindent{The agent Y accepts X claiming a right to FWB.}›
lemma AgentY_X_FWB: "⌊RightTo (Agent X) FWB⌋⇩Y" using AgentY_X_PPA PGC_strong by simp

text‹\noindent{The agent Y accepts an (other-directed) obligation of non-interference with X's FWB.}›
lemma AgentY_NonInterference_X_FWB: "⌊Oi(∀z. ¬InterferesWith z (FWB (Agent X)))⌋⇩Y" using AgentY_X_FWB RightTo_def by simp

text‹\noindent{Axiom consistency checked: Nitpick finds a two-world model (card w=2).}›
lemma True nitpick[satisfy, card c = 1, card e = 1, card w = 2] oops

(*<*)
end
(*>*)