TE
TechEcho
Home24h TopNewestBestAskShowJobs
GitHubTwitter
Home

TechEcho

A tech news platform built with Next.js, providing global tech news and discussions.

GitHubTwitter

Home

HomeNewestBestAskShowJobs

Resources

HackerNews APIOriginal HackerNewsNext.js

© 2025 TechEcho. All rights reserved.

Strong Types for Direct Logic

2 pointsby carlehewittalmost 7 years ago

1 comment

DonbunEf7almost 7 years ago
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.