module Debate.Arguments.Philosophy.Agnosticism exposing (..)

import Debate.Types exposing (..)


argumentAgnosticism : Argument
argumentAgnosticism =
    { argumentTitle = "Agnosticism Consistency Checker"
    , propositionTitle = "An interlocutor (who cannot unpack what evidence would lead them to change their doxastic attitude on a proposition) should temporarily withhold the belief that the proposition at hand is true"
    , propositionSummary = "Summary"
    , proofLink  = "https://www.umsu.de/trees/#(~6x~6y(~3Uxy~5~3Kxy)),(~6x~6y(~3Kxy~5Wxy)),(~3Uor)%7C=(Wor)"
    , definitionTable =
        [ { definiendum = "U(x,y)"
          , definiens = "(x) can unpack what evidence would lead them to change their doxastic attitude on (y)"
          }
        , { definiendum = "K(x,y)"
          , definiens = "(x) knows why they believe that (y) is true"
          }
        , { definiendum = "W(x,y)"
          , definiens = "(x) should temporarily withhold the belief that (y) is true"
          }
        , { definiendum = "o"
          , definiens = "the interlocutor"
          }
        , { definiendum = "r"
          , definiens = "the proposition at hand"
          }
        ]
    , argumentFormalization =
        [ { premises =
                [ { premise = "If one cannot unpack what evidence would lead them to change their doxastic attitude on a proposition, then one does does not know why they believe that a proposition is true."
                  , notation = "(∀x∀y(¬Uxy→¬Kxy))"
                  }
                , { premise = "If one does not know why they believe that a proposition is true, then one should temporarily withhold the belief that a proposition is true."
                  , notation = "(∀x∀y(¬Kxy→Wxy))"
                  }
                , { premise = "The interlocutor cannot unpack what evidence would lead them to change their doxastic attitude on the proposition at hand."
                  , notation = "(¬Uor)"
                  }
                ]
          , conclusion = "Therefore, the interlocutor should temporarily withhold the belief that the proposition at hand is true."
          , conclusionNotation = "(∴Wor)"
          }
        ]
    }