[goaty]

hope you get your original idea working.   sounds really good,   if its simple, its probably a good sign that it works.  everything is.

[ivan.moony]

hope you get your original idea working.   sounds really good,   if its simple, its probably a good sign that it works.  everything is.

Thank you for the kind words. Luckily, the original idea is not changed. The issue is only about the implementation which will hopefully stay simple. I also plan to support a kind of expression complementation which will have positive properties towards detecting forms of input (more precisely, detecting if an input is not following provided constraints)

[goaty]

Thank you for the kind words. Luckily, the original idea is not changed. The issue is only about the implementation which will hopefully stay simple. I also plan to support a kind of expression complementation which will have positive properties towards detecting forms of input (more precisely, detecting if an input is not following provided constraints)

have u heard of assimilation & accommodation?    its pretty easy idea, so maybe u don't need to look it up,  but its the psychology of having to let go of false beliefs, and how you never feel like it.

[ivan.moony]

have u heard of assimilation & accommodation?    its pretty easy idea, so maybe u don't need to look it up,  but its the psychology of having to let go of false beliefs, and how you never feel like it.

?

[goaty]

Ok Ill explain->
Just like a human, a robot is trying to complete the similar task, yet in an artificial way.  So there is actually an intersecting set between ppl and robots,  and when conflicting information enters the system, what is wrong?  the new information or the old information?   When you have a gpt-2 system, it has no ability to tell wrong from right, its all equally right to it,  continually contradicts itself, and the same thing happens to ppl,  only by a lot of experience, and getting punished a few times,  its hard to know if your doing the wrong thing, or what you are currently acting on is false.   But an artificial system has a very hard time with it,   you can set up a Boolean algebra model for answering "how do I fix a computer" if you give it the relation to "use a hammer" it may be a little biased, but as far as the robots concerned its solving the puzzle appropriately.

Its ok if you see evil,  it definitely happens in the world,  but the robot has to know what others do, is different from what it does,   and then its ok to store such information,  but its not motivated to repeat it itself, then it becomes a goal based problem.

But that might not be the right way to go about it,  and this is one of the unsolved mysteries of a.i. to date.

[ivan.moony]

I think it is about relating experience with theory. Experience is absolute truth about environment, and should be referred when constructing theories. Theory is a relative notion, and often there is more than one way to correctly explain experience by theory. If we build up two competing theories that contradict each other, we have only experience to decide which theory is correct.

We don't have yet a grand unified theory about everything, and according to Gödel, we will never have it. Hence, it will always be juggling between fragments which work in this or that occasion. Because of that, it would be necessary to have a mechanism for switching between this or that theory according to environment which is the only truly solid point.

Theories are about predicting data in spatial-temporal space. There can't exist a theory that would always predict correct data, whatever environment looks like, but we can have domain specific theories which we choose to operate on isolated specific environments. We can detect if those domain specific theories are correct by comparing their results to environmental data.

[LOCKSUIT]

What makes yous so sure you can't 'know it all'. The whole AI field is about learning patterns. A pattern let's you understand/ solve multiple cases. Our little brain already understands the whole universe, sorta. Just imagine when the Earth becomes all brains at the nano level - it will have so much more data; cats eat, dogs eat, cats sleep, dogs sleep. Discovery. The universe is made up out of just a few laws, so patterns are everywhere.

Yes goaty we have best candidate answers, sometimes the top 20 can all be the same rank. We do usually have only 1 or 2 favorites. GPT-2 does too, but it's not that good yet, but its truer than past generators, that's, for sure. It is already a very slightly useful discover/researcher.

[ivan.moony]

What makes yous so sure you can't 'know it all'.

See Gödel's incompleteness theorems. There are two notions when constructing theories: completeness (to describe all that exists), and consistency (to be noncontradictory). What Gödel proved is that we can't have both in the same time. Thus, a complete theory has to be contradictory, and as such, can't be described by classical logic in a single logical system. Implika tries to be complete, while providing mechanisms to constrain only parts of the whole system to be consistent, although these parts may contradict each other (illogical as a whole). These consistent parts would be switched by implication like:

Code

(
    Case1 -> (... Theory1 ...)
) /\ (
    Case2 -> (... Theory2 ...)
) /\ ...

Now, if we want to analyze some `(... Environment1 ...)` by `Theory1`, we write:

Code

(Analytics -> (Case1 /\ (... Environment1 ...)))

If `Analytics` turns out to be contradictory, then we may conclude that `Theory1` does not hold for `(... Environment1 ...)`, and we can move on to check `Case2`. Moreover, these checks may be done iteratively in a recursive loop to report which theory actually does hold for some environment, but it is already a matter of programming, and I don't want to complicate this post that much.

[LOCKSUIT]

Ok but you agree 10 patterns can allow the AGI agent to answer 100 questions, right? Patterns work for unseen cases, each has 10 per pattern hence 100. It still allows a smartness-explosion that is prepared for huge encounters of space lol.

If you happen to get any big question that involves a lot of possibilities, you can narrow down the search space.

[ivan.moony]

These are currently not working definitions of logical operators that I have to make to work with Implika:

Code

(@A -> @B)  (@A @B)
(@A /\ @B)  ((@A -> (@B -> @C)) -> @C)
(@A \/ @B)  ((@A -> @C) -> ((@B -> @C) -> @C))
(~ @A)      (@A -> @C)
(! @X . @F) (@X -> @F)
(? @X . @F) ((@X -> (@F -> @C)) -> @C)

First, the logical implication is being defined. Then everything else is being defined from that implication and complement `@c`, including universal quantificator `!` and existential quantificator `?`. I think I'll have to implant the complementation behavior in a form of one of DeMorgan's and double complementation laws:

(A /\ B)^c = (A^c \/ B^c)
(A^c)^c = A

There is a story behind complementation in implika. A fresh variable that is not defined before stands for *any* possible expression. Since Implika is made to be complete (see Gödel's incompleteness theorems), it has to be inconsistent, so *any* expression also includes a falsehood, thus evaluates to a false, providing a case for complementation detection. So, to state `x -> @c`, is the same as stating `x -> false`, which is actually a definition of `not` operator in implicational logic. This behavior aligns with the principle of explosion that says: from falsehood anything follows.

There is also something interesting in the above definitions: if we take a look at `/\` (and), `\/` (or), and `~` (not) operators, we may interpret `@c` as complementation. But, we may also consider `@c` as a placeholder for any other expression, and then the definitions become theorems preserving ground properties of `\/`, `/\`, and `~` operators.

I could probably get away without low-level complementation support, but these properties seem so natural, so I decided to grapple with this dragon.

[goaty]

I think it is about relating experience with theory. Experience is absolute truth about environment, and should be referred when constructing theories. Theory is a relative notion, and often there is more than one way to correctly explain experience by theory. If we build up two competing theories that contradict each other, we have only experience to decide which theory is correct.

We don't have yet a grand unified theory about everything, and according to Gödel, we will never have it. Hence, it will always be juggling between fragments which work in this or that occasion. Because of that, it would be necessary to have a mechanism for switching between this or that theory according to environment which is the only truly solid point.

Theories are about predicting data in spatial-temporal space. There can't exist a theory that would always predict correct data, whatever environment looks like, but we can have domain specific theories which we choose to operate on isolated specific environments. We can detect if those domain specific theories are correct by comparing their results to environmental data.

I see...  so the model isn't the environment,   in all my studies I actually make the model THE environment,  but that isn't worth basing behaviour on!  thanks for that one Ivan.    But it definitely is easier to just make the model the environment,  but to develop the robots behaviour - you have to copy whats in it,  so its not the true solution to a.i..

[ivan.moony]

I've been trying to detect if a formula is not a consequence of some assumptions (i.e. if `A -> B` is not the case). This particular question represented an issue to me, as long as I wanted to separate the some-kind-of-solid logic language definition from dirty programming tricks.

I think there is a thing about semantics in classical logic in which it is possible to detect a contradiction or a tautology, while it is a problem to detect merely satisfiable formulas. I think what I really needed was a way to detect if the negation of `A -> B` that translates to `(A /\ ¬B)` is satisfiable, and the detection problem arose.

In classical logic, I think to derive `failure` from `(A /\ ¬B) -> failure` requires to explicitly state or derive both `A` and `¬B`. But if B does not follow from `A`, then `¬B` is not automatically concluded, thus `failure` doesn't get propagated.

So I decided to bend rules a bit, to match the last remark. I planned to make a system where if `B` does not follow from `A`, then `~B` is automatically concluded from `A` (or at least treated like so, not to bloat an output). In fact, in this system, if `X` is not a part of formula set, then `~X` automatically is. In this system, to prove that `B` doesn't follow from `A`, it would be enough to derive `~(A -> B)`. This completely changes raw logic semantics and it is not classical logic anymore.

However, classical not operation can still coexist in a form of `(¬X) = (X -> false)` statement, but now the negation `¬` is completely different operator than complementation `~`. The important thing is they should be able to both exist in the same system.

Last time I checked Martin Löf's type theory (a long time ago), it had an interesting property: sets are being inhabitated with proofs of their existence, while sets not being inhabitated at all are considered being false. This would somewhat correspond to a little system of mine, so finally, all of this might not be a completely new thing after all.

And then I found that the subject bugging me is already worked out: autoepistemic logic, negation as a failure, and stable model semantics. Those are based on evidence, or a lack of evidence of some formula being true or false.

Of course, me wouldn't be me if I wasn't reinvent the hot water all by myself first. Why do I always have to do it the hard way?

[MikeB]

I don't know how you could ever get an A = B inference engine working...

"Does a ball bounce?" is the same as saying "do all balls always bounce anywhere everywhere anytime".

You could never link the data...

You'd need deep relationship.. "given this and this and this and this and this.. does this do this?". Then looking up if all those things are true... If the question is asked too simply it's their fault...

[ivan.moony]

I don't know how you could ever get an A = B inference engine working...

That's why we have variables. If we mention the same variable twice, like in expression `(@a = @a) -> equal`, the right part of implication would be deduced only if we say `5 = 5`, or `a = a`, but not `2 = 3`. The same variable at various places are expected to be substituted for the same expression.

[Zero]

Hi
I'd like to check whether I understand correctly. In the following example:

Code

(
    ((man @x) (mortal @x)) (
        (man Socrates) ()
    )
)

We first set a context ((man @x) (mortal @x)). That's our "rule". Then, our "current state of the world" is (man Socrates).
The dummy () is actually the place where we can finally use the conclusion we obtained (that Socrates is mortal), am I right?

How would I express a world where Plato is a man too? If I understand correctly, I would create a nested structure with (man Plato) and (man Socrates)? How would it look like?