coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Evgeny Makarov <emakarov AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Intuitionist semantic, Russell
- Date: Thu, 4 Mar 2010 19:38:17 +0300
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :content-type; b=MfvSs4iXD2ari0mxN5XdgMyQ2GhS+4ogxAP/cj0ZHbsrbmACnJVef0IrjUuc80g8kd 5qeejfJJFlNxq4WKgHuP9VXuUbtuxdw3pdLZ8a1eAFf0h0ckn10xcjpj2Yf2W64Y11xb mdMDvvVgW2XBj6GNwga7b0N5LjSim6hrbD6mM=
There are Heyting algebras, which are similar to Boolean algebras for
classical logic. Here is a quotation from the first place that came to
mind: the paper "Possible worlds and resources" about the logic of
bunched implications:
Heyting algebras are the algebraic models of intuitionistic
propositional logic. A Heyting algebra is a lattice with greatest and
least elements in which the meet a /\ b is residuated, which is to say
that there is an implication operator, ->, satisfying
a /\ b <= c iff a <= b -> c
Evgeny
- [Coq-Club] Intuitionist semantic, Russell, Loic Pottier
- Re: [Coq-Club] Intuitionist semantic, Russell, Evgeny Makarov
Archive powered by MhonArc 2.6.16.