量詞消去
量詞消去是數理邏輯、模型論與計算機科學中的一類技巧。我們稱一個理論T可消去量詞，若且唯若對每個公式\phi皆存在另一個不帶量詞的公式\psi，使得兩者在該理論中等價，即：T \models \phi \leftrightarrow \psi。 量詞消去在模型論有多種刻劃；即使一個理論可消去量詞，也不保證存在一個相應的演算法。 一個理論的量詞消去演算法係將一個帶量詞的公式轉成一個等價但不帶量詞的公式。利用這個演算法，我們能將任一句子（不帶…
标签：#模型論
共 7 篇文章
非标准分析
非標準分析（），又可稱為實無限分析或超标准分析，是一個數學分析的一个分支，它用嚴格定義的无穷小量的概念來構建分析學。1973年，直觉主义者阿兰德·海廷称赞非标准分析是“重要数学研究的标准模型”。 歷史 實無限的概念源自G·W·萊布尼茲，將微積分中的dx, dy等符號視為實際存在的無窮小量，而dy/dx則是它們之間的比值，也就是無限小尺度下的斜率。在G·W·萊布尼茲的時代，實無限的概念雖然符合直覺，但是被批評為不夠嚴謹。 在德國數學家卡尔…
字元集 (數理邏輯)
字元集在不同領域中有不同意義。在邏輯學（特別是數理邏輯中）代表的是列舉出形式語言中的一組集合；在泛代數中則是列舉出代數結構具代表性的運算。另外，在模型論中兩種用法皆有使用。 對邏輯學更哲學性的討論中，字元集的概念較少被提及。 定義 一個（單域）字元集在形式上定義為四元組 \sigma = \left(S_{\operatorname{func}}, S_{\operatorname{rel}}, S_{\operatorname{con…
飽和模型
在模型論中，飽和模型可以大致描述為一個實現夠小的型的模型。 定義 令 κ 為一個基數，\mathcal{M} 為某個一階語言中對某理論的模型。\mathcal{M} 被稱作是 κ-飽和 的，當且僅當對所有基數小於 κ 的子集 A \subset \mathcal{M}，以 A 為參數的完備型都被 \mathcal{M} 實現。\mathcal{M} 被稱作是飽和的，當且僅當它是 |\mathcal{M}|-飽和的。 例子 有理數作為稠密…
解釋 (邏輯)
解釋是一種將形式語言中的符號賦予意義的行為。許多使用於數學、邏輯及理論電腦科學的形式語言都會以純句法的方式定義，且直到給予某些解釋之前，不含有任何意義。一般研究形式語言的解釋的學科稱為形式語義學。 最常研究的形式邏輯為命題邏輯、謂詞邏輯及其衍生的邏輯，且此類的邏輯都已經有標準的方式來給出解釋。在這些情況下，解釋是一個可以提供目標語言的符號及符號字串外延的函數。例如，一個解釋函數可作用在謂詞T（表示「高」）上，並賦予其一個外延{a}（表示…
型 (模型论)
在模型論中，型是一階邏輯中的一個相容的公式集合。一個完備型是這類集合中的一個極大元素。 嚴格定義 首先固定以下對象： \mathcal{L} ：一個一階語言 T ：一個\mathcal{L}-理論 \mathcal{M} 為 T 的一個模型，A \subset \mathcal{M} 記 \mathcal{L}(A) = \mathcal{L} \cup \{c_a : a \in A \}（即：將 A 「加入」語言的常量符號）。於是 …
塔斯基-沃特测试
在模型論中，塔斯基-沃特測試（英文：Tarski-Vaught test）是用來判定一個子結構是否是基本子結構的定理。有時亦稱塔斯基判準。 陳述 給定一個一階語言 \mathcal{L}，令 \mathcal{N} 為一結構，\mathcal{M} 為其子結構，其域分別記為 M, N，M \subset N；則 \mathcal{M} 是基本子結構的充要條件是：對每個 \mathcal{L}-公式 \phi(v_1, \ldots, v…