On the most general concept of a formal logic

Let us look at 'logic' from the most abstract and general perspective possible. We fix a set of tokens $T$. We also consider a well-defined (computable) subset $ S \subset T^*$ of well-formed expressions. But now we must fix from the start a stratification of $S$ into disjoint syntactic categories $S_i$, $i=0,...n$, where $S_0$ is considered as a distinguished subset of $T^*$. In general a string in $S_i$ will have substrings in $S_j$ for $j> i$ but also possibly substrings in $S_m$ for $m \geq i$. We expect a general element of $S_0$ to be a concatenation of syntactic symbols $\square$ (tokens in the strings of $S_0$ which are not in the other $S_i$) and strings in the $S_i$: $ s_1\square_1 s_2\square_2... \square_k s_k$ and likewise for the $s_i$ until reaching atomic or indecomposable syntactic categories. We may think of the above decomposition in $S_0$ as expressing a sentence as a predicate with arguments. A type 1 logic $\mathbb{L}$ is a finite set of partial computable functions $\{L_m\}_{m \in M}$ \[ L_m: S_0^n \times P \rightarrow S_0\] where $n\geq 0$ is the arity of $L$ and $P$ is a subset of $S^p$ called the parameter space of arity $p \geq 0$. We can also write $L (s,p) = \bullet$ when $L$ is undefined. We write $L_{m,n,p}$ to indicate the index and arities. It is straightforward to define the notion of proof (either in linear or tree-form) and proof from a given set of hypotheses. For $H \subset S_0$ let $D(H)$ denote the set of all provable elements of $S_0$ using $H$. In general $D(\emptyset)$ will generalize both axioms and definitions (but there are some subtleties here). Note that if $s \in D(A)$ and for all $a \in A$ we have $a \in D(B)$ then $s \in D(B)$ (cut rule). If we interpret $S_0$ as 'sentences' then then type 1 logic have the problem of not being able to deal directly with discharging hypotheses natural deduction style. So instead we can generalize sequent calculus style logic by considering a further syntactic category $S_{-1}$ for sequents, that is, elements of $S_0^\star \times S_0^\star$. Then a type 2 logic is defined in terms of partial computable functions $\{L_m\}_{m \in M}$ \[ L_m: S_{-1}^n \times P \rightarrow S_{-1}\] In what follows we work with $S_0$ but there should, we hope, be no difficulty adapting the definitions to type 2 logics. It is clear that these two types of logic are directly based on Hilbert style and sequent calculi. We could of course also consider a type 3 logic based on natural deduction, that is, incorporating dependencies and discharging. We can look at logic from an even more general point of view. Take $S_T$ to be an concatenations of elements of $S_0$ (sentences). Then a logic is a computable relation \[ S_T \vdash_L S_T \] We can think of this relation as a 'transformer' in the sense of computational linguistics. A logic gives as for each set of sentences legitimate completion in the form of further text, a map $ L : S_T \rightarrow \mathbf{P} S_T$. It is now our task to give the most general and abstract versions of the usual logical notions. The easiest is conjunction. A logic is called conjunctive if there is a total computable function $\& : S_0 \times S_0 \rightarrow S_0$ such that for all $s,s' \in S_0$ we have that $ D(\{s,s'\}) = D(s)\cup D(s')$. A logic has absurdity if there is a $abs \in S_0$ such that $D(abs) = S_0$. An important property of $S$ involves abstraction. Given a $t \in S_i$ occurring in $s \in S_0$. Consider the set $\lambda t. s$ of all strings in $T^*$ obtained from $s$ by replacing $t$ with elements of $S_i$. Then $S$ has abstraction if $\lambda t.s \subset S_0$ for all such $t$ and $s$. A logic is called universalizing if for any $s \in S_0$ and $t \in S_i$ occurring in $s$ there is a $u(s,t) \in S_0$ such that $\lambda t.s \subset D(u(s,t)) $. This definition implies that the language has abstraction. I think being conjunctive and universalizing are the most basic conditions for a 'logic' to be a logic. Note that variables are optional, variable-free style logics can also deal with generality. Indeed variables do not seem directly relevant in our very abstract approach. Implication might be characterized as given $s,t \in S_0$ there is computably determined expression $Imp(s,t) \in S_0$ such that $ D(t) \subset D(\{s, Imp (s,t)\})$ and perhaps also: if $t \in D(s)$ then $ Imp(s,t) \in D(\emptyset)$. What is 'negation' ? We view negation as attaching to each sentence $s$ a subset $\dagger s \subset S_0$ of sentences which are interpreted as sentences immediately contradictory to $s$. All the elements of $\dagger s$ must be mutually derivable and if we consider $\dagger (\dagger s) = \{\dagger t : t \in \dagger s\}$ then $s$ itself must be in $\dagger (\dagger s)$. We can now define general versions of consistency, paraconsistency and compactness. We also obtain the famous tetralemma, all four possibilities can occur for a general logic. We can classify rules as anabolic, katabolic or mixed. Anabolic rules are when the application of the rule contains the arguments as substrings (this needs to be adapted slightly for sequents). Katabolic is when the result of the rule is a substring of an argument. Mixed when neither. A rule is uniformly determined when given the result of its application to concrete values its value on any argument can be obtained via a process of substitution on this concrete instance. Uniform rules are logical rules that can be given in standard table form via syntactic metavariables (and provisos). We can go more and more in the concrete direction until arriving at the concepts usually studied in philosophical logic. What about definitions of terms, that is, elements of $t \in S_i$ for $i> 0$. If we have some generalized concept of equality between elements of $S_i$ then things will be easier. For then we can convert this into a problem for $S_0$, into 'what is means to be $t$', finding a sentence which is 'satisfied' only by $t$ up to equality. But otherwise we can consider the set $C(t)$ of elements of $D(\emptyset)$ in which $t$ occurs. Then a type 1 definition is a small finite subset $\Delta(t)$ of $C(t)$ such that $C(t) \subset D(\Delta(t))$. A type 2 definition is a weakening of the previous type. It is a 'brief description' of $t$ giving some salient features of $t$ so that 'most' of $C(t)$ can be deduced from these. It is interesting to compare this to reconstructions of the Stoic theories of definition.