\documentclass{article}
\usepackage{proof}
\pagestyle{empty}
\textwidth18cm
\textheight26cm
\oddsidemargin-1cm
\evensidemargin\oddsidemargin
\headheight0cm
\headsep0cm
\footskip0cm
\topmargin0cm
\parindent0pt

\newenvironment{problem}{\begin{description}\item[Problem:]}{\end{description}}
\newenvironment{answer}{\begin{description}\item[Answer:]}{\end{description}}
\begin{document}
\title{Some Test Examples}
\author{M.~Ultseq}
\maketitle

\section{Derivability of Sequents}

\subsection{Example s1}

\begin{problem}
Is the sequent $[(A\supset B)^p, (A\lor C)^t]$ provable?
\end{problem}
\begin{answer}
No, it is not.
\end{answer}
Derivation of $[(A\supset B)^p, (A\lor C)^t]$:
\[
\infer{[(A\supset B)^p, (A\lor C)^t]}%
{\infer{[A^p, B^p, (A\lor C)^t]}%
{\deduce{[A^p, A^t, B^p, C^t]}%
{\mbox{hypothesis}}
}
&
\infer{[A^t, B^f, (A\lor C)^t]}%
{\deduce{[A^t, B^f, C^t]}%
{\mbox{hypothesis}}
}
}
\]
List of hypotheses:
\[\begin{array}{l}
[A^p, A^t, B^p, C^t]\\\relax
[A^t, B^f, C^t]
  \end{array}
\]
Derivation skeleton of $[(A\supset B)^p, (A\lor C)^t]$:
\[
\infer{1}%
{\infer{2}%
{\deduce{3}%
{}
}
&
\infer{4}%
{\deduce{5}%
{}
}
}
\]
Table of sequents:
\[\begin{array}{rl}
1{:} & [(A\supset B)^p, (A\lor C)^t]\\\relax
2{:} & [A^p, B^p, (A\lor C)^t]\\\relax
3{:} & [A^p, A^t, B^p, C^t]\\\relax
4{:} & [A^t, B^f, (A\lor C)^t]\\\relax
5{:} & [A^t, B^f, C^t]
  \end{array}
\]
List of counter-examples:
\[\begin{array}{l}
[A^f, B^f, C^f]\\\relax
[A^f, B^f, C^p]\\\relax
[A^f, B^p, C^f]\\\relax
[A^f, B^p, C^p]\\\relax
[A^f, B^t, C^f]\\\relax
[A^f, B^t, C^p]\\\relax
[A^p, B^p, C^f]\\\relax
[A^p, B^p, C^p]\\\relax
[A^p, B^t, C^f]\\\relax
[A^p, B^t, C^p]
  \end{array}
\]
\subsection{Example s2}

\begin{problem}
Is the sequent $[(A\supset (B\supset A))^t]$ provable?
\end{problem}
\begin{answer}
Yes, it is.
\end{answer}
Proof of $[(A\supset (B\supset A))^t]$:
\[
\infer{[(A\supset (B\supset A))^t]}%
{\infer{[A^f, A^p, (B\supset A)^t]}%
{\deduce{[A^f, A^p, A^t, B^f, B^p]}%
{\mbox{axiom for $A$}}
&
\deduce{[A^f, A^p, A^t, B^f]}%
{\mbox{axiom for $A$}}
}
&
\infer{[A^f, (B\supset A)^p, (B\supset A)^t]}%
{\infer{[A^f, A^p, B^p, (B\supset A)^t]}%
{\deduce{[A^f, A^p, A^t, B^f, B^p]}%
{\mbox{axiom for $A$}}
&
\deduce{[A^f, A^p, A^t, B^f, B^p]}%
{\mbox{axiom for $A$}}
}
&
\infer{[A^f, B^t, (B\supset A)^t]}%
{\deduce{[A^f, A^t, B^f, B^p, B^t]}%
{\mbox{axiom for $B$}}
&
\deduce{[A^f, A^p, A^t, B^f, B^t]}%
{\mbox{axiom for $A$}}
}
}
}
\]
Proof skeleton of $[(A\supset (B\supset A))^t]$:
\[
\infer{1}%
{\infer{2}%
{\deduce{3}%
{}
&
\deduce{4}%
{}
}
&
\infer{5}%
{\infer{6}%
{\deduce{3}%
{}
&
\deduce{3}%
{}
}
&
\infer{7}%
{\deduce{8}%
{}
&
\deduce{9}%
{}
}
}
}
\]
Table of sequents:
\[\begin{array}{rl}
1{:} & [(A\supset (B\supset A))^t]\\\relax
2{:} & [A^f, A^p, (B\supset A)^t]\\\relax
3{:} & [A^f, A^p, A^t, B^f, B^p]\\\relax
4{:} & [A^f, A^p, A^t, B^f]\\\relax
5{:} & [A^f, (B\supset A)^p, (B\supset A)^t]\\\relax
6{:} & [A^f, A^p, B^p, (B\supset A)^t]\\\relax
7{:} & [A^f, B^t, (B\supset A)^t]\\\relax
8{:} & [A^f, A^t, B^f, B^p, B^t]\\\relax
9{:} & [A^f, A^p, A^t, B^f, B^t]
  \end{array}
\]
\subsection{Example s3}

\begin{problem}
Is the sequent $[(A\land B)^f, A^p, (A\lor B)^t]$ provable?
\end{problem}
\begin{answer}
Yes, it is.
\end{answer}
Proof of $[(A\land B)^f, A^p, (A\lor B)^t]$:
\[
\infer{[(A\land B)^f, A^p, (A\lor B)^t]}%
{\infer{[A^f, A^p, B^f, (A\lor B)^t]}%
{\deduce{[A^f, A^p, A^t, B^f, B^t]}%
{\mbox{axiom for $A$}}
}
}
\]
Proof skeleton of $[(A\land B)^f, A^p, (A\lor B)^t]$:
\[
\infer{1}%
{\infer{2}%
{\deduce{3}%
{}
}
}
\]
Table of sequents:
\[\begin{array}{rl}
1{:} & [(A\land B)^f, A^p, (A\lor B)^t]\\\relax
2{:} & [A^f, A^p, B^f, (A\lor B)^t]\\\relax
3{:} & [A^f, A^p, A^t, B^f, B^t]
  \end{array}
\]
\subsection{Example s4}

\begin{problem}
Is the sequent $[(A\land B)^f, (A\land B)^p, B^t]$ provable?
\end{problem}
\begin{answer}
Yes, it is.
\end{answer}
Proof of $[(A\land B)^f, (A\land B)^p, B^t]$:
\[
\infer{[(A\land B)^f, (A\land B)^p, B^t]}%
{\infer{[A^f, B^f, B^t, (A\land B)^p]}%
{\deduce{[A^f, A^p, B^f, B^p, B^t]}%
{\mbox{axiom for $B$}}
&
\deduce{[A^f, A^p, A^t, B^f, B^t]}%
{\mbox{axiom for $A$}}
&
\deduce{[A^f, B^f, B^p, B^t]}%
{\mbox{axiom for $B$}}
}
}
\]
Proof skeleton of $[(A\land B)^f, (A\land B)^p, B^t]$:
\[
\infer{1}%
{\infer{2}%
{\deduce{3}%
{}
&
\deduce{4}%
{}
&
\deduce{5}%
{}
}
}
\]
Table of sequents:
\[\begin{array}{rl}
1{:} & [(A\land B)^f, (A\land B)^p, B^t]\\\relax
2{:} & [A^f, B^f, B^t, (A\land B)^p]\\\relax
3{:} & [A^f, A^p, B^f, B^p, B^t]\\\relax
4{:} & [A^f, A^p, A^t, B^f, B^t]\\\relax
5{:} & [A^f, B^f, B^p, B^t]
  \end{array}
\]
\subsection{Example s5}

\begin{problem}
Is the sequent $[(((A\supset B)\supset B)\supset ((B\supset A)\supset A))^t]$ provable?
\end{problem}
\begin{answer}
Yes, it is.
\end{answer}
Proof of $[(((A\supset B)\supset B)\supset ((B\supset A)\supset A))^t]$:
\[
\infer{[(((A\supset B)\supset B)\supset ((B\supset A)\supset A))^t]}%
{\infer{[((A\supset B)\supset B)^f, ((A\supset B)\supset B)^p, ((B\supset A)\supset A)^t]}%
{\infer{[(A\supset B)^t, ((A\supset B)\supset B)^p, ((B\supset A)\supset A)^t]}%
{\infer{[A^f, A^p, B^t, ((A\supset B)\supset B)^p, ((B\supset A)\supset A)^t]}%
{\infer{[A^f, A^p, B^p, B^t, (A\supset B)^p, ((B\supset A)\supset A)^t]}%
{\infer{[A^f, A^p, B^p, B^t, ((B\supset A)\supset A)^t]}%
{\deduce{[A^f, A^p, A^t, B^p, B^t, (B\supset A)^f, (B\supset A)^p]}%
{\mbox{axiom for $A$}}
&
\deduce{[A^f, A^p, A^t, B^p, B^t, (B\supset A)^f]}%
{\mbox{axiom for $A$}}
}
&
\deduce{[A^f, A^p, A^t, B^f, B^p, B^t, ((B\supset A)\supset A)^t]}%
{\mbox{axiom for $A$}}
}
&
\infer{[A^f, A^p, B^f, B^t, (A\supset B)^t, ((B\supset A)\supset A)^t]}%
{\infer{[A^f, A^p, B^f, B^t, ((B\supset A)\supset A)^t]}%
{\deduce{[A^f, A^p, A^t, B^f, B^t, (B\supset A)^f, (B\supset A)^p]}%
{\mbox{axiom for $A$}}
&
\deduce{[A^f, A^p, A^t, B^f, B^t, (B\supset A)^f]}%
{\mbox{axiom for $A$}}
}
&
\deduce{[A^f, A^p, B^f, B^p, B^t, ((B\supset A)\supset A)^t]}%
{\mbox{axiom for $B$}}
}
}
&
\infer{[A^f, B^p, B^t, ((A\supset B)\supset B)^p, ((B\supset A)\supset A)^t]}%
{\infer{[A^f, B^p, B^t, (A\supset B)^p, ((B\supset A)\supset A)^t]}%
{\infer{[A^f, A^p, B^p, B^t, ((B\supset A)\supset A)^t]}%
{\deduce{[A^f, A^p, A^t, B^p, B^t, (B\supset A)^f, (B\supset A)^p]}%
{\mbox{axiom for $A$}}
&
\deduce{[A^f, A^p, A^t, B^p, B^t, (B\supset A)^f]}%
{\mbox{axiom for $A$}}
}
&
\deduce{[A^f, A^t, B^f, B^p, B^t, ((B\supset A)\supset A)^t]}%
{\mbox{axiom for $B$}}
}
&
\deduce{[A^f, B^f, B^p, B^t, (A\supset B)^t, ((B\supset A)\supset A)^t]}%
{\mbox{axiom for $B$}}
}
}
&
\infer{[B^f, ((A\supset B)\supset B)^p, ((B\supset A)\supset A)^t]}%
{\infer{[B^f, B^p, (A\supset B)^p, ((B\supset A)\supset A)^t]}%
{\infer{[A^p, B^f, B^p, ((B\supset A)\supset A)^t]}%
{\infer{[A^p, A^t, B^f, B^p, (B\supset A)^f, (B\supset A)^p]}%
{\deduce{[A^p, A^t, B^f, B^p, B^t, (B\supset A)^p]}%
{\mbox{axiom for $B$}}
&
\deduce{[A^f, A^p, A^t, B^f, B^p, (B\supset A)^p]}%
{\mbox{axiom for $A$}}
}
&
\infer{[A^p, A^t, B^f, B^p, (B\supset A)^f]}%
{\deduce{[A^p, A^t, B^f, B^p, B^t]}%
{\mbox{axiom for $B$}}
&
\deduce{[A^f, A^p, A^t, B^f, B^p]}%
{\mbox{axiom for $A$}}
}
}
&
\infer{[A^t, B^f, B^p, ((B\supset A)\supset A)^t]}%
{\infer{[A^t, B^f, B^p, (B\supset A)^f, (B\supset A)^p]}%
{\deduce{[A^t, B^f, B^p, B^t, (B\supset A)^p]}%
{\mbox{axiom for $B$}}
&
\infer{[A^f, A^t, B^f, B^p, (B\supset A)^p]}%
{\deduce{[A^f, A^p, A^t, B^f, B^p]}%
{\mbox{axiom for $A$}}
&
\deduce{[A^f, A^t, B^f, B^p, B^t]}%
{\mbox{axiom for $B$}}
}
}
&
\infer{[A^p, A^t, B^f, B^p, (B\supset A)^f]}%
{\deduce{[A^p, A^t, B^f, B^p, B^t]}%
{\mbox{axiom for $B$}}
&
\deduce{[A^f, A^p, A^t, B^f, B^p]}%
{\mbox{axiom for $A$}}
}
}
}
&
\infer{[B^f, (A\supset B)^t, ((B\supset A)\supset A)^t]}%
{\infer{[A^f, A^p, B^f, B^t, ((B\supset A)\supset A)^t]}%
{\deduce{[A^f, A^p, A^t, B^f, B^t, (B\supset A)^f, (B\supset A)^p]}%
{\mbox{axiom for $A$}}
&
\deduce{[A^f, A^p, A^t, B^f, B^t, (B\supset A)^f]}%
{\mbox{axiom for $A$}}
}
&
\deduce{[A^f, B^f, B^p, B^t, ((B\supset A)\supset A)^t]}%
{\mbox{axiom for $B$}}
}
}
}
&
\infer{[((A\supset B)\supset B)^f, ((B\supset A)\supset A)^p, ((B\supset A)\supset A)^t]}%
{\infer{[(A\supset B)^t, ((B\supset A)\supset A)^p, ((B\supset A)\supset A)^t]}%
{\infer{[A^f, A^p, B^t, ((B\supset A)\supset A)^p, ((B\supset A)\supset A)^t]}%
{\infer{[A^f, A^p, B^t, (B\supset A)^p, ((B\supset A)\supset A)^t]}%
{\infer{[A^f, A^p, B^p, B^t, ((B\supset A)\supset A)^t]}%
{\deduce{[A^f, A^p, A^t, B^p, B^t, (B\supset A)^f, (B\supset A)^p]}%
{\mbox{axiom for $A$}}
&
\deduce{[A^f, A^p, A^t, B^p, B^t, (B\supset A)^f]}%
{\mbox{axiom for $A$}}
}
&
\infer{[A^f, A^p, B^t, ((B\supset A)\supset A)^t]}%
{\deduce{[A^f, A^p, A^t, B^t, (B\supset A)^f, (B\supset A)^p]}%
{\mbox{axiom for $A$}}
&
\deduce{[A^f, A^p, A^t, B^t, (B\supset A)^f]}%
{\mbox{axiom for $A$}}
}
}
&
\infer{[A^f, A^p, B^t, (B\supset A)^t, ((B\supset A)\supset A)^t]}%
{\deduce{[A^f, A^p, A^t, B^f, B^p, B^t, ((B\supset A)\supset A)^t]}%
{\mbox{axiom for $A$}}
&
\deduce{[A^f, A^p, A^t, B^f, B^t, ((B\supset A)\supset A)^t]}%
{\mbox{axiom for $A$}}
}
}
&
\infer{[A^f, B^p, B^t, ((B\supset A)\supset A)^p, ((B\supset A)\supset A)^t]}%
{\infer{[A^f, A^p, B^p, B^t, (B\supset A)^p, ((B\supset A)\supset A)^t]}%
{\infer{[A^f, A^p, B^p, B^t, ((B\supset A)\supset A)^t]}%
{\deduce{[A^f, A^p, A^t, B^p, B^t, (B\supset A)^f, (B\supset A)^p]}%
{\mbox{axiom for $A$}}
&
\deduce{[A^f, A^p, A^t, B^p, B^t, (B\supset A)^f]}%
{\mbox{axiom for $A$}}
}
&
\infer{[A^f, A^p, B^p, B^t, ((B\supset A)\supset A)^t]}%
{\deduce{[A^f, A^p, A^t, B^p, B^t, (B\supset A)^f, (B\supset A)^p]}%
{\mbox{axiom for $A$}}
&
\deduce{[A^f, A^p, A^t, B^p, B^t, (B\supset A)^f]}%
{\mbox{axiom for $A$}}
}
}
&
\infer{[A^f, B^p, B^t, (B\supset A)^t, ((B\supset A)\supset A)^t]}%
{\deduce{[A^f, A^t, B^f, B^p, B^t, ((B\supset A)\supset A)^t]}%
{\mbox{axiom for $B$}}
&
\deduce{[A^f, A^p, A^t, B^f, B^p, B^t, ((B\supset A)\supset A)^t]}%
{\mbox{axiom for $A$}}
}
}
}
&
\infer{[B^f, ((B\supset A)\supset A)^p, ((B\supset A)\supset A)^t]}%
{\infer{[A^p, B^f, (B\supset A)^p, ((B\supset A)\supset A)^t]}%
{\infer{[A^p, B^f, B^p, ((B\supset A)\supset A)^t]}%
{\infer{[A^p, A^t, B^f, B^p, (B\supset A)^f, (B\supset A)^p]}%
{\deduce{[A^p, A^t, B^f, B^p, B^t, (B\supset A)^p]}%
{\mbox{axiom for $B$}}
&
\deduce{[A^f, A^p, A^t, B^f, B^p, (B\supset A)^p]}%
{\mbox{axiom for $A$}}
}
&
\infer{[A^p, A^t, B^f, B^p, (B\supset A)^f]}%
{\deduce{[A^p, A^t, B^f, B^p, B^t]}%
{\mbox{axiom for $B$}}
&
\deduce{[A^f, A^p, A^t, B^f, B^p]}%
{\mbox{axiom for $A$}}
}
}
&
\infer{[A^f, A^p, B^f, B^t, ((B\supset A)\supset A)^t]}%
{\deduce{[A^f, A^p, A^t, B^f, B^t, (B\supset A)^f, (B\supset A)^p]}%
{\mbox{axiom for $A$}}
&
\deduce{[A^f, A^p, A^t, B^f, B^t, (B\supset A)^f]}%
{\mbox{axiom for $A$}}
}
}
&
\infer{[A^f, B^f, (B\supset A)^t, ((B\supset A)\supset A)^t]}%
{\infer{[A^f, A^t, B^f, B^p, ((B\supset A)\supset A)^t]}%
{\infer{[A^f, A^t, B^f, B^p, (B\supset A)^f, (B\supset A)^p]}%
{\deduce{[A^f, A^t, B^f, B^p, B^t, (B\supset A)^p]}%
{\mbox{axiom for $B$}}
&
\infer{[A^f, A^t, B^f, B^p, (B\supset A)^p]}%
{\deduce{[A^f, A^p, A^t, B^f, B^p]}%
{\mbox{axiom for $A$}}
&
\deduce{[A^f, A^t, B^f, B^p, B^t]}%
{\mbox{axiom for $B$}}
}
}
&
\deduce{[A^f, A^p, A^t, B^f, B^p, (B\supset A)^f]}%
{\mbox{axiom for $A$}}
}
&
\deduce{[A^f, A^p, A^t, B^f, ((B\supset A)\supset A)^t]}%
{\mbox{axiom for $A$}}
}
}
}
}
\]
Proof skeleton of $[(((A\supset B)\supset B)\supset ((B\supset A)\supset A))^t]$:
\[
\infer{1}%
{\infer{2}%
{\infer{3}%
{\infer{4}%
{\infer{5}%
{\infer{6}%
{\deduce{7}%
{}
&
\deduce{8}%
{}
}
&
\deduce{9}%
{}
}
&
\infer{10}%
{\infer{11}%
{\deduce{12}%
{}
&
\deduce{13}%
{}
}
&
\deduce{14}%
{}
}
}
&
\infer{15}%
{\infer{16}%
{\infer{6}%
{\deduce{7}%
{}
&
\deduce{8}%
{}
}
&
\deduce{17}%
{}
}
&
\deduce{18}%
{}
}
}
&
\infer{19}%
{\infer{20}%
{\infer{21}%
{\infer{22}%
{\deduce{23}%
{}
&
\deduce{24}%
{}
}
&
\infer{25}%
{\deduce{26}%
{}
&
\deduce{27}%
{}
}
}
&
\infer{28}%
{\infer{29}%
{\deduce{30}%
{}
&
\infer{31}%
{\deduce{27}%
{}
&
\deduce{32}%
{}
}
}
&
\infer{25}%
{\deduce{26}%
{}
&
\deduce{27}%
{}
}
}
}
&
\infer{33}%
{\infer{11}%
{\deduce{12}%
{}
&
\deduce{13}%
{}
}
&
\deduce{34}%
{}
}
}
}
&
\infer{35}%
{\infer{36}%
{\infer{37}%
{\infer{38}%
{\infer{6}%
{\deduce{7}%
{}
&
\deduce{8}%
{}
}
&
\infer{39}%
{\deduce{40}%
{}
&
\deduce{41}%
{}
}
}
&
\infer{42}%
{\deduce{9}%
{}
&
\deduce{43}%
{}
}
}
&
\infer{44}%
{\infer{45}%
{\infer{6}%
{\deduce{7}%
{}
&
\deduce{8}%
{}
}
&
\infer{6}%
{\deduce{7}%
{}
&
\deduce{8}%
{}
}
}
&
\infer{46}%
{\deduce{17}%
{}
&
\deduce{9}%
{}
}
}
}
&
\infer{47}%
{\infer{48}%
{\infer{21}%
{\infer{22}%
{\deduce{23}%
{}
&
\deduce{24}%
{}
}
&
\infer{25}%
{\deduce{26}%
{}
&
\deduce{27}%
{}
}
}
&
\infer{11}%
{\deduce{12}%
{}
&
\deduce{13}%
{}
}
}
&
\infer{49}%
{\infer{50}%
{\infer{51}%
{\deduce{52}%
{}
&
\infer{31}%
{\deduce{27}%
{}
&
\deduce{32}%
{}
}
}
&
\deduce{53}%
{}
}
&
\deduce{54}%
{}
}
}
}
}
\]
Table of sequents:
\[\begin{array}{rl}
1{:} & [(((A\supset B)\supset B)\supset ((B\supset A)\supset A))^t]\\\relax
2{:} & [((A\supset B)\supset B)^f, ((A\supset B)\supset B)^p, ((B\supset A)\supset A)^t]\\\relax
3{:} & [(A\supset B)^t, ((A\supset B)\supset B)^p, ((B\supset A)\supset A)^t]\\\relax
4{:} & [A^f, A^p, B^t, ((A\supset B)\supset B)^p, ((B\supset A)\supset A)^t]\\\relax
5{:} & [A^f, A^p, B^p, B^t, (A\supset B)^p, ((B\supset A)\supset A)^t]\\\relax
6{:} & [A^f, A^p, B^p, B^t, ((B\supset A)\supset A)^t]\\\relax
7{:} & [A^f, A^p, A^t, B^p, B^t, (B\supset A)^f, (B\supset A)^p]\\\relax
8{:} & [A^f, A^p, A^t, B^p, B^t, (B\supset A)^f]\\\relax
9{:} & [A^f, A^p, A^t, B^f, B^p, B^t, ((B\supset A)\supset A)^t]\\\relax
10{:} & [A^f, A^p, B^f, B^t, (A\supset B)^t, ((B\supset A)\supset A)^t]\\\relax
11{:} & [A^f, A^p, B^f, B^t, ((B\supset A)\supset A)^t]\\\relax
12{:} & [A^f, A^p, A^t, B^f, B^t, (B\supset A)^f, (B\supset A)^p]\\\relax
13{:} & [A^f, A^p, A^t, B^f, B^t, (B\supset A)^f]\\\relax
14{:} & [A^f, A^p, B^f, B^p, B^t, ((B\supset A)\supset A)^t]\\\relax
15{:} & [A^f, B^p, B^t, ((A\supset B)\supset B)^p, ((B\supset A)\supset A)^t]\\\relax
16{:} & [A^f, B^p, B^t, (A\supset B)^p, ((B\supset A)\supset A)^t]\\\relax
17{:} & [A^f, A^t, B^f, B^p, B^t, ((B\supset A)\supset A)^t]\\\relax
18{:} & [A^f, B^f, B^p, B^t, (A\supset B)^t, ((B\supset A)\supset A)^t]\\\relax
19{:} & [B^f, ((A\supset B)\supset B)^p, ((B\supset A)\supset A)^t]\\\relax
20{:} & [B^f, B^p, (A\supset B)^p, ((B\supset A)\supset A)^t]\\\relax
21{:} & [A^p, B^f, B^p, ((B\supset A)\supset A)^t]\\\relax
22{:} & [A^p, A^t, B^f, B^p, (B\supset A)^f, (B\supset A)^p]\\\relax
23{:} & [A^p, A^t, B^f, B^p, B^t, (B\supset A)^p]\\\relax
24{:} & [A^f, A^p, A^t, B^f, B^p, (B\supset A)^p]\\\relax
25{:} & [A^p, A^t, B^f, B^p, (B\supset A)^f]\\\relax
26{:} & [A^p, A^t, B^f, B^p, B^t]\\\relax
27{:} & [A^f, A^p, A^t, B^f, B^p]\\\relax
28{:} & [A^t, B^f, B^p, ((B\supset A)\supset A)^t]\\\relax
29{:} & [A^t, B^f, B^p, (B\supset A)^f, (B\supset A)^p]\\\relax
30{:} & [A^t, B^f, B^p, B^t, (B\supset A)^p]\\\relax
31{:} & [A^f, A^t, B^f, B^p, (B\supset A)^p]\\\relax
32{:} & [A^f, A^t, B^f, B^p, B^t]\\\relax
33{:} & [B^f, (A\supset B)^t, ((B\supset A)\supset A)^t]\\\relax
34{:} & [A^f, B^f, B^p, B^t, ((B\supset A)\supset A)^t]\\\relax
35{:} & [((A\supset B)\supset B)^f, ((B\supset A)\supset A)^p, ((B\supset A)\supset A)^t]\\\relax
36{:} & [(A\supset B)^t, ((B\supset A)\supset A)^p, ((B\supset A)\supset A)^t]\\\relax
37{:} & [A^f, A^p, B^t, ((B\supset A)\supset A)^p, ((B\supset A)\supset A)^t]\\\relax
38{:} & [A^f, A^p, B^t, (B\supset A)^p, ((B\supset A)\supset A)^t]\\\relax
39{:} & [A^f, A^p, B^t, ((B\supset A)\supset A)^t]\\\relax
40{:} & [A^f, A^p, A^t, B^t, (B\supset A)^f, (B\supset A)^p]\\\relax
41{:} & [A^f, A^p, A^t, B^t, (B\supset A)^f]\\\relax
42{:} & [A^f, A^p, B^t, (B\supset A)^t, ((B\supset A)\supset A)^t]\\\relax
43{:} & [A^f, A^p, A^t, B^f, B^t, ((B\supset A)\supset A)^t]\\\relax
44{:} & [A^f, B^p, B^t, ((B\supset A)\supset A)^p, ((B\supset A)\supset A)^t]\\\relax
45{:} & [A^f, A^p, B^p, B^t, (B\supset A)^p, ((B\supset A)\supset A)^t]\\\relax
46{:} & [A^f, B^p, B^t, (B\supset A)^t, ((B\supset A)\supset A)^t]\\\relax
47{:} & [B^f, ((B\supset A)\supset A)^p, ((B\supset A)\supset A)^t]\\\relax
48{:} & [A^p, B^f, (B\supset A)^p, ((B\supset A)\supset A)^t]\\\relax
49{:} & [A^f, B^f, (B\supset A)^t, ((B\supset A)\supset A)^t]\\\relax
50{:} & [A^f, A^t, B^f, B^p, ((B\supset A)\supset A)^t]\\\relax
51{:} & [A^f, A^t, B^f, B^p, (B\supset A)^f, (B\supset A)^p]\\\relax
52{:} & [A^f, A^t, B^f, B^p, B^t, (B\supset A)^p]\\\relax
53{:} & [A^f, A^p, A^t, B^f, B^p, (B\supset A)^f]\\\relax
54{:} & [A^f, A^p, A^t, B^f, ((B\supset A)\supset A)^t]
  \end{array}
\]
\subsection{Example s6}

\begin{problem}
Is the sequent $[((A\supset B)\supset B)^t]$ provable?
\end{problem}
\begin{answer}
No, it is not.
\end{answer}
Derivation of $[((A\supset B)\supset B)^t]$:
\[
\infer{[((A\supset B)\supset B)^t]}%
{\infer{[B^t, (A\supset B)^f, (A\supset B)^p]}%
{\infer{[A^t, B^t, (A\supset B)^p]}%
{\deduce{[A^p, A^t, B^p, B^t]}%
{\mbox{hypothesis}}
&
\deduce{[A^t, B^f, B^t]}%
{\mbox{hypothesis}}
}
&
\infer{[B^f, B^t, (A\supset B)^p]}%
{\deduce{[A^p, B^f, B^p, B^t]}%
{\mbox{axiom for $B$}}
&
\deduce{[A^t, B^f, B^t]}%
{\mbox{hypothesis}}
}
}
&
\infer{[B^p, B^t, (A\supset B)^f]}%
{\deduce{[A^t, B^p, B^t]}%
{\mbox{hypothesis}}
&
\deduce{[B^f, B^p, B^t]}%
{\mbox{axiom for $B$}}
}
}
\]
List of hypotheses:
\[\begin{array}{l}
[A^t, B^f, B^t]\\\relax
[A^t, B^p, B^t]
  \end{array}
\]
Derivation skeleton of $[((A\supset B)\supset B)^t]$:
\[
\infer{1}%
{\infer{2}%
{\infer{3}%
{\deduce{4}%
{}
&
\deduce{5}%
{}
}
&
\infer{6}%
{\deduce{7}%
{}
&
\deduce{5}%
{}
}
}
&
\infer{8}%
{\deduce{9}%
{}
&
\deduce{10}%
{}
}
}
\]
Table of sequents:
\[\begin{array}{rl}
1{:} & [((A\supset B)\supset B)^t]\\\relax
2{:} & [B^t, (A\supset B)^f, (A\supset B)^p]\\\relax
3{:} & [A^t, B^t, (A\supset B)^p]\\\relax
4{:} & [A^p, A^t, B^p, B^t]\\\relax
5{:} & [A^t, B^f, B^t]\\\relax
6{:} & [B^f, B^t, (A\supset B)^p]\\\relax
7{:} & [A^p, B^f, B^p, B^t]\\\relax
8{:} & [B^p, B^t, (A\supset B)^f]\\\relax
9{:} & [A^t, B^p, B^t]\\\relax
10{:} & [B^f, B^p, B^t]
  \end{array}
\]
List of counter-examples:
\[\begin{array}{l}
[A^f, B^f]\\\relax
[A^f, B^p]\\\relax
[A^p, B^f]\\\relax
[A^p, B^p]
  \end{array}
\]
\section{Consequence Relation on Sequents}

\subsection{Example cs1}

\begin{problem}
Is the consequence relation \[
[A^f, A^p, B^t], 
[A^f, B^p, B^t]\vdash [(A\supset B)^t]\]
 valid?
\end{problem}
The problem is equivalent to proving the following sequents:
\[\begin{array}{l}
[A^p, A^t, (A\supset B)^t]\\\relax
[A^t, B^f, (A\supset B)^t]\\\relax
[B^f, B^p, (A\supset B)^t]
  \end{array}
\]
\begin{answer}
Yes, the consequence relation holds.
\end{answer}
\subsection{Example cs2}

\begin{problem}
Is the consequence relation \[
[A^p, A^f, B^t], 
[A^f, B^p, B^t]\vdash [(A\supset B)^t]\]
 valid?
\end{problem}
The problem is equivalent to proving the following sequents:
\[\begin{array}{l}
[A^p, A^t, (A\supset B)^t]\\\relax
[A^t, B^f, (A\supset B)^t]\\\relax
[B^f, B^p, (A\supset B)^t]
  \end{array}
\]
\begin{answer}
Yes, the consequence relation holds.
\end{answer}
\subsection{Example cs3}

\begin{problem}
Is the consequence relation \[
[A^f, A^p, B^t], 
[A^f, B^p, B^t]\vdash [(A\supset B)^p]\]
 valid?
\end{problem}
The problem is equivalent to proving the following sequents:
\[\begin{array}{l}
[A^p, A^t, (A\supset B)^p]\\\relax
[A^t, B^f, (A\supset B)^p]\\\relax
[B^f, B^p, (A\supset B)^p]
  \end{array}
\]
\begin{answer}
No, the consequence relation does not hold.
\end{answer}
List of counter-examples:
\[\begin{array}{l}
[A^f, B^f]\\\relax
[A^f, B^p]\\\relax
[A^f, B^t]\\\relax
[A^p, B^p]\\\relax
[A^p, B^t]\\\relax
[A^t, B^t]
  \end{array}
\]
\subsection{Example cs4}

\begin{problem}
Is the consequence relation \[
[A^f, A^p, B^t], 
[A^f, B^p, B^t]\vdash [(A\supset B)^f]\]
 valid?
\end{problem}
The problem is equivalent to proving the following sequents:
\[\begin{array}{l}
[A^p, A^t, (A\supset B)^f]\\\relax
[A^t, B^f, (A\supset B)^f]\\\relax
[B^f, B^p, (A\supset B)^f]
  \end{array}
\]
\begin{answer}
No, the consequence relation does not hold.
\end{answer}
List of counter-examples:
\[\begin{array}{l}
[A^f]\\\relax
[A^p, B^p]\\\relax
[B^t]
  \end{array}
\]
\subsection{Example cs5}

\begin{problem}
Is the consequence relation \[
[(A\land B)^t]\vdash [A^t]\]
 valid?
\end{problem}
The problem is equivalent to proving the following sequent:
\[\begin{array}{l}
[A^t, (A\land B)^f, (A\land B)^p]
  \end{array}
\]
\begin{answer}
Yes, the consequence relation holds.
\end{answer}
\subsection{Example cs6}

\begin{problem}
Is the consequence relation \[
[(A\lor B)^t]\vdash [A^t]\]
 valid?
\end{problem}
The problem is equivalent to proving the following sequent:
\[\begin{array}{l}
[A^t, (A\lor B)^f, (A\lor B)^p]
  \end{array}
\]
\begin{answer}
No, the consequence relation does not hold.
\end{answer}
List of counter-examples:
\[\begin{array}{l}
[A^f, B^t]\\\relax
[A^p, B^t]
  \end{array}
\]
\section{Validity of Formulas}

\subsection{Example f1}

\begin{problem}
Let $\{t\}$ be the set of designated truth values. Is the formula $(A\supset (B\supset A))$ valid?
\end{problem}
The problem is equivalent to proving the following sequent:
\[\begin{array}{l}
[(A\supset (B\supset A))^t]
  \end{array}
\]
\begin{answer}
Yes, the formula is valid.
\end{answer}
\subsection{Example f2}

\begin{problem}
Let $\{p\}$ be the set of designated truth values. Is the formula $(A\supset (B\supset A))$ valid?
\end{problem}
The problem is equivalent to proving the following sequent:
\[\begin{array}{l}
[(A\supset (B\supset A))^p]
  \end{array}
\]
\begin{answer}
No, the formula is not valid.
\end{answer}
List of counter-examples:
\[\begin{array}{l}
[A^f, B^f]\\\relax
[A^f, B^p]\\\relax
[A^f, B^t]\\\relax
[A^p]\\\relax
[A^t, B^f]\\\relax
[A^t, B^p]\\\relax
[A^t, B^t]
  \end{array}
\]
\subsection{Example f3}

\begin{problem}
Let $\{f,t\}$ be the set of designated truth values. Is the formula $((A\lor \neg A)\supset (A\land \neg A))$ valid?
\end{problem}
The problem is equivalent to proving the following sequent:
\[\begin{array}{l}
[((A\lor \neg A)\supset (A\land \neg A))^f, ((A\lor \neg A)\supset (A\land \neg A))^t]
  \end{array}
\]
\begin{answer}
Yes, the formula is valid.
\end{answer}
\section{Consequence Relation on Formulas}

\subsection{Example cf1}

\begin{problem}
Let $\{t\}$ be the set of designated truth values. Is the consequence relation \[
(X\supset Y), 
X\vdash Y\]
 valid?
\end{problem}
The problem is equivalent to proving the following sequent:
\[\begin{array}{l}
[X^f, X^p, Y^t, (X\supset Y)^f, (X\supset Y)^p]
  \end{array}
\]
\begin{answer}
Yes, the consequence relation holds.
\end{answer}
\subsection{Example cf2}

\begin{problem}
Let $\{p\}$ be the set of designated truth values. Is the consequence relation \[
(X\supset Y), 
X\vdash Y\]
 valid?
\end{problem}
The problem is equivalent to proving the following sequent:
\[\begin{array}{l}
[X^f, X^t, Y^p, (X\supset Y)^f, (X\supset Y)^t]
  \end{array}
\]
\begin{answer}
No, the consequence relation does not hold.
\end{answer}
List of counter-examples:
\[\begin{array}{l}
[X^p, Y^f]
  \end{array}
\]
\subsection{Example cf3}

\begin{problem}
Let $\{p,t\}$ be the set of designated truth values. Is the consequence relation \[
(X\supset Y), 
X\vdash Y\]
 valid?
\end{problem}
The problem is equivalent to proving the following sequent:
\[\begin{array}{l}
[X^f, Y^p, Y^t, (X\supset Y)^f]
  \end{array}
\]
\begin{answer}
No, the consequence relation does not hold.
\end{answer}
List of counter-examples:
\[\begin{array}{l}
[X^p, Y^f]
  \end{array}
\]
\subsection{Example cf4}

\begin{problem}
Let $\{t\}$ be the set of designated truth values. Is the consequence relation \[
X\vdash (X\lor Y)\]
 valid?
\end{problem}
The problem is equivalent to proving the following sequent:
\[\begin{array}{l}
[X^f, X^p, (X\lor Y)^t]
  \end{array}
\]
\begin{answer}
Yes, the consequence relation holds.
\end{answer}
\section{Validity of Equations}

\subsection{Example e1}

\begin{problem}
Is the equation $\neg \neg A=A$ valid?
\end{problem}
The problem is equivalent to proving the following sequents:
\[\begin{array}{l}
[A^p, A^t, \neg \neg A^f]\\\relax
[A^f, A^t, \neg \neg A^p]\\\relax
[A^f, A^p, \neg \neg A^t]
  \end{array}
\]
\begin{answer}
Yes, the equation is valid.
\end{answer}
\section{Validity of Quasi-Equations}

\subsection{Example qe1}

\begin{problem}
Is the quasi-equation \[
A=B, 
B=C\vdash A=C\]
 valid?
\end{problem}
\begin{answer}
Yes, the quasi-equation is valid.
\end{answer}
\subsection{Example qe2}

\begin{problem}
Is the quasi-equation \[
A=B, 
C=D\vdash A=D\]
 valid?
\end{problem}
The problem is equivalent to proving the following sequents:
\[\begin{array}{l}
[A^f, A^t, B^f, B^t, C^p, C^t, D^p, D^t]\\\relax
[A^f, A^p, B^f, B^p, C^p, C^t, D^p, D^t]\\\relax
[A^p, A^t, B^p, B^t, C^f, C^t, D^f, D^t]\\\relax
[A^f, A^p, B^f, B^p, C^f, C^t, D^f, D^t]\\\relax
[A^p, A^t, B^p, B^t, C^f, C^p, D^f, D^p]\\\relax
[A^f, A^t, B^f, B^t, C^f, C^p, D^f, D^p]
  \end{array}
\]
\begin{answer}
No, the quasi-equation is not valid.
\end{answer}
List of counter-examples:
\[\begin{array}{l}
[A^f, B^f, C^p, D^p]\\\relax
[A^f, B^f, C^t, D^t]\\\relax
[A^p, B^p, C^f, D^f]\\\relax
[A^p, B^p, C^t, D^t]\\\relax
[A^t, B^t, C^f, D^f]\\\relax
[A^t, B^t, C^p, D^p]
  \end{array}
\]
\end{document}
