\documentclass{article}
%
\usepackage{amsfonts}
\usepackage{latexsym}
\usepackage{verbatim}
%
\newcommand{\nuprl}{{\sf Nuprl}}
\newcommand{\hol}{{\sf HOL}}
\newcommand{\PPP}{{\mathbb P}}
\newcommand{\subtype}{\subseteq_{\mathrm{TT}}}
\newcommand{\suptype}{\supseteq_{\mathrm{TT}}}
\newcommand{\wsubtype}{\sqsubseteq^{\gamma}}
\newcommand{\wsuptype}{\sqsupseteq^{\gamma}}
\newcommand{\supof}[1]{{#1\!\mbox{-}\sup}}
\newcommand{\infof}[1]{{#1\!\mbox{-}\inf}}
\newcommand{\wsubtypesup}{\sup^{\gamma}}
\newcommand{\wsubtypeinf}{\inf^{\gamma}}
\newcommand{\typeeq}{=_{\mathrm{ext}}}
\newcommand{\triprox}{\triangleleft}
\newcommand{\trisume}{\triangleright}
\newcommand{\leprox}{\preceq}
\newcommand{\geprox}{\succeq}
\newcommand{\eqprox}{\approx}
\newcommand{\compat}{\uparrow}
\newcommand{\incompat}{\not\uparrow}
\newcommand{\evalto}{\Downarrow}
\newcommand{\defeq}{:=}
\newcommand{\fedeq}{=:}
\newcommand{\nats}{\mathbb{N}}
\newcommand{\bools}{\mathbb{B}}
\newcommand{\univW}{\mathbf{W}}
\newcommand{\neoW}{\mathbf{W'}}
\newcommand{\preW}{\mathbf{\mbox{\sf pre}W'}}
\newcommand{\hemisup}{\mathrm{hemisup}}
\newcommand{\arrow}{\rightarrow}
\newcommand{\defed}[1]{{\rm\bf #1}}
\newcommand{\axiomchoice}{AC}
% new \newcommand  --##--  (insert-next-line-halves "\\newcommand{\\" "}{}")
\newcommand{\negb}{\neg_{\bools}}
\newcommand{\orb}{\vee_{\bools}}
\newcommand{\andb}{\wedge_{\bools}}
\newcommand{\vars}{\mathit{Var}}
\newcommand{\ptwo}{\mathbf{P^2}}
\newcommand{\subst}[2]{|^{#2}_{#1}}
\newcommand{\gsingle}[1]{\gamma(\{#1\})}
\newcommand{\igsingle}[1]{i(\gsingle{#1})}
\newcommand{\mmiff}{\mathrel{\hbox{\ iff\/\ }}}
\newcommand{\miff}{\mathrel{\hbox{\,iff\/\,}}}
\newcommand{\halmos}{{$\Box$}}
%
\newcommand{\marginal}[1]{\marginpar{\small\sf $\leftarrow$ #1}}
\newcommand{\gap}{{\bf [\ldots]}\marginal{gap}}
\newcommand{\arule}[2]{\begin{array}{c} {#1} \\ \hline {#2} \end{array}}
%
\newcommand{\under}{{\sf **** under construction ****}}
%
\newtheorem{lemmable}{Lemma}
\newtheorem{corrable}[lemmable]{Corollary}
\newtheorem{intconjable}[lemmable]{internal conjecture}
\newtheorem{factable}[lemmable]{Fact}
\newtheorem{defable}{Definition}
\newtheorem{theorable}[lemmable]{Theoroid}
%
\newenvironment{internal}{}{}
\newcommand{\internalnote}[1]{[{\small\sl #1}]}
\newenvironment{internalize}
   {\begin{itemize}\begin{small}\begin{sf}}
   {\end{sf}\end{small}\end{itemize}}
%
% #old  \newenvironment{internal}{\comment}{\endcomment}
% #old  \newcommand{\internalnote}[1]{}
% #old  \newenvironment{internalize}
   % #old  {\comment}
   % #old  {\endcomment}
%
% #old  \pagestyle{myheadings}
%
\setlength{\evensidemargin}{0in}
\setlength{\oddsidemargin}{0in}
\setlength{\textwidth}{6.5in}
\setlength{\topmargin}{0in}
\setlength{\textheight}{9in}
\setlength{\headheight}{0in}
\setlength{\headsep}{0in}
\begin{document}

% #old  \org{ithaca institute for pure and purity-impaired mathematics}

\section{metavariables}

\begin{tabular}{ll}
$p, q, r, \ldots$ & a propositional variable \\
$A, B, \ldots$ & a $\ptwo$ formula \\
$\Gamma, \Delta, \ldots$ & a finite set of $\ptwo$ formulas \\
\end{tabular}

\section{syntax of $\ptwo$}

The formulas of $\ptwo$ are generated by
\[
\begin{array}{rcl}
V & \rightarrow & p_0\ \mid\ p_1\ \mid\ p_2\ \mid\ \cdots\ \mid\ p_i\ \mid\ \cdots \qquad\mathrm{(a\ countably\ infinite\ set)} \\
A & \rightarrow & V\ \mid\ \bot\ \mid\ (A \supset A')\ \mid\ (\forall V A)
\end{array}
\]
examples:\quad$(p_0 \supset p_1)$, $(\forall p_0(p_0 \supset p_1))$,
         $(\forall p_1((\forall p_2(p_2 \supset p_2)) \supset \bot))$

The remaining connectives and quantifier can be defined in terms of $\bot$, $\supset$, and $\forall$:
\[
\begin{array}{rcl}
\neg A      & \leftrightarrow & A \supset \bot \\
A \wedge B  & \leftrightarrow & \neg (A \supset \neg B) \\
A \vee B    & \leftrightarrow & (\neg A) \supset B \\
\exists p A & \leftrightarrow & \neg \forall p \neg A
\end{array}
\]

\section{assignments}

Let $\vars$ be the type of propositional variables, and let $\bools = \{0, 1\}$ be the booleans
(with 0 meaning false and 1 meaning true).
An assignment is a function $v : \vars \rightarrow \bools$.

Given an assignment $v$,
a boolean $b$, and a propositional variable $p$,
the ``updated'' assignment $v \subst{b}{p}$ is the function (in $\vars \rightarrow \bools$) defined by
\[
(v \subst{b}{p})(q) = \left\{
\begin{array}{ll}
b & \mathrm{if}\ q = p \\
v(q) & \mathrm{o.w.}
\end{array}
\right.
\]

\section{semantics of $\ptwo$}

Let $A$ be a $\ptwo$-formula and let $v$ be an assignment; let $v[A]$ be the notation for
the (boolean) value of $A$ under $v$, and let $v[A] : \bools$ be defined recursively 
as follows:
% #old  Given an assignment $v$ and a $\ptwo$-formula $A$, the boolean value $v[A]$ (``the value of 
% #old  $A$ under $v$'') is defined recursively as
% #old  As in the first problem set, let $val(v, A)$ denote the
% #old  value of the $\ptwo$-formula $A$ under the assignment $v$.
% #old  The function $val$ is recursively defined as follows ($v[A]$ is an abbreviation of $val(v, A)$):
\[
\begin{array}{lcll}
v[\bot] & = & 0 \\
v[p]    & = & v(p) \\
v[A \supset B] & = & (\negb\, v[A])\ \orb\ v[B] \\
v[\forall p A] & = & (v \subst{0}{p})[A]\ \andb\ (v \subst{1}{p})[A] \\
\end{array}
\]
where $\negb : \bools \arrow \bools$, $\orb : \bools \times \bools \arrow \bools$,
and $\andb : \bools \times \bools \arrow \bools$ are the standard
boolean operators.

For a finite set of formulas $\Gamma$, define
$v_\wedge[\Delta] = \bigwedge_{\bools} \{\,v[A] \mid A \in \Delta \,\}$
and define
$v_\vee[\Gamma] = \bigvee_{\bools} \{\,v[A] \mid A \in \Gamma \,\}$,
where $\bigwedge_{\bools} S$ is the conjunction of the boolean values in the set $S$
and $\bigvee_{\bools} S$ is their disjunction.
(By convention, $\bigwedge_{\bools} \emptyset = 1$ and $\bigvee_{\bools} \emptyset = 0$.)
The value $v[\Delta \vdash \Gamma]$ of a sequent can now be defined
as $(\negb\, v_\wedge[\Delta])\ \orb\ v_\vee[\Gamma]$.

\section{free variables}

For $A$ a formula of $\ptwo$,
the set of propositional variables that are free in $A$, denoted $FV(A)$,
can be characterized by the following recursive definition:
\[
\begin{array}{lcll}
FV(\bot) & = & \emptyset \\
FV(p)    & = & \{p\} \\
FV(A \supset B) & = & FV(A) \cup FV(B) \\
FV(\forall p A) & = & FV(A) - \{p\}
\end{array}
\]
The set of all propositional variables that occur in $A$, $PV(A)$,
can likewise be defined as
\[
\begin{array}{lcll}
PV(\bot) & = & \emptyset \\
PV(p)    & = & \{p\} \\
PV(A \supset B) & = & PV(A) \cup PV(B) \\
PV(\forall p A) & = & PV(A) \cup \{p\}
\end{array}
\]
examples:
\[
\begin{array}{lcc}
 FV(p_0 \supset p_1) & = & \{p_0, p_1\} \\
PV(p_0 \supset p_1) & = & \{p_0, p_1\} \\
FV(\forall p_0(p_0 \supset p_1)) &  = & \{p_1\} \\
PV(\forall p_0(p_0 \supset p_1)) &  = & \{p_0, p_1\} \\
FV(\forall p_1((\forall p_2(p_2 \supset p_2)) \supset \bot)) & = & \emptyset \\
PV(\forall p_1((\forall p_2(p_2 \supset p_2)) \supset (\forall p_3 p_1))) & = & \{p_1, p_2, p_3\}
\end{array}
\]
Extend the definitions of $FV$ and $PV$ to finite sets of formulas by
taking
$FV(\Gamma) = \bigcup_{A \in \Gamma} FV(A)$
and likewise by taking
$PV(\Gamma) = \bigcup_{A \in \Gamma} PV(A)$.
For sequents, the definitions are
$FV(\Delta \vdash \Gamma) = FV(\Delta \cup \Gamma)$
and
$PV(\Delta \vdash \Gamma) = PV(\Delta \cup \Gamma)$.

\section{substitution}

Given formulas $A$ and $B$ of $\ptwo$ and a propositional variable $p$,
the $\ptwo$ formula $A \subst{B}{p}$ (``$A$ with $B$ substituted for $p$'')
is, as usual, defined recursively:

\[
\begin{array}{rcll}
\bot \subst{B}{p} & = & \bot \\
p    \subst{B}{p} & = & B    \\
q    \subst{B}{p} & = & q    & (q \ne p) \\
(A \supset A') \subst{B}{p} & = & (A \subst{B}{p}) \supset (A' \subst{B}{p}) \\
(\forall p A) \subst{B}{p} & = & \forall p A \\
(\forall q A) \subst{B}{p} & = & \forall q (A \subst{B}{p}) & (q \ne p,\ q \notin FV(B))  \\
(\forall q A) \subst{B}{p} & = & \forall q' (A \subst{q'}{q} \subst{B}{p}) &
  (q \ne p,\ q \in FV(B),\ q' \notin PV(A,B,p))  \\
\end{array}
\]
examples:
\[\vbox{\halign{\hfil$#$&$#$\hfil\quad&\hfil$#$\hfil&\quad$#$\hfil\cr
 (p_0 \supset p_1) & \subst{p_2 \supset p_3}{p_0} & = & ((p_2 \supset p_3) \supset p_1)\cr
                (p_0 \supset (p_0 \supset p_1)) & \subst{p_3}{p_0} & = & 
                 (p_3 \supset (p_3 \supset p_1))\cr
                (p_0 \supset p_0) & \subst{p_0 \supset p_0}{p_0} & = &
                 ((p_0 \supset p_0) \supset (p_0 \supset p_0))\cr
                (p_0 \supset (\forall p_0(p_0 \supset p_0))) & \subst {p_1}{p_0} & = &
                 (p_1 \supset (\forall p_0(p_0 \supset p_0)))\cr
                (\forall p_0(p_0 \supset p_3)) & \subst{p_0}{p_3} & = &
                 (\forall p_1(p_1 \supset p_0))\cr}}\]
One can extend substitution to finite sets of formulas and thence to
sequents by letting
$\Gamma \subst{B}{p} = \{\, A \subst{B}{p} \mid A \in \Gamma \,\}$
and
$(\Delta \vdash \Gamma) \subst{B}{p} = (\Delta \subst{B}{p}) \vdash (\Gamma \subst{B}{p})$.

\section{rules of $\ptwo$}

The multiple-conclusioned sequent proof rules for $\ptwo$ are (in ``root-down tree format'')
\nopagebreak

\[
\begin{array}{cc}
{\Delta, \bot \vdash \Gamma} \\
\\
\arule{\Delta \vdash A, \Gamma\qquad \Delta, B \vdash \Gamma}{\Delta, A \supset B \vdash \Gamma} &
  \arule{\Delta, A \vdash B, \Gamma}{\Delta \vdash A \supset B, \Gamma} \\
\\
\arule{\Delta, \forall p A, A \subst{B}{p} \vdash \Gamma}{\Delta, \forall p A \vdash \Gamma} &
\arule{\Delta \vdash A \subst{q}{p}, \Gamma}{\Delta \vdash \forall p A, \Gamma}\ (!) \\
\\
\Delta, A \vdash A, \Gamma \\
\\
 \arule{\Delta \vdash \Gamma}{\Delta, A \vdash \Gamma} &
 \arule{\Delta \vdash \Gamma}{\Delta \vdash A, \Gamma} \\
\\
\multicolumn{2}{c}{\mbox{$(!)$\quad this is only legal if
$q \notin FV(\Delta, \Gamma, \forall p A)$.}}
\end{array}
\]
The rules for $\exists$ 
can be derived from the rules given above:
\[
\begin{array}{cc}
\arule{\Delta, A \subst{q}{p} \vdash \Gamma}{\Delta, \exists p A \vdash \Gamma}\ (!) &
 \arule{\Delta \vdash A \subst{B}{p}, \Gamma}{\Delta \vdash \exists p A, \Gamma}
\end{array}
\]
The familiar rules for $\wedge$, $\vee$, and $\neg$ can also be derived.

\vskip 10pt
\noindent
an example proof:
\[
\arule{
  \arule{
      \bot \vdash \bot
    }
    {\forall p.p \vdash \bot}
  }
  {\vdash (\forall p.p) \supset \bot}
\]
The topmost step is the left $\forall$ rule, using $\bot$ as $B$; i.e., informally,
the proof is
\[
\arule{
  \arule{
      \arule{\bot \vdash \bot}{p \subst{\bot}{p} \vdash \bot}
    }
    {\forall p.p \vdash \bot}
  }
  {\vdash (\forall p.p) \supset \bot}
\]
where the topmost pseudo-step is justified (meta-theoretically) by the equality $p \subst{\bot}{p} = \bot$.

\end{document}