Minor improvements

Ch1_The_Coq_Proof_Assistant.v

@@ -5,7 +5,7 @@
 (** * Interactively viewing proofs *)
 (** %
 \urlstyle{same}
-The entire text of this dissertation is comprised of Coq source files which include all the proofs given. The reader is recommended to download CoqIde from \begin{center}\url{https://coq.inria.fr/download}\end{center} and use the Coq source files available from \begin{center}\url{https://github.com/Coda-Coda/MartinLoefTheorem-Dissertation}\end{center} This will allow the reader to step through any of the proofs in this dissertation interactively.
+The entire text of this dissertation is comprised of Coq source files which include all the proofs given. The reader is recommended to download CoqIde from \begin{center}\url{https://coq.inria.fr/download}\end{center} and use the Coq source files available from \begin{center}\url{https://github.com/Coda-Coda/MartinLoefTheorem-Dissertation/releases/tag/submission}\end{center} This will allow the reader to step through any of the proofs in this dissertation interactively.
 % *)
 
 (** * A typical Coq Proof *)
@@ -15,7 +15,7 @@ Inductive boolean :=
  | true
  | false.
 
-(** Above a datatype, [boolean], is defined which can have either of the values listed. Datatype definitions of this kind will be used to define propositional or modal formulas as their own type. *)
+(** Above a data type, [boolean], is defined which can have either of the values listed. Data type definitions of this kind will be used to define propositional or modal formulas as their own type. *)
 
 Definition not (x:boolean) : boolean :=
 match x with
@@ -71,7 +71,7 @@ reflexivity.
 Qed.
 
 (** %\item% *)
-(** [exact] will solve a goal that looks exactly like a current hypothesis. *)
+(** [exact] will solve a goal that looks exactly like a current hypothesis. In the example below, [p] is introduced as the hypothesis [H] and then the goal [p] can be solved with the tactic [exact H]. *)
 
 Example exact_example : forall p, p -> p.
 Proof.
@@ -114,7 +114,7 @@ exact example1_axiom.
 Qed.
 
 (** %\item% *)
-(** [apply] will apply a lemma to the current goal, as shown below. *)
+(** [apply] will apply a theorem to the current goal, as shown below. *)
 
 Example apply_example : forall p q, ~ p -> p \/ ~ q -> ~ q.
 Proof.
@@ -128,7 +128,7 @@ Qed.
 (** * Confidence in different types of Coq proofs *)
 
 (** It is important to note that different ways of using Coq have important implications for how trustworthy the resulting proofs are and for which sections of code need to be checked to be trustworthy before trusting a particular proof. %\par%
-When Coq is used without any additional assumptions added and for its regular usage we can be very confident of the system's consistency and the trustworthiness of proofs. In general, with a lemma for which the Coq definitions used in the lemma are fully understood, the user code leading to a proof of such a lemma a would not need to be manually checked carefully to be trustworthy. %\par%
+When Coq is used without adding any additional assumptions and for its regular usage we can be very confident of the system's consistency and the trustworthiness of proofs. In general, if the Coq definitions used in a theorem are fully understood, the user code leading to a proof of it would not need to be manually checked to be trustworthy. %\par%
 In contrast, when the code leading to a proof makes use of assumptions then it is important to carefully check that the assumptions do not lead to unintended results. For example, consider the statement below. *)
 
 Parameter i : Type.
@@ -137,7 +137,7 @@ Parameter i : Type.
 For example, the following use of [Parameter] would make Coq's logic inconsistent: %\par%
 [Parameter x: False.] %\par%
 This assumes the existence of [x] of type [False], which essentially assumes the existence of a proof of [False] (which should be impossible). %\par%
-A second consideration is whether the proof involves an embedding and `lifted connectives', such as is the case with the Modal Logic formalisation in a later chapter. This technically falls under the idea of being sure that "the Coq definitions used in the lemma are fully understood". Essentially, if an entire logical system has been newly defined, then any lemmas proven in such a system are only as trustworthy as the definitions given in the user code.
+A second consideration is whether the proof involves an embedding and `lifted connectives', such as is the case with the Modal Logic formalisation in a later chapter. This technically falls under the idea of being sure that "the Coq definitions used in the theorem are fully understood". Essentially, if an entire logical system has been newly defined, then any theorems proven in such a system are only as trustworthy as the definitions given in the user code.
  %\par%
 These considerations are relevant to aspects of the formalisations in this dissertation, and also relevant are the standard considerations outlined on a Coq FAQ site%~\cite{coqFAQtrust}% which include trusting the integrity of the system Coq is running on and trusting the theory behind Coq. 
 *)

Ch2_The_Martin_Loef_Theorem.v

@@ -4,7 +4,7 @@
 
 (** The Martin-%\Loef{}% Theorem is introduced in the paper Verificationism Then and Now (1995, 2013)%\cite{MartinLoef1995, ml}%. The conclusion of the paper is that, on the intuitionistic conception, there are no absolutely undecidable propositions. %\\%
 A large portion of the paper involves carefully unpacking the notions of a proposition, truth, falsity, knowledge and possibility. %\\%
-The purpose of this dissertation and the ongoing work in parrallel to it is to formalise the proof outlined by Martin-%\Loef{}% in some sound and complete logical system as well as in a proof assistant such as Coq. *)
+The purpose of this dissertation and the ongoing work in parallel to it is to formalise the proof outlined by Martin-%\Loef{}% in some sound and complete logical system as well as in a proof assistant such as Coq. *)
 
 (** * Unpacking the key notions *)
 
@@ -19,7 +19,7 @@ The purpose of this dissertation and the ongoing work in parrallel to it is to f
 (** ** Knowledge *)
 (** A proposition can be known to be true if there exists a proof for it. *)
 (** ** Possibility *)
-(** The `if there exists' in the definition of knowledge referes to an intuitionistic understanding of these words. That is, possibility in principle. For example, in order for a statement involving a large number to be known to be true, there need not be a proof detailing every step of that proof - rather it would be sufficient to demonstrate the existence of an algorithm that would, in principle, produce the required step by step proof. *)
+(** The `if there exists' in the definition of knowledge refers to an intuitionistic understanding of these words. That is, possibility in principle. For example, in order for a statement involving a large number to be known to be true, there need not be a proof detailing every step of that proof - rather it would be sufficient to demonstrate the existence of an algorithm that would, in principle, produce the required step by step proof. *)
 
 (** * Unpacking the Martin-%\Loef{}% Theorem *)
 
@@ -55,7 +55,7 @@ but he found Turing's argument \alert{inconclusive}:
 
 % *)
 
-(** ** Does objective mathematics coincide with subjective mathematics? *)
+
 (** %
 \Godel{}'s answer (Gibbs lecture ``Some Basic Theorems on the Foundations of Mathematics and their Implications'',~\cite{Godel51}) based on his incompleteness theorem is a \alert{disjunctive conclusion}:\medskip
 
@@ -125,7 +125,7 @@ methods currently not yet discovered.}
 {\bf Fact~1.} [Unknowability of truth entails knowability of falsity] {\em  If the proposition $A$ cannot be known to be true, then $A$ can be known to be false.}
 \\[2ex]
 
-{\it Proof}: To prove that $A$ can be known to be false we have to show that $\neg A = A \rightarrow (0=1)$ can be known to be true. To this aim we need an algorithm ${\mathcal B}$ to convert any proof of $A$ into a proof of $(0=1)$. The algorithm ${\mathcal B}$  returns anything output by  the algorithm  ${\mathcal A}$ provided by the hypothesis, i.e.~noting: vacuously, the implication holds.\\
+{\it Proof}: To prove that $A$ can be known to be false we have to show that $\neg A$, i.e. $A \rightarrow (0=1)$ can be known to be true. To this aim we need an algorithm ${\mathcal B}$ to convert any proof of $A$ into a proof of $(0=1)$. The algorithm ${\mathcal B}$  returns anything output by  the algorithm  ${\mathcal A}$ provided by the hypothesis, i.e.~noting: vacuously, the implication holds.\\
 
 Comment: The proof constructively produces positive information  from negative information. \\
 % *)
@@ -148,7 +148,7 @@ Comment: The proof constructively produces positive information  from negative i
 \\[2ex]
 
 
-{\it Proof}: By hypothesis we have a proof demonstrating $A$ and a proof demonstrating $\neg A= A \rightarrow (0=1)$. Then we can demonstrate $(0=1)$, contradicting Fact~3.
+{\it Proof}: By hypothesis we have a proof demonstrating $A$ and a proof demonstrating $\neg A$, i.e. $A \rightarrow (0=1)$. Then we can demonstrate $(0=1)$, contradicting Fact~3.
 
 
 \medskip

Ch3_Formalising_Modal_Logics_in_Coq.v

@@ -5,15 +5,15 @@
 (** %\chapter{Formalising Modal Logics in Coq}% *)
 
 (** * Motivation and background *)
-(** The Martin-%\Loef{}% Theorem includes the notion of knowledge as well as the notion of possibility in key ways within it. Both possibility and knowledge have been modeled using modal logics for many years, and so it seemed likely that incorporating or adapting some of those techniques would be useful in formalising the Martin-%\Loef{}% theorem and its proof. *)
+(** The Martin-%\Loef{}% Theorem includes the notion of knowledge as well as the notion of possibility in key ways. Both possibility and knowledge have been modelled using modal logics for many years, and so it seemed likely that incorporating or adapting some of those techniques would be useful in formalising the Martin-%\Loef{}% theorem and its proof. *)
 
 (** ** The Benzmuller and Paleo paper *)
-(** The paper `Interacting with Modal Logics in the Coq Proof Assistant'%~\cite{benzmuller}% sets out a great way to embed modal logics in the Coq proof assistant. The approach they put forward in their paper is also extensible and so had the potential to be adapted as necessary when formalising the Martin-%\Loef{}% Theorem. Their work was very helpful. %\par%*)
+(** The paper `Interacting with Modal Logics in the Coq Proof Assistant'%~\cite{benzmuller}% sets out a useful way to embed modal logics in the Coq proof assistant. The approach they put forward in their paper is also extensible and so had the potential to be adapted as necessary when formalising the Martin-%\Loef{}% Theorem. Their work was very helpful. %\par%*)
 (** In their paper they state: %\emph{"the main contribution described in this paper - convenient techniques for leveraging a powerful proof assistant such as Coq for interactive reasoning for modal logics - may serve as a starting point for many interesting projects."} \cite[p.~2]{benzmuller}%.*)
 
 
 (** ** Bi-modal logic *)
-(** One of the approaches was to formalise the theorem in a bi-modal logic, representing knowability and possibility as modal operators. This approach is shown below, based almost entirly on the Coq code from the Benzmuller paper, with some minor adaptations for it to be bi-modal logic. *)
+(** One of the approaches was to formalise the theorem in a bi-modal logic, representing knowability and possibility as modal operators. This approach is shown below, based almost entirely on the Coq code from the Benzmuller paper, with some minor adaptations for it to be bi-modal logic. *)
 
 
 (** * Coq formalisation of modal logic *)
@@ -22,9 +22,9 @@
 Module Modal.
 (*end hide *)
 (** ** Defining an embedding of modal logic in Coq *)
-(** %\emph{The Coq code in this subsection is directly from the Benzmuller and Paleo Paper~\cite{benzmuller}.}% *)
+(** %\emph{The Coq code in this subsection is directly from the Benzmuller and Paleo Paper~\cite{benzmuller}, the comments have been added.}% *)
 
-(** It is worth noting that to check the trustworthiness of any lemma using the techniques from the Benzmuller and Paleo paper, it is necessary to check the trustworthiness of the user code defining the modal logic embedding (below), and especially the impact of any adaptations to their original technique such as the adaptation to bi-modal logic later in this chapter. *)
+(** It is worth noting that to check the trustworthiness of any theorem using the techniques from the Benzmuller and Paleo paper, it is necessary to check the trustworthiness of the user code defining the modal logic embedding (below), and especially the impact of any adaptations to their original technique such as the adaptation to bi-modal logic later in this chapter. *)
 
 
 (** *** Worlds, objects, modal propositions and the accessibility relation *)
@@ -35,7 +35,7 @@ Parameter u: Type. (** Here we declare/assume a type [u] as the type for objects
 
 Definition o := i -> Prop. (** Here we define [o] to be the type which takes a world and gives a meta-language proposition. [o] then, is the type of modal propositions, which when given a world are then a meta-language proposition. %\par% *)
 
-(** The indended usage is to have a modal formula, say [p] (with type [o]), with the meaning of [(p w)] to be that the modal proposition represented by [p] is true at world [w] (where [w] is a world, with type [i]). %\par% *)
+(** The intended usage is to have a modal formula, say [p] (with type [o]), with the meaning of [(p w)] to be that the modal proposition represented by [p] is true at world [w] (where [w] is a world, with type [i]). %\par% *)
 
 (** The meanings of the definitions of [i], [u] and [o] are fixed further by their usage in the next definitions. It is also worth noting that the reason why undescriptive names are used is because [i], [u] and [o] will need to be written often and it would be inconvenient if their names were long. *)
 
@@ -45,7 +45,7 @@ Parameter r: i -> i -> Prop.  (** Here we declare/assume a function/predicate of
 
 (** *** Connectives *)
 
-(** Here the lifted connecties are defined. Each lifted connective (except [mnot]) takes two modal propositions (with type [o]) and a world (with type [i]) and gives a `meta-language' proposition (with the standard Coq type [Prop]) reflecting the meaning of the connective. *)
+(** Here the lifted connectives are defined. Each lifted connective (except [mnot]) takes two modal propositions (with type [o]) and a world (with type [i]) and gives a `meta-language' proposition (with the standard Coq type [Prop]) reflecting the meaning of the connective. *)
 
 Definition mnot (p: o)(w: i) := ~ (p w).
 Definition mand (p q:o)(w: i) := (p w) /\ (q w).
@@ -115,7 +115,7 @@ Definition dia (p: o) := fun w => exists w1, (r w w1) /\ (p w1).
 
 (** [dia] is defined similarly as a function which takes a modal proposition and a world, and returns a `meta-level' proposition stating that there exists a world related to that world, where the modal proposition is true. *)
 
-(** Since the type of both [dia] and [box] when applied to a modal proposition, is [i -> Prop] thus [box p] and [dia p] are of type [o] (the type of modal propositions). *)
+(** Since the type of both [dia] and [box] when applied to a modal proposition, is [i -> Prop], then [box p] and [dia p] are of type [o] (the type of modal propositions). *)
 
 (** *** Validity *)
 Definition V (p: o) := forall w, p w. (** Here the definition of validity for a modal formula is given. [V] is defined as a function/predicate that takes a modal proposition and gives a `meta-level' proposition stating that the given modal proposition is true at all worlds. So for any modal proposition [p], at the meta-level [V p] is true iff [p] is valid. *)
@@ -128,10 +128,10 @@ Notation "[ p ]" := (V p). (** Here a notation is defined so that we can write "
 
 (** ** Increasing the usability by defining tactics *)
 
-(** The tactics defined below allow proofs to be carried out without dealing directly with the intricate aspects of the definitions of the embedding. Instead, the familiar technique of working with introduction and elimination rules can be used. Only some new tactics are needed, as the standard Coq tactics work fine with many of the defined notions. Below a brief example of each new tactic is given, for a comprehensive explanation of these definitions see section 3 of the Benzmuller and Paleo paper%~\cite[p.~5]{benzmuller}%. *)
+(** The tactics defined below allow proofs to be carried out without dealing directly with the intricate aspects of the definitions of the embedding. Instead, the familiar technique of working with introduction and elimination rules can be used. Only some new tactics are needed, as the standard Coq tactics work fine with many of the defined notions. Below a brief example of each new tactic is given; for a comprehensive explanation of these definitions see section 3 of the Benzmuller and Paleo paper%~\cite[p.~5]{benzmuller}%. *)
 
 
-(** *** Modal Validity *)
+(** *** Modal validity *)
 Ltac mv := match goal with [|- (V _)] => intro end.
 
 (** Here the [mv] tactic is defined such that when the proof state requires proving that a modal formula is valid, applying [mv] will introduce a new arbitrary world and the goal of the proof state will then be to prove that the modal formula is true at the new world. *)
@@ -377,7 +377,7 @@ Qed.
 
 (** Tentative *) Theorem Third_Law : [mforall A, m~ (dia (K A)) m-> (dia (K (m~ A)))].
 Proof.
-Abort. (** A proof is not given here, further work may resolve whether this is provable in the future. *)
+Abort. (** A proof is not given here, further work may resolve whether this is provable. *)
 
 (* begin hide *)
 End BiModal.