Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]


Groups > sci.logic > #342033

Not all logicians are primarily interested in "computation" (Re: The illusion of set theories [Computational Logic Primate])

From Mild Shock <janburse@fastmail.fm>
Newsgroups sci.logic, sci.math, sci.lang
Subject Not all logicians are primarily interested in "computation" (Re: The illusion of set theories [Computational Logic Primate])
Date 2025-11-16 16:32 +0100
Message-ID <10fcqr2$49vt$1@solani.org> (permalink)
References (1 earlier) <10f7064$jag$2@solani.org> <10f7170$ju4$2@solani.org> <10fc8oq$3u06$2@solani.org> <10fcb5e$3vm2$1@solani.org> <10fcerr$5ogb$1@solani.org>

Cross-posted to 3 groups.

Show all headers | View raw


Hi,

While mathematics is possibly not subject to "deflationism":

"According to deflationists, such suggestions are
mistaken, and, moreover, they all share a common mistake.
The common mistake is to assume that truth has a nature
of the kind that philosophers might find out about and
develop theories of."
https://plato.stanford.edu/entries/truth-deflationary/

Its the other way around for "computation", since it is more real?

For example Roberts Kowalski AI booklet is a master class
in snake oil selling, only looking at the "Logic" in
"Computational Logic", communicating a certain fascination
in logic representation, including chain of thoughts and
complex dynamic situations. Largely ignoring serious

discussion of Algorithm = Logic + Control. So maybe besides
a chapter " The grass is wet ", adding a chapter " If
we were God " would have helped in putting "Computation" back
into the picture. After all solving a connection graph is
only a small part of reasoning. Its only the Matrix in

Herbrand's original method, but there is also another more
creative step related to quantifiers in Herbrand's original
method. See also Jens Ottens implementation of leanCoP.

Bye

See also here:

The Pocket Reasoner– Automatic Reasoning on Small Devices
https://www.ntnu.no/ojs/index.php/nikt/article/download/5368/4844/20629

Mild Shock schrieb:
> Hi,
> 
> Set theory was initially praised as a foundation
> for mathematics. But the reduction of mathematics
> to foundation, was also carried out in type theories.
> And we see that this reduction is rather arbitrary,
> 
> we now have dozen of competing set theories and
> type theories. Whats more stunning, the reduction
> allows us to view Model Theory in a Proof Theory
> fashion, possibly implying that Model Theory doesn't
> 
> exist or is not needed? But this is a dangerous
> conclusion, since the foundation might be a theoretical
> technical thing, far away from practical use.
> Take naive comprehension, was it wrong?
> 
> ∃x∀y(y e x <=> phi(y))
> 
> It was fixed after Russell/Frege by ?von Neumann?:
> 
> ∀z∃x∀y(y e x <=> y e z & phi(y))
> 
> But in reverse mathematics we find another refinement:
> 
> ∃x∀y(y e x <=> phi(y))   for phi a certain class
> 
> So instead introducing a set like upper bound z,
> where we would only look at the projection of
> comprehension to z, we take the naive intuition more
> seriously, born from informal usage, and say,
> 
> naive comprehension was not really wrong!
> 
> Bye
> 
> P.S.: It would be interesting to see whether
> Operational Set theory as presented today, has
> a developed Model Theoretic language? Or does it
> also subscribe to the Computational Logic Primate?
> 
> 5.3 Relativizing operational set theory
> It is shown in [45] that a direct relativization
> of operational reflection leads to theories that are
> significantly stronger than theories formalizing the
> admissible analogues of classical large cardinal axioms.
> This refutes the conjecture 14(1) on p. 977 of Feferman [19].
> https://home.inf.unibe.ch/ltg/publications/2018/jae18.pdf
> 
> Is relativizing the backdoor of a model theory,
> that might also be useful for OST? OST is used like
> Lego bricks here. Adding this or that, one gets different
> set theories (or maybe type theories).
> 
> Operational set theory and small large cardinals
> Solomon Feferman - 2006
> Conjecture 14.
>   (1) OST + (Inacc) ≡ KPi.
>   (2) OST + (Mahlo) ≡ KPM.
>   (3) OST + (Reg2) ≡ KPω +( 3 −Reflection).
> https://math.stanford.edu/~feferman/papers/OST-Final.pdf
> 
> One gets the impression of OST being a sub-foundation toy.
> 
> Mild Shock schrieb:
>> Hi,
>>
>> Something tells me the Prolog community has a
>> sever blind spot, in their Logic education.
>> Possibly never touch a book like this here,
>>
>> even not with tweezers:
>>
>> Undergraduate Texts in Mathematics - 1983
>> H .- D. Ebbinghaus et. al - Mathematical Logic
>> http://www.fuchs-braun.com/media/ca80d9e55f6d3bfaffff8005fffffff0.pdf
>>
>> The front cover features a smiling face,
>> illustrating Ehrenfeucht Fraisse (EF) games.
>> There is a compelling relationship between
>>
>> EF and Fuzzy Testing. Just take A and B, a formal
>> form of a spec and of some code. This is quite
>> different from Lorentz Games, where the initial
>>
>> set-up is different. But here if Anna plays
>> Player II in G(M1,M2) and Bert plays Player II
>> in G(M2,M1). Then if Anna has a winning strategy,
>>
>> then Bert has a winning strategy. Sounds like
>> Bisimulation again. One of the biggest struggels
>> for Boris the Loris and Nazi Retart Julio of
>>
>> all time. Or this complete blunder, navigating
>> in the dark, trying to identify an elephant:
>>
>> @kuniaki.mukai
>> https://swi-prolog.discourse.group/t/cyclic-terms-unification-x-f-f-x-x-y-f-y-f-y-x-y/9097/72 
>>
>>
>> Bye
>>
>> P.S.: Mostlikely the cardinal sin of the Prolog
>> Community is that they don't apply Proof Theoretic
>> methods and Model Theoretic methods on equal
>>
>> footing. They don't understand how the two
>> methods are related, even on the most basic
>> level, such as counter models, which is a level
>>
>> more basic than EF games. One of the future
>> challenges for the community could be extending
>> proof theoretic methods and model theoretic
>>
>> methods to (seemingly) higher order logic. This
>> could be quite messy, or not? I am currengly
>> fascinated by Feferman Operative Sets and
>>
>> like Melvin Fittings work in higher order logic.
>>
>> Mild Shock schrieb:
>>> Hi,
>>>
>>> How it started, some useless GOFAI framing and
>>> production systems lore:
>>>
>>> Computational Logic and Human Thinking:
>>> How to Be Artificially Intelligent
>>> https://www.cambridge.org/core/books/computational-logic-and-human-thinking/C2AFB0483D922944067DBC76FFFEB295 
>>>
>>>
>>> How its going, please note CodeMender from Google:
>>>
>>> New Google Riftrunner AI (Gemini 3) Shocks Everyone
>>> https://www.youtube.com/watch?v=F_YWQ12qQ8M
>>>
>>> Especially note the section about CodeMender(*), and AI
>>> built on Gemini, which does inspect and suggest changes
>>> to OpenSource projects.
>>>
>>> So whats the rule of predicting the future in AI. Well
>>> just take skeptics, like Boris the Loris (**) (nah we don't
>>> use Fuzzy Testing here, CodeMender uses this among other
>>>
>>> methods), Linus Torwald (nah, AI for OpenSource is still
>>> far away, CodeMender is here) etc.. Negate what they are
>>> saying and you get a perfect prediction for 2025 / 2026.
>>>
>>> LoL
>>>
>>> Bye
>>>
>>> (*) Already *old* anouncement from October 6, 2025:
>>>
>>> Introducing CodeMender: an AI agent for code security
>>> https://deepmind.google/blog/introducing-codemender-an-ai-agent-for-code-security/ 
>>>
>>>
>>> (**) Ok, when you don't find Boris the Loris on
>>> SWI-Prolog discourse, you might find him here:
>>>
>>> Hello. My name is Boris and this is my family. We're
>>> lorises and we are primates - a bit like small
>>> monkeys. We tend to move quite slowly which is
>>> why we are Slow Lorises. We have big eyes so we
>>> can see well in the dark to catch insects for our dinner.
>>>
>>> My name... is Boris
>>> https://x.com/mrborisloris
>>>
>>> Mild Shock schrieb:
>>>> Hi,
>>>>
>>>> Descartes’ “divide problems into parts” works
>>>> only for well-behaved, linear, decomposable systems.
>>>> But its just that parts might end up as Schrödingers
>>>>
>>>> equation. It could be that stable diffusion is the
>>>> new constraint solver. In a sense, stable diffusion
>>>> models (or other generative AI) are functioning as
>>>>
>>>> probabilistic, fuzzy constraint solvers — but in a
>>>> very different paradigm from classical logic or
>>>> formal methods. But what was neglected?
>>>>
>>>> - Cybernetics (1940s–50s)
>>>> Focused on feedback loops, control, and self-regulation
>>>> in machines and biological systems. Showed that
>>>> decomposition can fail because subparts are interdependent.
>>>>
>>>> - Chaos Theory (1960s–80s)
>>>> Nonlinear deterministic systems can produce unpredictable,
>>>> sensitive dependence on initial conditions. Decomposition
>>>> into parts is tricky: small errors explode, and “solving
>>>> subparts” may not help predict the whole.
>>>>
>>>> - Santa Fe Institute & Complex Systems (1980s–present)
>>>> Studied emergent behavior, networks, adaptation,
>>>> self-organization. Linear, reductionist thinking fails
>>>> to capture dynamics of economic, social, and ecological systems.
>>>>
>>>> Bye
>>>>
>>>> Mild Shock schrieb:
>>>>> Hi,
>>>>>
>>>>> How it started:
>>>>>
>>>>> https://conceptbase.sourceforge.net/
>>>>>
>>>>> How its going:
>>>>>
>>>>> https://www.ibm.com/products/datastax
>>>>>
>>>>> The problem with claims such as " Formal languages,
>>>>> such as KAOS, are based on predicate logic and
>>>>> capture additional details about an application
>>>>> in a precise manner. They also provide a foundation
>>>>> for reasoning with information models." is that
>>>>> every thing in the quoted sentence is wrong.
>>>>>
>>>>> Real AI systems scale by approximation,
>>>>> vectorization, distributed representations,
>>>>> and partial knowledge — not by globally
>>>>> consistent logical models. No classical requirements
>>>>> language or ontology captures the informal
>>>>> cognitive machinery that makes
>>>>> intelligence flexible. Intelligence needs the
>>>>> whole messy cognitive spectrum.
>>>>>
>>>>> Somehow DataStax looks like n8n married AI embedding.
>>>>> I hope Amazon, Meta, Google, etc.. get the message.
>>>>> I don't worry about Microsoft, they might come with
>>>>>
>>>>> something from their Encarta corner and Copilot+ is
>>>>> more Local AI. After all we need things like Wikidata
>>>>> in a Robot and not in a Data Center.
>>>>>
>>>>> LoL
>>>>>
>>>>> Bye
>>>>
>>>
>>
> 

Back to sci.logic | Previous | NextPrevious in thread | Next in thread | Find similar | Unroll thread


Thread

Rene Descartes "Discours de la méthode" has fizzled out Mild Shock <janburse@fastmail.fm> - 2025-11-14 11:27 +0100
  Philosophical Twist due to negligence (Re: Rene Descartes "Discours de la méthode" has fizzled out) Mild Shock <janburse@fastmail.fm> - 2025-11-14 11:44 +0100
    Re: Philosophical Twist due to negligence (Re: Rene Descartes "Discours de la méthode" has fizzled out) Ross Finlayson <ross.a.finlayson@gmail.com> - 2025-11-14 11:10 -0800
      NY is the next Detroit in 2035 (Was: Philosophical Twist due to negligence) Mild Shock <janburse@fastmail.fm> - 2025-11-14 23:12 +0100
        Its a little sad story with NY (Was: NY is the next Detroit in 2035) Mild Shock <janburse@fastmail.fm> - 2025-11-14 23:25 +0100
          Re: Its a little sad story with NY (Was: NY is the next Detroit in 2035) Mild Shock <janburse@fastmail.fm> - 2025-11-14 23:45 +0100
    How to not be Artificial Intelligent [Boris the Loris deeply shocked] (Re: Philosophical Twist due to negligence) Mild Shock <janburse@fastmail.fm> - 2025-11-16 11:24 +0100
      Abstraction refinement (CEGAR) etc.. [Community Blind Spot] (Was: How to not be Artificial Intelligent) Mild Shock <janburse@fastmail.fm> - 2025-11-16 12:05 +0100
        The illusion of set theories [Computational Logic Primate] (Was: Abstraction refinement (CEGAR) etc.. [Community Blind Spot]) Mild Shock <janburse@fastmail.fm> - 2025-11-16 13:08 +0100
          Not all logicians are primarily interested in "computation" (Re: The illusion of set theories [Computational Logic Primate]) Mild Shock <janburse@fastmail.fm> - 2025-11-16 16:32 +0100
  AnythingLLM QNN/ONNX: Massiv Computations versus John Sowa (Re: Rene Descartes "Discours de la méthode" has fizzled out) Mild Shock <janburse@fastmail.fm> - 2025-11-25 20:07 +0100
    Benchmark results DirectML versus QNN [Challenge for Geekbench AI] (Re: AnythingLLM QNN/ONNX: Massiv Computations versus John Sowa) Mild Shock <janburse@fastmail.fm> - 2025-11-25 20:17 +0100

csiph-web