\documentstyle[12pt,a4]{article} \date{} \input amssym.def \begin{document} \begin{center}{\bf AXIOMATIZABILITY OF LOGICAL MATRICES}\\ Piotr Wojtylak ,{\it Silesian University, Katowice} \end{center} {\bf 1.} The completeness theorem for classical propositional logic was proved by Emil Post [1921]. Let ${\goth M}_2$ be the classical two-valued matrix and let $E({\goth M}_2)$ denote the set of all its tautologies, that is propositional formulae valid in the matrix. The completeness theorem $$E({\goth M}_2)=Cn(\{r_0,r_*\},A_2).$$ says that any ${\goth M}_2$ tautology can be derived by use of two inferential rules: substitution for propositional variables $r_*$ and detachment (modus ponens) rule $r_0$ from a finite set $A_2$ of axioms (which are tautologies, too). This form of axiomatization (substitution, detachment and a finite set of axioms) became then a standard in propositional logic. Post referred to axioms given earlier by G.Frege and showed the completeness theorem using (conjunctive) normal forms of formulae. The completeness theorem, with the same argument, was then rediscovered by several logicians who were unaware of the earlier paper by E. Post. It shows the significance of the result and probably means that normal forms provide the most natural way of proving the theorem. Others, more interesting, methods of proving (for example by the construction of Lindenbaum algebra) were provided much later on. The completeness theorem is maintained as one of the most fundamental results in logic and is included in probably all elementary courses in logic. The possibility of elementary proving all classically valid formulae fascinates and attracts our attention. Nevertheless, let me make the following two general remarks.\\ \indent a) We still seem to believe that any concept in science is accompanied with a finite set of natural axioms characterizing it. We seem to forget that the axiomatizabilty method, the ingenious discovery of ancient Greeks, shows only certain weaknesses of human nature and is not occurring immanently in the nature. The development of logic did not confirm the priority of one axiom system (for propositional logic) over others. Axioms may differ very roughly and I would even say that each logician has its own preferred axiom system for classical propositional logic. The choice of the method of proving the completeness theorem decides mostly on the choice of the set of axioms. Certainly, not any set equivalent (with respect to the substitution and detachment rule) to $A_2$ may be widely accepted as a set of axioms. For instance, the proposal of J. /Lukasiewicz with a single axiom $$((((p\to q)\to(\neg u\to\neg s))\to u)\to t)\to((t\to p)\to (s\to p)),$$ which is known to be the shortest formula with this property, has not been widely accepted. Any axiom system for classical propositional logic should be intuitively clear and should consist of relatively simple formulae. Despite some attempts, no formal general conditions obeyed by any acceptable set of axioms was given. In this situation it seems to be proper to say about axiomatizabilty of the matrix ${\goth M}_2$ rather than the completeness theorem. \\ \indent b) In case of propositional logic there raises a more general question if any axiom system is really needed. What are the adventages of the axiomatizability method there. This question disappears in predicate logic where the axiomatizability method is in fact the only possibility to introduce all classically valid laws. To support the significance of the axiomatizability method in propositional logic one could refer today to results in complexity theory. But this kind of argument could not be used in Post times though the completeness theorem was valued. Probably, the most important fact as concerns the result in questions is the reduction of possibly infinite the set of classical tautologies to its finite subset.\\ {\bf 2. } As soon as non-classical systems appeared in logic, the problem of their axiomatizability was posed immediately. It was natural as much as the first systems of non-classical logics were introduced by logical matrices. There were the so-called systems of Post and /Lukasiewicz. Let me say that the main difference between these two groups of logics was the existence of a kind of philosophical motivation for /Lukasiewicz logics whereas Post systems were motivated only formally. This philosophical motivation, despite the fact if it was correct or not, attracted an interest. Let me focus on /Lukasiewicz logics. This is not due to the fact that any formal result confirms the philosophical significance of the systems. Contrary, it seems to me that it does not. But /Lukasiewicz logics provide a nice illustration for the discussed in this lecture question of axiomatizability. So, similarly as for Post systems, the motivation for /Lukasiewicz logics is only formal. \\ \indent a) The problem of axiomatizability of /Lukasiewicz logics was by no means one of the most important questions in the so-called Lwow-Warsaw school of logic in the twenties and thirties. The most important results in this field were achieved by M. Wajsberg. In particular, he provided an axiomatization for the three-valued logic, $$E({\goth M}_3)=Cn(\{r_0,r_*\},A_3).$$ This axiomatization was widely accepted and was often referred to. Wajsberg also confirmed /Lukasiewicz conjecture and showed the completeness theorem for the infinite valued logic $$E({\goth M}_\infty)=Cn(\{r_0,r_*\},A_\infty).$$ Let me recall that the set $A_\infty$ consists of the formulae $$ p\to(q\to p))\quad,\quad (p\to q)\to ((q\to s)\to (p\to s)),$$ $$((p\to q)\to q)\to((q\to p)\to p)\quad,\quad(\neg p\to\neg q)\to(q\to p).$$ In /Lukasiewicz conjecture there also occurred $((p\to q)\to (q\to p))\to(q\to p)$ which was showed to be dependent by D. Meredith. Unfortunately, Wajsberg's proof has never been published and first (non-elementary) proof of this theorem was given by C.C. Chang [1955]. An elementary proof of this theorem may be found in R. Cignoli, D. Mundici [1997]. \\ \indent b) For remaining /Lukasiewicz logics no sets of axioms was regarded in the thirties. Wajsberg [1935] showed a general theorem from which finite axiomatizability of any $n$-valued /Lukasiewicz logic immediately follows.\\ {\sl If ${\goth M}$ is a finite and normal (ie the detachment rule is normal) matrix and $A_w\subseteq E({\goth M})$, then $E({\goth M})$ finitely axiomatizable by use of substitution and detachment rule. The set $A_w$ consists of} $$ (p\to q)\to ((q\to s)\to (p\to s))\quad,\quad (q\to s)\to ((p\to q)\to (p\to s)),$$ $$(p\to p)\to(q\to q))\quad,\quad (p\to q)\to (\neg q\to \neg p)\quad,\quad\neg q\to ((p\to q)\to \neg p)).$$\\ The proof of this theorem contains an algorithm for searching of a finite set of axioms for any given finite matrix. But the algorithm is very difficult and useless for any practical reason. Apparently Wajsberg was unable to reduce the received, in the case of $n$-valued /Lukasiewicz logics, sets of axioms to an acceptable form. Some solution of this problem can be found in W.A. Pogorzelski , P.Wojtylak [1993] and R.Tuziak [1988]. There is shown that $$E({\goth M}_n)=Cn(\{r_0,r_*\},A_n)$$ where $A_n$ results from $A_\infty$ by addoing formulae of the form (for appropriate $k$'s) $$(p\to^nq)\to (p\to^{n-1}p)\quad ,\quad p\equiv (p\to^k\neg p)\to^{n-1}q$$ {\bf 3.} Results on axiomatizability of logical matrices achieved in the thirties though deep and sophisticated showed certain difficulties. Logicians could not overcome problems raised by additional informal restrictions on intuitive meaning of axioms and formal restrictions to axiomatizations based on two inferential rules of inference: substitution and detachment. The further progress in the area was mostly due to the change of the point of view on logical systems. Logic was ceased to be seen as a set of logical laws (tautologies) and more attention was given to its inferential rules. Logical systems were described in terms of consequence operations where not only the set of tautologies plays a role but all theories over the logic are important. If one takes into account logical rules other than substitution and detachment, then any restriction to detachment-substitutionary axiomatizations should be neglected. The change of the point of view, together with additional concepts such as matrix consequence operation and structural completeness, creates a number of new problems and benefits with a number of interesting results. It also made the theory of axiomatizability of logical matrices more attractive and interesting.\\ \indent a) In the theory of logical matrices, the change of the point of view realized by use of the concept of the matrix consequence operation; J. /Lo/s, R. Suszko [1958]. Let ${\goth M}=({\cal A},D)$ be a logical matrix in a propositional language $S$. The operation $\overrightarrow{{\goth M}}:2^S\to 2^S$ is defined as follows $$ \alpha\in\overrightarrow{{\goth M}}(X) \equiv \forall_{v:At\to A}\ [h^v(X)\subseteq D \rightarrow h^v(\alpha)\subseteq D]$$ One easily shows that $overrightarrow{{\goth M}}$ is a structural consequence operation. It means that for any sets $X, Y$ of formulae and any substitution $e$ $$X\subseteq \overrightarrow{{\goth M}}(X)$$ $$X\subseteq Y\rightarrow \overrightarrow{{\goth M}}(X)\subseteq \overrightarrow{{\goth M}}(Y)$$ $$\overrightarrow{{\goth M}}(\overrightarrow{{\goth M}}(X))\subseteq \overrightarrow{{\goth M}}(X)$$ $$h^e(\overrightarrow{{\goth M}}(X))\subseteq \overrightarrow{{\goth M}}(h^eX)$$ There immediately raises the question of axiomatizability of matrix consequences determined by certain known logical matrices, in particular those determined by /Lukasiewicz matrices. It is known as the problem of strong axiomatization and it relies on searching for a set $R$ of schematically defined rules and axioms $A$, such that for each set $X$ of formulae $$\overrightarrow{{\goth M}}(X)=Cn(R,Sb(A)\cup X). $$ Schematically defined rules are rules defined by one of their sequents. So, schematically define rule is any inferential rules consisting of all (and only) instances of this basic sequent. The detachment rule is schematically defined and determined by its sequent $\langle \{p, p\to q\}, q\rangle$. The simplification rule is also schematically defined $$\frac{\alpha}{\beta\to \alpha}$$ but the substitution rule is not. Let $Sb(A)$ be the set of all substitution instances of formulae in $A$. There is a clear coincidence between the schematically defined rules and axiom schemata. Axiom schemata may be seen as a special case of inferential rules in which the sets of premises is empty. Since for schematically defined (structural) rules $Cn(R\cup\{r_*\},A)=Cn(R,Sb(A))$, the strong axiomatizability of a matrix implies its usual (weak) axiomatizability by use of the same rules together with the substitution rule. \\ \indent b) Let me illustrate the concept of strong axiomatizability by referring to results on infinite valued /Lukasiewcz logic and related matrices. I shall refer to results included in R. W/ojcicki [1973] and P. Wojtylak [1978]. Clearly, $$Cn(\{r_0\},Sb(A_\infty))= E({{\goth M_\infty}})= \bigcap_{n=2}^\infty E({{\goth M_n}})= E( {\bf P}_{n=2}^\infty\goth M_n)= E({\goth L_\infty})$$ where $ {\bf P}_{n=2}^\infty\goth M_n$ is the product of the involved matrices and ${\goth L_\infty}$ is the Lindenbaum matrix for the infinite valued /Lukasiewicz logic. For any set $X$ of formulae the following inclusion hold and for certain sets they are proper $$Cn(\{r_0\},Sb(A_\infty)\cup X)\subseteq\overrightarrow{{\goth M_\infty}}(X)\subseteq \bigcap_{n=2}^\infty \overrightarrow{{\goth M_n}}(X)\subseteq \overrightarrow{{\bf P}_{n=2}^\infty{\goth M_n}}(X)\subseteq \overrightarrow{{\goth L_\infty}}(X)$$ So, the problem of strong axiomatizability of infinite valued /Lukasiewicz logic becomes more complicated as it is not quite clear which matrix should be axiomatized and what is a matrix strongly adequate for the propositional system $\langle\{r_0\},Sb(A_\infty)\rangle$. Moreover, one can easily extend the above sequence by adding new matrix consequences with the same set of tautologies; for instance the submatrix of ${\goth M_\infty}$ determined by rational numbers. It is only known that the matrix consequence determined by the Lindenbaum matrix ${\goth L_\infty}$ is structurally complete (cf.W.A Pogorzelski [1971]) and hence it is the greatest structural consequence with a given set of tautologies. \\ \indent c) The view that any of the above consequences represents infinite valued /Lukasiewicz logic could be questioned as the operations (except of the first one) are not finite. If one considers only finite sets $X$, then some of the inclusions can be replaced with equalities: $$Cn(\{r_0\},Sb(A_\infty)\cup X)\subseteq\overrightarrow{{\goth M_\infty}}(X)= \bigcap_{n=2}^\infty \overrightarrow{{\goth M_n}}(X)\subseteq \overrightarrow{{\bf P}_{n=2}^\infty{\goth M_n}}(X)\subseteq \overrightarrow{{\goth L_\infty}}(X).$$ In result, the matrix consequence operations should be axiomatized by use of inferential rules with infinite sets of premises and the problem is that there is no proper logical theory for such rules. The difference between finitary and infinitary rules are not so fundamental as one could expect. Let us consider, for instance, the substitution version of the above consequence operations. Then we get $$Cn(\{r_0,r_*\},A_\infty\cup X)\subseteq\overrightarrow{{\goth M_\infty}}(Sb(X))= \dots %\bigcap_{n=2}^\infty \overrightarrow{{\goth M_n}}(Sb(X)) = \overrightarrow{{\bf P}_{n=2}^\infty{\goth M_n}}(Sb(X))\subseteq \overrightarrow{{\goth L_\infty}}(Sb(X))$$ The last, strongest consequence operation (the structural complete extension of the infinite valued logic) is finite and contains exactly three theories: $E({{\goth M_\infty}})$, $E({{\goth M_2}})$ and $S$. So, all finite valued logics (except of the classical one) can be rejected on the ground of the infinite valued one. The admittance of the substitution rule corresponds to the admittance of all instances of a given set of premises and is acceptable form a finitistic point of view.\\ \indent d) Let us note that the above relations between consequence operations will change if we change (extend or restrict) the propositional language. The above inclusions concern the usual logical language with the usual logical operations including implications and negation. If we restrict to the positive fragment (that is the fragment without negation), then we get for any finite set $X$ of formulae $$Cn(\{r_0\},Sb(A_\infty^p)\cup X)=\overrightarrow{{\goth M}_\infty^p}(X)= \bigcap_{n=2}^\infty \overrightarrow{{\goth M_n^p}}(X)= \overrightarrow{{\bf P}_{n=2}^\infty{\goth M_n^p}}(X)= \overrightarrow{{\goth L_\infty^p}}(X).$$ So, the logic $\langle\{r_0\},Sb(A_\infty^p)\rangle$ is structurally complete for rules with finite sets of premises (but is not for arbitrary ones). If one considers, the extensions of the $n$-valued (for $n>2$) logic $\langle\{r_0\},Sb(A_n)\rangle$, then the situation changes a bit. The logic $\langle\{r_0\},Sb( A_n)\rangle$ is strongly adequate for $\overrightarrow{{\goth M_n}}$ but is not structurally complete. Its structural complete extension is $\overrightarrow{{\goth M_n}\times {\goth M_2}}$ and is received by extending $\langle\{r_0\},Sb( A_n)\rangle$ with the rule $$\frac{\alpha\lor\neg \alpha\to^{n+1}\alpha\land\neg \alpha}{\beta}$$ Some additional information on the lattice of strengthenings of any finite valued /Lukasiewicz logic can be found in G. Malinowski [1977].\\ {\bf 4.} As one easily notice, the above does not concern at all the fundamental (as one might think) question as concern the problem of axiomatizability of logical matrices - namely, the question of finite axiomatizablity (that is axiomatizability with a finite set of schematically defined rules and axioms) of finite matrices (or, more specifically the sets of tautologies or matrix consequences determined by finite matrices). A partial solution to this question was given by M. Wajsberg and we discussed it above. This question become central in research programme initiated by R. W/ojcicki [1977]. Let us call a consequence operation $Cn$ strongly finite (or $SF$ in short) iff $Cn=\overrightarrow{{\goth N_1}}\cap\dots\cap \overrightarrow{{ \goth N_n}}$ for some finite matrices ${{\goth N_1}},\dots,{{\goth N_n}}$. Then let us try to identify logical properties of strongly finite logics. If $SF$ logics have some ``nice'' logical properties, then finitness will get some logical meaning and it will turn out that finitness is significant from a logical point of view.\\ \indent a) The initial interest in $SF$ logics was supported by the following two general results\\ {(1) \it Each strongly finite logic $Cn$ is finite, that is $\alpha\in Cn(X)$ iff $\alpha\in Cn(Y)$ for some finite $Y\subseteq X$.}\\ {(2) \it If $Cn$ is strongly finite, then its degree of completeness (that is the number of theories closed under substitution) is finite.}\\ As concerns $(1)$ (see J. /Lo/s, R. Suszko [1958]) the argument used there is similar to that used if one wants to show the compactness theorem for satisfiability (ie. if one shows that a set is satisfiable iff all its finite subsets are satisfiable). One can simply make use of Boolean Prime Ideal Theorem or related (fundamental) results in set theory. In other words, our argument is set-theoretical, not logical, in nature. As concerns $(2)$ the concept of the degree of completeness was introduced by A. Tarski and the result that any finite valued /Lukasiewicz logic has a finite degree of completeness was noted in literature. From this point of view, the result $(2)$ (by R. W/ojcicki) was an essential strengthening of the known result. However, the result in question is an immediate corollary of the following characterization of the substitution version of the matrix consequence $$\overrightarrow{{\goth M}}(Sb(X))= \bigcap\{ E({\goth N}): X\subseteq E({\goth N}) \mbox{ oraz } {\goth N}\subseteq {\goth M}\}$$ given by P. Wojtylak [1978]. It does not mater here if the matrix $\goth M$ is finite or not. Since any finite matrix has only finitely many submatrices, the finitness of the degree of completeness of any strongly finite logic immediately follows. So, one can say that our argument with $(2)$ has little to do with finitness of matrices and properties of strongly finite logics.\\ \indent b) Nevertheless, the above ``positive" results encouraged to make several conjectures on strongly finite logics. In particular, \\ {(3) \it Each structural strengthening of any $SF$ logic is $SF$;} $$Cn_1\geq Cn\in SF\Rightarrow Cn_1\in SF$$ {(4) \it The supremum of two $SF$ logics is $SF$;}\\ $$Cn, Cn_1\in SF\Rightarrow Cn\cup Cn_1\in SF$$ {(5) \it Each strongly finite logic $Cn$ is finitely based ($FB$ in short) which means that for some finite set $R$ of inferential rules (including axiom schemata)} $$Cn(X)=Cn(R,X) \mbox{\it for every } X$$ It soon appeared that all the above conjecture (and also some others) are false. Counterexamples were provided by M. Tokarz [1976], A. Wro/nski [1976] and [1979], P. Wojtylak [1979]. For the considered in this paper question of axiomatizability, the most important is the negative answer to (5) provided by A. Wro/nski [1979]. If one wants to get a positive result on finite axiomatizability of a finite matrix one has to assume certain logical properties of the logic determined by this matrix. To illustrate this question let us consider the following general (positive) results on axiomatizability of finite matrice from my paper [1979]:\\ {\sl If ${\goth M}$ is a finite matrix and $\overrightarrow{{\goth M}}$ is a consequence operation with equivalence and disjunction, then $\overrightarrow{{\goth M}}$ jest finitely based}.\\ Let me give here a sketch of its proof. Then, each finite structural consequence operation, in particular $\overrightarrow{{\goth M}}$, can be given in the form $\bigcup_k Cn_k$ where $Cn_k$ is the fragment of $\overrightarrow{{\goth M}}$ determined by rules (and axioms) which can be defined by sequents containing at most $k$ variables. Since each $Cn_k$ can be easily shown to be finitely based, the by the known Tarski's criterion $\overrightarrow{{\goth M}}$ is finitely based iff it collapses to one of its fragments $Cn_k$. Next, let us consired the following formulae $$\bigvee\{p_i\equiv p_j: 0\leq i