Unification in intuitionistic logic

1999 ◽  
Vol 64 (2) ◽  
pp. 859-880 ◽  
Author(s):  
Silvio Ghilardi
Keyword(s):  
Intuitionistic Logic ◽  
Heyting Algebras ◽  
Unification Type ◽  
Finitely Presented

AbstractWe show that the variety of Heyting algebras has finitary unification type. We also show that the subvariety obtained by adding it De Morgan law is the biggest variety of Heyting algebras having unitary unification type. Proofs make essential use of suitable characterizations (both from the semantic and the syntactic side) of finitely presented projective algebras.

scholarly journals Finitely Presented Heyting Algebras

1998 ◽  
Vol 5 (30) ◽  
Author(s):  
Carsten Butz
Keyword(s):  
Simple Proof ◽  
Heyting Algebra ◽  
Distributive Lattices ◽  
Heyting Algebras ◽  
Model Property ◽  
Disjunction Property ◽  
Irreducible Elements ◽  
Finite Set ◽  
Finite Distributive Lattices ◽  
Finitely Presented

In this paper we study the structure of finitely presented Heyting<br />algebras. Using algebraic techniques (as opposed to techniques from proof-theory) we show that every such Heyting algebra is in fact co- Heyting, improving on a result of Ghilardi who showed that Heyting algebras free on a finite set of generators are co-Heyting. Along the way we give a new and simple proof of the finite model property. Our main technical tool is a representation of finitely presented Heyting algebras in terms of a colimit of finite distributive lattices. As applications we construct explicitly the minimal join-irreducible elements (the atoms) and the maximal join-irreducible elements of a finitely presented Heyting algebra in terms of a given presentation. This gives as well a new proof of the disjunction property for intuitionistic propositional logic.<br />Unfortunately not very much is known about the structure of Heyting algebras, although it is understood that implication causes the complex structure of Heyting algebras. Just to name an example, the free Boolean algebra on one generator has four elements, the free Heyting algebra on one generator is infinite.<br />Our research was motivated a simple application of Pitts' uniform interpolation theorem [11]. Combining it with the old analysis of Heyting algebras free on a finite set of generators by Urquhart [13] we get a faithful functor J : HAop<br />f:p: ! PoSet; sending a finitely presented Heyting algebra to the partially ordered set of its join-irreducible elements, and a map between Heyting algebras to its leftadjoint<br />restricted to join-irreducible elements. We will explore on the induced duality more detailed in [5]. Let us briefly browse through the contents of this paper: The first section<br />recapitulates the basic notions, mainly that of the implicational degree of an element in a Heyting algebra. This is a notion relative to a given set of generators. In the next section we study nite Heyting algebras. Our contribution is a simple proof of the nite model property which names in particular a canonical family of nite Heyting algebras into which we can<br />embed a given finitely presented one.<br />In Section 3 we recapitulate the standard duality between nite distributive lattices and nite posets. The `new' feature here is a strict categorical<br />formulation which helps simplifying some proofs and avoiding calculations. In the following section we recapitulate the description given by Ghilardi [8]<br />on how to adjoin implications to a nite distributive lattice, thereby not destroying a given set of implications. This construction will be our major technical ingredient in Section 5 where we show that every nitely presented<br />Heyting algebra is co-Heyting, i.e., that the operation (−) n (−) dual to implication is dened. This result improves on Ghilardi's [8] that this is true<br />for Heyting algebras free on a finite set of generators. Then we go on analysing the structure of finitely presented Heyting algebras<br />in Section 6. We show that every element can be expressed as a finite join of join-irreducibles, and calculate explicitly the maximal join-irreducible elements in such a Heyting algebra (in terms of a given presentation). As a consequence we give a new proof of the disjunction property for propositional intuitionistic logic. As well, we calculate the minimal join-irreducible elements, which are nothing but the atoms of the Heyting algebra. Finally, we show how all this material can be used to express the category of finitely presented Heyting algebras as a category of fractions of a certain category with objects morphism between finite distributive lattices.

scholarly journals Preserving Filtering Unification by Adding Compatible Operations to Some Heyting Algebras

2016 ◽  
Vol 45 (3/4) ◽  
Author(s):  
Wojciech Dzik ◽  
Sándor Radeleczki
Keyword(s):  
Residuated Lattices ◽  
Heyting Algebras ◽  
Direct Products ◽  
Unification Type

We show that adding compatible operations to Heyting algebras and to commutative residuated lattices, both satisfying the Stone law ¬x ⋁ ¬¬x = 1, preserves filtering (or directed) unification, that is, the property that for every two unifiers there is a unifier more general then both of them. Contrary to that, often adding new operations to algebras results in changing the unification type. To prove the results we apply the theorems of [9] on direct products of l-algebras and filtering unification. We consider examples of frontal Heyting algebras, in particular Heyting algebras with the successor, γ and G operations as well as expansions of some commutative integral residuated lattices with successor operations.

A sheaf representation and duality for finitely presented Heyting algebras

1995 ◽  
Vol 60 (3) ◽  
pp. 911-939 ◽  
Author(s):  
Silvio Ghilardi ◽  
Marek Zawadowski
Keyword(s):  
Equivalence Relations ◽  
Heyting Algebras ◽  
Sheaf Representation ◽  
Subobject Classifier ◽  
Finitely Presented ◽  
Open Maps ◽  
The Way

AbstractA. M.Pitts in [Pi] proved that is a bi-Heyting category satisfying the Lawvere condition. We show that the embedding Φ: → Sh(P0, J0) into the topos of sheaves, (P0 is the category of finite rooted posets and open maps, J0 the canonical topology on P0) given by H ↦ HA(H, (−)) : P0 → Set preserves the structure mentioned above, finite coproducts, and subobject classifier; it is also conservative. This whole structure on can be derived from that of Sh(P0, J0) via the embedding Φ. We also show that the equivalence relations in are not effective in general. On the way to these results we establish a new kind of duality between and a category of sheaves equipped with certain structure defined in terms of Ehrenfeucht games. Our methods are model-theoretic and combinatorial as opposed to proof-theoretic as in [Pi].

scholarly journals Residuated Structures and Orthomodular Lattices

Studia Logica ◽  
2021 ◽  
Author(s):  
D. Fazio ◽  
A. Ledda ◽  
F. Paoli
Keyword(s):  
Algebraic Logic ◽  
Residuated Lattices ◽  
Quantum Structures ◽  
Heyting Algebras ◽  
Quantum Algebras ◽  
Orthomodular Lattices ◽  
Lattice Of Subvarieties ◽  
Residuated Structures ◽  
Common Framework ◽  
Mv Algebras

AbstractThe variety of (pointed) residuated lattices includes a vast proportion of the classes of algebras that are relevant for algebraic logic, e.g., $$\ell $$ ℓ -groups, Heyting algebras, MV-algebras, or De Morgan monoids. Among the outliers, one counts orthomodular lattices and other varieties of quantum algebras. We suggest a common framework—pointed left-residuated $$\ell $$ ℓ -groupoids—where residuated structures and quantum structures can all be accommodated. We investigate the lattice of subvarieties of pointed left-residuated $$\ell $$ ℓ -groupoids, their ideals, and develop a theory of left nuclei. Finally, we extend some parts of the theory of join-completions of residuated $$\ell $$ ℓ -groupoids to the left-residuated case, giving a new proof of MacLaren’s theorem for orthomodular lattices.

scholarly journals On the correspondence between nested calculi and semantic systems for intuitionistic logics

2020 ◽  
Author(s):  
Tim Lyon
Keyword(s):  
Intuitionistic Logic ◽  
Structural Rules ◽  
First Order ◽  
Constant Domains ◽  
The Relationship ◽  
Intuitionistic Logics

Abstract This paper studies the relationship between labelled and nested calculi for propositional intuitionistic logic, first-order intuitionistic logic with non-constant domains and first-order intuitionistic logic with constant domains. It is shown that Fitting’s nested calculi naturally arise from their corresponding labelled calculi—for each of the aforementioned logics—via the elimination of structural rules in labelled derivations. The translational correspondence between the two types of systems is leveraged to show that the nested calculi inherit proof-theoretic properties from their associated labelled calculi, such as completeness, invertibility of rules and cut admissibility. Since labelled calculi are easily obtained via a logic’s semantics, the method presented in this paper can be seen as one whereby refined versions of labelled calculi (containing nested calculi as fragments) with favourable properties are derived directly from a logic’s semantics.

scholarly journals On Correspondence between Selective CPS Transformation and Selective Double Negation Translation

Mathematics ◽  
2021 ◽  
Vol 9 (4) ◽  
pp. 385
Author(s):  
Hyeonseung Im
Keyword(s):  
Programming Languages ◽  
Intuitionistic Logic ◽  
Reference Point ◽  
Classical Logic ◽  
Proof System ◽  
Double Negation

A double negation translation (DNT) embeds classical logic into intuitionistic logic. Such translations correspond to continuation passing style (CPS) transformations in programming languages via the Curry-Howard isomorphism. A selective CPS transformation uses a type and effect system to selectively translate only nontrivial expressions possibly with computational effects into CPS functions. In this paper, we review the conventional call-by-value (CBV) CPS transformation and its corresponding DNT, and provide a logical account of a CBV selective CPS transformation by defining a selective DNT via the Curry-Howard isomorphism. By using an annotated proof system derived from the corresponding type and effect system, our selective DNT translates classical proofs into equivalent intuitionistic proofs, which are smaller than those obtained by the usual DNTs. We believe that our work can serve as a reference point for further study on the Curry-Howard isomorphism between CPS transformations and DNTs.

Sign in / Sign up

Export Citation Format

Share Document