{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T20:57:01Z","timestamp":1768251421279,"version":"3.49.0"},"reference-count":46,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2018,12,3]],"date-time":"2018-12-03T00:00:00Z","timestamp":1543795200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["The Review of Symbolic Logic"],"published-print":{"date-parts":[[2019,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We introduce unification in first-order logic. In propositional logic, unification was introduced by S. Ghilardi, see Ghilardi (1997, 1999, 2000). He successfully applied it in solving systematically the problem of admissibility of inference rules in intuitionistic and transitive modal propositional logics. Here we focus on superintuitionistic predicate logics and apply unification to some old and new problems: definability of disjunction and existential quantifier, disjunction and existential quantifier under implication, admissible rules, a basis for the passive rules, (almost) structural completeness, etc. For this aim we apply modified specific notions, introduced in propositional logic by Ghilardi, such as projective formulas, projective unifiers, etc.<\/jats:p><jats:p>Unification in predicate logic seems to be harder than in the propositional case. Any definition of the key concept of substitution for predicate variables must take care of individual variables. We allow adding new free individual variables by substitutions (contrary to Pogorzelski &amp; Prucnal (1975)). Moreover, since predicate logic is not as close to algebra as propositional logic, direct application of useful algebraic notions of finitely presented algebras, projective algebras, etc., is not possible.<\/jats:p>","DOI":"10.1017\/s1755020318000011","type":"journal-article","created":{"date-parts":[[2018,12,3]],"date-time":"2018-12-03T07:31:26Z","timestamp":1543822286000},"page":"37-61","source":"Crossref","is-referenced-by-count":4,"title":["UNIFICATION IN SUPERINTUITIONISTIC PREDICATE LOGICS AND ITS APPLICATIONS"],"prefix":"10.1017","volume":"12","author":[{"given":"WOJCIECH","family":"DZIK","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"PIOTR","family":"WOJTYLAK","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2018,12,3]]},"reference":[{"key":"S1755020318000011_ref10","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511983474.012"},{"key":"S1755020318000011_ref14","volume-title":"Unification Types in Logic","author":"Dzik","year":"2007"},{"key":"S1755020318000011_ref4","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2007.03.001"},{"key":"S1755020318000011_ref29","doi-asserted-by":"publisher","DOI":"10.2307\/2963675"},{"key":"S1755020318000011_ref22","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1096901773"},{"key":"S1755020318000011_ref40","first-page":"115","article-title":"On axiomatizability of some intermediate logics","volume":"22","author":"Skvortsov","year":"1988","journal-title":"Reports on Mathematical Logic"},{"key":"S1755020318000011_ref20","doi-asserted-by":"publisher","DOI":"10.2307\/2586506"},{"key":"S1755020318000011_ref17","doi-asserted-by":"publisher","DOI":"10.1215\/00294527-3636512"},{"key":"S1755020318000011_ref15","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/jzr028"},{"key":"S1755020318000011_ref18","volume-title":"Quantification in Nonclassical Logic","volume":"1","author":"Gabbay","year":"2009"},{"key":"S1755020318000011_ref12","first-page":"37","article-title":"Chains of structurally complete predicate logics with the application of Prucnal\u2019s substitution","volume":"38","author":"Dzik","year":"2004","journal-title":"Reports on Mathematical Logic"},{"key":"S1755020318000011_ref44","first-page":"287","volume-title":"Proofs, Categories and Computations: Essays in Honor of Grigori Mints","author":"van Benthem","year":"2010"},{"key":"S1755020318000011_ref28","doi-asserted-by":"publisher","DOI":"10.1017\/jsl.2015.5"},{"key":"S1755020318000011_ref35","first-page":"349","article-title":"Structural completeness of the propositional calculus","volume":"19","author":"Pogorzelski","year":"1971","journal-title":"Bulletin de l\u2019Acad\u00e9mie Polonaise des Sciences, s\u00e9rie des Sciences Math\u00e9matiques, Astronomiques et Physiques"},{"key":"S1755020318000011_ref11","first-page":"19","article-title":"On structural completeness of some nonclassical predicate calculi","volume":"5","author":"Dzik","year":"1975","journal-title":"Reports on Mathematical Logic"},{"key":"S1755020318000011_ref3","first-page":"439","volume-title":"Handbook of Automated Reasoning","author":"Baader","year":"2001"},{"key":"S1755020318000011_ref36","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19750210138"},{"key":"S1755020318000011_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-010-3332-9"},{"key":"S1755020318000011_ref37","doi-asserted-by":"publisher","DOI":"10.1007\/BF00405383"},{"key":"S1755020318000011_ref1","first-page":"1","volume-title":"Contributions to Mathematical Logic: Proceeding of the Logic Colloquium, Hannover 1966","author":"Aczel","year":"1968"},{"key":"S1755020318000011_ref41","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exl031"},{"key":"S1755020318000011_ref8","volume-title":"Introduction to Mathematical Logic I","author":"Church","year":"1956"},{"key":"S1755020318000011_ref43","doi-asserted-by":"publisher","DOI":"10.2307\/2964756"},{"key":"S1755020318000011_ref24","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2013.09.003"},{"key":"S1755020318000011_ref6","first-page":"1","article-title":"Exact unification and admissibility","volume":"11","author":"Cabrer","year":"2015","journal-title":"Logical Methods in Computer Science"},{"key":"S1755020318000011_ref31","first-page":"199","volume-title":"Proceedings of the Meeting \u201cLogica e Filosofia della Scienza, oggi\u201d","volume":"I","author":"Minari","year":"1986"},{"key":"S1755020318000011_ref21","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(99)00032-9"},{"key":"S1755020318000011_ref7","first-page":"499","article-title":"Negation-free intermediate predicate logics","volume":"6","author":"Casari","year":"1983","journal-title":"Bolletino dell\u2019Unione Matematica Italiana"},{"key":"S1755020318000011_ref33","doi-asserted-by":"publisher","DOI":"10.2977\/prims\/1195192964"},{"key":"S1755020318000011_ref2","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/jzq008"},{"key":"S1755020318000011_ref45","first-page":"105","article-title":"Transparent unification problem","volume":"29","author":"Wro\u0144ski","year":"1995","journal-title":"Reports on Mathematical Logic"},{"key":"S1755020318000011_ref16","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/jzv024"},{"key":"S1755020318000011_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/BF00370118"},{"key":"S1755020318000011_ref23","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511862359"},{"key":"S1755020318000011_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/s00153-006-0320-8"},{"key":"S1755020318000011_ref30","first-page":"456","article-title":"The non-derivability of $\\neg \\left( x \\right)A\\left( x \\right) \\to \\left( {Ex} \\right)\\neg A\\left( x \\right)$, A primitive recursive, in intuitionistic formal systems","volume":"23","author":"Kreisel","year":"1958","journal-title":"Journal of Symbolic Logic"},{"key":"S1755020318000011_ref34","first-page":"55","article-title":"Some problems in intermediate predicate logics","volume":"21","author":"Ono","year":"1987","journal-title":"Reports on Mathematical logic"},{"key":"S1755020318000011_ref38","first-page":"291","article-title":"Algebraic models for axiomatics theories","volume":"4","author":"Rasiowa","year":"1954","journal-title":"Fundamenta Mathematicae"},{"key":"S1755020318000011_ref39","first-page":"145","article-title":"An essay on unification and inference rules for modal logic","volume":"28","author":"Rybakov","year":"1999","journal-title":"Bulletin of the Section of Logic"},{"key":"S1755020318000011_ref13","first-page":"71","article-title":"Splittings of lattices of theories and unification types","volume":"17","author":"Dzik","year":"2006","journal-title":"Contributions to General Algebra"},{"key":"S1755020318000011_ref27","first-page":"713","article-title":"On rules","volume":"80","author":"Iemhoff","year":"2015","journal-title":"Journal of Philosophical Logic"},{"key":"S1755020318000011_ref42","doi-asserted-by":"publisher","DOI":"10.1007\/BF00370376"},{"key":"S1755020318000011_ref25","doi-asserted-by":"publisher","DOI":"10.2307\/2964334"},{"key":"S1755020318000011_ref46","first-page":"16","volume-title":"Abstracts of the 54th Conference in History of Mathematics","author":"Wro\u0144ski","year":"2008"},{"key":"S1755020318000011_ref19","first-page":"733","article-title":"Unification through projectivity","volume":"7","author":"Ghilardi","year":"1997","journal-title":"Journal of Symbolic Computation"},{"key":"S1755020318000011_ref32","first-page":"21","article-title":"The property (HD) in intuitionistic logic. A partial solution of a problem of H. Ono","volume":"22","author":"Minari","year":"1988","journal-title":"Reports on Mathematical Logic"}],"container-title":["The Review of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1755020318000011","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,12]],"date-time":"2019-04-12T19:00:24Z","timestamp":1555095624000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1755020318000011\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,12,3]]},"references-count":46,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,3]]}},"alternative-id":["S1755020318000011"],"URL":"https:\/\/doi.org\/10.1017\/s1755020318000011","relation":{},"ISSN":["1755-0203","1755-0211"],"issn-type":[{"value":"1755-0203","type":"print"},{"value":"1755-0211","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,12,3]]}}}