编者按：这是 Martin Zirulnik 的客座文章，他最近为 LangChain 贡献了 HTML 头部文本分割器。要阅读更多 Martin 关于生成式 AI 的文章，请访问他的博客。

chunking-blog - LangChain 博客

构建上下文感知 LLM 应用程序通常始于系统的去语境化过程，这本身就具有某种结构性的讽刺意味，其中

源文本被分成或多或少任意大小的片段，然后
每个片段都经过向量嵌入过程，旨在理解上下文，捕捉片段之间关系中固有的信息。

人工智能应用程序依赖于检索增强生成 (RAG)，这与人类读者与自然语言互动的方式并非完全不同，它必须平衡从短字符序列中进行推断的分析精度（你的英语老师会称之为“细读”）与对意义的上下文绑定结构的理解，这些结构随着这些序列长度的增加而或多或少地持续出现（你的特别酷的英语老师会称之为“远读”）。

本博客探讨了一种新颖的方法，用于在 HTML 内容中实现这种平衡，利用文档结构中固有的重要上下文信息，这些信息在 LLM 应用程序构建于网络抓取数据或其他 HTML 源之上时通常会丢失。特别是，我们将测试一些将自查询与 LangChain 新的 HTML 头部文本分割器相结合的方法，这是一种“结构感知”的分块器，它在元素级别分割文本，并根据头部文本为每个块添加元数据。

导入和环境设置¶

我们将首先导入我们预先需要的所有内容并设置环境，包括使用 LangSmith 进行追踪。虽然这些追踪记录未在本博客中直接展示，但当链变得更复杂时，它们对于可观察性、调试、评估等非常有用。

在 [5]

import os
import re
import getpass
from typing import List, Dict
from langchain.schema import Document
from langchain.chat_models import ChatOpenAI
from langchain.embeddings.openai import OpenAIEmbeddings
from langchain.vectorstores import Redis
from langchain.document_loaders import UnstructuredURLLoader
from langchain.text_splitter import HTMLHeaderTextSplitter, RecursiveCharacterTextSplitter
from langchain.chains import RetrievalQA
from langchain.retrievers.self_query.base import SelfQueryRetriever
from langchain.chains.query_constructor.base import (
    get_query_constructor_prompt,
    load_query_constructor_runnable,
    AttributeInfo)

os.environ["OPENAI_API_KEY"] = getpass.getpass("OpenAI API Key:")
os.environ["LANGCHAIN_API_KEY"] = getpass.getpass("Langchain API key:")
os.environ["LANGCHAIN_TRACING_V2"] = "true"
os.environ['LANGCHAIN_ENDPOINT'] = "https://api.smith.langchain.com"
os.environ["LANGCHAIN_PROJECT"] = "html-chunking"

使用非结构化分块进行问答¶

首先，让我们使用基于任意字符计数的文本分割来实现一种朴素的检索策略，遵循 LLM 应用程序设计中的常见模式。

在 [10]

# assign chat and embeddings models
llm = ChatOpenAI(
    model='gpt-4',
    temperature=0
)
embeddings = OpenAIEmbeddings()

# load and split unstructured text content from web URL
loader = UnstructuredURLLoader(['https://plato.stanford.edu/entries/goedel/'])
splitter = RecursiveCharacterTextSplitter(
    chunk_size=1000,
    chunk_overlap=0
)
doc = loader.load()
docs = splitter.split_documents(doc)

# create vectorstore and QA retriever
vectorstore = Redis.from_documents(
    docs,
    embeddings,
    # running Redis server locally with Docker
    redis_url='redis://localhost:6379'
)
retriever = RetrievalQA.from_chain_type(
    llm=llm,
    chain_type="stuff",
    retriever=vectorstore.as_retriever(),
    # we'll want to see source documents for comparison
    return_source_documents=True
)

现在我们可以运行一个测试查询并打印结果以及源文档，以便我们可以了解检索器的性能，即它找到了哪些文本块作为 LLM 上下文添加到查询之前。

在 [12]

def print_result(response_obj):
    print("SOURCES: \n")
    cnt = 1
    for source_doc in response_obj["source_documents"]:
        print(f"Chunk #{cnt}")
        cnt += 1
        print("Source Metadata: ", source_doc.metadata)
        print("Source Text:")
        print(source_doc.page_content)
        print("\n")
    print("RESULT: \n")
    print(response_obj["result"] + "\n\n")

query = "explain godel's first incompleteness theorem."
response = retriever({"query":query})
print_result(response)

SOURCES:

Chunk #1
Source Metadata: {'id': 'doc:1c6f3e3f7ee14027bc856822871572dc:26e9aac7d5494208a56ff0c6cbbfda20', 'source': 'https://plato.stanford.edu/entries/goedel/'}
Source Text:
2.2.1 The First Incompleteness Theorem

In his Logical Journey (Wang 1996) Hao Wang published the
full text of material Gödel had written (at Wang’s request)
about his discovery of the incompleteness theorems. This material had
formed the basis of Wang’s “Some Facts about Kurt
Gödel,” and was read and approved by Gödel:

We see that Gödel first tried to reduce the consistency problem
for analysis to that of arithmetic. This seemed to require a truth
definition for arithmetic, which in turn led to paradoxes, such as the
Liar paradox (“This sentence is false”) and Berry’s
paradox (“The least number not defined by an expression
consisting of just fourteen English words”). Gödel then
noticed that such paradoxes would not necessarily arise if truth were
replaced by provability. But this means that arithmetic truth and
arithmetic provability are not co-extensive — whence the First
Incompleteness Theorem.

Chunk #2
Source Metadata: {'id': 'doc:1c6f3e3f7ee14027bc856822871572dc:d15f62c453c64072b768e136080cb5ba', 'source': 'https://plato.stanford.edu/entries/goedel/'}
Source Text:
The First Incompleteness Theorem provides a counterexample to
completeness by exhibiting an arithmetic statement which is neither
provable nor refutable in Peano arithmetic, though true in the
standard model. The Second Incompleteness Theorem shows that the
consistency of arithmetic cannot be proved in arithmetic itself. Thus
Gödel’s theorems demonstrated the infeasibility of the
Hilbert program, if it is to be characterized by those particular
desiderata, consistency and completeness.

As an aside, von Neumann understood the two theorems this way, even
before Gödel did. In fact von Neumann went much further in taking
the view that they showed the infeasibility of classical mathematics
altogether. As he wrote to Carnap in June of 1931:

And the previous fall von Neumann had written to Gödel in even
stronger terms:

It would take Gödel himself a few years to see that those aspects
of the Hilbert Program had been decisively refuted by his results
(Mancosu 2004).

Chunk #3
Source Metadata: {'id': 'doc:1c6f3e3f7ee14027bc856822871572dc:f4dc52218cd040cfa7734b86b6d429ea', 'source': 'https://plato.stanford.edu/entries/goedel/'}
Source Text:
On concluding the proof of the first theorem, Gödel remarks,
“we can readily see that the proof just given is constructive;
that is … proved in an intuitionistically unobjectionable
manner…” (Gödel 1986, p. 177). This is because, as
he points out, all the existential statements are based on his theorem
V (giving the numeralwise expressibility of primitive recursive
relations), which is intuitionistically unobjectionable.

2.2.3 The Second Incompleteness Theorem

The Second Incompleteness Theorem establishes the unprovability, in
number theory, of the consistency of number theory. First we have to
write down a number-theoretic formula that expresses the consistency
of the axioms. This is surprisingly simple. We just let
Con(P) be the sentence ¬Prov(⌈0 =
1⌉).

Theorem 4 (Gödel’s Second Incompleteness
Theorem) If P is consistent, then Con(P) is not
provable from P.

Chunk #4
Source Metadata: {'id': 'doc:1c6f3e3f7ee14027bc856822871572dc:a69082427ddf43f999690f21531f1ca7', 'source': 'https://plato.stanford.edu/entries/goedel/'}
Source Text:
This account of Gödel’s discovery was told to Hao Wang very
much after the fact; but in Gödel’s contemporary
correspondence with Bernays and Zermelo, essentially the same
description of his path to the theorems is given. (See Gödel
2003a and Gödel 2003b respectively.) From those accounts we see
that the undefinability of truth in arithmetic, a result credited to
Tarski, was likely obtained in some form by Gödel by 1931. But he
neither publicized nor published the result; the biases logicians had
expressed at the time concerning the notion of truth, biases which
came vehemently to the fore when Tarski announced his results on the
undefinability of truth in formal systems 1935, may have served as a
deterrent to Gödel’s publication of that theorem.

2.2.2 The proof of the First Incompleteness Theorem

RESULT:

Gödel's First Incompleteness Theorem states that in any consistent formal system that is sufficiently powerful to describe the arithmetic of the natural numbers, there are statements that can't be proven or disproven within the system itself. This means that there are true statements about the natural numbers that can't be proven within the system. The theorem came about when Gödel replaced the concept of truth with provability, realizing that arithmetic truth and arithmetic provability are not the same. This theorem provides a counterexample to completeness by showing an arithmetic statement which is neither provable nor refutable in Peano arithmetic, even though it's true in the standard model.

初步看来，这看起来像是我们朴素的 QA 链的相当可靠的输出。虽然强大的 RAG 评估不在本博客的范围内，但我们可以粗略地观察到，生成的答案本身听起来是合理的，即它可能在忠实度和相关性评估中获得良好的评分，并且每个文本块似乎都包含关于哥德尔第一不完备性定理的信号。

但是，在上下文精确度和召回率方面，检索器的表现非常差——很大程度上是因为这些块随意地跨越了源文档中指示的章节分隔符。

例如，块 #3 包含一些关于第一不完备性定理的结论性评论，这些评论与查询相关，但它也包含来自标题为“2.2.3 第二不完备性定理”的后续章节的文本，这与查询无关；更糟糕的是，块 #4 包含哥德尔证明的“斩首”（“2.2.2 第一不完备性定理的证明”），但看不到证明！

我们可能会在某种程度上优化此检索器，例如，通过改变块大小并在块之间添加一些字符重叠，但这样做并不能解决这里的更根本的问题：自然语言往往不按顺序编码信息。即使是简单的叙事散文也可能包含复杂的时间框架和信息嵌套——因此，在包括这种情况在内的许多情况下，将连续的文本块转换为节点序列的粗略过程具有扁平化效应，折叠了比链状更像树状的隐式和显式意义结构。

使用结构化分块进行问答¶

然而，标记语言（以及在某种程度上，markdown）呈现了一个有趣的边缘案例：从某种意义上说，它们旨在按顺序传达非顺序的——即结构化的——信息，因此可以为我们的分割过程提供至少一些语义支架。

让我们尝试一种更结构化的 RAG 方法，使用 HTML 头部文本分割器，它（如上所述）通过在元素级别分割 HTML 文档并将每个头部（假设是相关的）的元数据附加到任何给定的块来工作。

在 [107]

# select headers to split on, and map these to metadata field names
headers_to_split_on = [
    ("h1", "article_h1_main"),
    ("h2", "article_h2_subsection"),
    ("h3", "article_h3_subsection"),
    ("h4", "article_h4_subsection"),
]

html_splitter = HTMLHeaderTextSplitter(
    headers_to_split_on=headers_to_split_on,
    # combine elements with the same metadata by setting return_each_element to False (default)
    return_each_element=False
)
docs = html_splitter.split_text_from_url('https://plato.stanford.edu/entries/goedel/' )

# print sample chunk page content and metadata
for attr in docs[12]:
    print(attr, "\n")

('page_content', 'Gödel’s proof of the consistency of the continuum hypothesis with the axioms of Zermelo-Fraenkel set theory is a tour de force and arguably the greatest achievement of his mathematical life. This is because aside from the arithmetization, virtually all of the technical machinery used in the proof had to be invented ab initio.  \nThe Continuum Hypothesis (henceforth CH) was formulated by Georg Cantor, and was the first problem on Hilbert’s list of twenty-three unsolved problems as given in his famous address to the International Mathematical Congress in Paris in 1900. The problem as stated by Hilbert is as follows: Let A be an infinite set of real numbers. Then A is either countable, or has cardinality 2ℵ0, i.e., A is in one-to-one correspondence either with the set of natural numbers or with the set of all real numbers (otherwise known as the continuum). Another way to state the continuum hypothesis is that (the first uncountably infinite cardinal) ℵ1 = 2ℵ0.  \nAs early as 1922 Skolem speculated that the CH was independent of the axioms for set theory given by Zermelo in 1908. Nevertheless Hilbert published a (false) proof of the CH in Hilbert 1926. In 1937 Gödel proved its consistency with the axioms of ZF set theory. (Henceforth we use the standard abbreviations for Zermelo-Fraenkel set theory, ZF, and Zermelo-Fraenkel set theory with the Axiom of Choice, ZFC.) The consistency of the negation of the CH was shown by Paul Cohen in 1961 (see Cohen 1963) and hence together with Gödel’s result one infers that the CH is independent of ZF (and ZFC).  \nCohen invented an important new technique called forcing in the course of proving his result; this technique is at present the main method used to construct models of set theory. Forcing led to a revival of formalism among set theorists, the plurality of models being an indication of the “essential variability in set theory,” (Dehornoy 2004) and away from the notion that there is an intended model of set theory—a perspective Gödel advocated since at least 1947, if not earlier.[14] Recently there have been signs that the CH may again be coming to be regarded as a problem to be solved mathematically (with the help of course of some new evident axioms extending ZF). (See for example Woodin 2001a, 2002, 2001b, and Foreman 1998.) If any of the proposed solutions gain acceptance, this would confirm Gödel’s view that the CH would eventually be decided by finding an evident extension of the ZF axioms for set theory. The program associated with this view is called “Gödel’s Large Cardinal Program.”')

('metadata', {'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': '2. Gödel’s Mathematical Work', 'article_h3_subsection': '2.4 Gödel’s Work in Set theory', 'article_h4_subsection': '2.4.1 The consistency of the Continuum Hypothesis and the Axiom of Choice'})

在其当前配置中，分割器将具有相同头部元数据的所有元素的文本聚合到一个文档块中——相关的 h4 级标题（如果存在）的文本分配给元数据字段“article_h4_subsection”，并且每个先前相关标题的文本分别分配给 h3、h2 和 h1 的字段。

如果需要更小的块大小，可以通过让 HTML 头部文本分割器逐元素返回文档，或者通过将输出管道传输到另一个分割器来实现；但在任何情况下，源文档的元素树的层次结构都将作为元数据中的层次结构保留。

在 [41]

for doc in docs:
    if doc.metadata:
        print(doc.metadata, "\n")

{'article_h1_main': 'Kurt Gödel'}

{'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': '1. Biographical Sketch'}

{'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': '2. Gödel’s Mathematical Work'}

{'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': '2. Gödel’s Mathematical Work', 'article_h3_subsection': '2.1 The Completeness Theorem', 'article_h4_subsection': '2.1.1 Introduction'}

{'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': '2. Gödel’s Mathematical Work', 'article_h3_subsection': '2.1 The Completeness Theorem', 'article_h4_subsection': '2.1.2 Proof of the Completeness Theorem'}

{'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': '2. Gödel’s Mathematical Work', 'article_h3_subsection': '2.1 The Completeness Theorem', 'article_h4_subsection': '2.1.3 An Important Consequence of the Completeness Theorem'}

{'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': '2. Gödel’s Mathematical Work', 'article_h3_subsection': '2.2 The Incompleteness Theorems'}

{'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': '2. Gödel’s Mathematical Work', 'article_h3_subsection': '2.2 The Incompleteness Theorems', 'article_h4_subsection': '2.2.1 The First Incompleteness Theorem'}

{'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': '2. Gödel’s Mathematical Work', 'article_h3_subsection': '2.2 The Incompleteness Theorems', 'article_h4_subsection': '2.2.2 The proof of the First Incompleteness Theorem'}

{'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': '2. Gödel’s Mathematical Work', 'article_h3_subsection': '2.2 The Incompleteness Theorems', 'article_h4_subsection': '2.2.3 The Second Incompleteness Theorem'}

{'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': '2. Gödel’s Mathematical Work', 'article_h3_subsection': '2.3 Speed-up Theorems'}

{'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': '2. Gödel’s Mathematical Work', 'article_h3_subsection': '2.4 Gödel’s Work in Set theory', 'article_h4_subsection': '2.4.1 The consistency of the Continuum Hypothesis and the Axiom of Choice'}

{'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': '2. Gödel’s Mathematical Work', 'article_h3_subsection': '2.4 Gödel’s Work in Set theory', 'article_h4_subsection': '2.4.2 Gödel’s Proof of the Consistency of the Continuum Hypothesis and the Axiom of Choice with the Axioms of Zermelo-Fraenkel Set Theory'}

{'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': '2. Gödel’s Mathematical Work', 'article_h3_subsection': '2.4 Gödel’s Work in Set theory', 'article_h4_subsection': '2.4.3 Consequences of Consistency'}

{'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': '2. Gödel’s Mathematical Work', 'article_h3_subsection': '2.4 Gödel’s Work in Set theory', 'article_h4_subsection': '2.4.4 Gödel’s view of the Axiom of Constructibility'}

{'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': '2. Gödel’s Mathematical Work', 'article_h3_subsection': '2.5 Gödel’s Work in Intuitionistic Logic and Arithmetic'}

{'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': '2. Gödel’s Mathematical Work', 'article_h3_subsection': '2.5 Gödel’s Work in Intuitionistic Logic and Arithmetic', 'article_h4_subsection': '2.5.1 Intuitionistic Propositional Logic is not Finitely-Valued'}

{'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': '2. Gödel’s Mathematical Work', 'article_h3_subsection': '2.5 Gödel’s Work in Intuitionistic Logic and Arithmetic', 'article_h4_subsection': '2.5.2 Classical Arithmetic is Interpretable in Heyting Arithmetic'}

{'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': '2. Gödel’s Mathematical Work', 'article_h3_subsection': '2.5 Gödel’s Work in Intuitionistic Logic and Arithmetic', 'article_h4_subsection': '2.5.3 Intuitionistic Propositional Logic is Interpretable in S4'}

{'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': '2. Gödel’s Mathematical Work', 'article_h3_subsection': '2.5 Gödel’s Work in Intuitionistic Logic and Arithmetic', 'article_h4_subsection': '2.5.4 Heyting Arithmetic is Interpretable into Computable Functionals of Finite Type.'}

{'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': '3. Gödel’s Philosophical Views'}

{'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': '3. Gödel’s Philosophical Views', 'article_h3_subsection': '3.1 Gödel’s Rationalism'}

{'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': '3. Gödel’s Philosophical Views', 'article_h3_subsection': '3.2 Gödel’s Realism'}

{'article_h1_main': 'Kurt Gödel'}

{'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': 'Bibliography', 'article_h3_subsection': 'Primary Sources', 'article_h4_subsection': 'Gödel’s Writings'}

{'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': 'Bibliography', 'article_h3_subsection': 'Primary Sources', 'article_h4_subsection': 'The Collected Papers of Kurt Gödel'}

{'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': 'Bibliography', 'article_h3_subsection': 'Secondary Sources'}

{'article_h1_main': 'Kurt Gödel'}

{'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': 'Academic Tools'}

{'article_h1_main': 'Kurt Gödel'}

{'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': 'Other Internet Resources'}

{'article_h1_main': 'Kurt Gödel'}

{'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': 'Related Entries'}

{'article_h1_main': 'Kurt Gödel'}

{'article_h1_main': 'Kurt Gödel', 'article_h3_subsection': 'Acknowledgments'}

{'article_h4_subsection': 'Browse'}

{'article_h4_subsection': 'About'}

{'article_h4_subsection': 'Support SEP'}

{'article_h4_subsection': 'Mirror Sites'}

即使我们在检索期间忽略所有这些元数据，根据文档自身显式的信息结构分割文档，从理论上讲也应该改进我们的检索链。让我们在实施自查询之前尝试一下。

由于我们正在使用 Redis 作为向量数据库，并且现在为我们的文档提供了自定义元数据字段，因此我们需要构建自定义索引模式。有关更多信息，请参阅此文档。

在 [29]

def build_index_schema(documents: List[Document]) -> Dict:
    schema = {"text": []}
    for doc in documents:
        for key in doc.metadata:
            name_dict = {"name": f"{key}"}
            if name_dict not in schema["text"]:
                schema["text"].append(name_dict)
    return schema

index_schema = build_index_schema(docs)
print(index_schema)

{'text': [{'name': 'article_h1_main'}, {'name': 'article_h2_subsection'}, {'name': 'article_h3_subsection'}, {'name': 'article_h4_subsection'}]}

vectorstore = Redis.from_documents(
    docs,
    embeddings,
    redis_url='redis://localhost:6379',
    index_schema = index_schema
)
retriever = RetrievalQA.from_chain_type(
    llm=llm,
    chain_type="stuff",
    retriever=vectorstore.as_retriever(),
    return_source_documents=True
)

query = "explain godel's first incompleteness theorem."
response = retriever({"query": query})
print_result(response)

SOURCES:

Chunk #1
Source Metadata:  {'id': 'doc:c39d409b58e3444691ad91c34b5c3ee1:2b0ffb3f19f94dd0812b72507bb83c23', 'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': '2. Gödel’s Mathematical Work', 'article_h3_subsection': '2.2 The Incompleteness Theorems', 'article_h4_subsection': '2.2.3 The Second Incompleteness Theorem'}
Source Text:
The Second Incompleteness Theorem establishes the unprovability, in number theory, of the consistency of number theory. First we have to write down a number-theoretic formula that expresses the consistency of the axioms. This is surprisingly simple. We just let Con(P) be the sentence ¬Prov(⌈0 = 1⌉).
Theorem 4 (Gödel’s Second Incompleteness Theorem) If P is consistent, then Con(P) is not provable from P.
Proof: Let φ be as in (3). The reasoning used to infer ‘if P ⊢ φ, then P ⊢ 0 ≠ 1‘ does not go beyond elementary number theory, and can therefore, albeit with a lot of effort (see below), be formalized in P. This yields: P ⊢ (Prov(⌈φ⌉) → ¬Con(P)), and thus by (3), P ⊢ (Con(P) → φ). Since P ⊬ φ, we must have P ⊬ Con(P).
The above proof (sketch) of the Second Incompleteness Theorem is deceptively simple as it avoids the formalization. A rigorous proof would have to establish the proof of ‘if P ⊢ φ, then P ⊢ 0 ≠ 1’ in P.
It is noteworthy that ω-consistency is not needed in the proof of Gödel’s Second Incompleteness Theorem. Also note that neither is ¬Con(P) provable, by the consistency of P and the fact, now known as Löb’s theorem, that P ⊢ Prov(⌈φ⌉) implies P ⊢ φ.
The assumption of ω-consistency in the First Incompleteness Theorem was eliminated by Rosser in 1936, and replaced by the weaker notion of consistency. Rosser’s generalization involves applying the fixed point theorem to the formula R(x): ‘for all z: either z is not the Gödel number of a proof of the formula with Gödel number x or there is a proof shorter than z of the negation of (the formula with Gödel number) x’ (see Rosser 1936).
With regard to the Second Incompleteness Theorem, the argument relies in part on formalizing the proof of the First Incompleteness Theorem as we saw. This step is omitted in Gödel 1931. He planned to include the step in what would have been a second part II (see footnote 48a of Gödel 1931). But instead of writing it he turned to the continuum problem.[13] (Part II was to elaborate on other points too: the ‘true reason for incompleteness,’ and the applicability of the two theorems to other systems.) He perhaps did not feel compelled to attend to what looked like an exercise in formalization, relying instead on the informal argument to convince (in which it succeeded). However this step turned out to be somewhat non-trivial. As Kleene puts it in his introduction to Gödel 1931, of the informal presentation, “Certainly the idea of the argument for Theorem XI (consistency) was very convincing; but it turned out that the execution of the details required somewhat more work and care than had been anticipated.” (See pp. 126–141 of Gödel 1986.) Eventually a complete proof of the Second Theorem was given by Hilbert and Bernays in some seventy pages in their Hilbert and Bernays 1939. A much more compact treatment of the theorem was given by Löb in his Löb 1956, and subsequently Feferman, in his 1960 “Arithmetization of Metamathematics in a General Setting” (Feferman 1960/1961), gave a succinct and completely general treatment of both the First and Second Theorems. But see the supplementary document:
Did the Incompleteness Theorems Refute Hilbert’s Program?
For more detailed discussion, see the entry on Gödel’s incompleteness theorems.


Chunk #2
Source Metadata:  {'id': 'doc:c39d409b58e3444691ad91c34b5c3ee1:88cbf09a1af64dc78b6ac0c34170b725', 'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': 'Related Entries', 'article_h3_subsection': None, 'article_h4_subsection': None}
Source Text:
Gödel, Kurt: incompleteness theorems | Hilbert, David: program in the foundations of mathematics | Husserl, Edmund | Leibniz, Gottfried Wilhelm | mathematics, philosophy of: intuitionism | mathematics, philosophy of: Platonism | model theory | model theory: first-order | phenomenology | realism | set theory | set theory: continuum hypothesis | set theory: large cardinals and determinacy


Chunk #3
Source Metadata:  {'id': 'doc:c39d409b58e3444691ad91c34b5c3ee1:65d27ea51ab0470e82b59678ccf471ce', 'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': '2. Gödel’s Mathematical Work', 'article_h3_subsection': '2.2 The Incompleteness Theorems', 'article_h4_subsection': '2.2.2 The proof of the First Incompleteness Theorem'}
Source Text:
We now describe the proof of the two theorems, formulating Gödel’s results in Peano arithmetic. Gödel himself used a system related to that defined in Principia Mathematica, but containing Peano arithmetic. In our presentation of the First and Second Incompleteness Theorems we refer to Peano arithmetic as P, following Gödel’s notation.
Before proceeding to the details of the formal proof, we define the notion of ω-consistency used by Gödel in the First Incompleteness Theorem: P is ω-consistent if P ⊢ ¬φ(n) for all n implies P ⊬ ∃xφ(x). Naturally this implies consistency and follows from the assumption that the natural numbers satisfy the axioms of Peano arithmetic.
One of the main technical tools used in the proof is Gödel numbering, a mechanism which assigns natural numbers to terms and formulas of our formal theory P. There are different ways of doing this. The most common is based on the unique representation of natural numbers as products of powers of primes. Each symbol s of number theory is assigned a positive natural number #(s) in a fixed but arbitrary way, e.g.
#(0) = 1 #(=) = 5 #(¬) = 9 #(1) = 2 #( ( ) = 6 #(∀) = 10 #(+) = 3 #( ) ) = 7 #(vi) = 11 + i #(×) = 4 #(∧) = 8  
The natural number corresponding to a sequence w = < w0,…, wk > of symbols is
⌈w⌉ = 2#(w0) · 3#(w1) · … · pk#(wk),
where pk is the k+1st prime. It is called its Gödel number and denoted by ⌈w⌉. In this way we can assign Gödel numbers to formulas, sequences of formulas (once a method for distinguishing when one formula ends and another begins has been adopted), and most notably, proofs.
An essential point here is that when a formula is construed as a natural number, then the numeral corresponding to that natural number can occur as the argument of a formula, thus enabling the syntax to “refer” to itself, so to speak (i.e., when a numeral is substituted into a formula the Gödel number of which the numeral represents). This will eventually allow Gödel to formalize the Liar paradox (with “provability” in place of “truth”) by substituting into the formula which says, ‘the formula, whose code is x, is unprovable,’ its own natural number code (or more precisely the corresponding numeral).
Another concept required to carry out the formalization is the concept of numeralwise expressibility of number theoretic predicates. A number-theoretic formula φ(n1, …, nk) is numeralwise expressible in P if for each tuple of natural numbers (n1, …, nk):
N ⊨ φ(n1, …, nk) ⇒ P ⊢ φ(n1, …, nk) N ⊨ ¬φ(n1, …, nk) ⇒ P ⊢ ¬φ(n1, …, nk)
where n is the formal term which denotes the natural number n. (In P, this is S(S(…S(0)…), where n is the number of iterations of the successor function applied to the constant symbol 0.) One of the principal goals is to numeralwise express the predicate
Prf(x, y): ‘the sequence with Gödel number x is a proof of the sentence with Gödel number y.’
Reaching this goal involves defining forty-five relations, each defined in terms of the preceding ones. These relations are all primitive recursive.[10] Relations needed are, among others, those which assert of a natural number that it codes a sequence, or a formula, or an axiom, or that it is the code, denoted by Sb(ru1…unZ(x1)…Z(xn)), of a formula obtained from a formula with code r by substituting for its free variable ui the xi th numeral for i = 1, …, n. The forty-fifth primitive recursive relation defined is Prf(x, y), and the forty-sixth is
Prov(y): ‘the sentence with Gödel number y is provable in P’
which without being primitive recursive, is however obtained from Prf(x, y) by existentially quantifying x. (Prov(y) satisfies only the ‘positive’ part of numeralwise expressibility, and not the negative part; but the negative part is not needed.)
In Theorem V of his paper, Gödel proves that any number theoretic predicate which is primitive recursive is numeralwise expressible in P. Thus since Prf(x, y) and substitution are primitive recursive, these are decided by P when closed terms are substituted for the free variables x and y. This is the heart of the matter as we will see. Another key point about numeralwise expressibility is that although we informally interpret, for example, Prov(Sb(ru1…unZ(x1)…Z(xn))), by: ‘the formula with Gödel number r is provable if the Gödel number for the xi th numeral is substituted in place of the i th variable,’ neither the formal statement within the theory P nor anything we prove about it appeals to such meanings. On the contrary Prov(Sb(ru1…unZ(x1)…Z(xn))), is a meaningless string of logical and arithmetical symbols. As Gödel puts it in his introduction to his theorem V, ‘The fact that can be formulated vaguely by saying that every recursive relation is definable in the system P (if the usual meaning is given to the formulas of this system) is expressed in precise language, without reference to any interpretation of the formulas of P, by the following Theorem (V) (Gödel 1986, p. 171, italics Gödel’s).
Gödel in his incompleteness theorems uses a method given in what is called nowadays Gödel’s Fixed Point Theorem. Although Gödel constructs a fixed point in the course of proving the incompleteness theorem, he does not state the fixed point theorem explicitly. The fixed point theorem is as follows:
Theorem 2 (Gödel’s Fixed Point Theorem) If φ(v0) is a formula of number theory, then there is a sentence ψ such that P ⊢ ψ ↔ φ(⌈ψ⌉), where ⌈ψ⌉ is the formal term corresponding to the natural number code of ⌈ψ⌉.
Proof: Let σ(x,y,z) be a formula that numeralwise expresses the number theoretic predicate ‘y is the Gödel number of the formula obtained by replacing the variable v0 in the formula whose Gödel number is x by the term z’. Let θ(v0) be the formula ∃v1(φ(v1) ∧ σ(v0, v1, v0)). Let k = ⌈θ(v0)⌉ and ψ = θ(k). Now directly by the construction P ⊢ ψ ↔ φ(⌈ψ⌉).
A sentence is refutable from a theory if its negation is provable. The First Incompleteness Theorem as Gödel stated it is as follows:
Theorem 3 (Gödel’s First Incompleteness Theorem) If P is ω-consistent, then there is a sentence which is neither provable nor refutable from P.
Proof: By judicious coding of syntax referred to above, write a formula Prf(x,y)[11] of number theory, representable in P, so that
n codes a proof of φ ⇒ P ⊢ Prf(n, ⌈φ⌉).
and
n does not code a proof of φ ⇒ P ⊢ ¬Prf(n, ⌈φ⌉).
Let Prov(y) denote the formula ∃x Prf(x,y)[12]. By Theorem 2 there is a sentence φ with the property
P ⊢ (φ ↔ ¬Prov(⌈φ⌉)).
Thus φ says ‘I am not provable.’ We now observe, if P ⊢ φ, then by (1) there is n such that P ⊢ Prf(n, ⌈φ⌉), hence P ⊢ Prov(⌈φ⌉), hence, by (3) P ⊢ ¬φ, so P is inconsistent. Thus
P ⊬ φ
Furthermore, by (4) and (2), we have P ⊢ ¬Prf(n, ⌈φ⌉) for all natural numbers n. By ω-consistency P ⊬ ∃x Prf(x, ⌈φ⌉). Thus (3) gives P ⊬ ¬φ. We have shown that if P is ω-consistent, then φ is independent of P.
On concluding the proof of the first theorem, Gödel remarks, “we can readily see that the proof just given is constructive; that is … proved in an intuitionistically unobjectionable manner…” (Gödel 1986, p. 177). This is because, as he points out, all the existential statements are based on his theorem V (giving the numeralwise expressibility of primitive recursive relations), which is intuitionistically unobjectionable.


Chunk #4
Source Metadata:  {'id': 'doc:c39d409b58e3444691ad91c34b5c3ee1:5eda575b170248b5a6f1cc45dc318dab', 'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': '2. Gödel’s Mathematical Work', 'article_h3_subsection': '2.2 The Incompleteness Theorems', 'article_h4_subsection': None}
Source Text:
Gödel mentioned the possibility of the unsolvability of a question about the reals already in his 1929 thesis, in arguing against the formalist principle of Hilbert’s, that consistency is a criterion for existence. In fact, giving a finitary proof of the consistency of analysis was a key desideratum of what was then known as the Hilbert program, along with proving its completeness. Accordingly it was Gödel’s turn to these questions, especially the first, which led him to the two incompleteness theorems. (For a discussion of the Hilbert Program the reader is referred to the standard references: Sieg 1990, 1988, 1999; Mancosu 1998, Zach 2003, Tait 1981 and Tait 2002.)
The First Incompleteness Theorem provides a counterexample to completeness by exhibiting an arithmetic statement which is neither provable nor refutable in Peano arithmetic, though true in the standard model. The Second Incompleteness Theorem shows that the consistency of arithmetic cannot be proved in arithmetic itself. Thus Gödel’s theorems demonstrated the infeasibility of the Hilbert program, if it is to be characterized by those particular desiderata, consistency and completeness.
As an aside, von Neumann understood the two theorems this way, even before Gödel did. In fact von Neumann went much further in taking the view that they showed the infeasibility of classical mathematics altogether. As he wrote to Carnap in June of 1931:
Thus today I am of the opinion that 1. Gödel has shown the unrealizability of Hilbert’s program. 2. There is no more reason to reject intuitionism (if one disregards the aesthetic issue, which in practice will also for me be the decisive factor). Therefore I consider the state of the foundational discussion in Königsberg to be outdated, for Gödel’s fundamental discoveries have brought the question to a completely different level.[9]
And the previous fall von Neumann had written to Gödel in even stronger terms:
Thus, I think that your result has solved negatively the foundational question: there is no rigorous justification for classical mathematics. (Gödel 2003b, p. 339)
It would take Gödel himself a few years to see that those aspects of the Hilbert Program had been decisively refuted by his results (Mancosu 2004).


RESULT:

Gödel's First Incompleteness Theorem states that in any consistent formal system that is sufficiently expressive to include at least arithmetic, there exists a statement that cannot be proven true or false within the system itself.

The proof of this theorem involves a technique known as Gödel numbering, which assigns unique natural numbers to each symbol, formula, or sequence of formulas in the system. This allows the system to "refer to itself" in a sense.

Gödel then constructs a specific statement (often informally described as "This statement cannot be proven") within the system. If this statement could be proven true within the system, it would be false, creating a contradiction. If it could be proven false, that would mean it could be proven, which would make it true, again a contradiction. Therefore, this statement can neither be proven true nor false within the system, demonstrating the system's incompleteness.

It's important to note that the system must be consistent (it cannot produce contradictory results) and sufficiently expressive (capable of expressing at least basic arithmetic) for the theorem to apply.

瞧！检索器现在成功检索到正确定理的完整证明——这在之前被“斩首”并丢失为上下文——即使它检索到的 4 个块中有 2 个不包含相关上下文，但最终答案明显更清晰、更详细和更精确，因为相关块包含原始源文档的完整、语义连贯的子章节。

使用结构化分块和自查询进行问答¶

现在是实施自查询的时候了。应该注意的是，在查询构造领域存在大量未知的领域，以下方法应以探索的精神对待，而不是作为使用自查询检索器的终极建议。

第一步是为文档和每个元数据字段创建描述。这可以使用硬编码和 LLM 生成的文本以编程方式完成。（LLM 驱动的）查询构造器将使用这些描述作为上下文来生成特定于向量存储的过滤器，因此在字段描述中指定有效的比较器和运算符会很有帮助。

在 [85]

document_content_description = "a section of an encyclopedia article about a philosopher"

def generate_metadata_desc(field_name: str, header_info: List[tuple], qa_retriever: RetrievalQA) -> str:
    query = f"""
    given a list of tuples indicating all possible metadata fields for this article
    provide a very brief description (15 words or less) of the specified field
    including its position in the hierarchy of headers (h1, h2, h3, etc)
    
    all fields {header_info}
    specified field: {field_name}
    """

    return qa_retriever({"query": query})["result"]

def build_metadata_field_info(schema: Dict, header_info: List[tuple], qa_retriever: RetrievalQA) -> List[AttributeInfo]:
    filter_instructions = \
        "ALWAYS filter with one or more CONTAINS comparators, and use the OR operator to check ALL other fields."\
        "if the value of this field contains a word or phrase that is very similar to a word or phrase in the query, " \
        "filter for the exact string from the value rather than the query."
    filter_h1 = \
        "this field contains the name of a philosopher. "\
        "if the query contains a misspelling or an alternate spelling of this name, "\
        "filter for the value of this field rather than the name in the query."\
        "the h1-level filter should ALWAYS be combined with subsection filters using an AND operator. \n"
    filter_exclusion = \
        " NEVER filter this field on the value of 'article_h1_main'."
    attr_info_list = []
    for field in schema["text"]:
        desc = generate_metadata_desc(field["name"], header_info, qa_retriever) + filter_instructions
        if field["name"] == "article_h1_main":
            new_attr = AttributeInfo(
                name=field["name"],
                description = filter_h1 + desc,
                type="string"
            )
        else:
            new_attr = AttributeInfo(
                name=field["name"],
                description = desc + filter_exclusion,
                type="string"
            )
        attr_info_list.append(new_attr)
    return attr_info_list

metadata_field_info = build_metadata_field_info(index_schema, headers_to_split_on, retriever)

接下来，我们将为查询构造器编写一些少样本示例。这些将特定于我们的数据。这里要强调的一个重要指示是，为了构建与字符串匹配的过滤器，包含拼写错误、替代拼写、不精确措辞等的查询字符串应被视为等同于元数据中存在的“规范”字符串。因此，例如，如果查询引用“goodle 的连续统理论”，则构造器应知道在 “Kurt Gödel” 上过滤 h1 头部文本，并在 “Continuum Hypothesis” 上过滤其他元数据值，因为这些确切的字符串存在于元数据中，并且可以被视为等同于 “goodle” 和 “continuum theory”。

在 [86]

# example queries contain misspellings / imprecise phrases
# example filters use the spelling / phrasing from the metadata values rather than the query
examples = [
    (
        "what does russell say about descriptors?",
        {"query": "russell, descriptors",
         "filter": 'and(contain("article_h1_main", "Bertrand Russell"), or(contain("article_h2_subsection", "descriptions"), '
                   'contain("article_h3_subsection", "descriptions"), contain("article_h4_subsection", "descriptions")))'}
    ),
    (
        "explain leibniz's idea of sufficient reason.",
        {"query": "leibniz, idea of sufficient reason",
         "filter": 'and(contain("article_h1_main", "Gottfried Wilhelm Leibniz"), or(contain("article_h2_subsection", "Principle of Sufficient Reason"), '
                   'contain("article_h3_subsection", "Principle of Sufficient Reason"), contain("article_h4_subsection", "Principle of Sufficient Reason")))'}
    ),
    (
        "what was goodel's continuum theory?",
        {"query": "goodel, continuum theory",
         "filter": 'and(contain("article_h1_main", "Kurt Gödel"), or(contain("article_h2_subsection", "Continuum Hypothesis"), '
                   'contain("article_h3_subsection", "Continuum Hypothesis"), contain("article_h4_subsection", "Continuum Hypothesis")))'}
    ),
]

现在让我们看看将为查询构造器构建的完整提示

在 [87]

prompt = get_query_constructor_prompt(
    document_content_description,
    metadata_field_info,
    examples=examples
)
print(prompt.format(query="{query}"))

Your goal is to structure the user's query to match the request schema provided below.

<< Structured Request Schema >>
When responding use a markdown code snippet with a JSON object formatted in the following schema:

```json
{
    "query": string \ text string to compare to document contents
    "filter": string \ logical condition statement for filtering documents
}
```

The query string should contain only text that is expected to match the contents of documents. Any conditions in the filter should not be mentioned in the query as well.

A logical condition statement is composed of one or more comparison and logical operation statements.

A comparison statement takes the form: `comp(attr, val)`:
- `comp` (eq | ne | gt | gte | lt | lte | contain | like | in | nin): comparator
- `attr` (string):  name of attribute to apply the comparison to
- `val` (string): is the comparison value

A logical operation statement takes the form `op(statement1, statement2, ...)`:
- `op` (and | or | not): logical operator
- `statement1`, `statement2`, ... (comparison statements or logical operation statements): one or more statements to apply the operation to

Make sure that you only use the comparators and logical operators listed above and no others.
Make sure that filters only refer to attributes that exist in the data source.
Make sure that filters only use the attributed names with its function names if there are functions applied on them.
Make sure that filters only use format `YYYY-MM-DD` when handling timestamp data typed values.
Make sure that filters take into account the descriptions of attributes and only make comparisons that are feasible given the type of data being stored.
Make sure that filters are only used as needed. If there are no filters that should be applied return "NO_FILTER" for the filter value.

<< Data Source >>
```json
{
    "content": "a section of an encyclopedia article about a philosopher",
    "attributes": {
    "article_h1_main": {
        "description": "this field contains the name of a philosopher. if the query contains a misspelling or an alternate spelling of this name, filter for the value of this field rather than the name in the query.the h1-level filter should ALWAYS be combined with subsection filters using an AND operator. \nThe 'article_h1_main' is the main title of the article, positioned at the highest level in the header hierarchy.ALWAYS filter with one or more CONTAINS comparators, and use the OR operator to check ALL other fields.if the value of this field contains a word or phrase that is very similar to a word or phrase in the query, filter for the exact string from the value rather than the query.",
        "type": "string"
    },
    "article_h2_subsection": {
        "description": "The 'article_h2_subsection' field represents the secondary headers or subsections within the main article content.ALWAYS filter with one or more CONTAINS comparators, and use the OR operator to check ALL other fields.if the value of this field contains a word or phrase that is very similar to a word or phrase in the query, filter for the exact string from the value rather than the query. NEVER filter this field on the value of 'article_h1_main'.",
        "type": "string"
    },
    "article_h3_subsection": {
        "description": "The 'article_h3_subsection' field represents the third level headers in the article, under the main and secondary headers.ALWAYS filter with one or more CONTAINS comparators, and use the OR operator to check ALL other fields.if the value of this field contains a word or phrase that is very similar to a word or phrase in the query, filter for the exact string from the value rather than the query. NEVER filter this field on the value of 'article_h1_main'.",
        "type": "string"
    },
    "article_h4_subsection": {
        "description": "The 'article_h4_subsection' field represents the fourth level headers in the article, under h1, h2, and h3 headers.ALWAYS filter with one or more CONTAINS comparators, and use the OR operator to check ALL other fields.if the value of this field contains a word or phrase that is very similar to a word or phrase in the query, filter for the exact string from the value rather than the query. NEVER filter this field on the value of 'article_h1_main'.",
        "type": "string"
    }
}
}
```


<< Example 1. >>
User Query:
what does russell say about descriptors?

Structured Request:
```json
{
    "query": "russell, descriptors",
    "filter": "and(contain(\"article_h1_main\", \"Bertrand Russell\"), or(contain(\"article_h2_subsection\", \"descriptions\"), contain(\"article_h3_subsection\", \"descriptions\"), contain(\"article_h4_subsection\", \"descriptions\")))"
}
```


<< Example 2. >>
User Query:
explain leibniz's idea of sufficient reason.

Structured Request:
```json
{
    "query": "leibniz, idea of sufficient reason",
    "filter": "and(contain(\"article_h1_main\", \"Gottfried Wilhelm Leibniz\"), or(contain(\"article_h2_subsection\", \"Principle of Sufficient Reason\"), contain(\"article_h3_subsection\", \"Principle of Sufficient Reason\"), contain(\"article_h4_subsection\", \"Principle of Sufficient Reason\")))"
}
```


<< Example 3. >>
User Query:
what was goodel's continuum theory?

Structured Request:
```json
{
    "query": "goodel, continuum theory",
    "filter": "and(contain(\"article_h1_main\", \"Kurt G\u00f6del\"), or(contain(\"article_h2_subsection\", \"Continuum Hypothesis\"), contain(\"article_h3_subsection\", \"Continuum Hypothesis\"), contain(\"article_h4_subsection\", \"Continuum Hypothesis\")))"
}
```


<< Example 4. >>
User Query:
{query}

Structured Request:

现在可以将查询构造器构建为可运行的链。考虑到我们提示的相对较高的令牌计数，我们可以在此组件中使用 gpt-3.5-turbo（而不是 gpt-4）作为模型。

（请注意，根据数据，gpt-3.5-turbo 可能需要额外的示例才能像 gpt-4 一样可靠地构造查询并处理边缘情况。）

在 [83]

chain = load_query_constructor_runnable(
    llm=ChatOpenAI(
        model="gpt-3.5-turbo",
        temperature=0
    ),
    attribute_info=metadata_field_info,
    document_contents=document_content_description,
    examples=examples,
    fix_invalid=True
)

为了检查构造器是否会为匹配元数据值而不是原始查询的字符串/子字符串正确构建过滤器，让我们尝试等效单词的替代拼写

query = "explain goedel's 1st incompleteness theory"
chain.invoke(({"query": query}))

StructuredQuery(query='goedel, 1st incompleteness theory', filter=Operation(operator=, arguments=[Comparison(comparator=, attribute='article_h1_main', value='Kurt Gödel'), Operation(operator=, arguments=[Comparison(comparator=, attribute='article_h2_subsection', value='First Incompleteness Theorem'), Comparison(comparator=, attribute='article_h3_subsection', value='First Incompleteness Theorem'), Comparison(comparator=, attribute='article_h4_subsection', value='First Incompleteness Theorem')])]), limit=None)

成功！看来查询构造器链可以输出有效的、格式良好的查询，以便在我们的向量数据库上执行。此查询应返回元数据字段 “article_h1_main” 的值包含 “Kurt Gödel” 且任何其他元数据字段的值包含 “First Incompleteness Theorem” 的文档。

现在我们可以将所有内容组合成一个问答检索链。

在 [80]

sq_retriever = SelfQueryRetriever(
    query_constructor=chain,
    vectorstore=vectorstore,
    verbose=True,
)
sq_qa = RetrievalQA.from_chain_type(
    llm=llm,
    chain_type="stuff",
    retriever=sq_retriever,
    return_source_documents=True
)

在 [90]

response = sq_qa({"query": query})
print_result(response)

SOURCES:

Chunk #1
Source Metadata:  {'id': 'doc:c39d409b58e3444691ad91c34b5c3ee1:6c1de40a549245b7a6c3d56b7dda8da4', 'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': '2. Gödel’s Mathematical Work', 'article_h3_subsection': '2.2 The Incompleteness Theorems', 'article_h4_subsection': '2.2.1 The First Incompleteness Theorem'}
Source Text:
In his Logical Journey (Wang 1996) Hao Wang published the full text of material Gödel had written (at Wang’s request) about his discovery of the incompleteness theorems. This material had formed the basis of Wang’s “Some Facts about Kurt Gödel,” and was read and approved by Gödel:
In the summer of 1930 I began to study the consistency problem of classical analysis. It is mysterious why Hilbert wanted to prove directly the consistency of analysis by finitary methods. I saw two distinguishable problems: to prove the consistency of number theory by finitary number theory and to prove the consistency of analysis by number theory … Since the domain of finitary number theory was not well-defined, I began by tackling the second half… I represented real numbers by predicates in number theory… and found that I had to use the concept of truth (for number theory) to verify the axioms of analysis. By an enumeration of symbols, sentences and proofs within the given system, I quickly discovered that the concept of arithmetic truth cannot be defined in arithmetic. If it were possible to define truth in the system itself, we would have something like the liar paradox, showing the system to be inconsistent… Note that this argument can be formalized to show the existence of undecidable propositions without giving any individual instances. (If there were no undecidable propositions, all (and only) true propositions would be provable within the system. But then we would have a contradiction.)… In contrast to truth, provability in a given formal system is an explicit combinatorial property of certain sentences of the system, which is formally specifiable by suitable elementary means…
We see that Gödel first tried to reduce the consistency problem for analysis to that of arithmetic. This seemed to require a truth definition for arithmetic, which in turn led to paradoxes, such as the Liar paradox (“This sentence is false”) and Berry’s paradox (“The least number not defined by an expression consisting of just fourteen English words”). Gödel then noticed that such paradoxes would not necessarily arise if truth were replaced by provability. But this means that arithmetic truth and arithmetic provability are not co-extensive — whence the First Incompleteness Theorem.
This account of Gödel’s discovery was told to Hao Wang very much after the fact; but in Gödel’s contemporary correspondence with Bernays and Zermelo, essentially the same description of his path to the theorems is given. (See Gödel 2003a and Gödel 2003b respectively.) From those accounts we see that the undefinability of truth in arithmetic, a result credited to Tarski, was likely obtained in some form by Gödel by 1931. But he neither publicized nor published the result; the biases logicians had expressed at the time concerning the notion of truth, biases which came vehemently to the fore when Tarski announced his results on the undefinability of truth in formal systems 1935, may have served as a deterrent to Gödel’s publication of that theorem.


Chunk #2
Source Metadata:  {'id': 'doc:c39d409b58e3444691ad91c34b5c3ee1:65d27ea51ab0470e82b59678ccf471ce', 'article_h1_main': 'Kurt Gödel', 'article_h2_subsection': '2. Gödel’s Mathematical Work', 'article_h3_subsection': '2.2 The Incompleteness Theorems', 'article_h4_subsection': '2.2.2 The proof of the First Incompleteness Theorem'}
Source Text:
We now describe the proof of the two theorems, formulating Gödel’s results in Peano arithmetic. Gödel himself used a system related to that defined in Principia Mathematica, but containing Peano arithmetic. In our presentation of the First and Second Incompleteness Theorems we refer to Peano arithmetic as P, following Gödel’s notation.
Before proceeding to the details of the formal proof, we define the notion of ω-consistency used by Gödel in the First Incompleteness Theorem: P is ω-consistent if P ⊢ ¬φ(n) for all n implies P ⊬ ∃xφ(x). Naturally this implies consistency and follows from the assumption that the natural numbers satisfy the axioms of Peano arithmetic.
One of the main technical tools used in the proof is Gödel numbering, a mechanism which assigns natural numbers to terms and formulas of our formal theory P. There are different ways of doing this. The most common is based on the unique representation of natural numbers as products of powers of primes. Each symbol s of number theory is assigned a positive natural number #(s) in a fixed but arbitrary way, e.g.
#(0) = 1 #(=) = 5 #(¬) = 9 #(1) = 2 #( ( ) = 6 #(∀) = 10 #(+) = 3 #( ) ) = 7 #(vi) = 11 + i #(×) = 4 #(∧) = 8  
The natural number corresponding to a sequence w = < w0,…, wk > of symbols is
⌈w⌉ = 2#(w0) · 3#(w1) · … · pk#(wk),
where pk is the k+1st prime. It is called its Gödel number and denoted by ⌈w⌉. In this way we can assign Gödel numbers to formulas, sequences of formulas (once a method for distinguishing when one formula ends and another begins has been adopted), and most notably, proofs.
An essential point here is that when a formula is construed as a natural number, then the numeral corresponding to that natural number can occur as the argument of a formula, thus enabling the syntax to “refer” to itself, so to speak (i.e., when a numeral is substituted into a formula the Gödel number of which the numeral represents). This will eventually allow Gödel to formalize the Liar paradox (with “provability” in place of “truth”) by substituting into the formula which says, ‘the formula, whose code is x, is unprovable,’ its own natural number code (or more precisely the corresponding numeral).
Another concept required to carry out the formalization is the concept of numeralwise expressibility of number theoretic predicates. A number-theoretic formula φ(n1, …, nk) is numeralwise expressible in P if for each tuple of natural numbers (n1, …, nk):
N ⊨ φ(n1, …, nk) ⇒ P ⊢ φ(n1, …, nk) N ⊨ ¬φ(n1, …, nk) ⇒ P ⊢ ¬φ(n1, …, nk)
where n is the formal term which denotes the natural number n. (In P, this is S(S(…S(0)…), where n is the number of iterations of the successor function applied to the constant symbol 0.) One of the principal goals is to numeralwise express the predicate
Prf(x, y): ‘the sequence with Gödel number x is a proof of the sentence with Gödel number y.’
Reaching this goal involves defining forty-five relations, each defined in terms of the preceding ones. These relations are all primitive recursive.[10] Relations needed are, among others, those which assert of a natural number that it codes a sequence, or a formula, or an axiom, or that it is the code, denoted by Sb(ru1…unZ(x1)…Z(xn)), of a formula obtained from a formula with code r by substituting for its free variable ui the xi th numeral for i = 1, …, n. The forty-fifth primitive recursive relation defined is Prf(x, y), and the forty-sixth is
Prov(y): ‘the sentence with Gödel number y is provable in P’
which without being primitive recursive, is however obtained from Prf(x, y) by existentially quantifying x. (Prov(y) satisfies only the ‘positive’ part of numeralwise expressibility, and not the negative part; but the negative part is not needed.)
In Theorem V of his paper, Gödel proves that any number theoretic predicate which is primitive recursive is numeralwise expressible in P. Thus since Prf(x, y) and substitution are primitive recursive, these are decided by P when closed terms are substituted for the free variables x and y. This is the heart of the matter as we will see. Another key point about numeralwise expressibility is that although we informally interpret, for example, Prov(Sb(ru1…unZ(x1)…Z(xn))), by: ‘the formula with Gödel number r is provable if the Gödel number for the xi th numeral is substituted in place of the i th variable,’ neither the formal statement within the theory P nor anything we prove about it appeals to such meanings. On the contrary Prov(Sb(ru1…unZ(x1)…Z(xn))), is a meaningless string of logical and arithmetical symbols. As Gödel puts it in his introduction to his theorem V, ‘The fact that can be formulated vaguely by saying that every recursive relation is definable in the system P (if the usual meaning is given to the formulas of this system) is expressed in precise language, without reference to any interpretation of the formulas of P, by the following Theorem (V) (Gödel 1986, p. 171, italics Gödel’s).
Gödel in his incompleteness theorems uses a method given in what is called nowadays Gödel’s Fixed Point Theorem. Although Gödel constructs a fixed point in the course of proving the incompleteness theorem, he does not state the fixed point theorem explicitly. The fixed point theorem is as follows:
Theorem 2 (Gödel’s Fixed Point Theorem) If φ(v0) is a formula of number theory, then there is a sentence ψ such that P ⊢ ψ ↔ φ(⌈ψ⌉), where ⌈ψ⌉ is the formal term corresponding to the natural number code of ⌈ψ⌉.
Proof: Let σ(x,y,z) be a formula that numeralwise expresses the number theoretic predicate ‘y is the Gödel number of the formula obtained by replacing the variable v0 in the formula whose Gödel number is x by the term z’. Let θ(v0) be the formula ∃v1(φ(v1) ∧ σ(v0, v1, v0)). Let k = ⌈θ(v0)⌉ and ψ = θ(k). Now directly by the construction P ⊢ ψ ↔ φ(⌈ψ⌉).
A sentence is refutable from a theory if its negation is provable. The First Incompleteness Theorem as Gödel stated it is as follows:
Theorem 3 (Gödel’s First Incompleteness Theorem) If P is ω-consistent, then there is a sentence which is neither provable nor refutable from P.
Proof: By judicious coding of syntax referred to above, write a formula Prf(x,y)[11] of number theory, representable in P, so that
n codes a proof of φ ⇒ P ⊢ Prf(n, ⌈φ⌉).
and
n does not code a proof of φ ⇒ P ⊢ ¬Prf(n, ⌈φ⌉).
Let Prov(y) denote the formula ∃x Prf(x,y)[12]. By Theorem 2 there is a sentence φ with the property
P ⊢ (φ ↔ ¬Prov(⌈φ⌉)).
Thus φ says ‘I am not provable.’ We now observe, if P ⊢ φ, then by (1) there is n such that P ⊢ Prf(n, ⌈φ⌉), hence P ⊢ Prov(⌈φ⌉), hence, by (3) P ⊢ ¬φ, so P is inconsistent. Thus
P ⊬ φ
Furthermore, by (4) and (2), we have P ⊢ ¬Prf(n, ⌈φ⌉) for all natural numbers n. By ω-consistency P ⊬ ∃x Prf(x, ⌈φ⌉). Thus (3) gives P ⊬ ¬φ. We have shown that if P is ω-consistent, then φ is independent of P.
On concluding the proof of the first theorem, Gödel remarks, “we can readily see that the proof just given is constructive; that is … proved in an intuitionistically unobjectionable manner…” (Gödel 1986, p. 177). This is because, as he points out, all the existential statements are based on his theorem V (giving the numeralwise expressibility of primitive recursive relations), which is intuitionistically unobjectionable.


RESULT:

Gödel's First Incompleteness Theorem states that in any consistent formal system that is sufficiently expressive to include basic arithmetic, there are statements that cannot be proven or disproven within the system itself.

In other words, there are some truths that cannot be reached by the system's rules of logic. This is because, as Gödel discovered, the concept of arithmetic truth cannot be defined in arithmetic itself. If it were possible to define truth in the system itself, it would lead to paradoxes, such as the Liar paradox, showing the system to be inconsistent.

Gödel's proof of this theorem involves a technique known as Gödel numbering, which assigns natural numbers to terms and formulas of the formal system. This allows the syntax to "refer" to itself, enabling Gödel to formalize the Liar paradox by substituting into the formula which says, 'the formula, whose code is x, is unprovable,' its own natural number code.

The theorem concludes that if a formal system is ω-consistent (a stronger form of consistency), then there is a sentence which is neither provable nor refutable from the system. This means that there are always statements in the system that are true, but cannot be proven within the system.

自查询检索器在这里完全按预期工作，基于头部文本检索原始文档的最相关子章节——即 “2.2.1 第一不完备性定理” 和 “2.2.2 第一不完备性定理的证明”——作为上下文。

总结思考¶

在系统架构层面，有用的做法是（遵循最近的 CoALA 论文）将使用自查询的结构化分块视为一种改进语义记忆利用率的技术，可以将其调整为更具代理性的应用程序。尽管这里存在程序组件在起作用，例如硬编码在提示逻辑中的关于特定数据的知识，但该项目（以及，据我所知，更普遍的 RAG）的目标是以这样一种方式划分知识的外部来源，以便它们可以在语言生成过程中被重新捕获——或者，从某种意义上说，恢复到语言生成过程中。

“增强”不仅仅是一种文本详细说明的方式，也是一种保留上下文、建立来源和维护文本绑定信息片段的权威性的方式。实际上，当生成式 AI 被纳入教育工具和“批判性”知识系统（例如，用于医学和法律）时，此过程至关重要。

但是，除了倾向于突出长期存在的学术禁令“引用你的来源”之外，这些新的文本转换形式还对语言具有更深远的影响，为旧的后结构主义陈词滥调赋予了新的分量，正如德里达所说，“没有文本之外的东西”——对于持久的信念，即无论我们如何分块，自然语言都没有自然限制。

致谢

我与 Presidio Vantage 的 Benny Minkowsky (http://presidiovantage.com) 合作为 LangChain 创建了 HTML 头部文本分割器工具。如果您正在使用它构建，并且有一些反馈或想分享用例，我们很乐意听到您的意见！

非常感谢 LangChain 的 Bagatur Askaryan 在改进查询构造以及最近对自查询检索器 API 的升级方面提供的建议。

Chunk 的其他名称：结构化文本分割和元数据增强的 RAG

导入和环境设置¶

使用非结构化分块进行问答¶

使用结构化分块进行问答¶

使用结构化分块和自查询进行问答¶

更多示例¶

示例查询 #1：“解释胡塞尔的现象学还原。”¶

示例查询 #2：“什么是尼采的透视主义？”¶

示例查询 #3：“什么是德里达的解构？”¶

总结思考¶

致谢

标签

导入和环境设置¶

使用非结构化分块进行问答¶

使用结构化分块进行问答¶

使用结构化分块和自查询进行问答¶

更多示例¶

示例查询 #1：“解释胡塞尔的现象学还原。”¶

示例查询 #2：“什么是尼采的透视主义？”¶

示例查询 #3：“什么是德里达的解构？”¶

总结思考¶

致谢

标签

加入我们的新闻通讯