Algebraic semantics and model completeness for Intuitionistic Public Announcement Logic

Algebraic Semantics and Model Completeness for Intuitionistic Public Announcement Logic Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh TACL 2011, Marseille

28 July 2011

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

PAL

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

PAL The simplest dynamic epistemic logic.

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

PAL The simplest dynamic epistemic logic. Language

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

PAL The simplest dynamic epistemic logic. Language

ϕ ::= p ∈ AtProp | ¬ϕ | ϕ ∨ ψ | ^ϕ | hαiϕ.

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

PAL The simplest dynamic epistemic logic. Language

ϕ ::= p ∈ AtProp | ¬ϕ | ϕ ∨ ψ | ^ϕ | hαiϕ. Axioms

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

PAL The simplest dynamic epistemic logic. Language

ϕ ::= p ∈ AtProp | ¬ϕ | ϕ ∨ ψ | ^ϕ | hαiϕ. Axioms 1

hαip ↔ (α ∧ p )

2

hαi¬ϕ ↔ (α ∧ ¬hαiϕ)

3

hαi(ϕ ∨ ψ) ↔ (hαiϕ ∨ hαiψ)

4

hαi^ϕ ↔ (α ∧ ^(α ∧ hαiϕ)).

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

PAL The simplest dynamic epistemic logic. Language

ϕ ::= p ∈ AtProp | ¬ϕ | ϕ ∨ ψ | ^ϕ | hαiϕ. Axioms 1

hαip ↔ (α ∧ p )

2

hαi¬ϕ ↔ (α ∧ ¬hαiϕ)

3

hαi(ϕ ∨ ψ) ↔ (hαiϕ ∨ hαiψ)

4

hαi^ϕ ↔ (α ∧ ^(α ∧ hαiϕ)).

Not amenable to a standard algebraic treatment.

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Semantics of PAL

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Semantics of PAL

PAL-models are S5 Kripke models: M = (W , R , V )

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Semantics of PAL

PAL-models are S5 Kripke models: M = (W , R , V ) M , w hαiϕ

iff

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Semantics of PAL

PAL-models are S5 Kripke models: M = (W , R , V ) M , w hαiϕ

iff

M, w α

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Semantics of PAL

PAL-models are S5 Kripke models: M = (W , R , V ) M , w hαiϕ

iff

M, w α

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

and

M α , w ϕ,

Algebraic Semantics and Model Completeness for Intuitionistic Public

Semantics of PAL

PAL-models are S5 Kripke models: M = (W , R , V ) M , w hαiϕ

iff

M, w α

and

M α , w ϕ,

Relativized model M α = (W α , R α , V α ):

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Semantics of PAL

PAL-models are S5 Kripke models: M = (W , R , V ) M , w hαiϕ

iff

M, w α

and

M α , w ϕ,

Relativized model M α = (W α , R α , V α ): W α = [[α]]M ,

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Semantics of PAL

PAL-models are S5 Kripke models: M = (W , R , V ) M , w hαiϕ

iff

M, w α

and

M α , w ϕ,

Relativized model M α = (W α , R α , V α ): W α = [[α]]M , R α = R ∩ (W α × W α ),

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Semantics of PAL

PAL-models are S5 Kripke models: M = (W , R , V ) M , w hαiϕ

iff

M, w α

and

M α , w ϕ,

Relativized model M α = (W α , R α , V α ): W α = [[α]]M , R α = R ∩ (W α × W α ), V α (p ) = V (p ) ∩ W α .

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Methodology based on duality theory:

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Methodology based on duality theory:

Dualize epistemic update on Kripke models to epistemic update on algebras.

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Methodology based on duality theory:

Dualize epistemic update on Kripke models to epistemic update on algebras. Generalize epistemic update on algebras to much wider classes of algebras.

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Methodology based on duality theory:

Dualize epistemic update on Kripke models to epistemic update on algebras. Generalize epistemic update on algebras to much wider classes of algebras. Dualize back to relational models for non classically based logics.

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Algebraic models

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Algebraic models An algebraic model is a tuple M = (A, V ) s.t. A is a monadic Heyting algebra and V : AtProp → A.

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Algebraic models An algebraic model is a tuple M = (A, V ) s.t. A is a monadic Heyting algebra and V : AtProp → A. For every A and every a ∈ A, define the equivalence relation ≡a :

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Algebraic models An algebraic model is a tuple M = (A, V ) s.t. A is a monadic Heyting algebra and V : AtProp → A. For every A and every a ∈ A, define the equivalence relation ≡a : for every b , c ∈ A, b ≡a c iff b ∧ a = c ∧ a .

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Algebraic models An algebraic model is a tuple M = (A, V ) s.t. A is a monadic Heyting algebra and V : AtProp → A. For every A and every a ∈ A, define the equivalence relation ≡a : for every b , c ∈ A, b ≡a c iff b ∧ a = c ∧ a . Let [b ]a be the equivalence class of b ∈ A. Let

Aa := A/≡a Aa is ordered: [b ] ≤ [c ] iff b 0 ≤A c 0 for some b 0 ∈ [b ] and some c 0 ∈ [c ].

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Algebraic models An algebraic model is a tuple M = (A, V ) s.t. A is a monadic Heyting algebra and V : AtProp → A. For every A and every a ∈ A, define the equivalence relation ≡a : for every b , c ∈ A, b ≡a c iff b ∧ a = c ∧ a . Let [b ]a be the equivalence class of b ∈ A. Let

Aa := A/≡a Aa is ordered: [b ] ≤ [c ] iff b 0 ≤A c 0 for some b 0 ∈ [b ] and some c 0 ∈ [c ]. Let πa : A → Aa be the canonical projection. Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Properties of the (pseudo)-congruence

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Properties of the (pseudo)-congruence

For every A and every a ∈ A,

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Properties of the (pseudo)-congruence

For every A and every a ∈ A,

≡a is a congruence if A is a BA / HA / BDL / Fr.

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Properties of the (pseudo)-congruence

For every A and every a ∈ A,

≡a is a congruence if A is a BA / HA / BDL / Fr. ≡a is not a congruence w.r.t. modal operators.

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Properties of the (pseudo)-congruence

For every A and every a ∈ A,

≡a is a congruence if A is a BA / HA / BDL / Fr. ≡a is not a congruence w.r.t. modal operators. For every b ∈ A there exists a unique c ∈ A s.t. c ∈ [b ]a and c ≤ a.

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Properties of the (pseudo)-congruence

For every A and every a ∈ A,

≡a is a congruence if A is a BA / HA / BDL / Fr. ≡a is not a congruence w.r.t. modal operators. For every b ∈ A there exists a unique c ∈ A s.t. c ∈ [b ]a and c ≤ a. Crucial remark Each ≡a -equivalence class has a canonical representant. Hence, the map i 0 : Aa → A given by [b ] 7→ b ∧ a is injective.

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Modalities of the pseudo-quotient

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Modalities of the pseudo-quotient

Let (A, ^, ) be a HAO. Define for every b ∈ A,

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Modalities of the pseudo-quotient

Let (A, ^, ) be a HAO. Define for every b ∈ A,

^a [b ] := [^(b ∧ a ) ∧ a ] = [^(b ∧ a )]. a [b ] := [a → (a → b )] = [(a → b )].

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Modalities of the pseudo-quotient

Let (A, ^, ) be a HAO. Define for every b ∈ A,

^a [b ] := [^(b ∧ a ) ∧ a ] = [^(b ∧ a )]. a [b ] := [a → (a → b )] = [(a → b )].

For every HAO (A, ^, ) and every a ∈ A,

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Modalities of the pseudo-quotient

Let (A, ^, ) be a HAO. Define for every b ∈ A,

^a [b ] := [^(b ∧ a ) ∧ a ] = [^(b ∧ a )]. a [b ] := [a → (a → b )] = [(a → b )].

For every HAO (A, ^, ) and every a ∈ A,

^a , a are normal modal operators.

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Modalities of the pseudo-quotient

Let (A, ^, ) be a HAO. Define for every b ∈ A,

^a [b ] := [^(b ∧ a ) ∧ a ] = [^(b ∧ a )]. a [b ] := [a → (a → b )] = [(a → b )].

For every HAO (A, ^, ) and every a ∈ A,

^a , a are normal modal operators. If (A, ^, ) is an MHA, then (Aa , a , ^a ) is an MHA.

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Modalities of the pseudo-quotient

Let (A, ^, ) be a HAO. Define for every b ∈ A,

^a [b ] := [^(b ∧ a ) ∧ a ] = [^(b ∧ a )]. a [b ] := [a → (a → b )] = [(a → b )].

For every HAO (A, ^, ) and every a ∈ A,

^a , a are normal modal operators. If (A, ^, ) is an MHA, then (Aa , a , ^a ) is an MHA. If A = F + for some Kripke frame F , then Aa BAO F a + .

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Interpreting dynamic modalities in algebraic models

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Interpreting dynamic modalities in algebraic models Let i : M α ,→ M.

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Interpreting dynamic modalities in algebraic models Let i : M α ,→ M. The satisfaction condition M , w hαiϕ

iff

M , w α and M α , w ϕ :

can be equivalently written as follows:

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Interpreting dynamic modalities in algebraic models Let i : M α ,→ M. The satisfaction condition M , w hαiϕ

iff

M , w α and M α , w ϕ :

can be equivalently written as follows: w ∈ [[hαiϕ]]M

iff

∃w 0 ∈ W α s.t. i (w 0 ) = w ∈ [[α]]M and w 0 ∈ [[ϕ]]M α .

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Interpreting dynamic modalities in algebraic models Let i : M α ,→ M. The satisfaction condition M , w hαiϕ

iff

M , w α and M α , w ϕ :

can be equivalently written as follows: w ∈ [[hαiϕ]]M

iff

∃w 0 ∈ W α s.t. i (w 0 ) = w ∈ [[α]]M and w 0 ∈ [[ϕ]]M α .

Because i : M α ,→ M is injective, then w 0 ∈ [[ϕ]]M α

iff

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

w = i (w 0 ) ∈ i [[[ϕ]]M α ].

Algebraic Semantics and Model Completeness for Intuitionistic Public

Interpreting dynamic modalities in algebraic models Let i : M α ,→ M. The satisfaction condition M , w hαiϕ

M , w α and M α , w ϕ :

iff

can be equivalently written as follows: w ∈ [[hαiϕ]]M

iff

∃w 0 ∈ W α s.t. i (w 0 ) = w ∈ [[α]]M and w 0 ∈ [[ϕ]]M α .

Because i : M α ,→ M is injective, then w 0 ∈ [[ϕ]]M α

iff

w = i (w 0 ) ∈ i [[[ϕ]]M α ].

Hence: w ∈ [[hαiϕ]]M

iff

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

w ∈ [[α]]M ∩ i [[[ϕ]]M α ],

Algebraic Semantics and Model Completeness for Intuitionistic Public

Interpreting dynamic modalities in algebraic models Let i : M α ,→ M. The satisfaction condition M , w hαiϕ

M , w α and M α , w ϕ :

iff

can be equivalently written as follows: w ∈ [[hαiϕ]]M

iff

∃w 0 ∈ W α s.t. i (w 0 ) = w ∈ [[α]]M and w 0 ∈ [[ϕ]]M α .

Because i : M α ,→ M is injective, then w 0 ∈ [[ϕ]]M α

iff

w = i (w 0 ) ∈ i [[[ϕ]]M α ].

Hence: w ∈ [[hαiϕ]]M

iff

w ∈ [[α]]M ∩ i [[[ϕ]]M α ],

from which we get

[[hαiϕ]]M = [[α]]M ∩ i [[[ϕ]]M α ] = [[α]]M ∩ i 0 ([[ϕ]]M α ). Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

(1)

Algebraic Semantics and Model Completeness for Intuitionistic Public

Interpreting dynamic modalities in algebraic models

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Interpreting dynamic modalities in algebraic models For every algebraic model M = (A, V ), the extension map [[·]]M : Fm → A is defined recursively as follows:

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Interpreting dynamic modalities in algebraic models For every algebraic model M = (A, V ), the extension map [[·]]M : Fm → A is defined recursively as follows:

[[p ]]M [[⊥]]M [[>]]M [[ϕ ∨ ψ]]M [[ϕ ∧ ψ]]M [[ϕ → ψ]]M [[^ϕ]]M [[ϕ]]M [[hαiϕ]]M [[[α]ϕ]]M

= = = = = = = = = =

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

V (p )

⊥A >A [[ϕ]]M ∨A [[ψ]]M [[ϕ]]M ∧A [[ψ]]M [[ϕ]]M →A [[ψ]]M ^A [[ϕ]]M A [[ϕ]]M [[α]]M ∧A i 0 ([[ϕ]]M α ) [[α]]M →A i 0 ([[ϕ]]M α )

Algebraic Semantics and Model Completeness for Intuitionistic Public

Interpreting dynamic modalities in algebraic models For every algebraic model M = (A, V ), the extension map [[·]]M : Fm → A is defined recursively as follows:

[[p ]]M [[⊥]]M [[>]]M [[ϕ ∨ ψ]]M [[ϕ ∧ ψ]]M [[ϕ → ψ]]M [[^ϕ]]M [[ϕ]]M [[hαiϕ]]M [[[α]ϕ]]M

= = = = = = = = = =

V (p )

⊥A >A [[ϕ]]M ∨A [[ψ]]M [[ϕ]]M ∧A [[ψ]]M [[ϕ]]M →A [[ψ]]M ^A [[ϕ]]M A [[ϕ]]M [[α]]M ∧A i 0 ([[ϕ]]M α ) [[α]]M →A i 0 ([[ϕ]]M α )

M α := (Aα , V α ) s.t. Aα = A[[α]]M and V α : AtProp → Aα is π ◦ V , i.e. [[p ]]M α = V α (p ) = π(V (p )) = π([[p ]]M ) for every p. Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Intuitionistic PAL

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Intuitionistic PAL ϕ ::= p ∈ AtProp | ⊥ | > | ϕ∨ψ | ϕ∧ψ | ϕ → ψ | ^ϕ | ϕ | hαiϕ | [α]ϕ.

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Intuitionistic PAL ϕ ::= p ∈ AtProp | ⊥ | > | ϕ∨ψ | ϕ∧ψ | ϕ → ψ | ^ϕ | ϕ | hαiϕ | [α]ϕ. Interaction with logical constants

hαi⊥ = ⊥ [α]> = >

Preservation of facts hαip = α ∧ p [α]p = α → p

Interaction with disjunction

Interaction with conjunction

hαi(ϕ ∨ ψ) = hαiϕ ∨ hαiψ [α](ϕ ∨ ψ) = α → (hαiϕ ∨ hαiψ)

hαi(ϕ ∧ ψ) = hαiϕ ∧ hαiψ [α](ϕ ∧ ψ) = [α]ϕ ∧ [α]ψ

Interaction with implication

hαi(ϕ → ψ) = α ∧ (hαiϕ → hαiψ) [α](ϕ → ψ) = hαiϕ → hαiψ Interaction with ^

hαi^ϕ = α ∧ ^hαiϕ [α]^ϕ = α → ^hαiϕ Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Interaction with 

hαiϕ = α ∧ [α]ϕ [α]ϕ = α → [α]ϕ

Algebraic Semantics and Model Completeness for Intuitionistic Public

Results

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Results

IPAL is sound w.r.t. algebraic models (A, V ).

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Results

IPAL is sound w.r.t. algebraic models (A, V ). IPAL is complete w.r.t. relational models:

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Results

IPAL is sound w.r.t. algebraic models (A, V ). IPAL is complete w.r.t. relational models: (W , ≤, R , V )

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Results

IPAL is sound w.r.t. algebraic models (A, V ). IPAL is complete w.r.t. relational models: (W , ≤, R , V ) W is a nonempty set;

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Results

IPAL is sound w.r.t. algebraic models (A, V ). IPAL is complete w.r.t. relational models: (W , ≤, R , V ) W is a nonempty set; ≤ is a partial order on W ;

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Results

IPAL is sound w.r.t. algebraic models (A, V ). IPAL is complete w.r.t. relational models: (W , ≤, R , V ) W is a nonempty set; ≤ is a partial order on W ; R is an (equivalence) relation on W s.t. (R ◦≥) ⊆ (≥◦ R ) (≤◦ R ) ⊆ (R ◦≤)

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

R = (≥◦ R )∩(R ◦≤);

Algebraic Semantics and Model Completeness for Intuitionistic Public

Results

IPAL is sound w.r.t. algebraic models (A, V ). IPAL is complete w.r.t. relational models: (W , ≤, R , V ) W is a nonempty set; ≤ is a partial order on W ; R is an (equivalence) relation on W s.t. (R ◦≥) ⊆ (≥◦ R ) (≤◦ R ) ⊆ (R ◦≤) R = (≥◦ R )∩(R ◦≤); V (p ) is a down-set (or an up-set) of (W , ≤).

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Results

IPAL is sound w.r.t. algebraic models (A, V ). IPAL is complete w.r.t. relational models: (W , ≤, R , V ) W is a nonempty set; ≤ is a partial order on W ; R is an (equivalence) relation on W s.t. (R ◦≥) ⊆ (≥◦ R ) (≤◦ R ) ⊆ (R ◦≤) R = (≥◦ R )∩(R ◦≤); V (p ) is a down-set (or an up-set) of (W , ≤).

Epistemic updates defined exactly in the same way as in the Boolean case.

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public

Results

IPAL is sound w.r.t. algebraic models (A, V ). IPAL is complete w.r.t. relational models: (W , ≤, R , V ) W is a nonempty set; ≤ is a partial order on W ; R is an (equivalence) relation on W s.t. (R ◦≥) ⊆ (≥◦ R ) (≤◦ R ) ⊆ (R ◦≤) R = (≥◦ R )∩(R ◦≤); V (p ) is a down-set (or an up-set) of (W , ≤).

Epistemic updates defined exactly in the same way as in the Boolean case. Work in progress: Intuitionistic account of Muddy Children Puzzle.

Minghui Ma, Alessandra Palmigiano, Mehrnoosh Sadrzadeh

Algebraic Semantics and Model Completeness for Intuitionistic Public