Readit News logoReadit News
practal commented on Logical implication is a comparison operator   btdmaster.bearblog.dev/lo... · Posted by u/btdmaster
AbstractPlay · a month ago
> I am very clear that this is a conversation with a Claude impersonation of Graham Priest, not Graham Priest himself.

Only after you make the upfront claim, in bold letters, in words you chose: "A Conversation with Graham Priest About Abstraction Logic". You did not choose to title your blog post "A Conversation About Abstraction Logic With Claude Representing Graham Priest" which is the more honest title for your blog post, except that it's clear that Claude was not capable of representing Priest since "the real Graham Priest says that it doesn't really sound like his voice." You chose to title your blog post "A Conversation with Graham Priest About Abstraction Logic". Obviously this line gives the impression that you had an actual conversation with the actual Graham Priest. You must have recognized that the wording you chose is false and deceptive. Are you hoping that attaching Priest's name gives your work more gravitas or encourages more sales of your book?

> I don't see what is unethical about that.

You see nothing unethical about prompting an LLM to take on someone's persona and then presenting the resulting conversation in a blog post with a title which gives the initial impression that you had an actual conversation with the actual person?

Be clear about where you stand on this at least so that any university or elsewhere that might have any interest in offering a job for you to continue your work in abstraction logic might know where you stand on misrepresenting professional academics.

> Who is "we"?

The general public to which you are presenting your work and advertising your book.

> I don't even know who you are, AbstractPlay.

I'm a member of the general public to which you are presenting your work and advertising your book.

> The article exists because I personally find it interesting, and I actually learnt something through it. If somebody else finds it interesting, great. If you don't, too bad.

Okay, but you're presenting this pseudo-conversation on the website through which you are presenting your work and advertising your book to the general public. Presenting it there gives the impression that this pseudo-conversation is meant to support your work, not that it's some tangential, self-satisfying curiosity appropriate for a personal blog.

It would be far more interesting if you posted actual conversations you actually have with actual academics actually commenting on your work instead of this fantasy world of LLM regurgitation that you expect us to believe is ultimately intended to only be interesting and enlightening to you.

practal · a month ago
Wow. I am glad your problems are not my problems.
practal commented on Logical implication is a comparison operator   btdmaster.bearblog.dev/lo... · Posted by u/btdmaster
AbstractPlay · a month ago
On your website, you seem to claim in bold letters that you've talked to Graham Priest about your work:

> A Conversation with Graham Priest About Abstraction Logic

but admit afterward that you talked to Claude prompted to sound like Graham Priest:

> A conversation about abstraction logic with Claude representing Graham Priest.

You also wrote an update stating:

> Update: The real Graham Priest says that it doesn't really sound like his voice. So enjoy with caution .

Don't you find it unethical to claim that you had "a conversation with Graham Priest about Abstraction Logic"? You didn't have a conversation with Priest. You had an interaction with Claude in Priest clothing. It doesn't even sound like Priest agrees with what you prompted Claude to say. Do you think it's permissible to let LLMs speak on behalf of people without their consent? Do you think that what an LLM says when prompted to speak as though it were some person should be accepted as what the person would actually say and believe?

Why should we find it interesting what any LLM has to say about your work, regardless of whose voice you dress it up as?

practal · a month ago
All the information you need to know about that article is right at the top of it [1]. I am very clear that this is a conversation with a Claude impersonation of Graham Priest, not Graham Priest himself.

I don't see what is unethical about that.

> Why should we find it interesting what any LLM has to say about your work, regardless of whose voice you dress it up as?

Who is "we"? I don't even know who you are, AbstractPlay. The article exists because I personally find it interesting, and I actually learnt something through it. If somebody else finds it interesting, great. If you don't, too bad. Thanks for letting me know either way.

[1] https://practal.com/press/cwgpaal/1

practal commented on Logical implication is a comparison operator   btdmaster.bearblog.dev/lo... · Posted by u/btdmaster
fjfaase · a month ago
So, in Visual Basic one can use '>=' for imply.
practal · a month ago
Good one! (Q)Basic was my first language. Well, my second really, after .bat files.
practal commented on Logical implication is a comparison operator   btdmaster.bearblog.dev/lo... · Posted by u/btdmaster
practal · a month ago
In Terence Tao's book "Compactness and Contradiction", at the very start on page 1, he introduces material implication "If A Then B" (or "A implies B") as "B is at least as true as A", and then lists the various easy conclusions one can draw from this.

Very interesting, I think, that "A implies B" is the same as "A ≼ B", is apparently mathematical main stream, and not just popular in formal logic.

If you continue along these lines, you also not just need to ask, what is implication, but what are A and B? Well, they are things you can compare for their truth content, so let's call them truth values. Surely, "≼" should form a partial order, and if you want arbitrary conjunction and disjunction to exist, truth values with "≼" should form a complete lattice T. This means that "∧" and "∨" are now operations T×T → T. If you want implication ALSO to be such an operation "⇒", instead of just the comparison relation "≼", you can use the following condition (somebody already mentioned it in another comment here, via Galois connections), which just means that "A and B imply C" is the same as "A implies that (B implies C)", interpreting implication simultaneously as "⇒" and "≼":

    A ∧ B ≼ C iff A ≼ B ⇒ C   
That allows you to define B ⇒ C as the supremum of all A such that A ∧ B ≼ C, in every complete lattice. If the join-infinite distributive law [1] holds, above condition will hold with this definition, and you get a complete Heyting algebra this way.

This is exactly how I turn abstraction algebra into abstraction logic [2].

[1] https://proofwiki.org/wiki/Axiom:Infinite_Join_Distributive_...

[2] http://abstractionlogic.com

practal commented on Andrej Karpathy: Software in the era of AI [video]   youtube.com/watch?v=LCEmi... · Posted by u/sandslash
discreteevent · 2 months ago
indistinguishable from magic != magic
practal · 2 months ago
Exactly. Clearly LLMs are not magic, so why do people insist that using LLMs is the same as believing in magic?
practal commented on Andrej Karpathy: Software in the era of AI [video]   youtube.com/watch?v=LCEmi... · Posted by u/sandslash
lelanthran · 2 months ago
> Use informal English on the surface, while some of it is interpreted as a formal expression, put to work, and then reflected back in English? I think that is possible, if you have a formal language and logic that is flexible enough, and close enough to informal English.

That sounds like a paradox.

Formal verification can prove that constraints are held. English cannot. mapping between them necessarily requires disambiguation. How would you construct such a disambiguation algorithm which must, by its nature, be deterministic?

practal · 2 months ago
Going from informal to formal can be done using autoformalization [1]. The real question is, how do you judge that the result is correct?

[1] Autoformalization with Large Language Models — https://papers.nips.cc/paper_files/paper/2022/hash/d0c6bc641...

practal commented on Andrej Karpathy: Software in the era of AI [video]   youtube.com/watch?v=LCEmi... · Posted by u/sandslash
andrepd · 2 months ago
Not gonna lie, after skimming the website and a couple preprints for 10 minutes my crank detector is off the charts. Your very vague comments adds to it.

But maybe I just don't understand.

practal · 2 months ago
Yes, you just don't understand :-)

I am working on making it simpler to understand, and particularly, simpler to use.

PS: People keep browsing the older papers although they are really outdated. I've updated http://abstractionlogic.com to point to the newest information instead.

practal commented on Andrej Karpathy: Software in the era of AI [video]   youtube.com/watch?v=LCEmi... · Posted by u/sandslash
gylterud · 2 months ago
Why? Why would the language used to express proof of correctness have anything to do with English?

English was not developed to facilitate exact and formal reasoning. In natural language ambiguity is a feature, in formal languages it is unwanted. Just look at maths. The reasons for all the symbols is not only brevity but also precision. (I dont think the symbolism of mathematics is something to strive for though, we can use sensible names in our languages, but the structure will need to be formal and specialised to the domain.)

I think there could be meaningful work done to render the statements of the results automatically into (a restricted subset of) English for ease of human verification that the results proven are actually the results one wanted. I know there has been work in this direction. This might be viable. But I think the actual language of expressing results and proofs would have to be specialised for precision. And there I think type theory has the upper hand.

practal · 2 months ago
My answer is already in my previous comment: if you have two formal languages to choose from, you want the one closer to natural language, because it will be easier to see if informal and formal statements match. Once you are in formal land, you can do transformations to other formal systems as you like, as these can be machine-verified. Does that make sense?
practal commented on MCP Specification – version 2025-06-18 changes   modelcontextprotocol.io/s... · Posted by u/owebmaster
practal · 2 months ago
Does any popular MCP host support sampling by now?

u/practal

KarmaCake day251July 23, 2020
About
Researcher and freelancer. Developing Practal (https://practal.com).

GitHub: https://github.com/phlegmaticprogrammer email: obua@practal.com

View Original