diff --git a/Ch1_The_Coq_Proof_Assistant.v b/Ch1_The_Coq_Proof_Assistant.v index 36cde14..2f734a9 100644 --- a/Ch1_The_Coq_Proof_Assistant.v +++ b/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. *) \ No newline at end of file diff --git a/Ch2_The_Martin_Loef_Theorem.v b/Ch2_The_Martin_Loef_Theorem.v index 0482054..5e0dcc8 100644 --- a/Ch2_The_Martin_Loef_Theorem.v +++ b/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 diff --git a/Ch3_Formalising_Modal_Logics_in_Coq.v b/Ch3_Formalising_Modal_Logics_in_Coq.v index 747410d..a7e73d3 100644 --- a/Ch3_Formalising_Modal_Logics_in_Coq.v +++ b/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. diff --git a/Ch4_Formalising_the_Martin_Loef_Theorem___Challenges_and_Failed_Attempts.v b/Ch4_Formalising_the_Martin_Loef_Theorem___Challenges_and_Failed_Attempts.v index 3c114ef..55191ee 100644 --- a/Ch4_Formalising_the_Martin_Loef_Theorem___Challenges_and_Failed_Attempts.v +++ b/Ch4_Formalising_the_Martin_Loef_Theorem___Challenges_and_Failed_Attempts.v @@ -10,7 +10,7 @@ (** We can best demonstrate this by noting that neither [( ~ ~ q -> q)] nor [ ~ ( ~ ~ q -> q)] are intuitionistically provable. Thus there is a formula for which neither it nor its negation is intuitionistically provable. *) -(** Below, further details are given to show this is the case, and then the completeness theorems for intuitionistic logic are discussed in relation to this. We find that the intuitionistic completeness theorems do not mean that there don't exist formulae with neither a proof of themselves nor their negation, so in some sense these theorems are weaker than their classical counterparts. *) +(** Below, further details are given to show this is the case, and then the completeness theorems for intuitionistic logic are discussed in relation to this. We find that the intuitionistic completeness theorems do not mean that there don't exist formulae with neither a proof of themselves nor of their negation, so in some sense these theorems are weaker than their classical counterparts. *) (** ** Example: double negation elimination *) @@ -68,19 +68,30 @@ Qed. (** ** Completeness theorems *) -(** Completeness is a notion which in some sense does differ in meaning between classical%~\cite[p.~46]{completenessGodel, completenessBritannica, completenessDirk}% and intuitionistic%~\cite[p.~171]{intuitionisticLogicStanford, completenessDirk}% contexts, although it also retains its meaning in many ways between the contexts. One example of a difference is that in classical logic if some system is complete, then we can conclude that for every formula either it or its negation is provable. This however, is not the definition of completeness, but rather a consequence of it in classical contexts. For instance, in classical propositional logic, the fact that it is complete is generally defined to mean that every formula that is valid semantically is provable. For classical logic this then means that if we take an arbitrary formula, we can show that either it or its negation must be provable as follows, the key being the fact that $p \vee \lnot p$ is valid in classical logic for all propositions. %\\% *) +(** Completeness is a notion which in some sense does differ in meaning between classical%~\cite[p.~46]{completenessGodel, completenessBritannica, completenessDirk}% and intuitionistic%~\cite[p.~171]{intuitionisticLogicStanford, completenessDirk}% contexts, although it also retains many aspects of its meaning. One example of a difference is that in classical logic if some system is complete, then we can conclude that for every formula either it or its negation is provable. This however, is not the definition of completeness, but rather a consequence of it in classical contexts. For instance, in classical propositional logic, the fact that it is complete is generally defined to mean that every formula that is valid semantically is provable. For classical logic this then means that if we take an arbitrary formula, we can show that either it or its negation must be provable as follows, the key being the fact that $p \vee \lnot p$ is valid in classical logic for all propositions. %\\% *) (** Consider classical propositional logic, with semantics and provability (or deduction) defined such as in the Stanford Encyclopedia of Philosophy article on classical logic%~\cite{sep-logic-classical}%. %\\% -Here, if a formula [p] is valid semantically this is denoted by $\vDash p$. If a formula [q] is provable this is denoted $\vdash q$. - -% -\begin{figure}[H] - \centering - \includegraphics[width=1\linewidth]{proof2} -\end{figure} -% - -We see here that completeness for classical logic implies that for every $p$, either $p$ or $ \lnot p$ is provable. +Here, if a formula [p] is valid semantically this is denoted by $\vDash p$. If a formula [q] is provable this is denoted $\vdash q$. *) + +(** %\vspace{1em}% +Classical propositional logic is complete, so every valid formula is provable, if $\vDash p$ then $\vdash p$. +%\begin{enumerate} \setlength{\itemsep}{0pt} \setlength{\parskip}{0pt}% + %\item% Let $p$ be an arbitrary propositional formula. + %\item% [p \/ ~p] is valid, $\vDash$ [(p \/ ~p)] + %\item% Thus, by the definition of satisfaction, $\vDash$ [p] or $\vDash$ [~p] + %\item% Suppose $\vDash$ [p] + %\vspace{-0.5\topsep} \begin{enumerate} \setlength{\itemsep}{0pt} \setlength{\parskip}{0pt}% + %\item[a.]% Then, by completeness we have that $\vdash$ [p] so [p] is provable. We are done. (Either [p] or [~p] is provable.) + %\end{enumerate}% + %\item% Suppose $\vDash$ [~p] + %\vspace{-0.5\topsep} \begin{enumerate} \setlength{\itemsep}{0pt} \setlength{\parskip}{0pt}% + %\item[a.]% Then, by completeness we have that $\vdash$ [~p] so [~p] is provable. We are done. (Either [p] or [~p] is provable.) + %\end{enumerate}% + %\item% Therefore either [p] or [~p] is provable. +%\end{enumerate}% + *) + +(** We see here that completeness for classical logic implies that for every $p$, either $p$ or $ \lnot p$ is provable. For intuitionistic logic however, since we relied on $p \vee \lnot p$ as being valid in step 2 the above reasoning would not work since $p \vee \lnot p$ is not valid in intuitionistic logic. %\\% Clarifying this was helpful in the process of gaining a greater understanding of the key notions of the Martin-%\Loef{}% Theorem. @@ -168,7 +179,7 @@ Qed. Require Import Setoid. (* end hide *) -(** Now we can show that [absolutely_undecidable p] is equivalent to [~ (p \/ ~ p)]. This is not necessarily a problem, as it may only be showing that [absolutely_undecidable p] is false (since [~ (p \/ ~ p)] is false). But of concern is the simplicity of the proof which highlights that [absolutely_undecidable p] may have a similar _meaning_ to [~ (p \/ ~ p)]. This would seem to be an oversimplification of the intended meaning of the notion `absolutely undecidable'. *) +(** Now we can show that [absolutely_undecidable p] is equivalent to [~ (p \/ ~ p)]. This is not necessarily a problem, as it may only be showing that [absolutely_undecidable p] is false (since [~ (p \/ ~ p)] is false). But of concern is the simplicity of the proof, which highlights that [absolutely_undecidable p] may have a similar _meaning_ to [~ (p \/ ~ p)]. This would seem to be an oversimplification of the intended meaning of the notion `absolutely undecidable'. *) Lemma absolutely_undecidable_is_oversimplified : forall p, absolutely_undecidable p <-> ~ (p \/ ~ p). diff --git a/Ch5_Formalising_the_Martin_Loef_Theorem___Formalisation_in_CS4_plus_Int.v b/Ch5_Formalising_the_Martin_Loef_Theorem___Formalisation_in_CS4_plus_Int.v index 119a468..1ede481 100644 --- a/Ch5_Formalising_the_Martin_Loef_Theorem___Formalisation_in_CS4_plus_Int.v +++ b/Ch5_Formalising_the_Martin_Loef_Theorem___Formalisation_in_CS4_plus_Int.v @@ -177,7 +177,7 @@ Qed. Axiom diaT : forall A, True (A ⇒ (◊ A)). ] *) -(** This axiom claims that for all propositions in CS4 and intuitionistic logic, that if they are true then they can be known. This seems reasonable, however at the same time it also seems very close to saying there are no undecidable propositions (if everything that is true can be known then surely nothing is unknowable). So perhaps the axiom is stating too much. *) +(** This axiom claims that for all propositions in CS4 and intuitionistic logic, if they are true then they can be known. This seems reasonable, however at the same time it also seems very close to saying there are no undecidable propositions (if everything that is true can be known then surely nothing is unknowable). So perhaps the axiom is stating too much. *) (** %\vspace{1em}% *) @@ -223,13 +223,13 @@ Proof. intro. apply diaT. Qed. (** * Extending to Martin-%\Loef{}%'s Theorem *) -(** In order to prove Martin-%\Loef{}%'s Theorem, two additional axioms are required. They are Fact 2 and Fact 4 from Martin-%\Loef{}%'s argument as discussed in chapter 2 and in the Logicomp 301 slides%~\cite{crisslides}%. *) +(** In order to prove Martin-%\Loef{}%'s Theorem, two additional axioms are required. They are similar to Fact 2 and Fact 4 from Martin-%\Loef{}%'s argument as discussed in chapter 2 and in the Logicomp 301 slides%~\cite{crisslides}%. *) -(** Fact 2 states: %\emph{"If $A$ can be known to be true and $B$ can be known to be true, then $A\wedge B$ can be known to be true."}% It can be formalised as given below. *) +(** Fact 2 states: %\emph{"If $A$ can be known to be true and $B$ can be known to be true, then $A\wedge B$ can be known to be true."}% It turns out that slightly altered versions of Fact 2 and Fact 4 are required. The axioms needed are more basic. Informally, for Fact 2 we instead have %\emph{"If $A$ is true and $B$ is true, then $A\wedge B$ is true."}%. *) Axiom fact_2 : forall A B, (True A /\ True B) <-> True (A ∧ B). -(** Fact 4 states: %\emph{"One and the same proposition $A$ cannot both be known to be true and be known to be false."}% It can be formalised as given below. *) +(** Fact 4 states: %\emph{"One and the same proposition $A$ cannot both be known to be true and be known to be false."}%. Instead we have %\emph{%"For any proposition [A], it is not the case that [A ∧ (¬ A)] is true."%}%. *) Axiom fact_4 : forall A, ~ (True (A ∧ (¬ A))). diff --git a/Ch6_Formalising_the_Martin_Loef_Theorem___Formalisation_of_Intuitionistic_Logic.v b/Ch6_Formalising_the_Martin_Loef_Theorem___Formalisation_of_Intuitionistic_Logic.v index a32ee97..f27fbbd 100644 --- a/Ch6_Formalising_the_Martin_Loef_Theorem___Formalisation_of_Intuitionistic_Logic.v +++ b/Ch6_Formalising_the_Martin_Loef_Theorem___Formalisation_of_Intuitionistic_Logic.v @@ -48,7 +48,7 @@ Inductive proposition := Parameter Implication_Is_True : proposition -> proposition -> Prop. -(** Now we define what constitutes a proof of a [proposition]. By using an inductively defined proposition the notion that these rules are the only possible ways to obtain a proof is captured. *) +(** Now we define what constitutes a proof of a [proposition]. By using an inductively defined proposition, the notion that these rules are the only possible ways to obtain a proof is captured. *) Inductive Proof : proposition -> Prop := | atom_ev : forall (A:Atoms), AtomValuation A = true -> Proof (Atom A) @@ -68,7 +68,7 @@ Axiom implies_ev' : forall p q, Implication_Is_True p q <-> (exists (f: Proof p (** %\newpage% *) (** -------------- *) -(** In a similar way to with the bi-modal logic embedding, the definitions required to embed intuitionistic logic are now all defined. Only notation, lemmas and theorems are defined below and these do not alter what propositions are expressible and provable in this embedding of intuitionistic logic in Coq. *) +(** In a similar way to the bi-modal logic embedding, the definitions required to embed intuitionistic logic are now all defined. Only notation, lemmas and theorems are defined below and these do not alter what propositions are expressible and provable in this embedding of intuitionistic logic in Coq. *) (** -------------- *) (** ** Notation *) @@ -213,6 +213,6 @@ Qed. (** * Comments on this formalisation *) (** A key advantage of this formalisation is that it does not rely on axioms other than those fundamental to intuitionistic logic. The only two non-standard axioms are found in the definition of what constitutes a proof in the system. %\\% -[K_ev] is essentially an axiom which states that %$$%[forall (p : proposition), Proof p -> (Proof (K p))].%$$%This potentially does not capture the notion of knowability properly. It is part of an inductive definition, so implicit in the axiom is that the _only_ way one can show that a proposition is knowable is by exhibiting a Coq proof for [Proof p]. It may be that there are other ways of knowing that are not captured by this axiom. For instance we may be able to know by analysing the axioms of intuitionistic logic that double negation elimination, [ ~ ~ q -> q], is not knowable yet we would not be able to prove [Proof ~ (K ( ~ ( ~ q) -> q))]. %\\% +[K_ev] is essentially an axiom which states that %$$%[forall (p : proposition), Proof p -> (Proof (K p))].%$$%This potentially does not capture the notion of knowability properly. It is part of an inductive definition, so implicit in the axiom is that the _only_ way one can show that a proposition is knowable is by exhibiting a Coq proof for [Proof p]. It may be that there are other ways of knowing that are not captured by this axiom. For instance we may be able to know by analysing the axioms of intuitionistic logic that double negation elimination, [ ~ ~ q -> q], is not knowable, yet we would not be able to prove [Proof ~ (K ( ~ ( ~ q) -> q))]. %\\% The second non-standard axiom is that the only way to show that [Proof (A ⇒ B)] is true is to show that [(exists (f: Proof p -> Proof q), True )]. This can be simplified to [Proof p -> Proof q]. A possible concern with this axiom is it allows [Proof (A ⇒ B)] to be proven whenever the implication [Proof p -> Proof q] is true rather than when there is indeed a function that takes a proof of [p] and returns a proof of [q]. This means that alterations to the meta-language logic could sometimes filter down into the embedding of intuitionistic logic, potentially causing issues. %\\% Overall however, this formalisation does a good job at capturing certain elements from Martin-%\Loef{}%'s proof and is useful for gaining a deeper understanding of the Martin-%\Loef{}% Theorem. *) \ No newline at end of file