TE
科技回声
首页24小时热榜最新最佳问答展示工作
GitHubTwitter
首页

科技回声

基于 Next.js 构建的科技新闻平台,提供全球科技新闻和讨论内容。

GitHubTwitter

首页

首页最新最佳问答展示工作

资源链接

HackerNews API原版 HackerNewsNext.js

© 2025 科技回声. 版权所有。

Strong Types for Direct Logic

2 点作者 carlehewitt将近 7 年前

1 comment

DonbunEf7将近 7 年前
Hi Carl, it&#x27;s me, mathematics. I&#x27;m sure you recall that Turing machines (TMs) can be enumerated. ActorScript programs can also be enumerated, as can Direct Logic statements. I&#x27;m sure that you also have no problem with the basic concept of arithmetic encoding, nor with diagonalization widgets.<p>So, I&#x27;d like you to demonstrate that Direct Logic is, in fact, strictly more powerful than TMs, by constructing a DL program which cannot be computed by any TM.<p>Alternatively, I&#x27;d like you to prove the claim, &quot;In Direct Logic, categorical theories of the Natural Numbers, Real Numbers, Ordinal Numbers, Set Theory, the Lambda Calculus, and Actors are inferentially decidable, meaning that every true proposition is provable and every proposition is either provable or disprovable,&quot; from your abstract. Specifically, I&#x27;d like you to construct the Direct Logic program which proves or disproves any given theorem. If that is too difficult, it will suffice to demonstrate a use of Direct Logic to answer a tough question about numbers; I humbly invite you to consider Goldbach&#x27;s conjecture.<p>Thanks and good luck.