2023-11-22-declare-prove-use.tex (7880B)
1 \documentclass[../main.tex]{subfiles} 2 3 \begin{document} 4 5 \section{2023-11-22 Declare, prove, and use} 6 7 In the Logic of Assumptions, judgments appear under three 8 different \emph{moods}. That is, these syntactical objects wich 9 express judgments, without any commitment, can appear or be 10 refered to in places where they take on different meanings. 11 12 The three moods are those of \definiendum{declaration}, 13 \definiendum{assertion}, and \definiendum{use}. 14 15 There is also an interplay between them. The three moods grant 16 rights and impose demands (under the general obligation of the 17 user to say coherent things), which involve the other moods. 18 19 It works like this: 20 21 \begin{description} 22 \item[Declare] When one declares a judgment, one is taking it 23 to be true. This can be read in a few ways. For one, it can be 24 thought of as a \emph{postulate} -- \ie, the assertion that, 25 pragmatically, from now on, we'll take that judgement to the 26 the case. On the other hand, hooking into the double meaning 27 of theories in the Logic of Assumptions, we can understand a 28 declaration as a specification of part of the interface such a 29 theory is describing -- \ie, from then on, we're talking about 30 contexts which implement this judgment. 31 32 To declare something, one must \emph{prove} its 33 pressupositions. So, here, in order to \emph{be able} to declare, 34 one \emph{is required} to prove. 35 36 \item[Proof] To prove a judgment (in a collection of contexts) 37 means to establish that context implements that judgment. Or, in 38 the dual reading, that under the assumptions from such context, 39 we can conclude the given judgment. And, since judgments are 40 hypothetical, this means one can draw the conclusion of the 41 judgment if one has its hypothesis. 42 43 Proof is impositional. One, at least intentionally speaking, 44 doesn't \emph{choose} to prove. One is \emph{required} to do 45 so. But the counterpart is this: when such imposition is made, 46 we also get the right to \emph{use} the assumptions of the 47 judgment, besides the given context. The movement is ``assume 48 the hypotheses, show the conclusion'', and so the mood of proof 49 enables the mood of use. 50 51 \item[Use] To use a judgment means to refer to it when it is 52 already established -- that is, declared. But \emph{use}, in this 53 sense, means to apply judgments as rules. That is, if we wish 54 to use the conclusion (\eg, in the course of an ongoing proof), 55 one must first \emph{prove} the hypotheses of the judgment under 56 the current context. So \emph{use} demands both \emph{proof} 57 and \emph{declaration}. 58 59 \end{description} 60 61 To summarize: 62 63 \begin{itemize} 64 \item To declare, one must prove (the pressupositions). 65 \item To prove, one \emph{can} use. 66 \item To use, one must prove (and have declared). 67 \end{itemize} 68 69 In practice, the flow of theory development is a sequence 70 of declarations. On each declaration, we prove the 71 pressupositions. And then we alternate between \emph{having to 72 prove} judgmenets, thereby enabling the use of its hypotheses, 73 and \emph{being able to use} judgments, which requires us to 74 prove its hypotheses. 75 76 \subsection{Implementation} 77 78 Let's think of the data structures needed to keep track of all these needs ands cans. 79 80 When building a theory, on the top level, we are always declaring 81 judgments. On the context, we have two structures. 82 83 The first is the \definiendum{goal tree}, which is a tree made 84 of judgments. If the tree is not empty, the root represents the 85 judgment currently being declared, and it is a \definiendum{use 86 node}. Goal nodes have zero or one child, which (if it exists) 87 represent the judgment that is being used to prove that 88 goal. The children of a used judgment are the goals that it 89 entails. Additionally, the forest has a \emph{pointer}. 90 91 The other is for \definiendum{assets}, or things which we've 92 gotten granted the right of using, and it is an assoctiation 93 list between names and judgments (with links to the places 94 in the goal tree where they were introduced). 95 96 When focusing on something to prove, or when using something, 97 those lists will be modified. 98 99 So, at any point in top-level, we've got an empty tree of 100 goals (\ie, we have a valid theory so far), and all previous 101 declarations show up as assets. Here's how states work: 102 depending on the goal tree, the user has some valid actions, 103 and each action generates some changes to the state. 104 105 \begin{tabular}{lcr} 106 Condition & Actions & Parameters \\ 107 \hline 108 The tree is empty & Declare a judgment & A judgment \\ 109 The focused goal has a candidate & Focus on a subgoal & An index \\ 110 The focused goal has no candidate & Use an asset to prove the goal & A name 111 \end{tabular} 112 113 Here's what the actions do: 114 115 \begin{description} 116 \item[Declare] Place each pressuposition of the judgment as a 117 root in the goals tree, with no candidate. 118 119 \item[Focus] Add that subgoal's assumptions the assets table, 120 with a link to the subgoal. Focus on the subgoal. 121 122 \item[Use] Set the given name as the candidate for the focused 123 goal. If the name refers to an asset with assumptions, place those 124 assumptions as children of the current goal with no candidates. If 125 it does not, and it matches the focused goal, simply remove the 126 focused goal, remove assets introduced at that goal, and shift 127 focus to its parent. If instead it does not match, raise an error. 128 \end{description} 129 130 There's one thing missing from this description, which is 131 how to build subcontexts. Ideally, those would come from the 132 same process as the top-level context. And, actually, even the 133 top-level context can reasonably be expected to be packaged in 134 much the same way as the subcontexts. So, this suggests the 135 following approach, analogous to how we are handling goals: 136 build a context, then package it up into a subcontext of a new 137 goal. Repeat. 138 139 One choice: we have to either signal where we are \emph{starting} 140 a new subcontext (which drops us into the children of a 141 yet-to-be-defined judgment), or we can say, when \emph{closing} 142 it, where it starts (perhaps by refering to a label). The latter 143 is kinda clumsy and not very readable. So let's go for the first. 144 145 An alternative to the use-focus duo, and which would be terser, 146 would be to automatically focus on the first subgoal, when 147 applicable. An example of syntax for this second style could be 148 like this: 149 150 \begin{lstlisting} 151 #syntax suffix wff 152 #syntax infix : 153 #syntax suffix wft 154 155 { // start subcontext 156 [cv] x var 157 } [var-wff] x wff 158 159 { 160 [cc] c const // No pressups 161 } [cw] c wff; 162 163 [tc] type const // No pressup 164 [tt] type wft // Pressuposition: `type wff` 165 cw // Adds cc as subgoal 166 tc // Solves it, unifies `c` and `type` 167 168 169 { 170 [av] a var // No pressupositions 171 [at] a : type // Pressup `type wft`, `a wff` 172 tt // Solves first 173 var-wff // Adds cv 174 av // Solves it, unifies 175 } [type-wft] a wft 176 \end{lstlisting} 177 178 \subsection{Discussion} 179 180 The way we are approaching this is not the way its usually done 181 in logic, but rather in the narrow field of proofs assistants. In 182 the end, its the same thing: in logic, we describe these pristine 183 objects, regardless of how they could be built, and provide 184 validity conditions that distinguish them among the many others 185 syntactically correct, but invalid siblings. 186 187 In proof assistants, we describe \emph{programs} that run on 188 machines which \emph{build} such objects. A valid object, then, is 189 one that can be built by this machine using a particular program. 190 191 It's the same thing with grammars and automata. 192 193 The objects that we are describing are the contexts in the Logic 194 of Assumptions. They are a dependent list of assumptions, each 195 possibly using and refering to the previous ones, each carrying 196 with it the necessary proofs of its pressupositions. But, 197 of course, its easier to think about how one would go about 198 \emph{building} such a thing. 199 200 \end{document}