Galois Connection between Syntax and Semantics

 

Peter Fritz intro to propositional quantifiers里提到的 有点想去WG上讲

(Update (Jun 18 2023): 最后在DRP讲了!)

链接

[1 Peter Smith 的文章] [2前面那个文章的post] [3比较简短的介绍] [peter smith更general的intro][5知乎]

abstract interpretation 也有应用(开山?论文) 有课件:[版本一] [版本二] 跟topology的联系

Awodey课本 p.219-p.225 也有讲

Blackburn的modal logic课本有道习题也相关 p.217 引了一篇paper

Peter Smith 文章笔记

顺序:建立 poset 的一些基本概念 (最重要的是inclusion posets: you can build a complete lattice out of any set),然后讲 Galois Connection定义 及一堆推论 等价定义,uniqueness,closure;最后是重要的连接:

主要想法:

Def 3.2.1: Let A be the set of all L-sentences, and S be the set of all L-structures. Then put

  1. $\mathscr{A} = \langle \mathcal{P}(A), \subseteq \rangle$.

  2. $\mathscr{S} = \langle \mathcal{P}(S), \supseteq \rangle$.

  3. For $\alpha \subseteq A$, put $f_*(\sigma) =$ { $s$ $ | $ $\forall \varphi (\varphi \in \alpha \to s \models \varphi) $}

  4. For $\sigma \subseteq S$, put $f^*(\sigma) =$ { $\varphi$ $ | $ $\forall s (s \in \sigma \to s \models \varphi) $}

Then, $\langle f_* , f^* \rangle$ is a galois connection between $\mathscr{A} \text{ and } \mathscr{S}$.

Part 1 Poset的基本概念

Def 1.1.1 A partially ordered set $\mathscr{P} = \langle P, \preccurlyeq \rangle$ is a set P, carrying an ordered relaation $\preccurlyeq$ which is reflexive, anti-symmetric aand transitive.

Sidenote: A poset has no cycle (Thm 1.1.2)

Example in logic:

For intuitionistic logic (using Kripke frame), let W be the set of possible words, $\sqsubseteq$ be the accessibility relation between worlds. $\langle W, \sqsubseteq \rangle$ is a poset.

Inclusion posets:

Any set A, $\langle \mathcal{P}(A), \subseteq \rangle $ is a poset. Moreover, take any set $M \subseteq \mathcal {P}(A)$, $\langle M, \subseteq \rangle $ is a poset.

Maps between posets

Def 1.3.1: Suppose that $\mathscr P = \langle P, \preccurlyeq \rangle$ and $\langle L, \sqsubseteq \rangle$ are two posets, and let $f : P \rightarrow Q$ be a map between their carrier set. Then

  1. $f$ is monotone iff, $\forall p, p\prime \in P$, if $p \preccurlyeq p\prime$ then. $f(p) \sqsubseteq f()p\prime$
  2. $f$ is an order-embedding iff $\forall p, p\prime \in P, p \preccurlyeq p\prime$ iff $f(p) \sqsubseteq f(p\prime)$ (namely an injective map)

Def 1.3.3: $f$ is order isomorphism iff $f$ is a bijection.