主要公开日志

所有GSXAB的知识库公开日志的联合展示。您可以通过选择日志类型、输入用户名（区分大小写）或相关页面（区分大小写）筛选日志条目。

2023年7月2日 (日) 13:15 Gsxab 留言贡献创建了页面切消定理（创建页面，内容为“分类:证明论 {{InfoBox |name=切消定理 |eng_name=cut theorem |aliases=切割消去定理,cut elimination theorem,Cut }} '''切消定理'''('''cut theory''')是重要的元定理，由演绎的定义即可得出，因此适用于绝大多数常见公理系统。 == 定理 == 对任意公式集 <math>\Gamma</math> 、 <math>\Delta</math> 和公式 <math>\phi_1,\dots,\phi_k, \psi</math> ，若有 <math>\Gamma, \phi_1, \dots, \phi_k \vdash \psi…”）
2023年7月2日 (日) 11:07 Gsxab 留言贡献创建了页面分离规则（创建页面，内容为“分类:证明论 {{InfoBox |name=分离规则 |eng_name=modus ponens |aliases=mp,mp rule,rule of detachment }} '''分离规则'''('''modus ponens''', '''rule of detachment''')指证明论中一个常见于各种推理系统的推理规则，即<math>\phi, \phi \rightarrow \psi \vdash \psi</math>。在希尔伯特系统中通常称为'''MP规则'''('''MP rule''')，在自然推理系统中对应蕴含消除（<…”）
2023年7月2日 (日) 06:41 Gsxab 留言贡献移动页面模板:逻辑演算至模板:证明论
2023年7月2日 (日) 06:19 Gsxab 留言贡献创建了页面希尔伯特表示（创建页面，内容为“分类:证明论分类:命题逻辑分类:命题逻辑命题逻辑及谓词逻辑的形式化公理系统中，有多种方案，差别基本在于推理规则与公理的权衡。 <ins>希尔伯特</ins>风格的公理系统尽可能追求使用更少的推理规则，因此引入更多公理。其中一个典型的系统被称为'''<ins>希尔伯特</ins>系统'''('''the Hilbert system''')/'''<ins>希尔伯…”）
2023年7月2日 (日) 04:38 Gsxab 留言贡献创建了页面模型（重定向页面至解释（谓词逻辑））标签：新重定向
2023年7月2日 (日) 04:37 Gsxab 留言贡献创建了页面塔斯基真理定义（创建页面，内容为“{{InfoBox |name=真理定义 |eng_name=definition of truth |aliases=真定义 }} {{InfoBox |name=基本语义定义 |eng_name=basic semantic definition |aliases=真定义 }} 真理定义指<ins>塔斯基</ins>对“真”本身的递归定义。在命题逻辑及谓词逻辑中，为避免自我指涉（即命题直接或间接地涉及自身的真假），以及解决真假无法对应客观对象的问题，认为真假不是对象语言中的对…”）
2023年7月1日 (六) 11:26 Gsxab 留言贡献创建了页面分类:证明论（创建页面，内容为“{{#default_form:}} 分类:数理逻辑”）
2023年7月1日 (六) 09:43 Gsxab 留言贡献创建了页面解释（命题逻辑）（创建页面，内容为“分类:命题逻辑 {{InfoBox |name=解释 |eng_name=interpretation }} 对一个命题公式 <math>A</math> ，其中有 <math>P_1, P_2, \dots, P_n</math> 共 <math>n</math> 个命题变元，按照每个命题变元为真假，一共有 <math>2^n</math> 种指派（命题逻辑），在每种指派下，命题变元的真值和命题公式的真值共同构成命题公式的一个'''解释'''('''interpretation''')。 {{命题逻辑}}”）
2023年7月1日 (六) 09:42 Gsxab 留言贡献创建了页面指派（命题逻辑）（创建页面，内容为“分类:命题逻辑 {{InfoBox |name=指派 |eng_name=assignment |aliases=赋值 }} 对一个命题公式 <math>A</math> ，其中有 <math>P_1, P_2, \dots, P_n</math> 共 <math>n</math> 个命题变元，按照每个命题变元为真假，一共有 <math>2^n</math> 种取值，其中的每种取值称为一个'''指派'''('''assignment''')； {{命题逻辑}}”）
2023年7月1日 (六) 09:08 Gsxab 留言贡献创建了页面满足（谓词逻辑）（创建页面，内容为“分类:谓词逻辑分类:模型论 {{InfoBox |name=满足 |eng_name=satisfy }} 一个赋值'''满足'''('''satisfies''')一个谓词公式，指赋值使得这个公式变成真命题。满足公式集中的每个公式时，也说满足这个公式集。一个模型上的任意赋值均满足公式或公式集时，也说一个模型满足这个公式或公式集。 == 定义 == 对公式 <math>\phi</math> 及…”）
2023年7月1日 (六) 09:05 Gsxab 留言贡献创建了页面满足（命题逻辑）（创建页面，内容为“分类:谓词逻辑分类:模型论 {{InfoBox |name=满足 |eng_name=satisfy }} 一个赋值'''满足'''('''satisfies''')一个谓词公式，指赋值使得这个公式变成真命题。满足公式集中的每个公式时，也说满足这个公式集。一个模型上的任意赋值均满足公式或公式集时，也说一个模型满足这个公式或公式集。 == 定义 == 对公式 <math>\phi</math> 及…”）
2023年7月1日 (六) 08:33 Gsxab 留言贡献创建了页面赋值（谓词逻辑）（创建页面，内容为“分类:证明论分类:模型论 {{InfoBox |name=赋值 |eng_name=assignment |aliases=指派 }} '''赋值'''/'''指派'''('''assignment''')是对谓词公式的非逻辑符号和个体变项取值。即指定论域，并使其中所有个体常项、函项、谓词替换为论域上的具体对象后，继续指定其中的个体变项的取值，或指定其中所有个体变项的取值。 == 定义 == ===…”）
2023年7月1日 (六) 07:17 Gsxab 留言贡献移动页面函项（谓词逻辑）至函项
2023年7月1日 (六) 06:45 Gsxab 留言贡献创建了页面谓词语言（创建页面，内容为“分类:命题逻辑 {{非标准称呼}} 命题语言('''propositional language''')指命题逻辑的形式语言，包括命题变元和逻辑联结词，也被称为 <math>\mathcal{L}_0</math>。命题语言是对命题逻辑进行的基于形式语言理论的建模，其中对应的句子或公式就是命题公式。 == 形式语言定义 == 定义形式语言 <math>\mathcal{L}_0</math> 的字母表和规则如下： === 字母表 ==…”）
2023年7月1日 (六) 06:40 Gsxab 留言贡献创建了页面命题语言（创建页面，内容为“分类:命题逻辑 {{非标准称呼}} 命题语言('''propositional language''')指命题逻辑的形式语言，包括命题变元和逻辑联结词，也被称为 <math>\mathcal{L}_0</math>。命题语言是对命题逻辑进行的形式语言理论的分析，对应的句子或公式就是命题公式。 == 形式语言定义 == 定义形式语言 <math>\mathcal{L}_0</math> 的字母表和规则如下： === 字母表 === <math>\mathca…”）
2023年6月30日 (五) 05:34 Gsxab 留言贡献创建了页面超集（重定向页面至包含关系）标签：新重定向
2023年6月30日 (五) 05:31 Gsxab 留言贡献创建了页面子集（重定向页面至包含关系）标签：新重定向
2023年6月29日 (四) 15:18 Gsxab 留言贡献创建了页面形式语言（创建页面，内容为“分类:形式语言理论 {{InfoBox |name=形式语言 |eng_name=formal language }} '''形式语言'''('''formal language''')指通过定义语法规则的方式来定义的语言。通常包括一个'''字母表'''，和一组'''规则'''，按这个规则可以将字母表中的'''字母'''结合成良定义的'''单词'''。在一些领域中，将这里的字母表称为'''词汇表'''，称按规则将词汇表中的'''单词'''结合成良定义的…”）
2023年6月28日 (三) 16:37 Gsxab 留言贡献创建了页面解释（谓词逻辑）（创建页面，内容为“分类:证明论分类:模型论 '''解释'''('''explanation''')是对谓词公式的非逻辑符号，即指定论域，并对其中所有个体常项、函项、谓词替换为论域上的具体对象的。 == 定义 == === 定义1 === 对谓词公式 <math>G</math> ，其'''解释'''('''explanation''') <math>\mathfrak{I}</math> ，包括： * <math>D</math> 是非空集合，即'''…”）
2023年6月28日 (三) 15:54 Gsxab 留言贡献创建了页面函项（谓词逻辑）（创建页面，内容为“分类:谓词逻辑 {{InfoBox |name=函项 |eng_name=function |aliases=函数 }} '''函项'''('''function''')指个体域上的函数。相应地， <math>n</math> 元函数对应称为 <math>n</math> 元函项。 {{谓词逻辑}}”）
2023年6月28日 (三) 15:52 Gsxab 留言贡献创建了页面个体词（谓词逻辑）（创建页面，内容为“{{InfoBox |name=个体词 |eng_name=individual }} {{InfoBox |name=个体域 |eng_name=individual field |aliases=individual domain,论域 }} '''个体词'''('''individual''')（'''个体'''）是指命题中，指称某个东西（被称为'''个体对象'''）的词。个体词包括'''常项'''和'''变项'''（'''变元'''、'''变号'''）两种。其中，常项，可以简单理解为指向某个个体对象的'''专名'''，而这个个体对象被…”）
2023年6月24日 (六) 05:40 Gsxab 留言贡献创建了页面原子公式（创建页面，内容为“分类:谓词逻辑 {{InfoBox |name=原子公式 |eng_name=atomic formula }} '''原子公式'''(atomic proposition)指不含逻辑联结词、量化表达式的谓词公式。对命题逻辑而言，由于不关注命题的内部构造，原子公式相当于原子命题。原子公式的定义基于项， * 若 <math>t_1, t_2</math> 都是项，由等词 <math>=</math> 连接的 <math>t_1 = t_2</math> 是原子公式； * 若 <math>t…”）
2023年6月24日 (六) 05:10 Gsxab 留言贡献创建了页面谓词公式（创建页面，内容为“分类:谓词公式 {{InfoBox |name=谓词公式 |eng_name=predicate formula |aliases=谓词合式公式,predicate well-formed formula,合式公式,well-formed formula,WFF,公式,formula }} '''谓词公式'''指由个体变项、个体常项、函项、谓词、量词及逻辑联结词构成的形式合理的表达式。 == 定义 == '''谓词合式公式'''('''predicate well-formed formula''')，简称'''合式公式'''('''well-formed formula'''，缩写…”）
2023年6月23日 (五) 13:43 Gsxab 留言贡献创建了页面唯一量词（创建页面，内容为“分类:谓词逻辑 {{InfoBox |name=唯一量词 |eng_name=uniqueness quantifier |aliases=存在唯一量词,uniqueness existential quantifier }} '''唯一量词'''('''uniqueness quantifier''')是量词的一种，包括相当于自然语言中的“有且仅有（唯一）一个……满足……”。 == 定义 == 命题中，表达“存在唯一一个不同的……使得……”的含义的量词，记作 <math>\exists!</math> 。比如，对 <…”）
2023年6月23日 (五) 13:32 Gsxab 留言贡献创建了页面计数量词（创建页面，内容为“分类:谓词逻辑 {{InfoBox |name=数量词 |eng_name=numerical quantifier |aliases=numeric quantifier,counting quantifier }} {{非标准称呼}} '''数量词'''('''numerical quantifier''')是量词的一种，包括相当于自然语言中的“有（恰好、至多、至少） <math>N</math> 个不同的……满足……”。 == 定义 == 命题中，表达“存在恰好 <math>N</math> 个不同的……使得……”的含义的量词，记作…”）
2023年6月23日 (五) 12:51 Gsxab 留言贡献创建了页面存在量词（创建页面，内容为“分类:谓词逻辑 {{InfoBox |name=存在量词 |eng_name=existential quantifier |aliases=特称量词 }} '''存在量词'''('''existential quantifier''')是量词的一种，相当于自然语言中的“有一个……满足……”、“存在……使得……”。 == 定义 == {{Identity |name=存在量词 |type=量词 |symbol=<math>\exists</math> |latex=\exists }} 命题中，表达“存在一个……使得……”的含义的量词，记…”）
2023年6月23日 (五) 12:39 Gsxab 留言贡献创建了页面全称量词（创建页面，内容为“分类:谓词逻辑 {{InfoBox |name=全称量词 |eng_name=universal quantifier }} '''全称量词'''('''universal quantifier''')是量词的一种，相当于自然语言中的“对所有的……”、“对任意的……”。 == 定义 == {{Identity |name=全称量词 |type=量词 |symbol=<math>\forall</math> |latex=\forall }} 命题中，表达“对所有的……都”的含义的量词，记作 <math>\forall</math> ，称为'''全称量词'''…”）
2023年6月23日 (五) 11:54 Gsxab 留言贡献创建了页面量词（创建页面，内容为“{{InfoBox |name=量词 |eng_name=quantifier }} '''量词'''('''quantifier''')指命题中约束个体的数量的词汇，包括全称量词<math>\forall</math>和存在量词<math>\exists</math>。量词总是紧接着一个个体变项，这部分被称为'''量化表达式'''。量化表达式和所限制的命题共同构成一个命题，这里被限制的命题称为这个量词的'''辖域'''。”）
2023年6月23日 (五) 09:17 Gsxab 留言贡献创建了页面谓词（创建页面，内容为“分类:谓词逻辑 {{InfoBox |name=谓词 |eng_name=predicate |aliases=命题函数 }} '''谓词'''('''predicate''')是指命题中描述某个东西（被称为'''个体对象'''）的性质或某几个东西的关系的部分。可以被形式化为关系。 <math>n</math> 元关系对应地称为 '''<math>n</math> 元谓词'''。 {{命题逻辑}}”）
2023年6月23日 (五) 09:04 Gsxab 留言贡献创建了页面项（谓词逻辑）（创建页面，内容为“分类:谓词逻辑 {{InfoBox |name=个体词 |eng_name=individual }} '''个体词'''('''individual''')（'''个体'''）是指指称某个东西（被称为'''个体对象'''）的词，包括'''常项'''和'''变项'''（'''变元'''、'''变号'''）两种。其中，常项，可以简单理解为指向某个个体对象的'''专名'''，而这个个体对象被称为这个专名的'''所指'''。变项，既不是直接指称某个实际所指的专名…”）
2023年6月22日 (四) 13:32 Gsxab 留言贡献创建了页面独立性（创建页面，内容为“分类:逻辑演算 {{InfoBox |name=独立性 |eng_name=independency }} '''独立性'''('''independency''')指一个公理系统中，有公式在这个公理和推演规则下是不可证明或的；或者这个公理系统中的公式互相有着这个性质。 == 定义 == 对给定公理系统，包括公理及推演规则，若对公式 <math>\phi</math> ，不存在一条从 <math>\Gamma</math> 到 <math>\ph…”）
2023年6月22日 (四) 12:52 Gsxab 留言贡献创建了页面一致性（创建页面，内容为“分类:逻辑演算 {{InfoBox |name=一致性 |eng_name=consistency }} '''一致性'''('''consistency''')指一个公理系统中，不会同时演绎出一对互为否定的定理。也指一些前提不同时重言蕴含一对互为否定的结论。通常的可演绎关系都会满足 IE 成立，因此也等价于：公理系统是一致的，当且仅当其所有定理的集合不是所有公式的集合…”）
2023年6月22日 (四) 12:38 Gsxab 留言贡献创建了页面完全性（创建页面，内容为“分类:逻辑演算 {{InfoBox |name=完全性 |eng_name=completeness }} '''完全性'''('''completeness''')指一个公理系统中，一个前提所重言蕴含的命题都是能从前提演绎出的。 {{逻辑演算}}”）
2023年6月22日 (四) 12:33 Gsxab 留言贡献创建了页面可靠性（创建页面，内容为“分类:逻辑演算 {{InfoBox |name=可靠性 |eng_name=soundness }} '''可靠性'''('''soundness''')指一个公理系统中，能从一个前提演绎出的结论都是前提所重言蕴含的。也就是说，这个系统中不会演绎出一些在前提成立时却不总成立的结论。 {{逻辑演算}}”）
2023年6月22日 (四) 12:19 Gsxab 留言贡献创建了页面保存重言性（创建页面，内容为“分类:逻辑演算 {{InfoBox |name=保存重言性 |eng_name=tautology-preserving |aliases=validity-preserving }} '''保存重言性'''('''truth-preserving''')指一个推理规则，应用于重言式时只能得到重言式。反过来说，如果应用于可假的公式，即使在某个赋值下是真命题时，在这个赋值下对应的结果不一定是真命题；但如果原公式在任意赋值下都是真命题，得到的结果也会在任…”）
2023年6月22日 (四) 12:15 Gsxab 留言贡献创建了页面保存真实性（创建页面，内容为“分类:逻辑演算 {{InfoBox |name=保存真实性 |eng_name=truth-preserving }} '''保存真实性'''('''truth-preserving''')指一个推理规则，应用于真命题时只能得到真命题。 {{逻辑演算}}”）
2023年6月18日 (日) 12:25 Gsxab 留言贡献创建了页面公理（逻辑）（创建页面，内容为“分类:逻辑演算 {{InfoBox |name=公理 |eng_name=axiom }} {{InfoBox |name=公理模式 |eng_name=axiom schema }} '''公理'''('''axiom''')指没有经过证明，被当作不证自明的命题。若规定符合某形式的公式都是公理，则称为'''公理模式'''('''axiom schema''')。公理在相关理论中其真实性理所当然，且是作为推导、演绎的起点。 == 定义 == 形式化系统（形式语言）中，变换有起始点…”）
2023年6月18日 (日) 10:34 Gsxab 留言贡献创建了页面自然演绎系统（创建页面，内容为“'''自然演绎系统'''是命题演算系统的一种，公理集合为空，对应地通过推理规则解释。变换中允许引入假言推理规则。 == 常见规则 == 通常包括以下10条规则，通常称'''引入-消去规则'''或 '''intelim 规则'''。”）
2023年6月18日 (日) 10:12 Gsxab 留言贡献创建了页面公理系统（逻辑）（创建页面，内容为“分类:逻辑演算 {{InfoBox |name=公理系统 |eng_name=axiomatic system }} '''公理系统'''('''axiomatic system''')是形式化公理系统的一种，通过几个公理模式和推理规则进行演算。”）
2023年6月18日 (日) 07:51 Gsxab 留言贡献创建了页面原子命题（创建页面，内容为“{{InfoBox |name=原子命题 |eng_name=atomic proposition }} '''原子命题'''(atomic proposition)指不含逻辑联结词的命题。原子命题当然也有其他内部构造，但不存在再进一步细分为命题和逻辑联结词的构造。”）
2023年6月18日 (日) 07:21 Admin 留言贡献删除页面集合论（内容为：“分类:朴素集合论 == 集合论 == '''集合论'''('''set theory''')是研究集合的数学理论，包含集合和元素、关系等最基本数学概念。现代集合论的研究是在1870年代由数学家<ins>康托</ins>（<ins>Cantor</ins>，全名 <ins>Georg Ferdinand Ludwig Philipp Cantor</ins>）的朴素集合论开始。集合论最初来自康托…”，唯一贡献者是“Gsxab”（讨论））
2023年6月18日 (日) 07:09 Gsxab 留言贡献创建了页面集合论（创建页面，内容为“分类:朴素集合论 == 集合论 == '''集合论'''('''set theory''')是研究集合的数学理论，包含集合和元素、关系等最基本数学概念。现代集合论的研究是在1870年代由数学家<ins>康托</ins>（<ins>Cantor</ins>，全名 <ins>Georg Ferdinand Ludwig Philipp Cantor</ins>）的朴素集合论开始。集合论最初来自康托对无穷集合的研究，无穷的分类对应集合间一一对应关系的存…”）
2023年6月10日 (六) 13:24 Gsxab 留言贡献创建了页面元定理（创建页面，内容为“{{InfoBox |name=元定理 |eng_name=metatheorem |aliases=metathesis }} 当我们研究形式化公理系统（形式语言）时，会使用如可证明性、可演绎性等描述，这些词汇并不属于形式语言本身，而是属于描述其用的语言（'''元语言'''），因此相关的定理称为'''元定理'''。”）
2023年6月10日 (六) 12:13 Gsxab 留言贡献创建了页面定理（重定向页面至证明）标签：新重定向
2023年6月10日 (六) 11:59 Admin 留言贡献删除页面证明、演绎（内容为：“#重定向演绎”，唯一贡献者是“Gsxab”（讨论））
2023年6月10日 (六) 11:58 Gsxab 留言贡献移动页面证明、演绎至演绎
2023年6月10日 (六) 11:53 Gsxab 留言贡献创建了页面证明（创建页面，内容为“{{InfoBox |name=证明 |eng_name=proof }} {{InfoBox |name=定理 |eng_name=theorem }} '''证明'''('''proof''')指某个推理系统的变形规则下，从空前提到某一结论的步骤。对应地，这个步骤的存在性被称为'''可证明'''('''provable''')。 '''定理'''('''theorem''')即该系统中任一可证明的公式。 == 定义 == 在指定形式化公理系统 <math>\mathbf{H}</math> 中，从空…”）
2023年6月10日 (六) 09:53 Gsxab 留言贡献创建了页面形式化公理系统（逻辑）（创建页面，内容为“{{InfoBox |name=公理系统 |eng_name=axiomatic system }} '''形式化公理系统'''('''formal axiomatic system''')或公理系统，通常指形式化的、公理化的系统，即含有一系列公理的形式语言。通常包含一个公理的集合和一个推演规则的集合。”）
2023年6月10日 (六) 09:40 Gsxab 留言贡献创建了页面模板:逻辑演算（创建页面，内容为“{| class='wikitable' style='text-align:center;margin:0 auto;border-width:2px' width='100%' |- ! colspan=2 style='border-bottom-width:2px' | 演算理论 |- ! 元语言 | 公理系统（形式化、公理化） |- ! 命题、定理 | 命题、定理、内定理、元定理、变形规则 |- ! 演绎 | 证明、可证明、演绎、可演绎 |}”）
2023年6月10日 (六) 09:26 Gsxab 留言贡献创建了页面证明、演绎（创建页面，内容为“{{InfoBox |name=证明 |eng_name=proof }} {{InfoBox |name=演绎 |eng_name=deduction }} '''演绎'''('''deduction''')指某个推理系统的变形规则下，从一些前提到某一结论的一系列步骤。 '''证明'''('''proof''')指从空前提到某一结论的步骤。对应地，这个步骤的存在性被称为'''可演绎'''('''deductible''')和'''可证明'''('''provable''')。 {{命题逻辑}}”）