Skip to content
Snippets Groups Projects
Commit 1a7af4a2 authored by SimonGuilloud's avatar SimonGuilloud
Browse files

Merge conflicts in the manual

parent ee15e0c7
No related branches found
No related tags found
6 merge requests!62Easy tactics,!58Easy tactics,!55Front integration and various changes,!54Front integration,!53Front integration,!52Front integration
This commit is part of merge request !53. Comments created here will be created in the context of that merge request.
...@@ -56,11 +56,8 @@ escapeinside={(*@}{@*)} ...@@ -56,11 +56,8 @@ escapeinside={(*@}{@*)}
\begin{document} \begin{document}
\maketitle \maketitle
\chapter*{Introduction} \chapter*{Introduction}
<<<<<<< HEAD
This document aims to give a complete documentation on LISA. Tentatively, every chapter and section will explain a part or concept of LISA, and explains both its implementation and its theoretical foundations.
=======
This document aims to give a complete documentation on LISA. Tentatively, every chapter and section will explain a part or concept of LISA, and explains both its implementation and its theoretical foundations \cite{DBLP:conf/tacas/GuilloudK22}. This document aims to give a complete documentation on LISA. Tentatively, every chapter and section will explain a part or concept of LISA, and explains both its implementation and its theoretical foundations \cite{DBLP:conf/tacas/GuilloudK22}.
>>>>>>> main
\input{part1.tex} \input{part1.tex}
......
This diff is collapsed.
...@@ -8,11 +8,8 @@ ...@@ -8,11 +8,8 @@
An extension by definition is the formal way of introducing new symbols in a mathematical theory. An extension by definition is the formal way of introducing new symbols in a mathematical theory.
Theories can be extended into new ones by adding new symbols and new axioms to it. We're interested in a special kind of extension, called \textit{conservative extension}. Theories can be extended into new ones by adding new symbols and new axioms to it. We're interested in a special kind of extension, called \textit{conservative extension}.
\begin{defin}[Conservative Extension] \begin{defin}[Conservative Extension]
<<<<<<< HEAD
A theory $\mathcal{T}_2$ is a conservative extension over a theory $\mathcal{T}_1$ if:
=======
A theory $\mathcal{T}_2$ is a conservative extension of a theory $\mathcal{T}_1$ if: A theory $\mathcal{T}_2$ is a conservative extension of a theory $\mathcal{T}_1$ if:
>>>>>>> main
\begin{itemize} \begin{itemize}
\item $\mathcal{T}_1 \subset \mathcal{T}_2$ \item $\mathcal{T}_1 \subset \mathcal{T}_2$
\item For any formula $\phi$ in the language of $\mathcal{T}_1$, if $\mathcal{T}_2 \vdash \phi$ then $\mathcal{T}_1 \vdash \phi$ \item For any formula $\phi$ in the language of $\mathcal{T}_1$, if $\mathcal{T}_2 \vdash \phi$ then $\mathcal{T}_1 \vdash \phi$
...@@ -33,11 +30,8 @@ Moreover, in that case we require that ...@@ -33,11 +30,8 @@ Moreover, in that case we require that
$$ $$
\exists ! y. \phi_{y, x_1,...,x_k} \exists ! y. \phi_{y, x_1,...,x_k}
$$ $$
<<<<<<< HEAD
is a theorem of $\mathcal{T}_1$
=======
is a theorem of $\mathcal{T}_1$. is a theorem of $\mathcal{T}_1$.
>>>>>>> main
\end{itemize} \end{itemize}
\end{itemize} \end{itemize}
\end{defin} \end{defin}
...@@ -46,11 +40,9 @@ We also say that a theory $\mathcal{T}_k$ is an extension by definition of a the ...@@ -46,11 +40,9 @@ We also say that a theory $\mathcal{T}_k$ is an extension by definition of a the
For function definition, it is common in logic textbooks to only require the existence of $y$ and not its uniqueness. The axiom one would then obtain would only be $\phi[f(x_1,...,x_n)/y]$ This also leads to conservative extension, but it turns out not to be enough in the presence of axiom schemas (axioms containing schematic symbols). For function definition, it is common in logic textbooks to only require the existence of $y$ and not its uniqueness. The axiom one would then obtain would only be $\phi[f(x_1,...,x_n)/y]$ This also leads to conservative extension, but it turns out not to be enough in the presence of axiom schemas (axioms containing schematic symbols).
\begin{lemma} \begin{lemma}
<<<<<<< HEAD
In ZF, an extension by definition without uniqueness doesn't necessarily yields a conservative extension if the use of the new symbol is allowed in axiom schemas.
=======
In ZF, an extension by definition without uniqueness doesn't necessarily yield a conservative extension if the use of the new symbol is allowed in axiom schemas. In ZF, an extension by definition without uniqueness doesn't necessarily yield a conservative extension if the use of the new symbol is allowed in axiom schemas.
>>>>>>> main
\end{lemma} \end{lemma}
\begin{proof} \begin{proof}
In ZF, consider the formula $\phi_c := \forall x. \exists y. (x \neq \emptyset) \implies y \in x$ expressing that nonempty sets contain an element, which is provable in ZFC. In ZF, consider the formula $\phi_c := \forall x. \exists y. (x \neq \emptyset) \implies y \in x$ expressing that nonempty sets contain an element, which is provable in ZFC.
...@@ -66,13 +58,9 @@ For the definition with uniqueness, there is a stronger result than only conserv ...@@ -66,13 +58,9 @@ For the definition with uniqueness, there is a stronger result than only conserv
\begin{defin} \begin{defin}
A theory $\mathcal{T}_2$ is a fully conservative extension over a theory $\mathcal{T}_1$ if: A theory $\mathcal{T}_2$ is a fully conservative extension over a theory $\mathcal{T}_1$ if:
\begin{itemize} \begin{itemize}
<<<<<<< HEAD
\item It is conservative
\item For any formula $\phi_2$ with free variables $x_1, ..., x_k$ in the language of $\mathcal{T}_2$, there exists a formula $\phi_1$ in the language of $\mathcal{T}_1$ with free variables among $x_1, ..., x_k$ such that
=======
\item it is conservative, and \item it is conservative, and
\item for any formula $\phi_2$ with free variables $x_1, ..., x_k$ in the language of $\mathcal{T}_2$, there exists a formula $\phi_1$ in the language of $\mathcal{T}_1$ with free variables among $x_1, ..., x_k$ such that \item for any formula $\phi_2$ with free variables $x_1, ..., x_k$ in the language of $\mathcal{T}_2$, there exists a formula $\phi_1$ in the language of $\mathcal{T}_1$ with free variables among $x_1, ..., x_k$ such that
>>>>>>> main
$$\mathcal{T}_2 \vdash \forall x_1...x_k. (\phi_1 \leftrightarrow \phi_2)$$ $$\mathcal{T}_2 \vdash \forall x_1...x_k. (\phi_1 \leftrightarrow \phi_2)$$
\end{itemize} \end{itemize}
\end{defin} \end{defin}
...@@ -81,11 +69,8 @@ An extension by definition with uniqueness is fully conservative. ...@@ -81,11 +69,8 @@ An extension by definition with uniqueness is fully conservative.
\end{thm} \end{thm}
The proof is done by induction on the height of the formula and isn't difficult, but fairly tedious. The proof is done by induction on the height of the formula and isn't difficult, but fairly tedious.
\begin{thm} \begin{thm}
<<<<<<< HEAD
If an extension $\mathcal{T}_2$ of a theory $\mathcal{T}_1$ with axiom schemas is fully conservative, then for any instance of the axiom schemas of an axiom schemas $\alpha$ containing a new symbol, $\Gamma \vdash \alpha$ where $\Gamma$ contains no axiom schema instantiated with new symbols.
=======
If an extension $\mathcal{T}_2$ of a theory $\mathcal{T}_1$ with axiom schemas is fully conservative, then for any instance of the axiom schemas containing a new symbol $\alpha$, $\Gamma \vdash \alpha$ where $\Gamma$ contains no axiom schema instantiated with new symbols. If an extension $\mathcal{T}_2$ of a theory $\mathcal{T}_1$ with axiom schemas is fully conservative, then for any instance of the axiom schemas containing a new symbol $\alpha$, $\Gamma \vdash \alpha$ where $\Gamma$ contains no axiom schema instantiated with new symbols.
>>>>>>> main
\end{thm} \end{thm}
\begin{proof} \begin{proof}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment