\chapter{Basic Logic}

{\bf{Primitive.}} The name $\mname{Eps\_i}$ is a primitive term of type ${{({{\iota}\unicdbdjdcd{o}})}\unicdbdjdcd{\iota}}$.
Specifically it is ``Primitive 0'' in the Proofgold Egal theory.

\begin{axiom}\label{ax:feahdhpfjgpfbgih} ${\unicdcdadad P : {{\iota}\unicdbdjdcd{o}} .  {\unicdcdadad x : {\iota} .  {{{P}~{x}}\unicdbdjdcd{{P}~{({{\mname{Eps\_i}}~{P}})}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & c3f0de4cb966012957ca752938aa96a32c594389e7aea45227d571c0506618ba \\
Pure Prop Address: & TMaqNdrw1xUUqfmGqr4T5HNsS6X1kThiGJp \\
Theory Prop Id: & 756d6e520a540dee983a2bc983f030fca1e15bc5c01cd10daa59ba9846775a89 \\
Theory Prop Address: & TMZeDQEPZjtPy34irdW6qoDmhfGuT9rLoo3
\end{tabular}
\end{center}

\end{axiom}
\begin{definition}\label{def:efchfhfg}
We define $\mname{True}$ to be ${\unicdcdadad p : {o} .  {{p}\unicdbdjdcd{p}}}$ of type ${o}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & f81b3934a73154a8595135f10d1564b0719278d3976cc83da7fda60151d770da \\
Pure Object Address: & TMXh1PeTNoRdeQMkipsnTZ1NBoLMCSQGszg \\
Theory Object Id: & 94e6a74d7fb4010e37ca58528b5eefb6d84e85f0fcd9598afcfdb3000334a38a \\
Theory Object Address: & TMdZywkjk5BP16zSdFbfK4CcoVzmBS54DHA
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:gebgmgdhfg}
We define $\mname{False}$ to be ${\unicdcdadad p : {o} .  {p}}$ of type ${o}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 1db7057b60c1ceb81172de1c3ba2207a1a8928e814b31ea13b9525be180f05af \\
Pure Object Address: & TMVcBGjSsw48XJ4L45VWUk51f7pywF6kvVX \\
Theory Object Id: & 266ad502104b0eadbdf70b5ce22ec14cce255c0b312cfc3719813f538ed6de1b \\
Theory Object Address: & TMZx4Q2psRTfsQjwWdVEVQnyn3ZRxXosKPq
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:ogpgeh}
We define $\mname{not}$ to be ${\uniddcgcg A : {o} .  {{A}\unicdbdjdcd{\mname{False}}}}$ of type ${{o}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & f30435b6080d786f27e1adaca219d7927ddce994708aacaf4856c5b701fe9fa1 \\
Pure Object Address: & TMWAvR96ZU4RCj94CSoZhrtMR5rdaTaLB5R \\
Theory Object Id: & 0dc3c779c7cc720c63503b5ae618908388fe9f8ef7b20ce33a5baa0de6389c1b \\
Theory Object Address: & TMJJZawymNdUcMFLBwRqSW8DSQsHg76ans7
\end{tabular}
\end{center}

\end{definition}
{\bf{Notation.}} We use $\preoh{-}$ as a prefix operator  corresponding to applying term ${\mname{not}}$.
\begin{definition}\label{def:bgogeg}
We define $\mname{and}$ to be ${\uniddcgcg A B : {o} .  {\unicdcdadad p : {o} .  {{({{A}\unicdbdjdcd{{B}\unicdbdjdcd{p}}})}\unicdbdjdcd{p}}}}$ of type ${{o}\unicdbdjdcd{{o}\unicdbdjdcd{o}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 2ba7d093d496c0f2909a6e2ea3b2e4a943a97740d27d15003a815d25340b379a \\
Pure Object Address: & TMHVPoyLuccMxozW2JkzTcKaFNorhQvcqVz \\
Theory Object Id: & 37da83639bcf9d8c8a37734df867cfc15d7d22573b6c8ccfc52e5c2e7a5abc81 \\
Theory Object Address: & TMMEUAXx5wQ61b6khohvEMcR5eUbjjJSYAw \\
\end{tabular}
\end{center}
\end{definition}
{\bf{Notation.}} We use $\infpcmf$ as a left associative infix operator  corresponding to applying term ${\mname{and}}$.
\begin{definition}\label{def:pgch}
We define $\mname{or}$ to be ${\uniddcgcg A B : {o} .  {\unicdcdadad p : {o} .  {{({{A}\unicdbdjdcd{p}})}\unicdbdjdcd{{({{B}\unicdbdjdcd{p}})}\unicdbdjdcd{p}}}}}$ of type ${{o}\unicdbdjdcd{{o}\unicdbdjdcd{o}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 9577468199161470abc0815b6a25e03706a4e61d5e628c203bf1f793606b1153 \\
Pure Object Address: & TMRrSAiwhsGG8gNN8EukN1zLVibyVKQXaFq \\
Theory Object Id: & 86ae6491fbd8f20f1f7e4986f09463cdcc489bdedfda845c840df66cb8f76edb \\
Theory Object Address: & TMbacaYWYcRwAFxG4ALNMm3EyDKWEtRrh42
\end{tabular}
\end{center}

\end{definition}
{\bf{Notation.}} We use $\infmfpc$ as a left associative infix operator  corresponding to applying term ${\mname{or}}$.
\begin{definition}\label{def:jggggg}
We define $\mname{iff}$ to be ${\uniddcgcg A B : {o} .  {{{\mname{and}}~{({{A}\unicdbdjdcd{B}})}}~{({{B}\unicdbdjdcd{A}})}}}$ of type ${{o}\unicdbdjdcd{{o}\unicdbdjdcd{o}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 98aaaf225067eca7b3f9af03e4905bbbf48fc0ccbe2b4777422caed3e8d4dfb9 \\
Pure Object Address: & TMNPkfzmoJmg4Qsbe28fcbyaXL1XTynPhik \\
Theory Object Id: & 6588e5a76078e7919b50307e23503d854af1b869a2eedd6b091f6610609777ba \\
Theory Object Address: & TMc6fJsUiuiG3KCWP4EAREq7NWM56fQqJHi
\end{tabular}
\end{center}

\end{definition}
{\bf{Notation.}} We use $\infmdncod$ as an infix operator  corresponding to applying term ${\mname{iff}}$.

