main.tex (6187B)
1 \documentclass{article} 2 3 \usepackage[english]{personal} 4 5 \setmainfont{EB Garamond} 6 % \setmonofont{} 7 % \setsansfont{} 8 \setmainlanguage{english} 9 10 \title{A Logic of Assumptions} 11 \author{Juan F. Meleiro} 12 \date{2023} 13 14 \begin{document} 15 16 \maketitle 17 18 A logical system is usually composed of a series of data. At least a type of signatures; and for each signature a type of judgments; and for each judgment a type of proofs; or alternativelly a notion of (in)compatibility between the judgments; etc. 19 20 But could we subsume all this concepts into a single one? Yes, I believe, and that would be the concept of \emph{assumption}. More specifically, of \emph{relative assumptions}. Let's get straight into it. 21 22 The system is composed of two layers. The first, purely combinatorial. It has two concepts, which define just the plain syntactical objects (grammar notwithstanding). Those are \definiendum{terms} and \definiendum{judgment forms}. 23 24 Then, the second layer, properlyl logical. It contains five interconected concepts, the most substantial of which is the \definiendum{assumption}, as we said. Assumptions are organized into \definiendum{contexts}, which relate to one another via \definiendum{translations}, which can be \definiendum{applied} to terms, and that is the basis of \definiendum{proofs}, which finally make assumptions well-formed. 25 26 So, schematically, 27 28 \begin{center} 29 \parbox{\textwidth}{ 30 \framebox[0.5\textwidth]{Terms} 31 \framebox[0.5\textwidth]{Judgments} 32 } 33 \parbox{\textwidth}{ 34 \framebox[0.2\textwidth]{Assumptions} 35 \framebox[0.2\textwidth]{Contexts} 36 \framebox[0.2\textwidth]{Translations} 37 \framebox[0.2\textwidth]{Application} 38 \framebox[0.2\textwidth]{Proofs} 39 } 40 \end{center} 41 42 \section{Definitions} 43 44 We start by supposing a fixed type for symbols \note{which must include three distinguished symbols called $\mathsf{symb}$, $\mathsf{var}$, and $\mathsf{judg}$}. 45 46 \begin{definition}[Terms] 47 \definiendum{Terms} are labelled trees of symbols. That is, a symbol called its \definiendum{head} plus a list of terms called its \definiendum{subterms}. 48 \end{definition} 49 50 \begin{definition}[Judgment forms] 51 \definiendum{Judgment forms} are a family of symbols associated with arities. Each judgment form has some \definiendum{pressupositions} which are other judgment forms using the same arguments. 52 \end{definition} 53 54 That's it for syntax. 55 56 Now for the logic. 57 58 \begin{definition}[Context] 59 A \definiendum{context} is either empty or a context (called its \definiendum{precontext}) and an assumption over it. 60 \end{definition} 61 62 \begin{definition}[Assumption] 63 An \definiendum{assumption} over a context is a judgment, a context (called its \definiendum{subcontext}), plus proofs for its pressupositions under the given context and the subcontext. 64 \end{definition} 65 66 \begin{definition}[Proof] 67 A \definiendum{proof} of a judgment in a collection of contexts is an assumption in one of them, plus a morphism from its subcontext into the collection. 68 \end{definition} 69 70 \begin{definition}[Morphism] 71 A morphism from a context (the \definiendum{domain}) into a collection of contexts (the \definiendum{codomain}) is 72 \begin{itemize} 73 \item If the domain is empty, nothing. 74 \item If the domain is a precontext and an assumption, a morphism from that precontext to the codomain plus a function taking a morphism from the assumptions subcontext to the codomain to a proof in the codomain of the translation of the assumption's judgment under the precontext morphism. 75 \end{itemize} 76 \end{definition} 77 78 \begin{definition}[Translation] 79 The translation of a judgment via a morphism is that same judgment form applied to the translated terms. A term translated via a morphism is the term associated with its head symbol with the translated subterms substituted into the variables. 80 \end{definition} 81 82 \section{Examples} 83 84 Let's build modus ponens. Our judgments are unary $\mathsf{true}$, unary $\mathsf{prop}$, plus the standard ones $\mathsf{symb}$ and $\mathsf{var}$. $\mathsf{true}$ judgments pressupose $\mathsf{prop}$ ones, and $\mathsf{prop}$ ones pressupose $\mathsf{var}$ ones (this means \emph{not} that all propositions are variables, but that to \emph{assume} something is a proposition, it must be known to be a variable). 85 86 \begin{lstlisting}[ 87 mathescape=true, 88 literate={=>}{{$\Rightarrow$}{ }}{2}{:=}{{$\defeq$}}{1}{->}{{$\to$}{ }}{2}, 89 basicstyle=\sffamily, 90 ] 91 var2prop { 92 var$_\alpha$ {} $\alpha$ var 93 triv 94 } $\alpha$ prop 95 96 fn-form { 97 var$_\alpha$ {} $\alpha$ var 98 triv 99 var$_\beta$ {} $\beta$ var 100 triv 101 prop$_\alpha$ {} $\alpha$ prop 102 prop$_\beta$ {} $\beta$ prop 103 } $\alpha$ -> $\beta$ prop 104 105 mp { 106 var$_\alpha$ {} $\alpha$ var 107 triv 108 var$_\beta$ {} $\beta$ var 109 triv 110 maj {} $\alpha$ -> $\beta$ true 111 fn-form 112 var$_\alpha$ => $\alpha$ 113 var$_\beta$ => $\beta$ 114 prop$_\alpha$ => var2prop 115 var$_\alpha$ => $\alpha$ 116 prop$_\beta$ => var2prop 117 var$_\alpha$ => $\alpha$ 118 min {} $\alpha$ true 119 var2prop 120 var$_\alpha$ => $\alpha$ 121 } $\beta$ true 122 var2prop 123 var$_\alpha$ => @var$_\beta$ 124 125 dt { 126 var$_\beta$ {} $\beta$ var 127 triv 128 var$_\alpha$ {} $\alpha$ var 129 triv 130 prop$_\beta$ {} $\beta$ prop 131 var$_\beta$ 132 prop$_\alpha$ {} $\alpha$ prop 133 var$_\alpha$ 134 hyp { 135 cond {} $\alpha$ true 136 prop$_\alpha$ 137 } $\beta$ true 138 prop$_\beta$ 139 } $\alpha$ -> $\beta$ true 140 fn-form 141 var$_\alpha$ => @var$_\alpha$ 142 var$_\beta$ => @var$_\beta$ 143 prop$_\alpha$ => var2prop 144 var$_\alpha$ => @var$_\alpha$ 145 prop$_\beta$ => var2prop 146 var$_\alpha$ => @var$_\beta$ 147 \end{lstlisting} 148 149 \end{document}