Object logic and morphism logic
Nobuyoshi Motoháshi · Journal of the Mathematical Society of Japan · 1972
In studying model theory by using proof theoretic techniques, the author -noticed the utility of distinguishing two kinds of logics, which will be called here " object logic " and " morphism logic ".The former are those to which :algebraic structures are related, while the morphisms between algebraic structures are related to the latter.The exact definitions of these logics will hbe given below in \S 1 and \S 2; however we explain here briefiy how to construct a morphism logic from a family of object logics $\{L_{\lambda}\}_{\lambda}\Lambda$ .Let $PC$ be 'of bound individual variables (this set will be denoted by $BV$ ).\ c o p y r i g h t $\{FM_{\lambda}\}_{\lambda\in\Lambda}$ are mutually disjoint sets.O Every formula in $L_{\lambda}$ has only finitely many free individual variables.O For any sequences of free individual variables X, $\vec{y}$ of the same length such that all the variables in $\rightarrow x$ are distinct, $\theta(\vec{x})\in FM_{\lambda}$ implies $\theta(\vec{y})\in FM_{\lambda}$ , and $\theta(\vec{x})\in PFM_{\lambda}$ implies $\theta(\vec{y})\in PFM_{\lambda}$ .$O5$ If $\theta\in FM_{\lambda}$ then $-7\theta\in FM_{\lambda}$ .\ c o p y r i g h t If $\Phi$ is a non-empty countable set of formulas in $FM_{\lambda}$ which has only iinitely many free individual variables, then $\wedge\Phi,$ $\vee\Phi\in FM_{\lambda}$ .O If $\theta(x)\in FM_{\lambda},$ $x\in FV$ and $v\in BV$ does not occur in $\theta(x)$ , then $(\forall v)\theta(v)$ , $'(\exists v)\theta(v)\in FM_{\lambda}$ .By $x,$ $y,$ $z$ (with or without suffixes) we shall denote elements in $FV$ and by $u,$ $v,$ $w$ (with or without suffixes) we shall denote elements in $BV$ .By $\theta,$ $\varphi,$ $\psi$ (with or without suffixes) we shall denote elements in $\bigcup_{\grave{A}_{-\Lambda}^{\subset}}FM_{\lambda}$ .\S 2. Morphism logic $L=L(L_{\lambda})_{\lambda\in\Lambda}$ .Roughly speaking, the morphism logic $L=L(L_{\lambda})_{\lambda\in\Lambda}$ for a family of object logics $\{L_{\lambda}\}_{\lambda^{-}\Lambda}$ is a logic obtained from $\{L_{\lambda}\}_{\lambda=\Lambda}$ by applying first order opera- tions.Now we give the explicit definition of $L$ .Let $PC$ be a set of predicate constants which are not contained in $L_{\lambda}$ for any $\lambda\in\Lambda$ .Then the set of formulas in $L$ (denoted by $FM$ ) is defined recursively by the following rules: O If $P\in PC$ is an n-ary predicate constant and $x_{1}$ , $\cdot$ .. , $x_{n}\in FV$ then $P(x_{1}$ , $\cdot$ .. , $x_{n})$ is a formula in $L$ (called an atomic m-formula).