Analogy calculus (Q1802070)

The paper is devoted to the problem of analogical reasoning. The authors proposed a calculus \(LK_ A\), the system is based on Gentzen's \(LK\) calculus of sequents. First, two \(LK\)-rules are modified, then some additional initial segments, called equality axioms and analogy axioms are introduced. An analogy relation \(\sim\) is defined by the axioms (1) \(t\sim s\to s\sim t\) (2) \(t\sim s\), \(s\sim r\to t\sim r\), where \(t\), \(s\), and \(r\) are terms. Cut elimination and interpolation theorems are proven. It is shown that \(LK_ A\) is consistent and \(LK_ A\) is a conservative extension of \(LK_ e\), an equational logic calculus. Analogy correspondence is a set of sentences of the following forms: \[ \forall x_ 1\cdots\forall x_ n\forall y_ 1\cdots\forall y_ n\bigl(x_ 1\sim y_ 1\wedge\cdots\wedge x_ n\sim y_ n\supset f(x_ 1,\ldots,x_ n)\sim g(y_ 1,\ldots,y_ n)\bigr) \] \[ \forall x_ 1\cdots\forall x_ n\forall y_ 1\cdots\forall y_ n\bigl(x_ 1\sim y_ 1\wedge\cdots\wedge x_ n\sim y_ n\supset P(x_ 1,\ldots,x_ n)\equiv Q(y_ 1,\ldots,y_ n)\bigr) \] It is defined when an analogy correspondence \(A_ c\) is consistent with (suitable for, proper to) a formula \(A\). Then for any formulas \(A,B\) without analogy symbol \(\sim\) is defined when \(A\) is analogous (strongly analogous) to \(B\) based on \(A_ c\), and \(A\) is (strongly) analogous to \(B\). A model semantics of \(LK_ A\) is given, it is shown that \(LK_ A\) is sound. The final theorem characterizes the concept of analogy: Let \(A\) be analogous to \(B\) based on \(A_ c\), and \(M\) be a model of \(A_ c\), then \(M\) is a model of \(A\) iff \(M\) is a model of \(B\).