531 lines
38 KiB
TeX
531 lines
38 KiB
TeX
% !TeX spellcheck = en_US
|
||
\documentclass[10pt,a4paper]{article}
|
||
|
||
\include{./header.tex}
|
||
|
||
\title{Completeness Proof for different logical frameworks
|
||
\\[1ex] \large Notes on my 3 month internship at Faculty of Informatics (ELTE, Budapest)}
|
||
\hypersetup{pdftitle={Completeness Proof for different kinds of logical frameworks}}
|
||
\author{Samy Avrillon, supervised by
|
||
\\[1ex] Ambrus Kaposi (ELTE, Budapest)
|
||
\\[1ex] and Thorsten Altenkirsch (University of Notthingham, United Kingdom)}
|
||
|
||
\begin{document}
|
||
\doparttoc
|
||
\maketitle
|
||
|
||
\hsep
|
||
|
||
\tableofcontents
|
||
|
||
\newpage
|
||
|
||
|
||
\section{Introduction}
|
||
|
||
In the first place, i was supposed to do this internship in Nottingham (UK) with Thorsten Altenkirsh. But, because of administrative issues, i was not able to go there, and Thorsten Altenkirsh contacted Ambrus Kaposi in Budapest, whose university agreed to accept me. Therefore, i went to Budapest and i did the internship under the physical supervision of Ambrus Kaposi, and the remote supervision of Thorsten Altenkirsch.
|
||
|
||
The original subject of the internship was \enquote{Developping a simplified account of normalization by evaluation using the theory of categories with families}. But there was a lot to do, starting with learning how to use Agda.
|
||
|
||
\subsection{Introduction to the problem}
|
||
What i do call a \enquote{logic} is a set of definitions containing formulæ and a notion of provability of those formulæ, plus a set of operators/equalities to construct or reduce these rules. I have studied the most common logical frameworks, that is, Propositional Logic, First-order logic with infinitary predicates, and Predicate Logic. For each of those logics, one can define a notion of \emph{model}. A model of a certain kind of logic is something that implements all of the logic's definitions, operators and equalities. From all of those models, one can extract the \emph{initial model}, also called \emph{syntax}. It is the smallest of all models, which means that from any model of that logic, we have a morphism from the syntax to that model.
|
||
|
||
Then, our goal is for each logic to prove the completeness of a specific class of models. Completeness can be stated as such: \enquote{For any formula that is \emph{true} in all models of the specified class, then the formula has a proof in the syntax}. By being true in the model, one can understand that the formula has a proof from the model.
|
||
\subsection{Motivation}
|
||
Ambrus is currently studying Second Order Generalized Algebraic Theories (or SOGAT) and he is trying to state a better definition than that first defined in Taichi Uemura's thesis \cite{UemuraThesis2021}. He also wants to write a paper with examples to show why they are useful, and adding some examples for different frameworks of logic can help with that.
|
||
\subsection{Structure of this report}
|
||
\section{Propositional Logic}
|
||
\subsection{Propositional Logic as a SOGAT}
|
||
|
||
The first and most simple logical framework we can work with is that of Propositional Logic (refered as Zero Order Logic or ZOL in the code). We also work in the most simple framework in which we only have one axiom rule for creating formulæ: the $\iota$ rule. Propositional Logic is usually done with a fixed set of propositional variables instead of only one that is fixed, but adding them does not make the construction more interesting, only more complicated.
|
||
|
||
In order to state all the definitions, functions and more importantly, all the equalities that a model of Propositional Logic has to verify, we will write down Propositional Logic as a SOGAT. It goes as described in \autoref{fig:zol-sogat}.
|
||
|
||
\begin{figure}
|
||
\begin{tcolorbox}
|
||
\[
|
||
\begin{array}{lcl}
|
||
\For & : & \Set \\
|
||
- \implies - & : & \For \rightarrow \For \rightarrow \For\\
|
||
ι & : & \For \\
|
||
\\
|
||
\Pf & : & \For \rightarrow \Prop^+ \\
|
||
\lam & : & (\Pf A \rightarrow^+ \Pf B) \rightarrow \Pf (A \implies B)\\
|
||
\app & : & \Pf (A \implies B) \rightarrow (\Pf A \rightarrow \Pf B)
|
||
\end{array}
|
||
\]
|
||
\end{tcolorbox}
|
||
\caption{ZOL Sogat Presentation}
|
||
\label{fig:zol-sogat}
|
||
\end{figure}
|
||
|
||
We can see that in this Sogat, we have two sorts ($\For$ and $\Pf$), each of which have two constructors. Although SOGATs can have equations in them, i won't use any in that report.
|
||
|
||
A keen eye may have seen that there should be a problem with the \lam constructor. Its type is indeed not strictly positive (i.e. the type \Pf appears to the left of an arrow in the arguments of the constructor). That's why we use a ${}^+$ on the arrow, and we use the same ${}^+$ on the sort of \Pf. These arrow means that \Pf should be \emph{locally representable}. It basically means that we have to use \emph{proof variables} to implement this SOGAT.
|
||
|
||
\subsection{From a SOGAT to GAT}
|
||
|
||
|
||
Unfortunately, Agda cannot understand SOGATs directly (yet). So we have to convert this SOGAT into a GAT. I will describe the process in this section, each line of the SOGAT giving birth to a set of sorts, constructors and equations in the GAT.
|
||
|
||
The first thing we need to define any SOGAT-derived GAT is a base category with a terminal object. We will call \emph{contexts} the objects of this category and \emph{substitutions} the morphisms of the category.
|
||
|
||
You can see that the equations for the category ($\circ$-associativity, identity to the right and to the left) have not been written down. This is because substitutions are defined as \AgdaPrimitive{Prop}s and not \AgdaPrimitive{Set}s. The difference between those two kinds of objects is that the former are said to be \emph{proof-irrelevant}. You can understand it as \enquote{there is at most one object into a type that is in prop}. Therefore, the equality described above are trivially true, because any substitution from $\Gamma$ to $\Delta$ is equal to any other substitution from $\Gamma$ to $\Delta$. This trick of using \AgdaPrimitive{Prop} instead of \AgdaPrimitive{Set} will be used through the report, and it will allow us to write down (and prove) a lot less equations.
|
||
|
||
\begin{tcolorbox}
|
||
\agda{agda/ZOL-1.tex}
|
||
\end{tcolorbox}
|
||
|
||
Once we have our base category, we can start to describe the sorts ze have in our SOGAT. Every sort from the SOGAT will be translated into a functor from our base category to \AgdaPrimitive{Set} or \AgdaPrimitive{Prop}. Therefore, we have to define an action on objects, an action on morphisms (we will always write contra-variant, and we will use the $\_[\_]$ notation), and some equalities that we will call \emph{functorality} or \enquote{\textit{Type} respects substitution}
|
||
|
||
\begin{tcolorbox}
|
||
\agda{agda/ZOL-3.tex}
|
||
\agdasep
|
||
\agda{agda/ZOL-4.tex}
|
||
\end{tcolorbox}
|
||
|
||
Now, we will translate the ${}^+$ in the type of proofs. As i said before, this translates into the fact that we have \emph{proof variables}. Therefore, we should be able to move from a context to another context in which we added a variable. We call that \emph{context extension}. For proof-variables, this context extension takes a parameter, as the proof-variables have a \enquote{type} (which is the formula that they prove).
|
||
|
||
With those context extensions, we also have to add a way to extend substitutions (which are the morphisms from the base category). We do that by adding a \emph{comma} operator that takes a substitution and a proof and which extends the goal of the substitution. (If we see a proof context as a list of formulæ and a proof substitution as a list of proofs, then we are only adding one proof to the list). We also need to be able to extract the proof and the base substitution from a substitution into an extended context (called \emph{weakening} operation). Therefore, we add two $\pi$ projections that extract the data from the substitution. We also need some equalities, that are saying that $(\pi_p¹ , \pi_p²)$ and $,_p$ are reciprocal, plus one equality saying that thet comma operator also transposes the substitution. But as both \AgdaField{Pf} and \AgdaField{Sub} are in Prop, those equations are unneeded.
|
||
|
||
\begin{tcolorbox}
|
||
\agda{agda/ZOL-5.tex}
|
||
\end{tcolorbox}
|
||
|
||
The last step is to add the constructors of our objects into the algebra. We write them directly as they were presented in the SOGAT, except for the new \AgdaField{Con} parameter that we need to add to everything. We also need to add one equation for each constructor saying that the constructors do respects substitutions. And we don't add any for \AgdaField{Pf} constructors as they are unneeded as \AgdaField{Pf} are in \AgdaPrimitive{Prop}.
|
||
|
||
The only one we cannot translate directly is the $\rightarrow^+$ from the $\AgdaField{lam}$ constructor from the SOGAT. Well, to translate this \emph{locally representable application}, we only transform the parameter of the arrow into a context extension of the appropriate type. Therefore, a function $\Pf A \rightarrow^+ \Pf B$ only becames a proof $\Pf (\Gamma \triangleright_p A)\; B$ (except that we have to transform B that is a $\For\;\Gamma$ into a $\For\;(\Gamma \triangleright_p A)$, and for that, we use the \emph{weakening} substitution $\text{\AgdaField{$\pi_p^1$}}\;\text{\AgdaField{id}}\;:\;\AgdaField{Sub}\;\Gamma\;(\Gamma \triangleright_p X)$ for any Γ-formula $X$
|
||
|
||
\begin{tcolorbox}
|
||
\agda{agda/ZOL-8.tex}
|
||
\agdasep
|
||
\agda{agda/ZOL-9.tex}
|
||
\agdasep
|
||
\agda{agda/ZOL-11.tex}
|
||
\end{tcolorbox}
|
||
|
||
We now have completed our definition of a model for Propositional Logic, in the SOGAT setting. We can also define (categorical) morphisms between models. They are composed of mappings for every sort of the GAT, plus equations for the categorical objects (terminal object, identity and composition), for the action of the functors on morphisms ($[]f$ and $[]p$) and finally equations to say that the constructors are also transported. A lot of those equation are not written because \AgdaField{Pf} and \AgdaField{Sub} are in \AgdaPrimitive{Prop}.
|
||
\begin{tcolorbox}
|
||
\agda{agda/ZOL-13.tex}
|
||
\agdasep
|
||
\agda{agda/ZOL-15.tex}
|
||
\end{tcolorbox}
|
||
|
||
\subsection{Finding a strict Syntax}
|
||
|
||
What will be the use of these morphisms ? One thing we want to do is to find the \emph{initial} syntax for this class of models. It means, we want to find a model from which, for any model $M$, there exists one and only one morphism from this model to $M$. We can also call the syntax the \emph{minimal model}, as it is the model that contains just the objects something needs to be a model of Propositional Logic.
|
||
|
||
Mathematically, this model is really easy to find. We only have to take all the sorts defined in the GAT and apply a quotient on every equations of the GAT. But this is not really interesting, as the defined model would not be \emph{strict}, meaning that all of the equations are definitional. Having only strict definition for objects allows us to study completeness in a much better framework, as we can, for example, do an induction on the types as they are defined in the syntax.
|
||
|
||
So we have three things to do :
|
||
\begin{enumerate}
|
||
\setlength{\itemsep}{-1ex}
|
||
\item Create a model $I$ for Propositional Logic that we think is minimal
|
||
\item For any other model $M$, create a morphism $m_I : I \to M$
|
||
\item Show that any morphism $I \to M$ is equal to $m_I$
|
||
\end{enumerate}
|
||
|
||
Let's get started. This framework of Propositional logic has one property that we can make use of to make the construction of the syntax much more simpler. (Actually, we don't know if we could have made the syntax with this method if we haven't had this property. We will try to investigate it further in the future) This property is that Formula doesn't depend on contexts. One can understand it as \enquote{a formula is the same whichever are the proof variables associated with it, as it doesn't use any of them}. Without this property, we would have to define mutually every sort of our theory, which would be awfully complicated.
|
||
|
||
Contexts also only have two constructors in the GAT, the terminal object of the category or created from a proof context extension.
|
||
|
||
Our first step is to define our sorts, no difficulty, we only make one datatype constructor for each constructor in the SOGAT or in the GAT. For contexts, the only two constructors are as the terminal object of the base category, or as a context extension of another context. That's where we use the fact that Formulæ don't depend on Contexts, it allows us to define \AgdaDatatype{For} and \AgdaDatatype{Con} separately, but also to define \AgdaDatatype{Pf} and \AgdaOperator{Sub} separately (as in the algebra, the \AgdaField{lam} constructor refers to \AgdaOperator{\_[\_]f}, which is removed when formulæ doesn't depend on contexts). There is also another special constructor for proofs, which is that of proof variables, and which corresponds to the \enquote{constructor} which is \AgdaField{$\pi_p^2$}
|
||
|
||
\begin{tcolorbox}
|
||
\agda{agda/ZOL-I-1.tex}
|
||
\agdasep
|
||
\agda{agda/ZOL-I-3.tex}
|
||
\end{tcolorbox}
|
||
|
||
The next step is to define substitutions. But we will first define a weaker property than substitution called \enquote{renamings}. The two definition are put one next to the other, and we can see that when \AgdaDatatype{Sub} are a list of complete proofs, \AgdaDatatype{Ren} are only a list of Proof variables (or direct proof assumed from the contexts). This weaker form of substitution is needed to define the identity substitution, as we cannot directly define it recursively for fully-featured substitutions.
|
||
|
||
The projections are simply a pattern-matching against the datatype.
|
||
|
||
\begin{tcolorbox}
|
||
\agda{agda/ZOL-I-4.tex}
|
||
\agdasep
|
||
\agda{agda/ZOL-I-6.tex}
|
||
\agda{agda/ZOL-I-7.tex}
|
||
\end{tcolorbox}
|
||
|
||
Because we need to refer to \AgdaField{id}, and more precisely to \AgdaField{$\pi_p^1 id$} in the notion of proof substitution, we first define proof \emph{renamings} so we can define \AgdaOperator{wkSub} (which is the same as \AgdaField{$\pi_p^1 id$}) and only after that, we define fully featured substitution.
|
||
|
||
\begin{tcolorbox}
|
||
\agda{agda/ZOL-I-9.tex}
|
||
\agdasep
|
||
\agda{agda/ZOL-I-10.tex}
|
||
\end{tcolorbox}
|
||
|
||
The last step is then to define substitution composition, which is only applying the second part of the substitution to every element of the first part.
|
||
|
||
\begin{tcolorbox}
|
||
\agda{agda/ZOL-I-11.tex}
|
||
\end{tcolorbox}
|
||
|
||
And we now have a working model for Propositional Logic. We can implement our previously defined record, and all the equation can be directly understood by Agda (\AgdaInductiveConstructor{refl} is enough proof)
|
||
|
||
I won't dive into the contsruction of the initial morphism and the proof that it is unique, because it is a bit ugly because of some \emph{transport hell} (see \autoref{sec:transport-hell} for an explanation of the issue).
|
||
|
||
Still, i give you the construction of the Con and For mappings, as they show the basic idea of these construction. The idea is simple, you pattern-match against the datatype definition of your Sort in your syntax, and for each constructor, you call the corresponding one in the algebra.
|
||
|
||
And the uniqueness proof is pretty simple again because you only need to prove that the \AgdaDatatype{Con} and \AgdaDatatype{For} mappings are unique, because the other ones are in \AgdaPrimitive{Prop}, so they are automatically unique. And to prove the unicity, you split again on the sort's datatype and for each constructor, you use the fact that a morphism preserves constructors, and you have a nice proof by recursion (except it's ugly because of transport hell).
|
||
|
||
\begin{tcolorbox}
|
||
\agda{agda/ZOL-I-13.tex}
|
||
\end{tcolorbox}
|
||
|
||
\subsection{Stating and Proving Completeness}
|
||
|
||
Now that we have our syntax, we can try to state and prove completeness in our specific categorical framework.
|
||
|
||
The general idea of completeness proofs is to take a class of model (here we will take Kripke Models), and to state that for any formlæ that has a proof in every Kripke model, then it has a proof in the syntax. The other direction is called \emph{soundness}, but we already have proven that when we created our initial morphism. This morphism can indeed turn proofs in the syntax into proofs in any model.
|
||
|
||
This completeness proof is often done by taking some specific model of the class that is said to be \emph{universal}, and by showing that you can go between proofs in the universal model and proofs from the syntax freely. We often try to distinguish two reciprocal functions: \AgdaOperator{quote} that turns a proof from the syntax into a proof in the kripke model, and an \AgdaOperator{unquote} function that does the converse.
|
||
|
||
In order to state this into our categorical layout, we will use an other mapping going from the initial model to our Kripke model that is called the \emph{Yoneda mapping}. TODO explain what is the yoneda mapping, and why it does a completeness proof.
|
||
|
||
\begin{center}
|
||
\begin{tikzpicture}[thick, scale=5]
|
||
\node at (-1,0) (nI) {$\mathcal{I}$};
|
||
\node at (1,0) (nU) {$\mathcal{U}$};
|
||
|
||
\draw[->] (nI) to[bend left] node[midway,above,inner sep=1ex] {$\llbracket\_\rrbracket$} (nU);
|
||
\draw[->] (nI) to[bend right] node[midway,below,inner sep=1ex] {$y$} (nU);
|
||
|
||
\node at (-.15,+.25) (I0) {};
|
||
\node at (-.15,-.25) (Y0) {};
|
||
\draw[->,double distance=.4ex] (I0) to node[midway,left,inner sep=1ex] {$u$} (Y0);
|
||
\node at (+.15,+.25) (I1) {};
|
||
\node at (+.15,-.25) (Y1) {};
|
||
\draw[->,double distance=.4ex] (Y1) to node[midway,right,inner sep=1ex] {$q$} (I1);
|
||
\end{tikzpicture}
|
||
\end{center}
|
||
|
||
\section{First order logic (or Predicate Logic)}
|
||
|
||
In this part, we will try to implemeent the same as we did for Propositional Logic, but this time for Predicate Logic. We again work in a simpler layout where we don't have function symbols and only have one binary relation \AgdaField{R}. And again, adding relation and function symbols don't add a lot of new interesting content, but makes everything less readable and more complex to use.
|
||
|
||
\subsection{Infinitary First Order Logic}
|
||
|
||
A really naive version of first order logic can be done by implementing $\forall$ as a infinitary \enquote{and} operator. I have implemented this solution, and we can look at what it added to the code.
|
||
|
||
The trick is to use an external set of terms, that is a parameter of the algebra (and therefore of all the models). This external set is called $\operatorname{TM}$.
|
||
|
||
The SOGAT for this new logic is given in \autoref{fig:ifol-sogat}. We can see that we added one constructor for Formulæ: $\forall$ that takes as input a function from our external $\operatorname{TM}$ to formulæ, and make this a formula. We also add the introduction and elimination rule for $\forall$. We don't need to put a plus on this arrow as the set on which the recurring is external, so we don't have any strict positivity problem.
|
||
|
||
\begin{figure}
|
||
\begin{tcolorbox}
|
||
\[
|
||
\begin{array}{lcl}
|
||
\For & : & \Set \\
|
||
- \implies - & : & \For \rightarrow \For \rightarrow \For\\
|
||
\forall & : & (\operatorname{TM} \rightarrow \For) \rightarrow \For \\
|
||
\R & : & \operatorname{TM} \rightarrow \operatorname{TM} \rightarrow \For\\
|
||
\\
|
||
\Pf & : & \For \rightarrow \Prop^+ \\
|
||
\lam & : & (\Pf A \rightarrow^+ \Pf B) \rightarrow \Pf (A \implies B)\\
|
||
\app & : & \Pf (A \implies B) \rightarrow (\Pf A \rightarrow \Pf B)\\
|
||
\foralli & : & (t : \operatorname{TM} \rightarrow \Pf A\;t) \rightarrow \Pf (\forall A)\\
|
||
\foralle & : & \Pf (\forall A) \rightarrow (t : \operatorname{TM}) \rightarrow \Pf (A\;t)\\
|
||
\end{array}
|
||
\]
|
||
\end{tcolorbox}
|
||
\caption{IFOL Sogat Presentation}
|
||
\label{fig:ifol-sogat}
|
||
\end{figure}
|
||
|
||
Therefore, the GAT we deduce from this is not really harder, we only add the operators as we described them in the SOGAT, while still adding the functorality equalities for the types that are not in \AgdaPrimitive{Prop}.
|
||
|
||
\begin{tcolorbox}
|
||
\agda{agda/IFOL-1.tex}
|
||
\agdasep
|
||
\agda{agda/IFOL-3.tex}
|
||
\end{tcolorbox}
|
||
|
||
The same goes to add the constructors from the syntax, this is pretty straightforward. We add a simple constructor taking a function from $\operatorname{TM}$ to \AgdaDatatype{For}, and two proofs constructors which don't break strict positivity as $\forall i$ takes as input a \enquote{list of proofs indexed by TM}.
|
||
|
||
We also need to add cases for proof substitutions but they are really trivial cases. The same goes for the initial morphism and the proof of initiality, feel free to look at the code if you want to check it.
|
||
|
||
\begin{tcolorbox}
|
||
\agda{agda/IFOL-I-1.tex}
|
||
\agdasep
|
||
\agda{agda/IFOL-I-3.tex}
|
||
\end{tcolorbox}
|
||
|
||
And Completeness proof is not harder, we just have to add Kripke interpretation of this external forall, which is very natural, and we also need to add the following lines to our $u$ and $q$ definition so we get all cases done.
|
||
|
||
\begin{tcolorbox}
|
||
TODO add the lines described above, need to refer to what has been said (and shown) for ZOL completeness
|
||
%\agda{TODO}
|
||
\end{tcolorbox}
|
||
|
||
\subsection{(Finitary) Predicate Logic as a SOGAT}
|
||
|
||
\subsubsection{Making the SOGAT}
|
||
|
||
The first step is again to create the SOGAT of Predicate Logic. The SOGAT is given \autoref{fig:ffol-sogat}. We can see that \emph{terms} are now part of the theory, and we see that they have to be locally representable (into $\AgdaPrimitive{Set}^+$). This is because the proof constructor $\forall i$ now has a strictly positive arrow, because Term are not extrenal anymore.
|
||
|
||
\begin{figure}
|
||
\begin{tcolorbox}
|
||
\[
|
||
\begin{array}{lcl}
|
||
\Tm & : & \Set^+ \\
|
||
\\
|
||
\For & : & \Set \\
|
||
- \implies - & : & \For \rightarrow \For \rightarrow \For\\
|
||
\forall & : & (\Tm \rightarrow \For) \rightarrow \For \\
|
||
\R & : & \Tm \rightarrow \Tm \rightarrow \For\\
|
||
\\
|
||
\Pf & : & \For \rightarrow \Prop^+ \\
|
||
\lam & : & (\Pf A \rightarrow^+ \Pf B) \rightarrow \Pf (A \implies B)\\
|
||
\app & : & \Pf (A \implies B) \rightarrow (\Pf A \rightarrow \Pf B)\\
|
||
\foralli & : & (t : \Tm \rightarrow^+ \Pf A\;t) \rightarrow \Pf (\forall A)\\
|
||
\foralle & : & \Pf (\forall A) \rightarrow (t : \Tm) \rightarrow \Pf (A\;t)\\
|
||
\end{array}
|
||
\]
|
||
\end{tcolorbox}
|
||
\caption{FFOL Sogat Presentation}
|
||
\label{fig:ffol-sogat}
|
||
\end{figure}
|
||
|
||
\subsubsection{Making a GAT out of it}
|
||
|
||
So now that we want to encode a GAT from this SOGAT, we can follow the same process as we followed before. One difference is that \AgdaField{Sub} now have to be in \AgdaPrimitive{Set}, and so we have a lot more equations that were trivial before. For example, the base category now has to make explicit the categorical equations.
|
||
|
||
\begin{tcolorbox}
|
||
|
||
\agda{agda/FFOL-1.tex}
|
||
|
||
\end{tcolorbox}
|
||
|
||
We also have to add a term extension operator like we did for formula extension. One difference is that this new kind of extension has no parameter. However, it makes it so \AgdaField{Sub} have to be in \AgdaPrimitive{Set}, and so we have to add a lot of equation concerning the two term extensions.
|
||
|
||
Please ignore the \AgdaFunction{substP} for now, this notion will be explained in \autoref{sec:transport-hell}, you can just consider that this function returns its third argument unchanged and ignore the two firsts.
|
||
|
||
\begin{tcolorbox}
|
||
|
||
\agda{agda/FFOL-3.tex}
|
||
\agdasep
|
||
\agda{agda/FFOL-7.tex}
|
||
\agda{agda/FFOL-8.tex}
|
||
|
||
\end{tcolorbox}
|
||
|
||
We also have to add a \Tm functor, that will have no other constructor than that of \AgdaField{$\pi_t^2$}. We don't need to change the other constructors except for $\forall i$ in which the strictly positive application become a proof from a term-extended context, and for $\forall e$ in which we have to \enquote{compute} what it means to apply a formula at some specific term.
|
||
|
||
\begin{tcolorbox}
|
||
\agda{agda/FFOL-2.tex}
|
||
\agdasep
|
||
\agda{agda/FFOL-14.tex}
|
||
\end{tcolorbox}
|
||
|
||
We now have a complete GAT for Predicate logic, and we already see that we have a lot more equations to prove.
|
||
|
||
\subsection{Finding a Syntax for First Order Logic}
|
||
|
||
Even though this new SOGAT don't seem a lot more complex than the one for IFOL, there is three reasons why making the Syntax will be much harder.
|
||
|
||
\begin{enumerate}
|
||
\item We cannot make Sub to be in \AgdaPrimitive{Prop} anymore, because we have term extensions, and terms are in \AgdaPrimitive{Set}, and therefore we have a lot more equations.
|
||
\item We have anothe parrallel way of extending contexts which squares the difficulty
|
||
\item Formulæ now have to depend on contexts too.
|
||
\end{enumerate}
|
||
|
||
However, we can still do something that simplifies greatly the making of the syntax. We can split the $\bCon$ category in two. A first part will be related to term-extensions and the second part will be related to proof-extensions.
|
||
|
||
The difficulty is that those two parts are not independent. Indeed, a proof-extension related context (or \emph{proof context}) will depend on formulæ, that will themselves depend on term-extension related contexts (or \emph{term contexts}).
|
||
|
||
So, let's first define the term contexts, which simply describes how many terms they are in the context (therefore, it is isomorphic to Nat).
|
||
|
||
\begin{tcolorbox}
|
||
\agda{agda/FFOL-I-1.tex}
|
||
\end{tcolorbox}
|
||
|
||
Then, we can define already define terms (which can only be term variables, because \AgdaField{$\pi_t^2$} is the only constructor in our simplified version), and formulæ. Both types are indexed only by a \textbf{term} context, and we will need later to make them $\bCon \rightarrow \bSet$ rather than $\textbf{Cont} \rightarrow \bSet$. This follows the same reasoning we did when we said that Formulæ didn't have to depend on Contexts. Formulæ never need to access proof variables, and that is the reason why we can do the separation.
|
||
|
||
\begin{tcolorbox}
|
||
\agda{agda/FFOL-I-3.tex}
|
||
\agdasep
|
||
\agda{agda/FFOL-I-4.tex}
|
||
\end{tcolorbox}
|
||
|
||
We now can define \textbf{term} substitutions. The algebra gives us two ways of constructing them: with $,_t$ and as a morphism from the initial object, like we did for Propositional Logic. That's how we make our constructor The two projections $\pi_t^1$ and $\pi_t^2$ are then simply obtained by destroying the $,_t$ constructor and getting the first or second term. The equalities between $\pi_t¹$, $\pi_t²$ and $,_t$ can be proven easily in that layout.
|
||
|
||
We also have to define the action of term substitutions on terms and formulæ. The definitions are really natural, as we just go down the formulæ to get to the term variables and transform them into the terms specified in the substitution.
|
||
|
||
We also define the categorical constructors for the $\textbf{Cont}$ category, that is, the $id_t$ and $\circ_t$ operators, and we obviously have to show their three categorical laws. Please note that these are not the equalities we will use in the final algebra, because they are only related to \AgdaDatatype{Subt} (but we will surely use them later).
|
||
|
||
We also show the functorality of $\_\left[\_\right]\!t$ and $\_\left[\_\right]\!f$. You can see we use some helper functions that are called $\operatorname{wk}_t$ and $\operatorname{lf}_t$. Those stands for weakening and lifting. I don't show their definitions here, because they are only helper functions, but $\operatorname{wk}_t$ means that from something going from a context $\Gamma$, we create something going from the context $\Gamma \triangleright_t$ that does not uses the added variable. $\operatorname{lf}_t$ means that we add one variable in the source, one variable in the goal, and that this variable is mapped to itself.
|
||
|
||
I did not need renamings this time to define them because i don't have any term constructor aside from term variables.
|
||
|
||
\begin{tcolorbox}
|
||
\agda{agda/FFOL-I-5.tex}
|
||
\agdasep
|
||
\agda{agda/FFOL-I-7.tex}
|
||
\agdasep
|
||
\agda{agda/FFOL-I-9.tex}
|
||
\agdasep
|
||
\agda{agda/FFOL-I-10.tex}
|
||
\end{tcolorbox}
|
||
|
||
We can now start creating the other category. For that, we can define the base set of the category like we did with term contexts. But this time, our extension constructor has another parameter: The formula the added proof proves. Therefore, we have a dependency of $\operatorname{Conp}$ on $\operatorname{Cont}$, because formulæ are defined in \AgdaDatatype{Cont}.
|
||
|
||
This new $\textbf{Conp}$ category is in fact a functor from $\textbf{Cont}$ to $\bSet$. So we have to define its action on $\textbf{Cont}$'s morphisms. And we also have to proove that this action respects the functorality of $\operatorname{Conp}$.
|
||
|
||
We will finally create another operator on $\textbf{Conp}$: $\triangleright tp$. This operator does a term extension of a proof context, which doesn't add any information to the proofs, it only adds one unused variable to them (we substitute all the proofs with $\operatorname{wk}_t \operatorname{id}_t$). It can be understood as the action of the general $\triangleright_t$ functor on $\textbf{Conp}$.
|
||
|
||
\begin{tcolorbox}
|
||
\agda{agda/FFOL-I-12.tex}
|
||
\agdasep
|
||
\agda{agda/FFOL-I-14.tex}
|
||
\agdasep
|
||
\agda{agda/FFOL-I-16.tex}
|
||
\end{tcolorbox}
|
||
|
||
We now have everything we need to define proofs, and we simply implement all the constructors from the GAT. You can notice that we have separated term and proof contexts in the definitions, but it is only for the sake of readability, because operations on proofs will often modify the proof context without changing the term context.
|
||
|
||
\begin{tcolorbox}
|
||
\agda{agda/FFOL-I-18.tex}
|
||
\end{tcolorbox}
|
||
|
||
We also define the action of term-substitutions on proofs (because Pf is a functor that is indexed by $\textbf{Cont}$). Terms substitutions does nothing to the proofs, they only affect formulæ and terms, which you cannot find inside a proof. So it is only changing the type of a proof from $\Pf Δ_t\;Δ_p\;A$ to $\Pf Γ_t\;Δ_p[σ]\; A[σ]$.
|
||
|
||
\begin{tcolorbox}
|
||
\agda{agda/FFOL-I-19.tex}
|
||
\end{tcolorbox}
|
||
|
||
Again, before we can define proof substitutions, we need to define \emph{renamings} like we did for Propositional Logic. They allow us to define proof-weakening and the identity substitution. With them, we can define the complete proof substitutions like we did for Propositional Logic. But please note that those proof substitutions are defined with a fixed term-context. So they are weaker than the final substitutions we well have to define for our algebra, that have to be able to be morphisms between contexts that can differ on term-contexts and proof context at the same time. But this is not an issue and we can define all substitutions using only those restricted proof-substitutions.
|
||
|
||
Again, these substitutions are a functor over the category $\textbf{Cont}$, so we have to construct the action on morphisms, which is simply applying the transformations to all the proofs contained in the substitution.
|
||
|
||
\begin{tcolorbox}
|
||
\agda{agda/FFOL-I-20.tex}
|
||
\agdasep
|
||
\agda{agda/FFOL-I-22.tex}
|
||
\agdasep
|
||
\agda{agda/FFOL-I-24.tex}
|
||
\end{tcolorbox}
|
||
|
||
With this new kind of substitution, we can substitute on proofs (that's what they're for). In other words, we have to describe the action of the $\Pf$ functor on the morphisms of the category $\textbf{Conp}$.
|
||
|
||
Proof substitution of proofs is simple to define, as we only get down the proof until we find a proof variable, in which case we replace it with the proof in the substitution, like we did for term-substitutions and formulæ.
|
||
|
||
Again, we have defined \AgdaFunction{wk${}_p$} and \AgdaFunction{lf${}_p$}. The former will add an unused proof variable (an assumption) in a substitution, and the latter adds a formula in the goal which is proven using an assumption.
|
||
|
||
\begin{tcolorbox}
|
||
\agda{agda/FFOL-I-26.tex}
|
||
\end{tcolorbox}
|
||
|
||
This definition of proof substitutions allows us to define the categorical operators for proof substitutions.
|
||
|
||
Of course, we have to show that the categorical laws apply to them, that $\_[\_]\sigma_p$ respects them, as we did for the Subt's laws.
|
||
|
||
The proofs of these laws contains a lot of transports which make them not very readable, but this problem will be described more precisly in \autoref{sec:transport-hell}.
|
||
|
||
\begin{tcolorbox}
|
||
\agda{agda/FFOL-I-27.tex}
|
||
\end{tcolorbox}
|
||
|
||
The last step is to merge our two kinds of contexts and substitutions in order to match the algebra.
|
||
|
||
For contexts, we simply have a record type. But for substitutions, we defined Subp to only describe substitutions between Conp{\footnotesize s} with \emph{the same Conp}. Our solution is to understand global substitutions as a sequence of two substitutions, first on terms, and then on proofs. That's why the \enquote{proof} part of the substitution can only be applyed to proofs on $\Delta_p [t]p$, i.e. proofs that have already been term-substituted by the \enquote{term} part of the substitution. The definition of the algebra's substitution is given after, and you can see that substitutions works exactly as described, first, the proof and everything inside is substituted using the \enquote{term} part of the substitution, and only after that the \enquote{proof} part of the substitution is applied.
|
||
|
||
\begin{tcolorbox}
|
||
|
||
\agda{agda/FFOL-I-28.tex}
|
||
\agdasep
|
||
\agda{agda/FFOL-I-30.tex}
|
||
|
||
\agdasep
|
||
|
||
\begin{code}
|
||
\>[4]\AgdaOperator{\AgdaField{\AgdaUnderscore{}[\AgdaUnderscore{}]p}}\AgdaSpace{}%
|
||
\AgdaSymbol{=}\AgdaSpace{}%
|
||
\AgdaSymbol{λ}\AgdaSpace{}%
|
||
\AgdaBound{pf}\AgdaSpace{}%
|
||
\AgdaBound{σ}\AgdaSpace{}%
|
||
\AgdaSymbol{→}\AgdaSpace{}%
|
||
\AgdaSymbol{(}\AgdaBound{pf}\AgdaSpace{}%
|
||
\AgdaOperator{\AgdaFunction{[}}\AgdaSpace{}%
|
||
\AgdaField{Sub.t}\AgdaSpace{}%
|
||
\AgdaBound{σ}\AgdaSpace{}%
|
||
\AgdaOperator{\AgdaFunction{]pₜ}}\AgdaSymbol{)}\AgdaSpace{}%
|
||
\AgdaOperator{\AgdaFunction{[}}\AgdaSpace{}%
|
||
\AgdaField{Sub.p}\AgdaSpace{}%
|
||
\AgdaBound{σ}\AgdaSpace{}%
|
||
\AgdaOperator{\AgdaFunction{]p}}\<%
|
||
\end{code}
|
||
|
||
\end{tcolorbox}
|
||
|
||
And we can finally define our categorical operators for the merged version. They are only concatenation of the previously defined operators, so no hard logic here. Those constructions are obviously followed by equations needed for the algebra.
|
||
|
||
\begin{tcolorbox}
|
||
|
||
\agda{agda/FFOL-I-32.tex}
|
||
|
||
\agdasep
|
||
\agda{agda/FFOL-I-33.tex}
|
||
|
||
\end{tcolorbox}
|
||
|
||
And we now have a working syntax for Predicate Logic. Unfortunately, i did not prove yet that it was really an initial model, because for the proof i need to work with a lot of transport hell, which are not really hard to solve, but takes a lot of time.
|
||
|
||
\subsection{Transport Hell}
|
||
|
||
\label{sec:transport-hell}
|
||
|
||
In order for you to understand the code, i have to explain what are transports. I'll do this with the example of the definition of \AgdaFunction{id} in the Finitary First Order Logic syntax.
|
||
.
|
||
To construct it, we use \AgdaFunction{idₜ} and \AgdaFunction{id${}ₚ$}, merged together with the constructor \AgdaInductiveConstructor{sub}. Here are the types of the different elements in an array.
|
||
|
||
\begin{center}
|
||
\renewcommand{\arraystretch}{1.2}
|
||
\begin{tabular}{l|l}
|
||
\AgdaFunction{id} & \AgdaRecord{Sub} (\AgdaInductiveConstructor{con} Γₜ Γₚ) (\AgdaInductiveConstructor{con} Γₜ Γₚ) \\\hline
|
||
\AgdaFunction{idₜ} & \AgdaDatatype{Subt} Γₜ Γₜ \\
|
||
\AgdaFunction{idₚ} & \AgdaDatatype{Subp} Γₚ Γₚ \\
|
||
\AgdaInductiveConstructor{sub} & (σ : \AgdaDatatype{Subt} Γₜ Δₜ) \\
|
||
& \AgdaSymbol{$\rightarrow$} \AgdaDatatype{Subp} Γₚ (Δₚ[σ]c) \\
|
||
& \AgdaSymbol{$\rightarrow$} \AgdaRecord{Sub} (\AgdaInductiveConstructor{con} Γₜ Γₚ) (\AgdaInductiveConstructor{con} Δₜ Δₚ) \\
|
||
\end{tabular}
|
||
\end{center}
|
||
|
||
But if we try to construct \AgdaFunction{id}, then we will eventually end up with the following goal:
|
||
|
||
\begin{center}
|
||
\AgdaFunction{id} = \AgdaInductiveConstructor{sub} \AgdaFunction{idₜ} \textbf{?} $\implies$ \textbf{?} : \AgdaDatatype{Subp} Γₚ (Γₚ[\AgdaFunction{idₜ}]c)
|
||
\end{center}
|
||
|
||
But then agda will complain if we give it as a goal the expression \enquote{\AgdaFunction{idₚ}}. Indeed, it is not trivial for them that \AgdaDatatype{Subp} Γₚ (Γₚ[\AgdaFunction{idₜ}]c) is the same as \AgdaDatatype{Subp} Γₚ Γₚ. Even if we can easily prove the equality between those two elements of \AgdaPrimitive{Prop} (the proof of the equality is derived from the fact that Conp is a functor from $\textbf{Cont}$ to $\bSet$, and therefore it has to respect the identity of $\textbf{Conp}$).
|
||
|
||
That's where transports comes in. Its definition is as follows:
|
||
|
||
\begin{center}
|
||
\AgdaFunction{substP} : \{A : \AgdaPrimitive{Set}\}(P : A → \AgdaPrimitive{Prop})\{a a' : A\} → a ≡ a' → P a → P a'
|
||
\end{center}
|
||
|
||
This is exactly the thing that will solve our problem. With the equality between the two elements of \AgdaPrimitive{Prop}, we can now convert \AgdaFunction{idₚ} to something that will correctly match the goal required by Agda.
|
||
|
||
This section is called \enquote{Transport Hell} because those transports between equal sets can get really annoying. In former version of the syntax, the \AgdaDatatype{Subp} were \AgdaPrimitive{Set}s instead of \AgdaPrimitive{Prop}s. And that created a lot of equalities related to polymorphic functions (quite all \AgdaDatatype{Subp}'s related functions were then polymorphic, as they would depend on proof contexts). And to solve those equalities, you have to extract what are precisely the polymorphic functions you are working with. You can see those proofs on \href{https://github.com/MysaaJava/m1-internship/commit/2728c60633a80631ed7b61bbfae5c81a1e0e193a#diff-99bc55bebd36ad0afbae3c6448793992086091c5b6b25973f73dd779690d7dd2}{former versions of the syntax}, they are really long and not interesting (as it is basically trying to tweak our equation so that Agda understands that two types are equal).
|
||
|
||
\section{Summary}
|
||
|
||
|
||
\section{Bibliography}
|
||
\begingroup
|
||
\renewcommand{\section}[2]{}%
|
||
\printbibliography
|
||
\endgroup
|
||
|
||
\newpage
|
||
\addappheadtotoc
|
||
\appendix
|
||
\addtocontents{toc}{\protect\setcounter{tocdepth}{-1}}
|
||
\appendixpage
|
||
|
||
\section{Agda Code}
|
||
|
||
\end{document}
|