Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Intuitionist semantic, Russell

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Intuitionist semantic, Russell


chronological Thread 
  • 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



Archive powered by MhonArc 2.6.16.

Top of Page