%        File: 11-03-2021.tex
%     Created: 10:16:20 Wed, 03 Nov 2021 EDT
% Last Change: 10:16:20 Wed, 03 Nov 2021 EDT
%
\documentclass[letterpaper]{article}
\usepackage{amsmath}
\usepackage{graphicx}
\usepackage{cancel}
\usepackage{amssymb}
\usepackage{listings}
\usepackage[shortlabels]{enumitem}
\usepackage{soul}
%\usepackage[smartEllipses,hashEnumerators,hybrid]{markdown}
\usepackage{minted}
\usepackage{geometry}
\usepackage{dirtytalk}
\usepackage{lplfitch}

\geometry{portrait, margin=1in}

%\begin{minted}[linenos,bgcolor=LightGray]{[language]}

\date{11/03/2021}
\title{%
        Expanded TFL Proofs\\
    \large PHIL--205--01:Symbolic Logic}
\author{Blizzard MacDougall}
\begin{document}
\maketitle
\pagenumbering{arabic}
Below is a complete list of available rules for TFL Proofs.
\section{Conjunction $\land$ Rules}

\subsection{$\land$ Elim}
\fitchctx
{
    \pline[m.]{A\land B}\\
    \pline[n.]{A}[\lande{m}]
}
\subsection{$\land$ Intro}
\fitchctx
{
    \pline[m.]{A}\\
    \pline[n.]{B}\\
    \pline[r.]{A\land B}[\landi{m, n}]
                
}
\section{Disjunction $\lor$ Rules}
\subsection{$\lor$ Intro}
\fitchctx
{
    \pline[m.]{A}\\
    \pline[n.]{A\lor B}[\lori{m}]
            
}
\subsection{$\lor$ Elim}
\fitchctx
{
    \pline[m.]{A\lor B}\\
    \subproof
    {
        \pline[i.]{A}
    }
    {
        \pline[j.]{C}
    }
    \subproof
    {
        \pline[k.]{B}
    }
    {
        \pline[l.]{C}
    }
    \pline[r.]{C}[\lore{m}{i--j}{k--l}]
}

\section{Conditional $\rightarrow$ Rules}
\subsection{$\rightarrow$ Elim (\textit{Modus Ponens})}
\fitchctx
{
    \pline[m.]{P\lif Q}\\
    \pline[n.]{P}\\
    \pline[r.]{Q}[\life{m}{n}]
}
Note that order in the reference is important. You must first reference the conditional before referencing the anticedent.

\subsection{$\rightarrow$ Intro}
\fitchctx
{
    \subproof
    {
        \pline[i.]{A}
    }
    {
        \pline[j.]{B}
    }
    \pline[r.]{A\lif B}[\lifi{i--j}]
}

\section{Biconditional $\leftrightarrow$ Rules}
\subsection{$\leftrightarrow$ Intro}
\fitchctx
{
    \subproof
    {
        \pline[i.]{A}
    }
    {
        \pline[j.]{B}
    }
    \subproof
    {
        \pline[k.]{B}
    }
    {
        \pline[l.]{A}
    }
    \pline{A\liff B}[\liffi{i--j}{k--l}]
}
\subsection{$\leftrightarrow$ Elim}
\fitchctx
{
    \pline[m.]{A\liff B}\\
    \pline[n.]{A}\\
    \pline[r.]{B}[\liffe{m}{n}]
}

As with $\rightarrow$'s reference, first list the biconditional, then the condition.

\section{Negation $\neg$ Rules}
\subsection{$\neg$ Elim}
Any double negation can be eliminated.

\subsection{$\bot$ Intro}
This is proven by showing a contradiction.\\
\fitchctx
{
    \pline[1.]{P}\\
    \pline[2.]{\neg P}\\
    \pline[3.]{\lfalse}
}
\subsection{$\neg$ Intro}
We have to prove this by proof by contradiction. (Shown below)\\
\fitchctx
{
    \subproof
    {
        \pline[1.]{P}
    }
    {
        \pline[2.]{\lfalse}
    }
    \pline[3.]{\neg P}[\lfalsei{1--2}]
}

\subsection{Explosions}
\fitchctx
{
    \pline[m.]{\lfalse}\\
    \pline[r.]{A}[\textbf{X:} m]
}
Anything can be proven after a contradiction.

\subsection{Tertium non datur}
Latin for \say{no third way}.\\
\fitchctx
{
    \subproof
    {
        \pline[i.]{A}
    }
    {
        \pline[j.]{B}
    }
    \subproof
    {
        \pline[k.]{\lnot A}
    }
    {
        \pline[l.]{B}
    }
    \pline[r.]{B}[\textbf{TND:} i--j, k--l]
}

\section{New Additions}
\subsection{Disjunctive Syllogism}
\fitchctx
{
    \pline[m.]{P\lor Q}\\
    \pline[n.]{\lnot Q}\\
    \pline[r.]{P}[\textbf{DS:} 1, 2]
}
\subsection{Modus Tollens}
\fitchctx
{
    \pline[m.]{P\lif Q}\\
    \pline[n.]{\lnot Q}\\
    \pline[r.]{\lnot P}[\textbf{MT:} 1, 2]
}
\section{Example Theorem Proofs}
\subsection{Frege's Theorem}
\fitchprf
{}
{
    \subproof
    {
        \pline[1.]{P\lif (Q\lif R)}
    }
    {
        \subproof
        {
            \pline[2.]{P\lif Q}
        }
        {
            \subproof
            {
                \pline[3.]{P}
            }
            {
                \pline[4.]{Q\lif R}[\life{1}{3}]\\
                \pline[5.]{Q}[\life{2}{3}]\\
                \pline[6.]{R}[\life{4}{5}]
            }
            \pline[7.]{P\lif R}[\lifi{3--6}]
        }
        \pline[8.]{(P\lif Q)\lif(P\lif R)}[\lifi{2--7}]
    }
    \pline[9.]{(P\lif (Q\lif R))\lif((P\lif Q)\lif(P\lif R))}[\lifi{1--8}]
}
\end{document}