Unification in intermediate logics. (English) Zbl 1357.03059

Iemhoff, Rosalie; Rozière, Paul

J. Symb. Log. 80, No. 3, 713-729 (2015).

Unification is concerned with the problem whether two given terms can be identified via a substitution in a theory of equality. The paper presents a proof-theoretic treatment of unification in intermediate logics.
In this context, unification is the study of substitutions under which a formula becomes provable in logic. In classical propositional logic, every formula has a most general unifier while this is not true in intermediate logics: for example, in intuitionistic logic the formula \(p \vee \neg p\) has not a most general unifier. The purpose of the article is to study when an intermediate logic has finitary of unitary unification.
Although many results are already known, the method to deduce the presented results is new and relies on syntax only, not involving semantics, like, e.g., in S. Ghilardi’s work [J. Symb. Log. 64, No. 2, 859–880 (1999; Zbl 0930.03009)]. In particular, the paper shows how a proof of a formula under a projective unifier can be obtained from the closure under the Visser rules, clarifying the connection between valuations and most general unifiers. So, many existing and well-known results can be extended to logical frameworks containing at least conjunction and implication.
The article is of interest to everyone working in the proof theory of propositional intermediate logics and, although it requires some technical knowledge, it contains a number of useful results, obtained through a uniform method which is flexible enough to allow generalisations.

Reviewer: Marco Benini (Buccinasco)

MSC:

03B55	Intermediate logics
03B20	Subsystems of classical logic (including intuitionistic logic)
03B70	Logic in computer science
03F03	Proof theory in general (including proof-theoretic semantics)

Keywords:

unification; admissible rules; intermediate logics; fragments

Citations:

Zbl 0930.03009

References:

[1]	ACM Transactions on Computational Logic 9 (2008)
[2]	Reports on Mathematical Logic 29 pp 105– (1995)
[3]	Admissibility of Logical Inference Rules (1997) · Zbl 0872.03002
[4]	DOI: 10.1017/S0960129500000165 · Zbl 0797.03001
[5]	DOI: 10.1007/BF00405383 · Zbl 0436.03018
[6]	Reports on Mathematical Logic 6 pp 103– (1976)
[7]	A note on consequence 314 (2013)
[8]	DOI: 10.1305/ndjfl/1107220674 · Zbl 1102.03032
[9]	DOI: 10.1016/S0168-0072(01)00056-2 · Zbl 0988.03045
[10]	DOI: 10.1016/j.apal.2013.09.003 · Zbl 1316.03016
[11]	DOI: 10.1007/BF02123815 · Zbl 0345.02036
[12]	DOI: 10.1016/j.apal.2003.11.010 · Zbl 1058.03020
[13]	Logic Journal of IGPL 20 pp 121– (2011)
[14]	Logic Journal of the IGPL 10 pp 227– (2002)
[15]	Proceedings of the Workshop on General Algebra, 70 pp 71– (2006)
[16]	DOI: 10.1016/S0168-0072(99)00032-9 · Zbl 0949.03010
[17]	Soviet Mathematics Doklady, 19 pp 816– (1978)
[18]	DOI: 10.1016/j.apal.2010.09.001 · Zbl 1225.03011
[19]	DOI: 10.1215/00294527-2009-004 · Zbl 1190.03027
[20]	Unification theory (2001) · Zbl 1011.68126
[21]	Term Rewriting and All That (1998)
[22]	Studia Logica 32 pp 45– (1973)
[23]	Bulletin de l’Académie Polonaise des Sciences. Série des Sciences Mathématiques 19 pp 349– (1971)
[24]	DOI: 10.1093/jigpal/jzn014 · Zbl 1168.03012
[25]	32 pp 85– (1972)
[26]	Reports on Mathematical Logic 22 pp 21– (1988)
[27]	DOI: 10.1007/s00153-006-0028-9 · Zbl 1115.03010
[28]	DOI: 10.1093/logcom/exi029 · Zbl 1077.03011
[29]	Proceedings of LFCS ’09 5407 pp 230– (2009)
[30]	DOI: 10.1016/j.apal.2008.10.011 · Zbl 1174.03024
[31]	DOI: 10.1093/jigpal/jzs015 · Zbl 1277.03004