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
-
$\mathscr{A} = \langle \mathcal{P}(A), \subseteq \rangle$.
-
$\mathscr{S} = \langle \mathcal{P}(S), \supseteq \rangle$.
-
For $\alpha \subseteq A$, put $f_*(\sigma) =$ { $s$ $ | $ $\forall \varphi (\varphi \in \alpha \to s \models \varphi) $}
-
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
- $f$ is monotone iff, $\forall p, p\prime \in P$, if $p \preccurlyeq p\prime$ then. $f(p) \sqsubseteq f()p\prime$
- $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.