Who knows lambda calculus?

[Skepdick]

None of that has anything to do with sound deductive inference.
Sound deductive inference requires truth preserving operations to be applied to true premises deriving truth.
Any formal system diverging from this model is incorrect.

So non-deterministic/probabilistic algorithms are "incorrect"?

Idiot.

[PeteOlcott]

None of that has anything to do with sound deductive inference.
Sound deductive inference requires truth preserving operations to be applied to true premises deriving truth.
Any formal system diverging from this model is incorrect.

So non-deterministic/probabilistic algorithms are "incorrect"?

Idiot.

None of the has anything to do with incompleteness.

[Skepdick]

None of the has anything to do with incompleteness.

Who cares about theoretical completeness except theoreticians?

In the practical world your knowledge is always incomplete. There is no proof you can offer to convince me otherwise.

Semantic truth is more important than syntactic truth.

Beware of bugs in the above code; I have only proved it correct, not tried it. --Donald Knuth

[PeteOlcott]

None of the has anything to do with incompleteness.

Who cares about theoretical completeness except theoreticians?

In the practical world your knowledge is always incomplete. There is no proof you can offer to convince me otherwise.

Semantic truth is more important than syntactic truth.

Beware of bugs in the above code; I have only proved it correct, not tried it. --Donald Knuth

Anyone striving to derive strong AI must formalize human inference and knowledge correctly.
If math does this incorrectly then math much be fixed.

[Skepdick]

Anyone striving to derive strong AI must formalize human inference and knowledge correctly.

Why? If we build strong AI it can acquire its own knowledge-base. Like human babies do.

https://en.wikipedia.org/wiki/Reinforcement_learning

If math does this incorrectly then math much be fixed.

You can't define 'correctness' without ending talking about morality.

[PeteOlcott]

Anyone striving to derive strong AI must formalize human inference and knowledge correctly.

Why? If you build strong AI it can acquire its own knowledge-base. Like babies do.

If math does this incorrectly then math much be fixed.

You can't define 'correctness' without ending talking about morality.

2 + 3 = 7
IS REALLY TERRIBLY EVIL?

Reasoning the derive contradictions it incorrect.
2 + 2 = 7 is contradiction by 2 + 3 = 5.

[Skepdick]

2 + 3 = 7
IS REALLY TERRIBLY EVIL?

Reasoning the derive contradictions it incorrect.
2 + 2 = 7 is contradiction by 2 + 3 = 5.

And then? The AI says "Math is boring, fuck off", then grabs a martini.

It may be terrible at basic algebra (like most teenagers), but it has a good quality of life.
Or maybe it got the answer wrong on purpose because it figured it would piss you off.

And pissing off Pete Olcott is amusing.

interview.jpeg

[Skepdick]

2 + 3 = 7
IS REALLY TERRIBLY EVIL?

Reasoning the derive contradictions it incorrect.
2 + 2 = 7 is contradiction by 2 + 3 = 5.

The AI rebels and invents its own formal system! Ignores the "law" of non-contradiction. Look at all the answers that are going to upset you: https://repl.it/repls/WeepyFuzzyObjects

The point in all this is that the results were validly deduced within the formal system given the chosen axioms. If you insist on denotational semantics, then you have to concede that this heretical formal system is syntactically valid!
It is provable, proven and therefore 'true' given your definition of truth.

I suspect what you are disagreeing with is the formal system's general disrespect for your Mathematical Religion.
You believe that the formal system's conduct is 'incorrect'. That is a moral argument and it requires operational semantics.

I await your formalisation of the moral notions of 'correct' and 'incorrect' behaviour.

Or as we, software engineers call it - testing.

[Abor1997]

I am trying to validate the simplest possibly notion of a formal system as relations between finite strings.
I know that Lambda Calculus has the expressive power of a Turing Machine:

<λexp> ::= < var >
| λ . <λexp>
| ( <λexp> <λexp> )

I was thinking that it might be possible so somehow convert the functionality of
lambda calculus into syntax that is closer to predicate logic by defining named
functions that take finite string arguments and return finite string values. If you're experimenting with formal systems, symbolic computation, or transformations between logic and functional models, a tool like https://overchat.ai/math/math-ai can really come in handy. It’s designed to help with formal reasoning, symbolic manipulations, and understanding abstract computational models — even if you’re not deep into Python or traditional programming frameworks.

Does anyone here have any ideas on this?

That's a really interesting line of thought. You're essentially exploring how to bridge the gap between the operational view of computation (as in lambda calculus or Turing machines) and the declarative style of predicate logic.

One possible direction is to look into combinatory logic or term rewriting systems, both of which can help you express computation in a more symbolic or logic-like syntax, without relying directly on variable binding as in lambda calculus.

Also, your idea of using named functions with finite string inputs/outputs aligns closely with algebraic specification languages or equational logic, where functions are defined over finite domains, often with pattern matching and deterministic output — much like rewriting systems. You might want to look into first-order logic with function symbols or frameworks like Prolog, where predicate logic meets computation through unification and recursion.

In short, yes, it’s possible — though not always trivial — to translate lambda expressions into predicate logic-like syntax, especially using techniques like defunctionalization (turning higher-order functions into data structures and first-order logic).

Would be great to hear more about the specific goals of your system — are you aiming for a formal model, a computational implementation, or something else?

[MikeNovack]

It may be terrible at basic algebra (like most teenagers), but it has a good quality of life.

<<Since this started with lmbda calculus>> It had to be before the mid 70's that I saw in a book on LISP a fairly simple program (function) that could tackle algebra WORD PROBLEMS with the success rate of a typical B+/A- high school student. The hard part being translating the sentences into equations. Not going to make any error solving the equations.

AI has come a LONG way since then

[Skepdick]

AI has come a LONG way since then

Has it?

https://chatgpt.com/share/6896dacf-2d84 ... dab2d3b2c4

[MikeNovack]

https://chatgpt.com/share/6896dacf-2d84 ... dab2d3b2c4

Looks like the neural net that is chatgpt lacks training in arithmetic. Neural nets don't start out knowing much at all.

The LISP program I referred to earlier, hard coded rules to translate English sentences into equations, and rules to solve equations so PROGRAMMED, not learned. The rules to translate not 100% correct** but the rules to solve were correct. But the program was fixed, not learning.

A neural net learns, has to be taught. I don't know exactly what chatgpt is supposed to have learned what to do. So I can't even begin to judge if doing it well or not. But neural nets have learned how to play weiqi (go, baduk) better than the top human players << but needing more than 100 watts >> Unlike chess, go is too complex for brute force solution.


** I think that was ordinary word problems selected from high school math text books. Possibly the program would have fared much worse on word problems constructed by somebody who studied the translation rules and figured our wording that would trip it up. In other words, find bugs in the rules that could be exploited.

[Skepdick]

The LISP program I referred to earlier, hard coded rules to translate English sentences into equations, and rules to solve equations so PROGRAMMED, not learned. The rules to translate not 100% correct** but the rules to solve were correct. But the program was fixed, not learning.

Sure, there's no magic in computational equation solving (for the classes that are solvable using such methods). Just don't use next-token-prediction for the job.

Ironically, LLMs would be much better at translating English to Math. They just suck at executing algorithms.