"Meta-logic" 和 "object-logic"（作为单词）在 Isabelle 中的定义
"Meta-logic" and "object-logic" (as word) definition in Isabelle
Isabelle 中 "meta-logic" 和 "object-logic" 这两个词的正式完整定义是什么？我看到人们一直在使用这些，但找不到它们的任何定义。
你找不到它们是因为它们是 Isabelle 特有的（据我所知）。 "Object-logic" 和 "meta-logic" 是 Larry Paulson 引入的术语（据我所知）。一般来说，虽然不是特别明确，但它们与逻辑和集合论等学科的一般术语 "metalanguage" 和 "object language" 相关。对这些进行搜索，您将获得标准的 wiki 页面，因为它们是逻辑的标准部分。
这里，我正在查看第 16 页，2.2.3 元和对象语言 of Logic and Computation - Interactive Proof with Cambridge LCF，Larry Paulson 于 1987 年出版。当时他仍然遵守标准条款，但后来他改变了。我忘了我在哪里读到的，但他在某处切换到 "meta-logic" 和 "object-logic"，以出于他自己的目的澄清事情。这两个术语在他的论文和 Isabelle 分发文档中。
其他人可以给你他们的专业知识，但元逻辑具体是你在导入理论时得到的Pure，特别是一组最小的逻辑连接词，==>， \<And>、&&& 和 ==。对这些的讨论遍布整个 Isabelle 分发文档。
我对直觉逻辑知之甚少，除了它不提供排中律，但你会读到它们提供了一个最小的直觉逻辑。
不用谢我。我只是在这里和那里读了一些东西，然后听了。其他人可以提供专业知识。
我对这个问题的调查结果如下。
我在 Clemens Ballarin slides, slide 20. 中找到：
Meta logic: The logic used to formalize another logic.
Example: Mathematics used to formalize derivations in formal logic.
并与以下内容并列：
Meta language: The language used to talk about another language.
Examples: German in a Spanish class, English in an English class.
维基百科在 Metalogic 上有一个条目，其中一个部分是元语言 - 对象语言：
In metalogic, formal languages are sometimes called object languages.
The language used to make statements about an object language is
called a metalanguage. This distinction is a key difference between
logic and metalogic. While logic deals with proofs in a formal system,
expressed in some formal language, metalogic deals with proofs about a
formal system which are expressed in a metalanguage about some object
language.
这是来自 Ballarin 的第 21 张幻灯片：
Isabelle 中 "meta-logic" 和 "object-logic" 这两个词的正式完整定义是什么？我看到人们一直在使用这些，但找不到它们的任何定义。
你找不到它们是因为它们是 Isabelle 特有的（据我所知）。 "Object-logic" 和 "meta-logic" 是 Larry Paulson 引入的术语（据我所知）。一般来说，虽然不是特别明确，但它们与逻辑和集合论等学科的一般术语 "metalanguage" 和 "object language" 相关。对这些进行搜索，您将获得标准的 wiki 页面，因为它们是逻辑的标准部分。
这里，我正在查看第 16 页，2.2.3 元和对象语言 of Logic and Computation - Interactive Proof with Cambridge LCF，Larry Paulson 于 1987 年出版。当时他仍然遵守标准条款，但后来他改变了。我忘了我在哪里读到的，但他在某处切换到 "meta-logic" 和 "object-logic"，以出于他自己的目的澄清事情。这两个术语在他的论文和 Isabelle 分发文档中。
其他人可以给你他们的专业知识，但元逻辑具体是你在导入理论时得到的Pure，特别是一组最小的逻辑连接词，==>， \<And>、&&& 和 ==。对这些的讨论遍布整个 Isabelle 分发文档。
我对直觉逻辑知之甚少，除了它不提供排中律，但你会读到它们提供了一个最小的直觉逻辑。
不用谢我。我只是在这里和那里读了一些东西，然后听了。其他人可以提供专业知识。
我对这个问题的调查结果如下。
我在 Clemens Ballarin slides, slide 20. 中找到：
Meta logic: The logic used to formalize another logic.
Example: Mathematics used to formalize derivations in formal logic.
并与以下内容并列：
Meta language: The language used to talk about another language.
Examples: German in a Spanish class, English in an English class.
维基百科在 Metalogic 上有一个条目，其中一个部分是元语言 - 对象语言：
In metalogic, formal languages are sometimes called object languages. The language used to make statements about an object language is called a metalanguage. This distinction is a key difference between logic and metalogic. While logic deals with proofs in a formal system, expressed in some formal language, metalogic deals with proofs about a formal system which are expressed in a metalanguage about some object language.
这是来自 Ballarin 的第 21 张幻灯片：