examples/tutorial/Tutorial.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Tutorial \n",
    "\n",
    "## Imports\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {
    "execution": {
     "iopub.execute_input": "2021-01-15T08:36:43.035193Z",
     "iopub.status.busy": "2021-01-15T08:36:43.028122Z",
     "iopub.status.idle": "2021-01-15T08:36:43.191585Z",
     "shell.execute_reply": "2021-01-15T08:36:43.192323Z"
    }
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "1.0\n"
     ]
    }
   ],
   "source": [
    "from exh import *\n",
    "from exh.utils import jprint # for fancy displays in Jupyter Notebook\n",
    "import exh # This import is just to access the version\n",
    "print(exh.__version__)\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Create formulas\n",
    " \n",
    "Formulas are created from propositions (0-ary predictates) and predicates.\n",
    "Both of these are created by class ``Pred``.\n",
    "Predicates have names, which govern how they are displayed.\n",
    "Predicates have indices : two predicates with the same index always have the same truth-value and two predicates with different indices are logically independent. Here is a code to create a predicate with index 4.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {
    "execution": {
     "iopub.execute_input": "2021-01-15T08:36:43.201870Z",
     "iopub.status.busy": "2021-01-15T08:36:43.200232Z",
     "iopub.status.idle": "2021-01-15T08:36:43.203082Z",
     "shell.execute_reply": "2021-01-15T08:36:43.203603Z"
    }
   },
   "outputs": [],
   "source": [
    "d  = Pred(index = 4, name = \"d\") \n",
    "# both \"name\" and \"index\" are optional, \"name\" makes prettier display with print and helps for evaluation of formulas\n",
    "d1 = Pred(index = 7) \n",
    "d2 = Pred(name  = \"d2\") \n",
    "\n",
    "\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "By default, *exh.formula* creates 3 propositions a,b and c with indices 0, 1, 2 respectively. Once some propositions are defined, one can create complex formulas with & (and), | (or) and \\\\~ (not).\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {
    "execution": {
     "iopub.execute_input": "2021-01-15T08:36:43.221546Z",
     "iopub.status.busy": "2021-01-15T08:36:43.220261Z",
     "iopub.status.idle": "2021-01-15T08:36:43.228408Z",
     "shell.execute_reply": "2021-01-15T08:36:43.228917Z"
    }
   },
   "outputs": [
    {
     "data": {
      "text/html": [
       "$a \\lor b$"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "$a \\land b$"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "$a \\lor (\\neg[a] \\land b)$"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "# f1: a or b\n",
    "f1 = a | b\n",
    "jprint(f1)\n",
    "\n",
    "# f2: a and b\n",
    "f2 = a & b\n",
    "jprint(f2)\n",
    "\n",
    "# f3: a or (not a and b)\n",
    "f3 = a | (~a & b)\n",
    "jprint(f3)\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "To turn a proposition into a n-ary predicate (for use in quantified formulas), one needs to specify the number of variables it depends on. Optionally, one may indicate which variable or variables the predicate depends on by default. That way, we don't need to specify the dependencies in formulas\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {
    "execution": {
     "iopub.execute_input": "2021-01-15T08:36:43.232839Z",
     "iopub.status.busy": "2021-01-15T08:36:43.232315Z",
     "iopub.status.idle": "2021-01-15T08:36:43.234261Z",
     "shell.execute_reply": "2021-01-15T08:36:43.234785Z"
    }
   },
   "outputs": [],
   "source": [
    "d.depends(1) # Making a unary predicate\n",
    "\n",
    "# Alternatively, making a unary predicate with a default variable name\n",
    "d.depends(\"x\")\n",
    "# For predicates with more than one variable we would write:\n",
    "# d.depends(\"x\", \"y\") # Default named variables\n",
    "# d.depends(2)        # Anonymous variables\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Once this is done, one can use the following syntax to create a universal statement.  A(\"x\") creates a quantifier over \"x\", which combines with \">\" and a formula to form a quantified formula.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {
    "execution": {
     "iopub.execute_input": "2021-01-15T08:36:43.239102Z",
     "iopub.status.busy": "2021-01-15T08:36:43.238548Z",
     "iopub.status.idle": "2021-01-15T08:36:43.241480Z",
     "shell.execute_reply": "2021-01-15T08:36:43.241980Z"
    }
   },
   "outputs": [
    {
     "data": {
      "text/html": [
       "$\\forall x, d(x)$"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "# f4: for all x, d(x)\n",
    "f4 = A(\"x\") > d(\"x\")\n",
    "jprint(f4)\n",
    "# We don't have to mark explicitly the varaibles that d depends on, if \"d\" has default name for its variable\n",
    "f4 = A(\"x\") > d\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Two simplifying tips:\n",
    " - Existential and universal quantifiers over x, y, z are created by default under the names Ax, Ey, etc.\n",
    " - If v is propositional variable, v(\"x\") returns v and sets v to depend on x\n",
    "\n",
    "Most straigthforwardly, one can create a quantified formula as follows:\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {
    "execution": {
     "iopub.execute_input": "2021-01-15T08:36:43.251143Z",
     "iopub.status.busy": "2021-01-15T08:36:43.249585Z",
     "iopub.status.idle": "2021-01-15T08:36:43.255483Z",
     "shell.execute_reply": "2021-01-15T08:36:43.256168Z"
    }
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "WARNING: More variables were provided than the predicate None depends on ; changing the arity of the predicate to 1. Universe objects will need to be recreated.\n"
     ]
    },
    {
     "data": {
      "text/html": [
       "$\\exists y, A7(y)$"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "# f5: there exists y, d(y)\n",
    "f5 = Ey > d1(\"y\") # a warning is displayed, because we hadn't specified that \"d1\" was a predicate\n",
    "jprint(f5) # displays as A7 because we haven't given d1 a name\n",
    "\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Evaluate formulas\n",
    "The simplest way to evaluate a formula uses the method *evaluate* and the predicates' names.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {
    "execution": {
     "iopub.execute_input": "2021-01-15T08:36:43.265437Z",
     "iopub.status.busy": "2021-01-15T08:36:43.263654Z",
     "iopub.status.idle": "2021-01-15T08:36:43.271117Z",
     "shell.execute_reply": "2021-01-15T08:36:43.270359Z"
    }
   },
   "outputs": [
    {
     "data": {
      "text/html": [
       "'$a \\lor b$' is True"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "# Evaluate f1 with a True and b True.\n",
    "value = f1.evaluate(a = True, b = False)\n",
    "jprint(\"'{}' is {}\".format(f1, value))\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "In quantified formulas, one needs to provide as many values for a predicate as there are individuals in the domain. The number of individuals in the domain is set in the module *exh.model.options* and defaults to 3. The three values are provided as a list.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {
    "execution": {
     "iopub.execute_input": "2021-01-15T08:36:43.278352Z",
     "iopub.status.busy": "2021-01-15T08:36:43.277754Z",
     "iopub.status.idle": "2021-01-15T08:36:43.285945Z",
     "shell.execute_reply": "2021-01-15T08:36:43.286596Z"
    }
   },
   "outputs": [
    {
     "data": {
      "text/html": [
       "$\\forall x, d(x)$  is  True"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "# Evaluate f4 with d(0) True, d(1) True and d(2) True\n",
    "value = f4.evaluate(d = [True, True, True])\n",
    "jprint(f4, \" is \", value)\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "One may sometimes want to evaluate a formula against all possible assignments of truth-values. To do so, one constructs a *Universe* object.\n",
    "This object constructs all possible assignments of truth-values to propositions and predicates within a given set of formulas, passed as an argument to the universe constructor.\n",
    " The *truth_table* method displays the evaluated formula in a fancy chart.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {
    "execution": {
     "iopub.execute_input": "2021-01-15T08:36:43.295955Z",
     "iopub.status.busy": "2021-01-15T08:36:43.294128Z",
     "iopub.status.idle": "2021-01-15T08:36:43.300906Z",
     "shell.execute_reply": "2021-01-15T08:36:43.300370Z"
    }
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[[False False False]\n",
      " [ True False  True]\n",
      " [ True False  True]\n",
      " [ True  True  True]\n",
      " [False False False]\n",
      " [ True False  True]\n",
      " [ True False  True]\n",
      " [ True  True  True]]\n"
     ]
    },
    {
     "data": {
      "text/html": [
       "<table style = \"\n",
       "\tborder: 1px solid black; \n",
       "    border-collapse: collapse;\n",
       "    font-weight: normal; \n",
       "\t\"><thead><tr><th style =\"\">a</th><th style =\"\">b</th><th style =\"border-right-style: double !important;\">c</th><th style =\"border-left-style: double !important;\">$a \\lor b$</th><th style =\"\">$a \\land b$</th><th style =\"\">$a \\lor (\\neg[a] \\land b)$</th></tr></thead><tr><th style =\"\">False</th><th style =\"\">False</th><th style =\"border-right-style: double !important;\">False</th><th style =\"border-left-style: double !important;\">False</th><th style =\"\">False</th><th style =\"\">False</th></tr><tr><th style =\"\">True</th><th style =\"\">False</th><th style =\"border-right-style: double !important;\">False</th><th style =\"border-left-style: double !important;\">True</th><th style =\"\">False</th><th style =\"\">True</th></tr><tr><th style =\"\">False</th><th style =\"\">True</th><th style =\"border-right-style: double !important;\">False</th><th style =\"border-left-style: double !important;\">True</th><th style =\"\">False</th><th style =\"\">True</th></tr><tr><th style =\"\">True</th><th style =\"\">True</th><th style =\"border-right-style: double !important;\">False</th><th style =\"border-left-style: double !important;\">True</th><th style =\"\">True</th><th style =\"\">True</th></tr><tr><th style =\"\">False</th><th style =\"\">False</th><th style =\"border-right-style: double !important;\">True</th><th style =\"border-left-style: double !important;\">False</th><th style =\"\">False</th><th style =\"\">False</th></tr><tr><th style =\"\">True</th><th style =\"\">False</th><th style =\"border-right-style: double !important;\">True</th><th style =\"border-left-style: double !important;\">True</th><th style =\"\">False</th><th style =\"\">True</th></tr><tr><th style =\"\">False</th><th style =\"\">True</th><th style =\"border-right-style: double !important;\">True</th><th style =\"border-left-style: double !important;\">True</th><th style =\"\">False</th><th style =\"\">True</th></tr><tr><th style =\"\">True</th><th style =\"\">True</th><th style =\"border-right-style: double !important;\">True</th><th style =\"border-left-style: double !important;\">True</th><th style =\"\">True</th><th style =\"\">True</th></tr></table>"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "# A Universe can be created from formulas ; \n",
    "# the constructor extracts all the independent predicates and propositions and creates all possible logical possibilities\n",
    "prop_universe = Universe(fs = [a, b, c])\n",
    "\n",
    "print(prop_universe.evaluate(f1, f2, f3))\n",
    "prop_universe.truth_table(f1, f2, f3)\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Universes come with methods to check standard logical relations: entailment, equivalence and consistency\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {
    "execution": {
     "iopub.execute_input": "2021-01-15T08:36:43.308096Z",
     "iopub.status.busy": "2021-01-15T08:36:43.307542Z",
     "iopub.status.idle": "2021-01-15T08:36:43.310737Z",
     "shell.execute_reply": "2021-01-15T08:36:43.311617Z"
    }
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "False\n",
      "True\n",
      "True\n"
     ]
    }
   ],
   "source": [
    "# The first three propositions entail that \"not a\" and \"b\", contradicting the fourth. \n",
    "value = prop_universe.consistent(a | b,\n",
    "                                 ~a | ~b,\n",
    "                                 b | ~a,\n",
    "                                 a | ~b)\n",
    "print(value)\n",
    "\n",
    "value = prop_universe.entails(a | ~ b & c,\n",
    "                              ~(b & ~a) )\n",
    "# NB: \"a | b & c\"  is parsed as \"a | (b & c)\"\n",
    "\n",
    "print(value)\n",
    "\n",
    "# De Morgan's law\n",
    "value = prop_universe.equivalent(~a | ~c,\n",
    "                                ~(a & c) )\n",
    "print(value)\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Exhaustification\n",
    "\n",
    "Exhaustification can be computed against a set of stipulated alternatives.\n",
    "\n",
    "**NB:** Innocent exclusion is computed upon creation of the object, slowdowns will happen at this stage if the number of worlds is large.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {
    "execution": {
     "iopub.execute_input": "2021-01-15T08:36:43.323734Z",
     "iopub.status.busy": "2021-01-15T08:36:43.322766Z",
     "iopub.status.idle": "2021-01-15T08:36:43.325280Z",
     "shell.execute_reply": "2021-01-15T08:36:43.325954Z"
    }
   },
   "outputs": [],
   "source": [
    "e  = Exh(Ex > d, alts = [Ax > d])      # Number of worlds: 2^3 = 8 \n",
    "e1 = Exh(a | b, alts = [a, b, a & b]) # Number of worlds: 2^2 = 2\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "To see the results of the computations, you can use a couple of methods:\n",
    "    1. the method ``diagnose()`` from the Exhaust object lists the innocently excludable alternatives (along with the maximal sets).\n",
    "    2. alternatively, the method ``unpack()`` creates an equivalent formula in the form \"prejacent and not alternative and not alternative' ...\"\n",
    "    3. like any formula, we can evaluate *e* and check that it behaves like \"some but not all\", our predicted meaning.\n",
    "\n",
    "**Caveat:** Neither the formula given by ``unpack()`` or the sets of alternatives in ``diagnose()`` are not simplified.\n",
    "Sometimes, multiple logically equivalent alternatives will be displayed. On complex examples, comparing the result obtained to a predicted result may be more helpful (i.e. method 3 above).\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {
    "execution": {
     "iopub.execute_input": "2021-01-15T08:36:43.337284Z",
     "iopub.status.busy": "2021-01-15T08:36:43.336083Z",
     "iopub.status.idle": "2021-01-15T08:36:43.361132Z",
     "shell.execute_reply": "2021-01-15T08:36:43.360602Z"
    }
   },
   "outputs": [
    {
     "data": {
      "text/html": [
       "Maximal Sets (excl):"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "{$\\forall x, d(x)$}"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "Innocently excludable:  $\\forall x, d(x)$"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "Maximal Sets (excl):"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "{$b$; $a \\land b$}"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "{$a$; $a \\land b$}"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "Innocently excludable:  $a \\land b$"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "$(\\exists x, d(x)) \\land \\land[\\neg[\\forall x, d(x)]]$"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "$(a \\lor b) \\land \\land[\\neg[a \\land b]]$"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\n"
     ]
    },
    {
     "data": {
      "text/html": [
       "<table style = \"\n",
       "\tborder: 1px solid black; \n",
       "    border-collapse: collapse;\n",
       "    font-weight: normal; \n",
       "\t\"><thead><tr><th style =\"\">d(0)</th><th style =\"\">d(1)</th><th style =\"border-right-style: double !important;\">d(2)</th><th style =\"border-left-style: double !important;\">$\\textbf{Exh}[\\exists x, d(x)]$</th><th style =\"\">$(\\exists x, d(x)) \\land \\neg[\\forall x, d(x)]$</th></tr></thead><tr><th style =\"\">False</th><th style =\"\">False</th><th style =\"border-right-style: double !important;\">False</th><th style =\"border-left-style: double !important;\">False</th><th style =\"\">False</th></tr><tr><th style =\"\">True</th><th style =\"\">False</th><th style =\"border-right-style: double !important;\">False</th><th style =\"border-left-style: double !important;\">True</th><th style =\"\">True</th></tr><tr><th style =\"\">False</th><th style =\"\">True</th><th style =\"border-right-style: double !important;\">False</th><th style =\"border-left-style: double !important;\">True</th><th style =\"\">True</th></tr><tr><th style =\"\">True</th><th style =\"\">True</th><th style =\"border-right-style: double !important;\">False</th><th style =\"border-left-style: double !important;\">True</th><th style =\"\">True</th></tr><tr><th style =\"\">False</th><th style =\"\">False</th><th style =\"border-right-style: double !important;\">True</th><th style =\"border-left-style: double !important;\">True</th><th style =\"\">True</th></tr><tr><th style =\"\">True</th><th style =\"\">False</th><th style =\"border-right-style: double !important;\">True</th><th style =\"border-left-style: double !important;\">True</th><th style =\"\">True</th></tr><tr><th style =\"\">False</th><th style =\"\">True</th><th style =\"border-right-style: double !important;\">True</th><th style =\"border-left-style: double !important;\">True</th><th style =\"\">True</th></tr><tr><th style =\"\">True</th><th style =\"\">True</th><th style =\"border-right-style: double !important;\">True</th><th style =\"border-left-style: double !important;\">False</th><th style =\"\">False</th></tr></table>"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\n",
      "Is e equivalent to 'some but not all'?\n",
      "True\n"
     ]
    }
   ],
   "source": [
    "# Method 1\n",
    "e.diagnose()\n",
    "e1.diagnose()\n",
    "\n",
    "# Method 2\n",
    "jprint(e.unpack())\n",
    "jprint(e1.unpack())\n",
    "\n",
    "# Method 3\n",
    "quant_universe = Universe(fs = [e])\n",
    "print()\n",
    "# Display truth table of \"e\" and compare it to truth table of \"some but not all\"\n",
    "quant_universe.truth_table(e, (Ex > d) & ~(Ax > d))\n",
    "\n",
    "\n",
    "# Or more directly check for equivalence\n",
    "print()\n",
    "print(\"Is e equivalent to 'some but not all'?\")\n",
    "print(\n",
    "    quant_universe.equivalent(\n",
    "    e,\n",
    "    (Ex > d) & ~(Ax > d)\n",
    "    ))\n",
    "\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Below is a more involved example with more alternatives:\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {
    "execution": {
     "iopub.execute_input": "2021-01-15T08:36:43.371968Z",
     "iopub.status.busy": "2021-01-15T08:36:43.371110Z",
     "iopub.status.idle": "2021-01-15T08:36:43.400843Z",
     "shell.execute_reply": "2021-01-15T08:36:43.401348Z"
    }
   },
   "outputs": [
    {
     "data": {
      "text/html": [
       "Maximal Sets (excl):"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "{$\\forall x, p1(x) \\land p2(x)$; $\\forall x, p2(x)$; $\\exists x, p1(x) \\land p2(x)$; $\\exists x, p2(x)$}"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "{$\\forall x, p1(x) \\land p2(x)$; $\\forall x, p1(x)$; $\\forall x, p2(x)$; $\\exists x, p1(x) \\land p2(x)$}"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "{$\\forall x, p1(x) \\land p2(x)$; $\\forall x, p1(x)$; $\\exists x, p1(x) \\land p2(x)$; $\\exists x, p1(x)$}"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "Innocently excludable:  $\\forall x, p1(x) \\land p2(x)$; $\\exists x, p1(x) \\land p2(x)$"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "Maximal Sets (excl):"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "{$\\forall x, p1(x) \\land p2(x)$; $\\forall x, p1(x)$; $\\forall x, p2(x)$}"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "Innocently excludable:  $\\forall x, p1(x) \\land p2(x)$; $\\forall x, p1(x)$; $\\forall x, p2(x)$"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n",
      "True\n"
     ]
    }
   ],
   "source": [
    "# constructing new predicates and immediately indicating dependency in x\n",
    "p1 = Pred(name = \"p1\", depends = [\"x\"]) \n",
    "p2 = Pred(name = \"p2\", depends = [\"x\"])\n",
    "\n",
    "prejacent = Ax > p1 | p2\n",
    "\n",
    "exh = Exh(prejacent, alts = [Ax > p1 & p2,\n",
    "                             Ax > p1,\n",
    "                             Ax > p2,\n",
    "                             Ex > p1 & p2,\n",
    "                             Ex > p1,\n",
    "                             Ex > p2])\n",
    "exh.diagnose()\n",
    "# Reads like \"none of them did both p1 and p2\" ; an embedded implicature\n",
    "# What if we didn't have existential alternatives?\n",
    "\n",
    "exh2 = Exh(prejacent, alts = [Ax > p1 & p2,\n",
    "                              Ax > p1,\n",
    "                              Ax > p2])\n",
    "exh2.diagnose()\n",
    "universe = Universe(fs = [exh2])\n",
    "print(universe.entails(exh2, Ex > p1 & ~p2))\n",
    "print(universe.entails(exh2, Ex > p2 & ~p1))\n",
    "# Two implicatures: 1) that someone did only p1, 2) that someone did only p2\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Automatic alternatives\n",
    "\n",
    "When not specified, the alternatives to the prejacent are computed in a Sauerlandian manner: all alternatives are considered that can be obtained from the prejacent by sub-constituent and scalar substitutions. Which alternatives were obtained by this process can be probed after the object is constructed.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {
    "execution": {
     "iopub.execute_input": "2021-01-15T08:36:43.408767Z",
     "iopub.status.busy": "2021-01-15T08:36:43.408054Z",
     "iopub.status.idle": "2021-01-15T08:36:43.411095Z",
     "shell.execute_reply": "2021-01-15T08:36:43.411627Z"
    }
   },
   "outputs": [
    {
     "data": {
      "text/html": [
       "Computed alternatives [$a \\lor b \\lor c$, $(a \\land b) \\lor c$, $a \\lor c$, $b \\lor c$, $(a \\lor b) \\land c$, $a \\land b \\land c$, $a \\land c$, $b \\land c$, $a \\lor b$, $a \\land b$, $a$, $b$, $c$]"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "h2 = Exh (a | b | c)\n",
    "jprint(\"Computed alternatives\", h2.alts)\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "It is possible to specify the scales and to decide whether to allow substitution by sub-consituent.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {
    "execution": {
     "iopub.execute_input": "2021-01-15T08:36:43.418394Z",
     "iopub.status.busy": "2021-01-15T08:36:43.417855Z",
     "iopub.status.idle": "2021-01-15T08:36:43.424409Z",
     "shell.execute_reply": "2021-01-15T08:36:43.424932Z"
    }
   },
   "outputs": [
    {
     "data": {
      "text/html": [
       "[$a \\lor b \\lor c$, $(a \\land b) \\lor c$, $(a \\lor b) \\land c$, $a \\land b \\land c$]"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "[$\\exists x, p1(x) \\lor p2(x)$, $\\exists x, p1(x) \\land p2(x)$, $\\exists x, p1(x)$, $\\exists x, p2(x)$]"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "h3 = Exh(a | b | c, subst = False) # no replacement by sub-constituent allowed (only scalar alternatives)\n",
    "jprint(h3.alts)\n",
    "\n",
    "h4 = Exh(Ex > p1 | p2, scales = [{Or, And}]) # no \"some\", \"all\" scale\n",
    "jprint(h4.alts)\n",
    "# NB: to avoid unbound variables, the quantifier's scope is not considered a sub-consituent of the quantifier\n",
    "# NB2: The \"scales\" argument is a list of sets of types. You can find out the type of any formula by running:\n",
    "# print(formula_of_unknown_type.__class__.__name__)  \n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {
    "execution": {
     "iopub.execute_input": "2021-01-15T08:36:43.428962Z",
     "iopub.status.busy": "2021-01-15T08:36:43.428480Z",
     "iopub.status.idle": "2021-01-15T08:36:43.445212Z",
     "shell.execute_reply": "2021-01-15T08:36:43.445719Z"
    }
   },
   "outputs": [
    {
     "data": {
      "text/html": [
       "Maximal Sets (excl):"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "{$(a \\land b) \\lor c$; $(a \\lor b) \\land c$; $a \\land b \\land c$}"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "Innocently excludable:  $(a \\land b) \\lor c$; $(a \\lor b) \\land c$; $a \\land b \\land c$"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "Maximal Sets (excl):"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "{$\\exists x, p1(x) \\land p2(x)$; $\\exists x, p2(x)$}"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "{$\\exists x, p1(x) \\land p2(x)$; $\\exists x, p1(x)$}"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "Innocently excludable:  $\\exists x, p1(x) \\land p2(x)$"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "\n",
    "\n",
    "\n",
    "h3.diagnose()\n",
    "h4.diagnose()\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Advanced usage\n",
    "\n",
    "### Formulas with multiple quantifiers\n",
    "\n",
    "One can create multiply quantified sentences ; the number of worlds grows exponentially. One predicate that depends on two variables will give rise to 9 independent variables ; we get 2^9 = 512 worlds.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "metadata": {
    "execution": {
     "iopub.execute_input": "2021-01-15T08:36:43.451798Z",
     "iopub.status.busy": "2021-01-15T08:36:43.451278Z",
     "iopub.status.idle": "2021-01-15T08:36:43.463593Z",
     "shell.execute_reply": "2021-01-15T08:36:43.464101Z"
    }
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "WARNING: More variables were provided than the predicate p3 depends on ; changing the arity of the predicate to 2. Universe objects will need to be recreated.\n"
     ]
    },
    {
     "data": {
      "text/html": [
       "Maximal Sets (excl):"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "{$\\forall x, \\exists y, p3(x,y)$; $\\exists y, \\forall x, p3(x,y)$}"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "Innocently excludable:  $\\forall x, \\exists y, p3(x,y)$; $\\exists y, \\forall x, p3(x,y)$"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "p3 = Pred(13, name = \"p3\")\n",
    "prejacent = Ex > Ay > p3(\"x\", \"y\") # Number of worlds 2^(3^2) = 512 (still quite reasonable)\n",
    "\n",
    "e = Exh(prejacent, alts = [Ay > Ex > p3, Ax > Ey > p3, Ey > Ax > p3])\n",
    "e.diagnose()\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Recursive exhaustification\n",
    "\n",
    "The object *Exh* is just like any other formula. It can be embedded, yielding recursive exhaustification. Here is for instance a replication of free choice:\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "metadata": {
    "execution": {
     "iopub.execute_input": "2021-01-15T08:36:43.485339Z",
     "iopub.status.busy": "2021-01-15T08:36:43.477147Z",
     "iopub.status.idle": "2021-01-15T08:36:43.546633Z",
     "shell.execute_reply": "2021-01-15T08:36:43.547167Z"
    }
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Alternatives:\n"
     ]
    },
    {
     "data": {
      "text/html": [
       "<ul><li>$\\textbf{Exh}[\\exists x, p1(x) \\lor p2(x)]$</li><li>$\\textbf{Exh}[\\exists x, p1(x)]$</li><li>$\\textbf{Exh}[\\exists x, p2(x)]$</li></ul>"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "Maximal Sets (excl):"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "{$\\textbf{Exh}[\\exists x, p1(x)]$; $\\textbf{Exh}[\\exists x, p2(x)]$}"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "Innocently excludable:  $\\textbf{Exh}[\\exists x, p1(x)]$; $\\textbf{Exh}[\\exists x, p2(x)]$"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Am I allowed to do p1?\n",
      "True"
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\n",
      "Am I allowed to do p2?\n",
      "True\n",
      "Does the sentence say that I can do p1 without doing p2?\n",
      "False\n",
      "Is the sentence compatible with a requirement to do both p1 and p2?\n",
      "True\n"
     ]
    },
    {
     "data": {
      "text/html": [
       "<ul><li>$\\textbf{Exh}[\\exists x, p1(x) \\lor p2(x)]$</li><li>$\\textbf{Exh}[\\exists x, p1(x)]$</li><li>$\\textbf{Exh}[\\exists x, p2(x)]$</li><li>$\\textbf{Exh}[\\forall x, p1(x) \\lor p2(x)]$</li><li>$\\textbf{Exh}[\\forall x, p1(x)]$</li><li>$\\textbf{Exh}[\\forall x, p2(x)]$</li></ul>"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "Maximal Sets (excl):"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "{$\\textbf{Exh}[\\exists x, p1(x)]$; $\\textbf{Exh}[\\exists x, p2(x)]$; $\\textbf{Exh}[\\forall x, p1(x) \\lor p2(x)]$; $\\textbf{Exh}[\\forall x, p1(x)]$; $\\textbf{Exh}[\\forall x, p2(x)]$}"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "Innocently excludable:  $\\textbf{Exh}[\\exists x, p1(x)]$; $\\textbf{Exh}[\\exists x, p2(x)]$; $\\textbf{Exh}[\\forall x, p1(x) \\lor p2(x)]$; $\\textbf{Exh}[\\forall x, p1(x)]$; $\\textbf{Exh}[\\forall x, p2(x)]$"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Does the sentence say that I can do p1 without doing p2?\n",
      "False\n",
      "Is the sentence compatible with a requirement to do both p1 and p2?\n",
      "False\n"
     ]
    }
   ],
   "source": [
    "# For fancy html display\n",
    "from IPython.core.display import display, HTML\n",
    "\n",
    "prejacent = Ex > p1 | p2 # The existential quantifier can be thought of as an existential modal\n",
    "\n",
    "free_choice = Exh(Exh(prejacent, scales = []), scales = []) \n",
    "# no scalar alternatives  for the moment\n",
    "\n",
    "# Let's see what has been computed\n",
    "# First, the alternatives\n",
    "print(\"Alternatives:\")\n",
    "\n",
    "to_display = \"<ul>\"\n",
    "for alt in free_choice.alts:\n",
    "    to_display += \"<li>{}</li>\".format(alt)\n",
    "to_display += \"</ul>\"\n",
    "display(HTML(to_display))\n",
    "\n",
    "# Second, the innocently excludable alternatives\n",
    "free_choice.diagnose()\n",
    "# The result seems right ; let's check entailments\n",
    "\n",
    "fc_universe = Universe(f = free_choice) # one can use f you only have one formula\n",
    "print(\"Am I allowed to do p1?\")\n",
    "print(fc_universe.entails(free_choice, Ex > p1))\n",
    "print(\"Am I allowed to do p2?\")\n",
    "print(fc_universe.entails(free_choice, Ex > p2))\n",
    "\n",
    "# We have weak FC ; what about strong free-choice?\n",
    "print(\"Does the sentence say that I can do p1 without doing p2?\")\n",
    "print(fc_universe.entails(free_choice, Ex > p1 & ~p2)) # We don't have strong FC\n",
    "print(\"Is the sentence compatible with a requirement to do both p1 and p2?\")\n",
    "print(fc_universe.consistent(free_choice, Ax > p1 & p2))\n",
    "\n",
    "# Can we derive strong FC with universal scalar alternatives?\n",
    "someall = [{Existential, Universal}] # we only allow some/all scale, not or/and scale\n",
    "fc_2 = Exh(Exh(prejacent, scales = someall), scales = someall) \n",
    "\n",
    "to_display = \"<ul>\"\n",
    "for alt in fc_2.alts:\n",
    "    to_display += \"<li>{}</li>\".format(alt)\n",
    "to_display += \"</ul>\"\n",
    "display(HTML(to_display))\n",
    "\n",
    "fc_2.diagnose()\n",
    "\n",
    "print(\"Does the sentence say that I can do p1 without doing p2?\")\n",
    "print(fc_universe.entails(fc_2, Ex > p1 & ~p2)) # We don't have strong FC\n",
    "print(\"Is the sentence compatible with a requirement to do both p1 and p2?\")\n",
    "print(fc_universe.consistent(fc_2, Ax > p1 & p2))\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "One may wonder why by sub-constituent replacement, \"Ex, p1(x)\" is not an alternative to \"Exh(Ex, p1(x) or p2(x))\"\n",
    "If this were so, note that free choice wouldn't be derived.\n",
    "\"exh\" is set to not be removable by sub-constituent replacement (you can modify this in *options.py*)\n",
    "\n",
    "\n",
    "### Innocent inclusion\n",
    "\n",
    "*Exh* can also compute innocent inclusion. \n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "metadata": {
    "execution": {
     "iopub.execute_input": "2021-01-15T08:36:43.555034Z",
     "iopub.status.busy": "2021-01-15T08:36:43.553996Z",
     "iopub.status.idle": "2021-01-15T08:36:43.604597Z",
     "shell.execute_reply": "2021-01-15T08:36:43.605114Z"
    }
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "### DISJUNCTION ###\n"
     ]
    },
    {
     "data": {
      "text/html": [
       "Maximal Sets (excl):"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "{$b$}"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "{$a$}"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "Innocently excludable:  nothing"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "Maximal Sets (incl):"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "{$a \\lor b$; $a$; $b$}"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "Innocently includable:  $a \\lor b$; $a$; $b$"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "### FREE CHOICE ###\n"
     ]
    },
    {
     "data": {
      "text/html": [
       "Maximal Sets (excl):"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "{$\\exists x, p1(x) \\land p2(x)$; $\\exists x, p2(x)$; $\\forall x, p1(x) \\lor p2(x)$; $\\forall x, p1(x) \\land p2(x)$; $\\forall x, p1(x)$; $\\forall x, p2(x)$}"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "{$\\exists x, p1(x) \\land p2(x)$; $\\exists x, p1(x)$; $\\forall x, p1(x) \\lor p2(x)$; $\\forall x, p1(x) \\land p2(x)$; $\\forall x, p1(x)$; $\\forall x, p2(x)$}"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "Innocently excludable:  $\\exists x, p1(x) \\land p2(x)$; $\\forall x, p1(x) \\lor p2(x)$; $\\forall x, p1(x) \\land p2(x)$; $\\forall x, p1(x)$; $\\forall x, p2(x)$"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "Maximal Sets (incl):"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "{$\\exists x, p1(x) \\lor p2(x)$; $\\exists x, p1(x)$; $\\exists x, p2(x)$}"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "Innocently includable:  $\\exists x, p1(x) \\lor p2(x)$; $\\exists x, p1(x)$; $\\exists x, p2(x)$"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Allowed to do p1 not p2: True\n",
      "Allowed to do p2 not p1: True\n",
      "Allowed to do both: False\n"
     ]
    }
   ],
   "source": [
    "# Strengthening to conjunction, when scalar alternatives are absent\n",
    "print(\"### DISJUNCTION ###\")\n",
    "conj = Exh(a | b, scales = [], ii = True) # ii parameter for innocent inclusion\n",
    "conj.diagnose()\n",
    "\n",
    "print(\"### FREE CHOICE ###\")\n",
    "fc_ii = Exh(Ex > p1 | p2, ii = True) # Automatic alternatives\n",
    "fc_ii.diagnose()\n",
    "\n",
    "print(\"Allowed to do p1 not p2:\", fc_universe.entails(fc_ii, Ex > p1 & ~p2))\n",
    "print(\"Allowed to do p2 not p1:\", fc_universe.entails(fc_ii, Ex > p2 & ~p1))\n",
    "print(\"Allowed to do both:\", fc_universe.consistent(fc_ii, Ex > p2 & p1))\n",
    "\n",
    "\n",
    "\n",
    "\n",
    "\n",
    "\n"
   ]
  }
 ],
 "metadata": {
  "anaconda-cloud": {},
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.6.11"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 4
}