diff --git a/refman/kernel.tex b/refman/kernel.tex
index 340d278cbb8609f51cdd0800d4d7cb457ed6fcde..f93de1cba9c52b5320ef4ce4984fada7ccd4be26 100644
--- a/refman/kernel.tex
+++ b/refman/kernel.tex
@@ -614,7 +614,7 @@ The root of the proof shows the concluding statement, and the leaves are either
\end{figure}
In the Lisa kernel, proof steps are organised linearly, in a list, to form actual proofs. Each proof step refers to its premises using numbers, which indicate the place of the premise in the proof.
-a proof step can also be refered to by multiple subsequent proof steps, so that proofs are actually directed acyclic graphs (DAG) rather than trees. For the proof to be the linearization of a rooted DAG, the proof steps must only refer to numbers smaller than their own in the proof. Indeed, using topological sorting, it is always possible to order the nodes of a directed acyclic graph such that for any node, its predecessors appear earlier in the list.
+a proof step can also be referred to by multiple subsequent proof steps, so that proofs are actually directed acyclic graphs (DAG) rather than trees. For the proof to be the linearization of a rooted DAG, the proof steps must only refer to numbers smaller than their own in the proof. Indeed, using topological sorting, it is always possible to order the nodes of a directed acyclic graph such that for any node, its predecessors appear earlier in the list.
\autoref{fig:exampleProofLinear} shows the proof of Pierce's Law as linearized in Lisa's kernel.
%
\begin{figure}[ht]
@@ -682,7 +682,7 @@ For every proof step, Lisa's kernel actually expects more than only the premises
\centering
\begin{lstlisting}[language=scala, showspaces=false]
val PierceLawProof = SCProof(IndexedSeq(
- Hypothesis(φ |- φ, φ),
+ Hypothesis( φ |- φ, φ),
Weakening( φ |- ( φ, ψ ), 0),
RightImplies(() |- ( φ, φ ==> ψ ), 1, φ, ψ)
LeftImplies(( φ ==> ψ ) ==> φ |- φ, 2, 0, φ ==> ψ, φ),
@@ -811,7 +811,7 @@ Once a definition has been introduced, future theorems can refer to those defini
Theorem(
name: String,
proposition: Sequent
- )
+ )
\end{lstlisting}
\\ %\hline
@@ -821,7 +821,7 @@ Once a definition has been introduced, future theorems can refer to those defini
Axiom(
name: String,
ax: Formula
- )
+ )
\end{lstlisting}
\\ %\hline
@@ -831,7 +831,7 @@ Once a definition has been introduced, future theorems can refer to those defini
PredicateDefinition(
label: ConstantAtomicLabel,
expression: LambdaTermFormula
- )
+ )
\end{lstlisting}
\\ %\hline
@@ -842,7 +842,7 @@ Once a definition has been introduced, future theorems can refer to those defini
label: ConstantFunctionLabel,
out: VariableLabel,
expression: LambdaTermFormula
- )
+ )
\end{lstlisting}
\\ %\hline
@@ -867,7 +867,7 @@ Once a definition has been introduced, future theorems can refer to those defini
statement: Sequent,
proof: SCProof,
justs: Seq[Justification]
- )
+ )
\end{lstlisting}
\\ %\hline
@@ -876,7 +876,7 @@ Once a definition has been introduced, future theorems can refer to those defini
addAxiom(
name: String,
f: Formula
- )
+ )
\end{lstlisting}
\\ %\hline
@@ -885,7 +885,7 @@ Once a definition has been introduced, future theorems can refer to those defini
makePredicateDefinition(
label: ConstantAtomicLabel,
expression: LambdaTermFormula
- )
+ )
\end{lstlisting}
\\ %\hline
@@ -897,7 +897,7 @@ Once a definition has been introduced, future theorems can refer to those defini
label: ConstantFunctionLabel,
out: VariableLabel,
expression: LambdaTermFormula
- )
+ )
\end{lstlisting}
\\ %\hline
\end{tabular}
@@ -1106,7 +1106,7 @@ This can be done automatically with implicit conversions. Implicit conversion is
given Conversion[TermLabel, Term] = (t: Term) => Term(t, Seq())
\end{lstlisting}
%
-Now, every time a \lstinline|TermLabel| is writen in a place where a \lstinline|Term| is expected, it will be converted implicitly.
+Now, every time a \lstinline|TermLabel| is written in a place where a \lstinline|Term| is expected, it will be converted implicitly.
To learn more about Scala 3 and its capabilities, see its documentation at {\footnotesize\url{https://docs.scala-lang.org/scala3/book/introduction.html}}.
diff --git a/refman/lisa.pdf b/refman/lisa.pdf
index e9c6913a9f232484957e0db00e7e50c88028430b..cd1bb87ae8e25ca998ff5ee7995f293a13ab3729 100644
Binary files a/refman/lisa.pdf and b/refman/lisa.pdf differ
diff --git a/refman/prooflib.tex b/refman/prooflib.tex
index 08853d820579d128022a255a9ffaddce69158872..7daebca45e7f900d4e92f25313775d5124e3c7ca 100644
--- a/refman/prooflib.tex
+++ b/refman/prooflib.tex
@@ -53,7 +53,7 @@ In this chapter, we will describe how each of these construct is made possible a
\subsection{Local Definitions}
\label{sec:localDefinitions}
-The following line of reasonning is standard in mathematical proofs. Suppose we have already proven the following fact:
+The following line of reasoning is standard in mathematical proofs. Suppose we have already proven the following fact:
$$\exists x. P(x)$$
And want to prove the property $\phi$.
A proof of $\phi$ using the previous theorem would naturally be obtained the following way:
@@ -80,10 +80,10 @@ This simulation is provided by Lisa through the \lstinline|witness|{} method. It
\begin{figure}
\begin{lstlisting}[language=lisa, frame=single]
val existentialAxiom = Axiom(exists(x, in(x, emptySet)))
- val falso = Theorem(⊥) {
+ val falso = Theorem( ⊥ ) {
val c = witness(existentialAxiom)
- have(⊥) by Tautology.from(
- c.definition, emptySetAxiom of (x:= c))
+ have( ⊥ ) by Tautology.from(
+ c.definition, emptySetAxiom of (x := c))
}
\end{lstlisting}
\caption{An example use of local definitions in Lisa}
@@ -104,7 +104,7 @@ With lisa's kernel, it is possible to instantiate a theorem proving $P(x)$ to ob
\end{lstlisting}
\lstinline|x := d| is called a substitution pair, and is equivalent to the tuple \lstinline|(x, d)|. Arbitrarily many substitution pairs can be given as argument to \lstinline|of|, and the instantiations are done simultaneously. \lstinline|ax of (x := c)| is called an \lstinline|InstantiatedFact|, whose statement is $P(c)$, and which can be used exactly like theorems, axioms and intermediate steps in the proof. Internally, Lisa produces a proof step corresponding to the instantiation using the \texttt{Inst} rule.
-The \lstinline|of| keyword can also instantiate universaly quantified formulas of a fact, when it contains a single formula. For example, the following code is valid:
+The \lstinline|of| keyword can also instantiate universally quantified formulas of a fact, when it contains a single formula. For example, the following code is valid:
\begin{lstlisting}[language=lisa, frame=single]
val ax = Axiom(∀(x, P(x)))
val thm = Theorem(P(c) /\ P(d)) {
@@ -113,7 +113,7 @@ The \lstinline|of| keyword can also instantiate universaly quantified formulas o
\end{lstlisting}
Here, \lstinline|ax of c| is a fact whose proven statement is again $P(c)$. It is possible to instantiate multiple $\forall$ quantifiers at once. For example if \lstinline|ax| is an axiom of the form $\forall x, \forall y, P(x, y)$, then \lstinline|ax of (c, d)| is a fact whose proven statement is $P(c, d)$. It is also possible to combine instantiation of free symbols and quantified variables. For example, if \lstinline|ax| is an axiom of the form $\forall x, \forall y, P(x, y)$, then \lstinline|ax of (c, y, P := ===)| is a fact whose proven statement is $(c = y)$.
-Formally, the \lstinline|of| keyword takes as argument arbitrarily many terms and substitution pairs. If there is at least on term given as argument, the base fact must have a single universaly quantified formula on the right (an arbitrarily many formulas on the left). The number of given terms must be at most the number of leading universal quantifiers. Moreover, a substitution cannot instantiate any locked symbol (i.e. a symbol part of an assumption or definition). The ordering of substitution pairs does not matter, but the ordering of terms does. The resulting fact is obtained by firstreplacing the free symbols in the formula by the given substitution pairs, and then instantiating the quantified variables in the formula by the given terms
+Formally, the \lstinline|of| keyword takes as argument arbitrarily many terms and substitution pairs. If there is at least one term given as argument, the base fact must have a single universally quantified formula on the right (an arbitrarily many formulas on the left). The number of given terms must be at most the number of leading universal quantifiers. Moreover, a substitution cannot instantiate any locked symbol (i.e. a symbol part of an assumption or definition). The ordering of substitution pairs does not matter, but the ordering of terms does. The resulting fact is obtained by first replacing the free symbols in the formula by the given substitution pairs, and then instantiating the quantified variables in the formula by the given terms
In general, for the following proof
\begin{lstlisting}[language=lisa, frame=single]
diff --git a/refman/quickguide.tex b/refman/quickguide.tex
index b3c683d50215e36854fd9d19ebab92c84cf41b73..30eef1cf8e5732f880b8be389d7676d424f9e8e1 100644
--- a/refman/quickguide.tex
+++ b/refman/quickguide.tex
@@ -64,8 +64,8 @@ A cheat sheet of the most common symbols and how to input them is in \autoref{ta
\begin{tabular}{c|c|c}
Rendering & Input & Name \\ \hline
\lstinline| === | & === & equality \\ \hline
- \lstinline| \/ | & \textbackslash / & and \\ \hline
- \lstinline| /\ | & /\textbackslash & or \\ \hline
+ \lstinline| \/ | & \textbackslash / & or \\ \hline
+ \lstinline| /\ | & /\textbackslash & and \\ \hline
\lstinline| ==> | & ==> & implies \\ \hline
\lstinline+ |- + & |- & vdash \\ \hline
\lstinline| ∀ | & U+2200 & forall \\ \hline
@@ -225,7 +225,7 @@ tries to justify \lstinline|statement| by showing it is equivalent to \lstinline
\end{lstlisting}
tries to justify \lstinline|statement| by showing it is equivalent to the previously proven \lstinline|premise|.
-\subsubsection*{Tautology}
+\subsubsection*{Tautology}\label{tact:Tautology}
\lstinline|Tautology| is a propositional solver based upon restate, but complete. It is able to prove every formula inference that holds in classical propositional logic. However, in the worst case its complexity can be exponential in the size of the formula. Usage:
\begin{lstlisting}[language=lisa]
diff --git a/refman/theory.tex b/refman/theory.tex
index 7eaa52d70dbb032e144bd40045d75e4b8877fe72..892d87b38349545c9712d54aba9ada1e61a6d473 100644
--- a/refman/theory.tex
+++ b/refman/theory.tex
@@ -15,7 +15,7 @@ ZF Set Theory stands for Zermelo-Fraenkel Set Theory. It contains a set of initi
In a more typical mathematical introduction to Set Theory, ZF would naturally only contain the set membership symbol $\in$. Axioms defining the other symbols would then only express the existence of functions or predicates with those properties, from which we could get the same symbols using extensions by definitions.
In a very traditional sense, an axiomatization is any possibly infinite semi-recursive set of axioms. Hence, in its full generality, Axioms should be any function producing possibly infinitely many formulas.
-This is however not a convenient definition. In practice, all infinite axiomatizations are schematic, meaning that they are expressable using schematic variables. Axioms \ref{axz:comprehension} (comprehension schema) and \ref{axzf:replacement} (replacement schema) are such examples of axiom schema, and motivates the use of schematic variables in Lisa.
+This is however not a convenient definition. In practice, all infinite axiomatizations are schematic, meaning that they are expressible using schematic variables. Axioms \ref{axz:comprehension} (comprehension schema) and \ref{axzf:replacement} (replacement schema) are such examples of axiom schema, and motivates the use of schematic variables in Lisa.
@@ -24,9 +24,9 @@ This is however not a convenient definition. In practice, all infinite axiomatiz
\begin{tabular}{l|c|l}
{} & Math symbol & Lisa Kernel \\ \hline
Set Membership predicate & $\in$ & \lstinline$in(s,t)$ \\
- Subset predicate & $\subset$ & \lstinline$subset(s,t)$ \\
+ Subset predicate & $\subseteq$ & \lstinline$subset(s,t)$ \\
Empty Set constant & $\emptyset$ & \lstinline$emptyset()$ \\
- Unordered Pair constant & $(\cdot, \cdot )$ & \lstinline$pair(s,t)$ \\
+ Ordered Pair constant & $(\cdot, \cdot )$ & \lstinline$pair(s,t)$ \\
Power Set function & $\mathcal P$ & \lstinline$powerSet(s)$ \\
Set Union/Flatten function & $\bigcup$ & \lstinline$union(x)$ \\
\end{tabular}
@@ -94,7 +94,7 @@ This also naturally corresponds to \textit{comprehensions} over collections in p
\caption{Comprehensions in various programming languages}
\label{tab:comprehensionsProgramming}
\end{table}
-Those are typicaly syntactic sugar for a more verbose expression. For example in scala, \lstinline|(0 to 9).filter(x => x % 2 == 0).map(x => -x)|. However this kind of expressions is not possible in first order logic: We can't built in any way a term that contains formulas as subexpressions, as in \lstinline|filter|. So if we want to use such constructions, we need to simulate it as we did for local definitions in \autoref{sec:localDefinitions}.
+Those are typically syntactic sugar for a more verbose expression. For example in scala, \lstinline|(0 to 9).filter(x => x % 2 == 0).map(x => -x)|. However this kind of expressions is not possible in first order logic: We can't built in any way a term that contains formulas as subexpressions, as in \lstinline|filter|. So if we want to use such constructions, we need to simulate it as we did for local definitions in \autoref{sec:localDefinitions}.
It turns out that the comprehension schema is a consequence of the replacement schema when the value plugged for $\psi(x, y)$ is $\phi(x) \land y = x$, i.e. when $\psi$ denotes a restriction of the diagonal relation. Hence, what follows is built only from replacement.
Note that the replacement axiom \autoref{axzf:replacement} is conditional of the schematic symbol $\psi$ being a functional relation. It is more convenient to move this condition inside the axiom, to obtain a non-conditional equivalence. This is the approach adopted in Isabelle/ZF \cite{noelExperimentingIsabelleZF1993}. We instead can prove and use