主要公开日志

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

2023年7月29日 (六) 10:28 Gsxab 留言贡献创建了页面Γ （创建页面，内容为“分类:希腊字母 Γ、γ是希腊字母的第一个字母。在英语中的名称为 gamma {{IPA|[ˈɡæ.mə]}}。汉字规范音译为伽马。古希腊语中名称为 {{Grc|γάμμα}} {{IPA|[alpʰa]}}，{{Latn|gámma}}，现代希腊语中名称为{{Grc|γάμμα}} {{IPA|[ˈɣa.ma]}}，{{Latn|gámm}}。 == 来源 == 希腊字母Γ来自腓尼基字母 {{Phnx|𐤂}}（gimel）。 == 读音 == 古希腊中代表浊硬腭塞音 {{IPA|[ɡ]}}…”）
2023年7月29日 (六) 10:20 Gsxab 留言贡献创建了页面Β （创建页面，内容为“分类:希腊字母 Β、β是希腊字母表的第二个字母。在英语中的名称为 beta {{IPA|[ˈbiː.tə]}}，美{{IPA|[ˈbeɪ̯.tə]}}}。汉字规范音译为贝塔。古希腊语中名称为 {{Grc|βῆτα}} {{IPA|[bɛːta]}}，{{Latn|bē̂ta}}，现代希腊语中名称为{{Grc|βήτα}} {{IPA|[ˈvi.ta]}}，{{Latn|víta}}。 == 来源 == 希腊字母Β来自腓尼基字母 {{Phnx|𐤁}}（beth）。 == 读音 == 古希腊中代表…”）
2023年7月29日 (六) 10:09 Gsxab 留言贡献创建了页面Α （创建页面，内容为“分类:希腊字母 Α、α是希腊字母的第一个字母。在英语中的名称为 alpha {{IPA|[ˈæɫ.fə]}}。汉字规范音译为阿尔法。古希腊语中名称为 {{Grc|ἄλφα}}，{{Latn|álpha}}，现代希腊语中名称为{{Grc|άλφα}}，{{Latn|álfa}}。 == 来源 == 希腊字母Α来自腓尼基字母 {{Phnx|𐤀}}（aleph）。 == 读音 == 古希腊中代表长短音 {{IPA|[a]}} 和 {{IPA|[aː]}}，有时通过附加符号…”）
2023年7月29日 (六) 07:36 Gsxab 留言贡献创建了页面单点集（重定向页面至单元素集）标签：新重定向
2023年7月28日 (五) 17:52 Gsxab 留言贡献创建了页面模板:GreekAlphabet （创建页面，内容为“ {| class='wikitable' style='text-align:center;margin:0 auto;border-width:2px' width='100%' |- ! colspan=27 style='border-bottom-width:2px' | 希腊字母 |- | Αα（Alpha） | Ββ（Beta） | Γγ（Gamma） | Δδ（Delta） | Εε（Epsilon） | Ζζ（Zeta） |- | Ηη（Eta） | Θθ（Theta） | Ιι（Iota） | Κκ（Kappa） | Λλ（Lambda） | Μμ（Mu） |- |…”）
2023年7月25日 (二) 18:12 Gsxab 留言贡献创建了页面模板:Latn （创建页面，内容为“{{{1}}}”）
2023年7月24日 (一) 17:43 Gsxab 留言贡献创建了页面模板:Grc （创建页面，内容为“{{{0}}}”）
2023年7月24日 (一) 17:37 Gsxab 留言贡献创建了页面模板:Phnx （创建页面，内容为“{{{0}}}”）
2023年7月23日 (日) 19:01 Gsxab 留言贡献创建了页面希腊字母（创建页面，内容为“ '''希腊字母'''('''Greek alphabet''')，指希腊使用的字母体系。是第一种全音素文字，也是使用时间最长的拼音文字。在大约公元前13世纪之前，希腊还在使用线形文字乙（Linear B）。在大约公元前13世纪，线形文字乙消失，希腊从青铜时代文化崩溃开始，进入黑暗时代，期间本土没有文字留存。到公元前9世纪，希腊出现了借用腓尼基字母的文字。腓…”）
2023年7月23日 (日) 10:44 Gsxab 留言贡献创建了页面Skolem范式（创建页面，内容为“分类:谓词逻辑 {{InfoBox |name=Skolem范式 |eng_name=Skolem normal form }} '''<ins>Skolem</ins>范式'''('''Skolem normal form''')指在前束范式基础上，将存在量词消除为个体常项或全称约束变元的函项，只留下全称量词的形式。与原公式有相同可满足性，但未必等值。 == 定义 == 对前束范式 <math>\mathsf{Q}_1 x_1 \dots \mathsf{Q}_n x_n \phi</math> ，对…”）
2023年7月22日 (六) 23:27 Gsxab 留言贡献创建了页面前束范式（创建页面，内容为“分类:谓词逻辑 {{InfoBox |name=前束范式 |eng_name=prenex normal form |aliases=PNF }} '''前束范式'''('''prenex normal form''', '''PNF''')指谓词公式的一种形式，将全部量化表达式都放在最前面，且这些量词均非否定无取值范围、辖域都覆盖到公式尾部。 == 定义 == 对谓词公式，若其具有形式 <math>\mathsf{Q}x_1 \dots \mathsf{Q}x_n \phi</math> ，其中 <math>\phi</math> 不含…”）
2023年7月16日 (日) 08:40 Gsxab 留言贡献创建了页面分类:谓词逻辑（创建页面，内容为“{{#default_form:}} 分类:数理逻辑”）
2023年7月15日 (六) 09:08 Gsxab 留言贡献创建了页面结构（逻辑）（重定向页面至解释（谓词逻辑））标签：新重定向
2023年7月15日 (六) 08:43 Gsxab 留言贡献创建了页面模型（逻辑）（重定向页面至解释（谓词逻辑））标签：新重定向
2023年7月15日 (六) 08:39 Gsxab 留言贡献创建了页面理论（逻辑）（创建页面，内容为“分类:证明论分类:模型论 {{InfoBox |name=理论 |eng_name=theory |aliases=形式理论,formal theory }} 指形式化公理系统中，从一组公理出发，按照给定推理规则，能演绎出的全体定理的集合。特点是对可演绎关系封闭。 {{证明论}} {{模型论}}”）
2023年7月14日 (五) 05:02 Gsxab 留言贡献创建了页面同构（模型）（创建页面，内容为“{{InfoBox |name=模型同构 |eng_name=isomorphism of models }} 模型的同构指两个模型有相同的构造。 == 定义 == 对模型 <math>\mathfrak{A}=\langle A,I \rangle,\mathfrak{B}=\langle B,J \rangle</math> ，若存在双射 <math>f: A\to B</math> 使得： * 对任意个体常项 <math>c</math> ， <math>f(c^{\mathfrak{A}}) = c^{\mathfrak{B}}</math> * 对任意 <math>n</math> 元谓词 <math>P</math> ，及 <math>a_1, \dots, a_n \in A</math>…”）
2023年7月9日 (日) 16:22 Gsxab 留言贡献创建了页面易字变形（创建页面，内容为“分类:谓词逻辑 {{InfoBox |name=易字变形 |eng_name= }} '''易字变形'''指一个谓词公式，其中的部分量化公式被替换成其易字式。 == 定义 == === 简单易字变形 === 对谓词公式 <math>\phi</math> 和 <math>\phi'</math> ，若存在公式 <math>\psi</math> 、原子公式 <math>p</math> 、互为易字式的两个量化公式 <math>\psi,\psi'</math> ，使得 <math>\phi=\chi(\psi/p),\phi'=\chi'(\psi…”）
2023年7月9日 (日) 12:52 Gsxab 留言贡献创建了页面易字式（创建页面，内容为“分类:谓词逻辑 {{InfoBox |name=易字式 |eng_name= }} 量化公式中，将被量化的个体变元及其辖域中的所有出现，同一更换一个变元名称，通常不改变语义，称为其'''易字式'''，操作称为'''易字变形'''。 == 定义 == 对公式 <math>\forall x\phi</math> 和 <math>\exists x\phi</math> ，个体变元 <math>y</math> 不在其中自由出现，且对 <math>x</math>…”）
2023年7月9日 (日) 12:50 Gsxab 留言贡献创建了页面易字（创建页面，内容为“分类:谓词逻辑 {{InfoBox |name=易字 |eng_name= }} 量化公式中，将被量化的个体变元及辖域中的所有出现，同一更换一个变元名称，通常不改变语义，称为其'''易字式'''，操作称为'''易字变形'''。 == 定义 == 对公式 <math>\forall x\phi</math> 和 <math>\exists x\phi</math> ，个体变元 <math>y</math> 不在其中自由出现，且对 <math>x</math> 在 <math>\phi</math> 中可自由代…”）
2023年7月9日 (日) 08:25 Gsxab 留言贡献创建了页面等项替换（创建页面，内容为“分类:等项替换 {{InfoBox |name=等项替换 |eng_name= }} '''等项替换'''指在任何谓词公式中，如果两个项相等，就能互相替换。这里项的相等指两个项在给定条件下的任意赋值下都相等，而且替换要求它们之间可自由代入。 == 定义 == 对公式 <math>\phi</math> 若 <math>s_1 \dots s_n</math> 和 <math>t_1 \dots t_n</math>…”）
2023年7月9日 (日) 07:00 Gsxab 留言贡献创建了页面真值指派（重定向页面至指派（命题逻辑））标签：新重定向
2023年7月9日 (日) 06:55 Gsxab 留言贡献创建了页面命题变元代入（创建页面，内容为“分类:命题逻辑 {{InfoBox |name=代入 |eng_name=subtitution }} 对命题变元的'''代入'''('''subtitution''')指在一个命题公式中，将某个命题变元的全体出现，全部用另一个公式来替换的操作。 == 定义 == === 代入 === 从全体命题变元所构成的集合到全体公式所构成的集合的映射，称为一个'''代入'''('''substitution''')。对于把 <math>p_1, \dots, p_n</math> 分别替…”）
2023年7月8日 (六) 22:44 Gsxab 留言贡献创建了页面可自由代入（个体变项）（创建页面，内容为“分类:谓词逻辑 {{InfoBox |name=可自由代入 |eng_name= }} 一个个体变项的'''可自由代入'''指，对一个谓词公式，将其中某个个体变项的全部出现替换为另一个项时，不会影响其语义的代入。实际上，影响语义的情况主要是指，新的项或其中某个个体变项，在代入后会落在某个作用在这一变项的量词的辖域内…”）
2023年7月8日 (六) 22:31 Gsxab 留言贡献创建了页面个体变项代入（创建页面，内容为“分类:谓词逻辑 {{InfoBox |name=代入 |eng_name=subtitution }} 对个体变项的'''代入'''('''subtitution''')指在一个项或一个谓词公式中，某个个体变项的全体出现，全部用另一个项来替换的操作。 == 定义 == === 代入 === 从全体个体项所构成的集合到全体项所构成的集合的映射，称为一个'''代入'''('''substitution''')。对…”）
2023年7月8日 (六) 16:12 Gsxab 留言贡献创建了页面逻辑蕴含（创建页面，内容为“分类:命题逻辑 {{InfoBox |name=逻辑蕴含 |eng_name=logical implication }} '''逻辑蕴含'''('''logical implication''')指两个谓词公式之间，在所有可能的指派下，若一个为真则另一个必为真的关系。或者说若第一个被满足则第二个被满足的关系。 == 定义 == {{Relation |name=重言蕴含 |symbol=<math>\Rightarrow</math>,<math>\vDash</math> |latex=\Rightarrow,\vDash |ope…”）
2023年7月8日 (六) 15:53 Gsxab 留言贡献创建了页面合同引理（创建页面，内容为“分类:证明论 {{InfoBox |name=合同引理 |eng_name= }} '''合同引理'''指项在赋值下的值、谓词公式在赋值下的真值，都仅依赖于赋值对其中出现的符号的解释。 == 定理 == 对模型 <math>\mathfrak{A} = \left\langle A, I \right\rangle, \mathfrak{A}' = \left\langle A', I'\right\rangle</math> ，有任意两个分别在两个模型上的赋值 <math>\sigma,\tau</math> ： # 若对项…”）
2023年7月8日 (六) 15:26 Gsxab 留言贡献移动页面希尔伯特表示至希尔伯特系统
2023年7月2日 (日) 13:47 Gsxab 留言贡献创建了页面演绎定理（创建页面，内容为“分类:证明论 {{InfoBox |name=演绎定理 |eng_name=deduction theory }} '''演绎定理'''是重要的元定理，由演绎的定义和mp规则即可得出，因此适用于绝大多数常见推理系统。 == 定理 == 对公式集 <math>\Gamma</math> 和公式 <math>\phi,\psi</math> ，有： <math>\Gamma, \phi \vdash \psi</math> 当且仅当 <math>\Gamma \vdash \phi\rightarrow\psi</math> 。 {{证明论}}”）
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…”）