examples/notebooks/Type Theory - Logic V2.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Symbolize - Type Theory Logic - New Style"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {
    "ExecuteTime": {
     "end_time": "2017-08-23T19:38:17.154099Z",
     "start_time": "2017-08-23T19:38:14.537937Z"
    }
   },
   "outputs": [],
   "source": [
    "import sys\n",
    "sys.path.insert(1, \"../..\")\n",
    "from symbolize.logic.argument import Argument\n",
    "from symbolize.logic.typetheory.proposition import *\n",
    "from symbolize.logic.typetheory.proof import *\n",
    "from symbolize.logic.typetheory.variables import A, B, C, Verum, Falsum"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Conjunction ##\n",
    "### Introduction ###"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$$\\frac{p : A \\quad q : B}{p, q : A \\land B}$$"
      ],
      "text/plain": [
       "<symbolize.logic.argument.Argument at 0x245169760b8>"
      ]
     },
     "execution_count": 2,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "p = A.get_proof('p')\n",
    "q = B.get_proof('q')\n",
    "r = ProofExpressionCombination(p,q)\n",
    "Argument([p,q], r)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Elimination ###"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$$\\frac{p, q : A \\land B}{fst(p, q) : A}$$"
      ],
      "text/plain": [
       "<symbolize.logic.argument.Argument at 0x2451698a080>"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "Argument([r], fst(r))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$$\\frac{r : A \\land B}{fst(r) : A}$$"
      ],
      "text/plain": [
       "<symbolize.logic.argument.Argument at 0x2451698d9b0>"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "A_and_B = and_(A, B)\n",
    "r = A_and_B.get_proof('r')\n",
    "Argument([r], fst(r))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$$snd(r) : B$$"
      ],
      "text/plain": [
       "snd(r) : B"
      ]
     },
     "execution_count": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "snd(r)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Example - From $A \\land B$ deduce $B \\land A$ - [ST] p72 ####"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$$\\frac{\\frac{r : A \\land B}{fst(r) : A} \\quad \\frac{r : A \\land B}{snd(r) : B}}{snd(r), fst(r) : B \\land A}$$"
      ],
      "text/plain": [
       "<symbolize.logic.argument.Argument at 0x2451699c550>"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "Argument([\n",
    "    Argument([r], fst(r)),\n",
    "    Argument([r], snd(r))\n",
    "],\n",
    "    ProofExpressionCombination(\n",
    "        snd(r),\n",
    "        fst(r)\n",
    "    )\n",
    ")"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Implication ##\n",
    "### Introduction ###"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {
    "ExecuteTime": {
     "end_time": "2017-08-23T19:25:22.696304Z",
     "start_time": "2017-08-23T19:25:22.632030Z"
    }
   },
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$$\\frac{\\begin{matrix}\n",
       "            [x : A]\\\\\n",
       "            \\vdots\\\\\n",
       "            e : B\\\\\n",
       "            \\end{matrix}}{\\lambda{}(x).e : A \\Rightarrow B}(\\Rightarrow{I})$$"
      ],
      "text/plain": [
       "<symbolize.logic.argument.Argument at 0x245169a04a8>"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "x = A.get_proof('x')\n",
    "e = B.get_proof('e')\n",
    "Argument([e], e.abstract(x), discharges=[x], label=r\"\\Rightarrow{I}\")"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Elimination ###"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$$q(a) : B$$"
      ],
      "text/plain": [
       "q(a) : B"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "A_implies_B = implies(A, B)\n",
    "q = A_implies_B.get_proof('q')\n",
    "a = A.get_proof('a')\n",
    "q(a)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Disjunction ##\n",
    "### Introduction ###"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {
    "ExecuteTime": {
     "end_time": "2017-08-23T19:38:22.301103Z",
     "start_time": "2017-08-23T19:38:22.273712Z"
    }
   },
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$$inl(q, B) : A \\lor B$$"
      ],
      "text/plain": [
       "inl(q, B) : ∨(A, B)"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "q = A.get_proof('q')\n",
    "inl(q, B)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {
    "ExecuteTime": {
     "end_time": "2017-08-23T19:38:27.260731Z",
     "start_time": "2017-08-23T19:38:27.249869Z"
    }
   },
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$$inr(r, A) : A \\lor B$$"
      ],
      "text/plain": [
       "inr(r, A) : ∨(A, B)"
      ]
     },
     "execution_count": 10,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "r = B.get_proof('r')\n",
    "inr(r, A)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {
    "ExecuteTime": {
     "end_time": "2017-08-23T19:31:33.369603Z",
     "start_time": "2017-08-23T19:31:33.358440Z"
    }
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "∅"
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "B.arity"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Example - Identity - [ST] p83 ####"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$$\\frac{\\begin{matrix}\n",
       "            [x : A]\\\\\n",
       "            \\vdots\\\\\n",
       "            x : A\\\\\n",
       "            \\end{matrix}}{\\lambda{}(x).x : A \\Rightarrow A}(\\Rightarrow{I})$$"
      ],
      "text/plain": [
       "<symbolize.logic.argument.Argument at 0x245169a7128>"
      ]
     },
     "execution_count": 12,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "Argument([x], x.abstract(x), discharges=[x], label=r\"\\Rightarrow{I}\")"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Example - From $A \\Rightarrow B$ and $B \\Rightarrow C$ deduce $A \\Rightarrow C$ - [ST] p83-84 ####"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [],
   "source": [
    "A_implies_B = implies(A, B)\n",
    "B_implies_C = implies(B, C)\n",
    "a = A_implies_B.get_proof('a')\n",
    "b = B_implies_C.get_proof('b')\n",
    "x = A.get_proof('x')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$$\\frac{x : A \\quad a : A \\Rightarrow B}{a(x) : B}$$"
      ],
      "text/plain": [
       "<symbolize.logic.argument.Argument at 0x245169b2d68>"
      ]
     },
     "execution_count": 14,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "Argument([x, a], a(x))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$$\\frac{\\frac{\\frac{x : A \\quad a : A \\Rightarrow B}{a(x) : B} \\quad b : B \\Rightarrow C}{b(a(x)) : C} \\quad x : A}{\\lambda{}(a).\\lambda{}(b).\\lambda{}(x).(b(a(x))) : (A \\Rightarrow B) \\Rightarrow ((B \\Rightarrow C) \\Rightarrow (A \\Rightarrow C))}$$"
      ],
      "text/plain": [
       "<symbolize.logic.argument.Argument at 0x245169ce518>"
      ]
     },
     "execution_count": 15,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "arg1 = Argument([x, a], a(x))\n",
    "arg2 = Argument([arg1, b], b(arg1.conclusion))\n",
    "arg3 = Argument([arg2, x], arg2.conclusion.abstract(x))\n",
    "arg4 = Argument([arg2, x], arg3.conclusion.abstract(b))\n",
    "arg5 = Argument([arg2, x], arg4.conclusion.abstract(a))\n",
    "arg5"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$$(A \\Rightarrow B) \\Rightarrow ((B \\Rightarrow ⟘) \\Rightarrow (A \\Rightarrow ⟘))$$"
      ],
      "text/plain": [
       "⟹(⟹(A, B), ⟹(⟹(B, ⟘), ⟹(A, ⟘)))"
      ]
     },
     "execution_count": 16,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "arg5.conclusion.proposition_type.substitute(C, Falsum)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$$(A \\Rightarrow B) \\Rightarrow ((B \\Rightarrow ⟘) \\Rightarrow (A \\Rightarrow ⟘))$$"
      ],
      "text/plain": [
       "⟹(⟹(A, B), ⟹(⟹(B, ⟘), ⟹(A, ⟘)))"
      ]
     },
     "execution_count": 17,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "foo = arg5.conclusion.proposition_type.substitute(C, Falsum).copy()\n",
    "def my_sub(wr):\n",
    "    if type(wr.expr) is PropositionBinaryInfixExpression and wr.expr.base == implies and wr.expr.children[1] == Falsum:\n",
    "        wr.obj[wr.index] = not_(wr.expr.children[0])\n",
    "foo.walk(my_sub)\n",
    "foo"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Example - $((A \\lor B) \\Rightarrow C) \\iff ((A \\Rightarrow C) \\land (B \\Rightarrow C))$ - [ST] p86-87 ####\n",
    "##### $((A \\lor B) \\Rightarrow C) \\Rightarrow ((A \\Rightarrow C) \\land (B \\Rightarrow C))$ #####"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "metadata": {},
   "outputs": [],
   "source": [
    "A_or_B_implies_C = implies(or_(A, B), C)\n",
    "y = A_or_B_implies_C.get_proof('y')\n",
    "x = A.get_proof('x')\n",
    "w = B.get_proof('w')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$$\\frac{\\frac{\\frac{\\frac{x : A}{inl(x, B) : A \\lor B} \\quad y : (A \\lor B) \\Rightarrow C}{y(inl(x, B)) : C}}{\\lambda{}(x).(y(inl(x, B))) : A \\Rightarrow C} \\quad \\frac{\\frac{\\frac{w : B}{inr(w, A) : A \\lor B} \\quad y : (A \\lor B) \\Rightarrow C}{y(inr(w, A)) : C}}{\\lambda{}(w).(y(inr(w, A))) : B \\Rightarrow C}}{\\lambda{}(x).(y(inl(x, B))), \\lambda{}(w).(y(inr(w, A))) : (A \\Rightarrow C) \\land (B \\Rightarrow C)}$$"
      ],
      "text/plain": [
       "<symbolize.logic.argument.Argument at 0x1808abd16d8>"
      ]
     },
     "execution_count": 19,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "arg1 = Argument([x], inl(x, B))\n",
    "arg2 = Argument([arg1, y], y(arg1.conclusion))\n",
    "arg3 = Argument([arg2], arg2.conclusion.abstract(x))\n",
    "\n",
    "arg4 = Argument([w], inr(w, A))\n",
    "arg5 = Argument([arg4, y], y(arg4.conclusion))\n",
    "arg6 = Argument([arg5], arg5.conclusion.abstract(w))\n",
    "\n",
    "arg7 = Argument([arg3, arg6], ProofExpressionCombination(arg3.conclusion, arg6.conclusion))\n",
    "arg7"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$$\\lambda{}(y).\\lambda{}(x).(y(inl(x, B))), \\lambda{}(w).(y(inr(w, A))) : ((A \\lor B) \\Rightarrow C) \\Rightarrow ((A \\Rightarrow C) \\land (B \\Rightarrow C))$$"
      ],
      "text/plain": [
       "(y)(x)y(inl(x, B)), (w)y(inr(w, A)) : ⟹(⟹(∨(A, B), C), ∧(⟹(A, C), ⟹(B, C)))"
      ]
     },
     "execution_count": 20,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "arg7.conclusion.abstract(y)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "##### $((A \\lor B) \\Rightarrow C) \\Leftarrow ((A \\Rightarrow C) \\land (B \\Rightarrow C))$ #####"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "metadata": {},
   "outputs": [],
   "source": [
    "A_or_B = or_(A, B)\n",
    "A_implies_C_and_B_implies_C = and_(implies(A, C),implies(B, C))\n",
    "z = A_or_B.get_proof('z')\n",
    "p = A_implies_C_and_B_implies_C.get_proof('p')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$$p : (A \\Rightarrow C) \\land (B \\Rightarrow C)$$"
      ],
      "text/plain": [
       "p : ∧(⟹(A, C), ⟹(B, C))"
      ]
     },
     "execution_count": 22,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "p"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 23,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$$\\frac{z : A \\lor B \\quad fst~p : A \\Rightarrow C \\quad snd~p : B \\Rightarrow C}{cases(z, fst~p, snd~p) : C}$$"
      ],
      "text/plain": [
       "<symbolize.logic.argument.Argument at 0x1808ac32278>"
      ]
     },
     "execution_count": 23,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "Argument([z, p.select(0).alias(\"fst~p\"), p.select(1).alias(\"snd~p\")],\n",
    "  cases(z, p.select(0).alias(\"fst~p\"), p.select(1).alias(\"snd~p\"))       \n",
    ")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 24,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$$\\lambda{}(p).\\lambda{}(z).(cases(z, fst~p, snd~p)) : ((A \\Rightarrow C) \\land (B \\Rightarrow C)) \\Rightarrow ((A \\lor B) \\Rightarrow C)$$"
      ],
      "text/plain": [
       "(p)(z)cases(z, fst~p, snd~p) : ⟹(∧(⟹(A, C), ⟹(B, C)), ⟹(∨(A, B), C))"
      ]
     },
     "execution_count": 24,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "cases(z, p.select(0).alias(\"fst~p\"), p.select(1).alias(\"snd~p\")).abstract(z).abstract(p)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Universal Quantifier ##\n",
    "### Introduction ###"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 25,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$$\\frac{\\begin{matrix}\n",
       "            [x : A]\\\\\n",
       "            \\vdots\\\\\n",
       "            p : P\\\\\n",
       "            \\end{matrix}}{\\lambda{}(x).p : \\forall{x}.P}(\\forall{I})$$"
      ],
      "text/plain": [
       "<symbolize.logic.argument.Argument at 0x1808aaf6898>"
      ]
     },
     "execution_count": 25,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "x = A.get_proof('x')\n",
    "P = PropositionSymbol('P', assume_contains=[x])\n",
    "p = P.get_proof('p')\n",
    "Argument([p], p.abstract(x), discharges=[x], label=r\"\\forall{I}\")"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Elimination ###"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 26,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$$\\frac{a : A \\quad f : \\forall{x}.P}{f(a) : P}(\\forall{E})$$"
      ],
      "text/plain": [
       "<symbolize.logic.argument.Argument at 0x1808ac6cfd0>"
      ]
     },
     "execution_count": 26,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "a = A.get_proof('a')\n",
    "forall_x_P = forall(x, P)\n",
    "f = forall_x_P.get_proof('f')\n",
    "\n",
    "Argument([a,f], f.apply(a), label=r\"\\forall{E}\")"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Existential Quantifier ##\n",
    "### Introduction ###"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 32,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$$\\frac{a : A \\quad p : P}{a, p : \\exists{x}.P}(\\exists{I})$$"
      ],
      "text/plain": [
       "<symbolize.logic.argument.Argument at 0x1808ac46588>"
      ]
     },
     "execution_count": 32,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "a = A.get_proof('a')\n",
    "x = Symbol('x')\n",
    "P = PropositionSymbol('P', assume_contains=[x])\n",
    "p = P.get_proof('p')\n",
    "Argument([a,p], ProofExpressionCombination(a,p, exists_expression=x), label=r\"\\exists{I}\")"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Elimination ###"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 33,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$$\\frac{p : \\exists{x}.P}{Fst(p) : A}(\\exists{E_1})$$"
      ],
      "text/plain": [
       "<symbolize.logic.argument.Argument at 0x1808aa6a0b8>"
      ]
     },
     "execution_count": 33,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "x = A.get_proof('x')\n",
    "P = PropositionSymbol('P', assume_contains=[x])\n",
    "\n",
    "exists_x_P = exists(x, P)\n",
    "p = exists_x_P.get_proof('p',  exists_expression=x)\n",
    "\n",
    "\n",
    "Argument([p], Fst(p), label=r\"\\exists{E_1}\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 34,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$$\\frac{p : \\exists{x}.P}{Snd(p) : P}(\\exists{E_2})$$"
      ],
      "text/plain": [
       "<symbolize.logic.argument.Argument at 0x1808aa6ff98>"
      ]
     },
     "execution_count": 34,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "Argument([p], Snd(p), label=r\"\\exists{E_2}\")"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### [ST] p92 ###"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 37,
   "metadata": {},
   "outputs": [],
   "source": [
    "x = A.get_proof('x')\n",
    "B = PropositionSymbol('B', assume_contains=[x])\n",
    "C = PropositionSymbol('C', assume_contains=[x])\n",
    "B_implies_C = implies(B, C)\n",
    "forall_x_B_implies_C = forall(x, B_implies_C)\n",
    "r = forall_x_B_implies_C.get_proof('r')\n",
    "forall_x_B = forall(x, B)\n",
    "p = forall_x_B.get_proof('p')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Argument([r, x], r.apply(x), label=r\"\\forall{E}\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Argument([x, p], p.apply(x), label=r\"\\forall{E}\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "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.4"
  },
  "varInspector": {
   "cols": {
    "lenName": 16,
    "lenType": 16,
    "lenVar": 40
   },
   "kernels_config": {
    "python": {
     "delete_cmd_postfix": "",
     "delete_cmd_prefix": "del ",
     "library": "var_list.py",
     "varRefreshCmd": "print(var_dic_list())"
    },
    "r": {
     "delete_cmd_postfix": ") ",
     "delete_cmd_prefix": "rm(",
     "library": "var_list.r",
     "varRefreshCmd": "cat(var_dic_list()) "
    }
   },
   "types_to_exclude": [
    "module",
    "function",
    "builtin_function_or_method",
    "instance",
    "_Feature"
   ],
   "window_display": false
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}