Premium
Categorical abstract algebraic logic: Gentzen π ‐institutions and the deduction‐detachment property
Author(s) -
Voutsadakis George
Publication year - 2005
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.200310132
Subject(s) - mathematics , property (philosophy) , equivalence (formal languages) , analogy , categorical variable , order (exchange) , institution , hierarchy , algebraic number , calculus (dental) , pure mathematics , law , epistemology , mathematical analysis , philosophy , medicine , statistics , dentistry , finance , political science , economics
Given a π ‐institution I , a hierarchy of π ‐institutions I ( n ) is constructed, for n ≥ 1. We call I ( n ) the n‐th order counterpart of I . The second‐order counterpart of a deductive π ‐institution is a Gentzen π ‐institution, i.e. a π ‐institution associated with a structural Gentzen system in a canonical way. So, by analogy, the second order counterpart I (2) of I is also called the “Gentzenization” of I . In the main result of the paper, it is shown that I is strongly Gentzen , i.e. it is deductively equivalent to its Gentzenization via a special deductive equivalence, if and only if it has the deduction‐detachment property . (© 2005 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)