logic - 我如何在精益中证明这一点？ p ∨ ¬p-6ren

logic - 我如何在精益中证明这一点？ p ∨ ¬p

转载作者：行者123 更新时间：2023-12-04 07:42:44

24

4

我有一个定理要在精益上证明，

theorem T (h : ¬ A) : ¬ (A ∨ B) ∨ (¬ A ∧ B)

为了证明，我想，我需要使用，

or.elim (B ∨ ¬B) (assume b: B, ...) (assume nb:¬B, ...)

为此，我必须再次证明

B v ¬B

那么，我该如何处理呢？有没有更好的方法？

最佳答案

p v ¬p是来自核心库的引理，名为 classical.em .

关于logic - 我如何在精益中证明这一点？ p ∨ ¬p，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/67370506/

24

4

0

文章推荐： python - kdeplot seaborn 中的自定义阴影调色板

文章推荐： Python pandas 计算分组后的份额

文章推荐： LISP 列表项的总和

文章推荐： python - 创建 AWS S3 存储桶时，无区域是什么意思？

c - while(*p){p++;}、while (*++p){;} 和 while(*p++){;} 有什么区别？
关于strcat函数。 while (*p) p++; 和 while (*++p) ; 两者都有效，但是 while (*p++) ; 不起作用。我认为 first 和 th
What is "
" in HTML?(HTML中的““是什么
？)
下面例子中的第一行代码是什么。我看到一个YouTuber在写下面的代码，它显示了一个设计在csswar Challenges中。我也尝试了一下，它很管用。但我以前从未在任何HTML教程上看到过它，我在
html - 处理不间断空格 :

vs.

是不间断空格，表示没有换行的空白处。如果我用我在两个段落之间有一个空格(更大的间隔)。如果我使用我在两个段落之间只有一个新行(没有中断)。为什么？最佳答案在 HTML 中
字符* p = "hello"; printf ("%c %c %c %c", *p, *++p, *p++, *p);
这个问题已经有答案了: Why are these constructs using pre and post-increment undefined behavior? (14 个回答) 已关闭 9
c - "for ( ; *p;++p) *p = tolower(*p);"在 c 中如何工作？
我对编程还很陌生，只是想知道为什么这段代码: for ( ; *p; ++p) *p = tolower(*p); 当 p 指向一个字符串时，可以降低 c 中字符串的大小写吗？最佳答案一般来说，这
c - 为什么对于指针 *p，p[0] 是存储在 p 的地址而 p[1] 是 p 本身的地址？
代码 int n = 25; int *p = &n; printf("%x\n %d\n %x\n", p, p[0], p[1]); 返回: \ 当然我永远不会这样做，但在 K&R 中声明
python - 考虑到 p 在 python 中是素数，当我执行 p/p+1 + p+1/p 操作时出错
所以，我想创建一个简单的程序，返回有关连续素数的计算结果。首先，我创建一个包含所有这些素数的列表，然后尝试计算结果，但这给了我一个超出范围的索引。有人可以帮助我吗？我的程序: primes = []
c++ - C/C++ 中 p[i] 、 i[p] 和 *(p+i) 、 *(i+p) 的区别
这个问题在这里已经有了答案: With arrays, why is it the case that a[5] == 5[a]? (20 个答案) 关闭 9 年前。我想知道 C/C++ 中以下四
C++ - *p vs &p vs p
我仍在努力理解 *p、&p 和 p 之间的区别。根据我的理解，* 可以被认为是“指向的值”，而 & 可以被认为是“地址”。换句话说，* 保存值，而 & 保存地址。如果这是真的，那么 *p 和 p 之间
java - 需要更换
你是吗？ [xxxrecipientFirstNamexxx]
和
你是吗？ {recipientFirstName}

需要更换你是吗？ [xxxrecipientFirstNamexxx] 和你是吗？ {recipientFirstName} 。我尝试使用边界匹配器。但结果并不符合预期。我尝试使用下面的代码 "A
c# - query = query.OrderBy(p => p.IsTop).ThenOrderByDescending(p => p.JobId)?
我想按 IsTop 属性升序排序对象，然后按 JobId 属性降序排序: query = query.OrderBy(p => p.IsTop).ThenOrderByDescending(p =
java - Apache POI 数据格式化程序无法应用自定义格式 "0.0 p.p.;(0.0 p.p.)"
在我尝试使用 Apache POI 进行转换的 Excel 文件中，我有一个单元格的数值为 -3.97819466831428，自定义格式为“0.0 p.p.;(0.0 p.p.)”。因此，在 Exc
c# - 如何创建一个扩展方法，允许我调用 ToSerializableDictionary(p => p.ID) 而不是 .ToDictionary(p => p.ID)
我想创建一个扩展方法，允许我调用 ToSerializableDictionary(p => p.ID)而不是 .ToDictionary(p => p.ID)在以下 LINQ 上下文中。虽然我不确定
javascript - $ ("p").each(function (){}) vs for( p in $ ("p") 返回不同的段落数值
在下面的 HTML 代码上运行此 jQuery 代码会返回不同的结果，我认为它们应该返回相同的值。 jQuery 代码: var counter = 0; $("p").each(function()
c++ - 我在哪里可以找到标准中对 *p 和 p[0]、*(p+1) 和 p[1]、... 之间等价关系的引用？
在下面的代码片段中，符号 *p 等同于 p[0]，*(p + 1) 等同于p[1]，依此类推。 int* p = new int[3] { 1, 2, 3}; cout << *p << ' ' <<
c++ - Foo *p = 0;p->p() 如何有效？
这个问题在这里已经有了答案: What will happen when I call a member function on a NULL object pointer? [duplicate]
c - "p = p + (*p)++ * 3 + c;"会导致未定义的行为吗？
这个问题在这里已经有了答案: 关闭 10 年前。 Possible Duplicate: Undefined Behavior and Sequence Points 按照标准中的定义，E1 +=
What is "
" in HTML?(在HTML中“
”是什么？)
以下示例中的第一行代码是什么。我看到一个youtube用户写下面的代码，它显示在cssbattle挑战的设计。我也试过，它的作品。但我从来没有见过它在任何HTML教程之前，我在谷歌上搜索它，但它只显示
php - < o : p > & nbsp ; display error
每当我收到来自 MS outlook 的电子邮件时，我都会收到此标记 & nbsp ; (没有空格)哪个显示为？在 <>. 当我将其更改为 ISO-8859-1 时，浏览器页面字符集编码为 UTF-8
python - 获取标签之间的字符串(
p1
TEST
p2
中的 TEST)
代码: from bs4 import BeautifulSoup soup = BeautifulSoup('p1TESTp2') print soup.div() 结果: [p1, p2] 为什么

首页

博学

6Ren·AI

商城

logic - 我如何在精益中证明这一点？ p ∨ ¬p