Logical Systems

This is a rehash of some ideas from my older blog. Basically, I'm trying to state the problem anew, in light of reading Jon Cogburn's paper Are Turing Machines Platonists? (Unfortunately not available online, but do email him if you want a copy, he is a nice fellow.)

Inferentialism is, roughly speaking, the view that the only thing that is important to our understanding of a statement is the way that statements interacts with the surrounding web of statements in our belief system. This is made precise by saying that we understand a statement precisely when we could recognize a proof or disproof of it.

Computationalism is the view that a mind can be represented as a computer program, that is, there is no fundamentally non-computable stuff going on up there: if a computer was fast enough, it could compute the proper outputs to the nerves based on the microsecond-to-microsecond inputs received.

Together, these two views entail that we cannot fully understand math in its present form. Goedel's semantic incompleteness theorem shows that for any computer program, there will exist statements in basic number theory which that computer program can recognize no proof or disproof of. Perhaps one might respond that this seems acceptable, as it becomes very difficult to understand complicated mathematical statements, and it doesn't seem implausible that we have some limit corresponding to Goedel-style incompleteness. However, in general our ability to understand the meaning of mathematical statements does not seem to correspond that well to our ability to prove or disprove them (or understand proofs provided by others). The continuum hypothesis, for example, seems understandable; yet it is known not to have a proof or disproof in any widely accepted set of axioms. It seems implausible (to me, at least) that it's understandability comes from its being provable or disprovable in our mental logic. The halting problem provides numerous other examples which I would claim were understandable yet not amenable to proof or disproof.

This means we've got to either give up inferentialism, computationalism, or classical mathematics. Very roughly speaking: people who give up classical mathematics are some variety of intuitionist or constructivist; people who give up computationalism are some variety of dualist or hypercomputationalist (like Roger Penrose).Now, I don't disagree in principle with restructuring math from the bottom up, but it seems desirable for a foundational program to capture as much as possible of the way mathematicians intuitively reason, so I'm hesitant to be a constructivist (though I may yet be converted). Similarly, I don't have anything against the possibility that some processes yet-unknown to physicists are endowing minds with special non-computational behaviors (and since I'm not a constructivist, I even believe that such behaviors can be well-defined and deterministic!). However, I don't know that this is the case, and neuroscience seems to suggest that much of neural processing can be accounted for in a computational way. Furthermore, as an artificial intelligence researcher, I hope that the essence of "mind" can be captured computationally. I fall in the third category, wanting to give up inferentialism.

Giving up inferentialism is not to be done lightly. It's a highly plausible assertion, especially for the computationalist: what else should matter about a statement then the computational interactions it has with other statements?

The solution I find plausible I'll call weak inferentialism: we understand a statement if we can compute a defining set of inferences. The statement's meaning is precisely that defining set; it is merited when all inferences in that set are merited, and (optionally?) false when one of them is false. (Should falseness be taken as a basic concept?) This does not mean that we can compute all of the statement's consequences, though. For example, the defining set of a universal statement P: "For all x, S is true of x" will be all the statements "S is true of A", "S is true of B", ... It's possible that another statement, Q, has a list of consequences which is some subset of P's list. In this case, Q would be a consequence not in the list for P. In some sense, however, Q does not add anything to the list: it just summarizes a portion of it. The weak inferentialist argues that this allows us to understand P without necessarily knowing that Q follows from it.

(There may be some interesting connections between these two types of inferentialism and the "Principle of Harmony" from proof theory, which states that the introduction rules and elimination rules for symbols should precisely mirror each other. This basically corresponds to a connection between the inferences from which we can conclude a statement and the inferences we can make from that statement. This principle may have to be spelled out differently for the two types of inferentialism. I don't know enough about the principle of harmony to make a well-considered connection, though.)

Now, the question: what foundational logics do the two different inferentialist pictures recommend? In particular, if we're also computationalist?

Strong inferentialism will only care about notions of logical consequence which have complete proof theories, like first-order logic. An inferentialist will only care about what structures of reasoning can be implemented in the logic. In particular, it seems natural to consider a logic as a programming language. Think of it like this: we have some basic domain of discourse we wish to talk about (such as the actual world), and we have the logic which allows us to make assertions which will cause some statements about the domain of discourse to entail other such statements. The logic is nothing more than a means for expressing these entailment relationships between the domain-level facts.

Ignoring computational efficiency and one or two other practical matters, it seems that little about the logic matters once we've determined that it is Turing complete. Classical first-order logic, intuitionistic first-order logic, and a host of others will all do equally well.

Interestingly, though, more powerful logics can be motivated even in this minimalistic worldview (if we bring practical matters like speed back into the picture). Goedel showed that mathematically more powerful logics (in a specific sense) will always have the following property: there will be some inferences which can be made in an astronomical number of inference steps in the less-powerful logic, but which the more-powerful logic proves in just a few steps. This theorem only holds for arbitrarily large domains of discourse, though, so it is an empirical question whether the phenomenon occurs in practical situations. The paper "A curious inference" by George Boolos and "Some More Curious Inferences" by Jeffrey Ketland discuss the issue (taking the affirmative).

Happily, the notion of "more powerful" here coincides at least to an extent with the more typical notions, which seems to mean that we can justify a good amount of normal math via this sort of reasoning, despite the fact that strong inferentialism will deny that math its standard meaning. However, I don't know the precise connection here, and I won't try to explore (in this blog post) precisely what of mathematics could be justified in that way.

In any case: what sort of view of logic does weak inferentialism suggest? Well, based on the idea of the defining set of consequences, we could say that a (non-basic) statement is a computer program for listing its own consequences. The "most expressive" logic will be one which uses a Turing-complete notation to do this. The key difference between this system and the previous is that we may not be able to infer a statement even if we can infer all of its defining consequences: we cannot implement the truth conditions computationally. Hence, we still have a (highly abstract, irrelevant of speed issues) concept of a more powerful logic: a more powerful logic will know more about which statements follow from which others. This is equivalent to knowing more about the halting problem (since we could check for implication A->B by making a program that halts when B implies something A does not, but keeps looping otherwise).

Fortunately, the extra information can always be expressed in the same logic! We never need to add more expressiveness, only more knowledge. The work done by any additional symbols can evidently be done without them, because the notation is Turing-complete.

The weak inferentialist logic includes the Liar sentence, ie, the sentence whose defining consequence is just its own negation. This can be dealt with via Kripke's fixed-point valuation: we enforce the constraint that a statement is considered true exactly when its defining inferences are merited, but we don't require that a sentence is either true or false. The inference "The Liar sentence is false" is neither right nor wrong; it remains undefined, since there is nothing for it to take its truth or falsehood from. The Liar sentence is ungrounded.

Exactly how this works will depend on whether we want falsehood as a basic concept, which I left open at the beginning. If we don't take it as basic, then falsehood might be defined as the property of implying everything.  The Liar paradox then becomes something very reminiscent of the Curry paradox: "This sentence implies everything." What the fixed-point construction tells us is that we can't in general use hypothetical reasoning to see if inferences are indeed justified: if we want to know whether sentence X, which asserts just X|-Y, is true, then it appears we should assume X and see if we can derive Y. (Read X|-Y as "from X  we can infer Y".) If we assume X, then we know X|-Y, but combining those two, we know Y. This hypothetical reasoning proves X|-Y, so we know X (un-hypothetically). But this entails Y, which might be "everything"! Logicians have provided weaker forms of hypothetical reasoning which conform to the fixed-point construction in order to avoid this problem. (Specifically, we can only make hypothetical assumptions which we already know are grounded.)

It's interesting that this means the sentence which just claims that inferring Y is justified is radically different from the sentence which claims that inferring Y from itself is justified, despite the fact that once we believe either, they justify the same inferences. The two even have the same conditions for being true: if we know Y, we can conclude both (since A|-B is true when B is inferable, that is, |-B implies A|-B, regardless of A). However, when Y is false, then the statement "infer Y" is false, but "From this statement, infer Y" is ungrounded and thus considered undefined.

The final thing to note is that, although no further expressiveness appears to be justified by weak inferentialism, the system described cannot fully express the concept of "groundedness" I've been using. (It can only mark it true, never false; but I've noted that statements are ungrounded more than once in this discussion.) Hence, we have an immediate example of a concept which appears to be mathematically well-defined, but which weak inferentialism does not seem to be able to account for. Yet, what is lost? After all, these supposed statements can't even be given a computable list of defining inferences they justify! Is it useful to state that something is ungrounded? (I think the more basic notion called into question here is negation itself: is it always meaningful to know that something is not the case? Negation has no defining set of inferences!)

Concerning Monetary Systems

It all started with a math-geek desire to come up with an "imaginary" dollar-- a unit of currency  equal to the square root of debt. Unfortunately, googling "imaginary dollar" just gets a load of people saying that money is already imaginary. :) So, I eventually googled "hypercomplex dollar" (the hypercomplex numbers go beyond imaginary numbers, introducing things like hyperbolic multiplication, et cetera). I got this:

http://www.halfbakery.com/lr/idea/Hypercomplex_20money

Sadly, this and the other proposals it links to are not really attempts to construct imaginary money: they just use the fact that the imaginary numbers (and hypercomplex numbers) are orthogonal to real money; they don't attempt to give an answer to what the square root of a monetary amount might be.

Anyway, these proposals referenced the LETS money system, which is interesting...

http://www.gmlets.u-net.com/home.html

The basic idea: everyone starts out with 0 money, but is free to spend anyway. This puts them in the negative, but negative is referred to as "commitment" rather than debt, and is not supposed to be a bad thing. There is always as much negative as positive, so being in the negative is normal and does not cause a problem (since you're still free to spend even more). The justification: scarcity of money causes a lot of problems. Scarcity of dollars stops local economies, even if there is really enough goods and labor to go around. This is why more US dollars are printed then go out of service each year: to fight the scarcity of money. Unfortunately, that leads to inflation, which has its own problems... LETS tries to fix this by letting anyone issue money whenever they like, creating "commitment" in doing so. This means there doesn't have to be money around in order for people to exchange commitment for goods and labor, so that money scarcity can never be a problem.

This basically relies on individuals to honor their commitment. I think this is a big part of why LETS is supposed to remain a local currency: it relies on the goodness of people, so if it got too big it would run into troublemakers.

My take on the future of money is that we are headed for a credit-based economy (in which credit is more important than raw money). We're already almost there! However, there are some serious flaws with the current credit economy... credit cards are a Bad Plan. Personally, I think things like kickstarter are a better sign of what's coming... people investing in people. The problem with banks and credit cards is that all the investing is being done by a few monolithic entities, whereas the "little guy" just gets the debt. The little guy needs to be able to give credit as readily as take it.

The idea of "debt" is owing money to one person. The LETS idea of "commitment" is to instead owe to a community. The problem is that this is too easy to take advantage of it becomes too mainstream (ie, if people don't feel a personal commitment to the whole community). The currency would just inflate.

To address this, I propose an idea of financial backers. Individuals back each other rather than being backed by a big bank. If a group of people back each other with no reservation, then they should automatically  form something like a LETS network: they can spend as many credits with each other as they want, making "commitment" with the group as they do so. When they get money, either within the group or from outside, the commitment gets payed off.

More commonly, people could offer each other limited lines of credit. The amount I offer to you would depend on a combination of how much I trust you, how much I can afford personally, and how much credit I have from other sources.

Obviously more details need to be worked out here. One principle from LETS is that no interest should be charged on commitments. It's not obvious whether that's preferable in the system I'm thinking about. It promotes a positive and friendly outlook (as does the option of offering an unlimited credit line to people you trust, rather than worrying about placing a $ cap). However, it also seems to make sense to pay people back for their hospitality... perhaps mutual credit agreements are better than interest for that purpose, though.

One conspicuous advantage of this scheme (in contrast to the currently mainstream big-bank approach!) is that the distributed nature of the system prevents large failures. An uncareful collective of individuals might fall together, but the impact would be limited.

EDIT: This proposal has already been thought of and is being implemented! If you extend me a little credit in ripplePay I'll extend you a little back. :) I may write a post soon on the differences between what I was imagining and what these people are doing.

Goal Systems

Continues this.

It seems fairly clear that backwards-chaining should be seen as a result of goal-oriented behaviour, whereas forward-chaining should be more a result of the reactive reasoning layer. This thought arises from several considerations (including efficiency), but mainly from the idea that backtracking is simply an attempt to achieve a goal by trying different possible (sets of) subgoals in turn.

A simple production-rules-vs-logic-programming view would see the issue as two different ways of interpreting the conditional from propositional logic; A->B either means "if you have A, conclude B" (if you're a production rules person) or "if you want B, try A" (if you're a logic programming person). I'm denying that that is what's going on. A->B in the knowledge base means just what it means in the declarative logic, and doesn't by itself trigger any inferences. For inferences to be triggered, procedural knowledge must be present. Procedural knowledge can always be put in a series of if-then type statements which are executed by forward-chaining; both "if you have A, conclude B" and "if you want B, try A" are just examples of this.

Now, for probabilistic-relational systems, goal-oriented reasoning is set within the framework of bayesian utility theory. The mathematical theory is simple and elegant (although there have been refinements over time, such as causal decision theory, timeless decision theory, updateless decision theory); but like pure probabilistic reasoning, it isn't immediately obviously how to efficiently implement/approximate. Much of the relevant research for this comes from the domain of reinforcement learning; also, an algorithm that's generating a lot of research right now is monte carlo tree search. It seems reasonable to follow these threads of research for a goal-system implementation.

For me, it seems natural to replace the on/off subgoals & backtracking which appear in crisp systems with a more continuous goal structure. This is based on the analogy to the way the truth values become continuous in these systems, which my be a bit hasty. Still, here is my rough outline:

I've been considering for some time a system which allocates time to different reasoning processes based on a currency of "effort". Effort could take two forms: a longer-term effort would represent percentage of processing time, while a shorter-term effort would represent amounts of time. There would be long-ish cycles in which every goal that has long-term effort attached to it gets a corresponding amount of short-term effort assigned to it. A goal can then cause subgoals to be spawned which it assigns some of its effort to.


This may or may not be a good idea. :) The shorter-term effort seems like a natural concept; it's been invented independently by two different people I've talked with (Ben Goertzel's group, and Russel Wallace). It seems useful for complex combinations of approximation algorithms that can be given more or less time to give better or worse answers, especially if they may employ each other or themselves in a loopy manner. Programs based on this sort of effort would be guaranteed to terminate in whatever amount of time they are given (though, perhaps not with a very good answer.)

The longer-term type of effort is not so obviously useful; hard to say.

Procedural Logic

I've decided to start using the term "procedural logic" for what I called action logic in the previous post on this topic. This better reflects the desire to merge the procedural and declarative; also, it steers clear of logics already named "action logic."

To pick up roughly where I left off...

Tactical theorem provers such as HOL Light and Coq are the modern-day epitome of procedural logic, in some ways. They work by the simple lack-of-mechanism which I gave as the minimal procedural logic in the previous post: they are simply programmable theorem provers. "Tactics" (aka "strategies") are created, which are simply programs for guiding inference; tactics can use each other, so that in a weak sense they are like goals and subgoals. What's really nice about them is that they cannot be made to return an incorrect result, no matter how wild the tactic. What they lack compared to SOAR and PLANNER is:

1. Reflexive inferences: SOAR automatically forward-chains for all rules in its KB. In a similar way, Prolog automatically backwards-chains for all programmed rules. PLANNER was designed to do both, with a declaration of which way a rule should be used upon its creation. (SOAR does something similar with a little work.) ACL2 probably has the most advanced facilities, from my cursory examination; there are many categories of possible reflexive inferences for different sorts of theorems, and the system has intelligent defaults which the user can override. However, the reflexive inferences are still clearly too simplistic sometimes; for example, the user can create an infinite loop just by proving both B = A and A = B... ACL2 will happily swap A for B indefinitely the next time either one appears in a statement.
2. Truth Maintenance: Some facts are of the sort that can change. Under strict logic, we should index them by time to account for this, but it seems necessary for efficiency to ignore this and just change the facts directly. If that's the strategy, then we have a truth maintenance problem: we may need to update our entire KB to reflect the change, withdrawing any statements we proved based on the now-false information. In SOAR, this is reflected in the distinction between o-support and i-support: o-support represents that the rule is intended as making a change to the KB in firing, which cannot be undone except by another o-rule, whereas i-support represents that the rule's consequences should be undone immediately when the premises become false (thanks to an o-rule changing something). This is probably the most advanced form of this sort of distinction. PLANNER also addressed the issue, however. (That's why I called SOAR a "descendant of planner" in my previous post on this topic; since then, though, I've asked Paul Rosenbloom about it. He indicated that PLANNER did not actually influence SOAR in any significant way, so it looks like SOAR came up with the idea quite independently.)

So, the question becomes: what should a probabilistic relational system do about all this?

Paul Rosenbloom's probabilistic-relational rethink of SOAR (see his publication page) takes the position that #2 can emerge in a simple way from the sum-product belief propagation algorithm; basically, this amounts to re-estimating all the weights in working memory whenever a change is made by a rule in long-term memory. The system also deals with time in additional ways. As for #1, there is some divergence from SOAR's system, but nothing as sophisticated as ACL2. Paul Rosenbloom's proposal does not have a reason to focus on proofs via mathematical induction in the way ACL2 does, so it would not benefit from a translated version of ACL2's guidance system... perhaps it's reasonable to say that much of the sophisticated stuff in ACL2 is fairly special-purpose for its domain of application.

Having sum-product as a basic dynamic seems like a good idea, but at the same time, I'm thinking of a system which can reason about inference guidance even for that. For example, it seems reasonable to (A) weigh the product-sum algorithm's attention to specific areas of the belief network based on multiple factors, including which variables are currently undergoing the most change, and which variables are most critical for the goals; (B) augment the product-sum algorithm with more accurate algorithms in areas of the belief network where accurate estimation is critical. In the Rosenbloom system, (A) would have to be an addition to the basic level, but he has discussed (B) as something which might be implemented on top of the basic level using rules. The second situation is preferable, but at the same time, any "basic level" of reactive inference/decision will have some built-in assumptions. There is a way around this, however: dynamic replacement of inference strategies in the manner of Hutter's Algorithm. Hutter's algorithm is tremendously inefficient, so it would be nice to find a small-scale, incremental way of employing the same trick. (Also, Hutter's algorithm would need to add probabilistic reasoning about algorithm speed and correctness, to satisfy the desire for a fully probabilistic-relational system.)

To summarise that disorganised paragraph: I like the idea of using sum-product as the reactive-level reasoner, but it may not be what I'm after for procedural logic. As a disclaimer: worrying about abstract asymptotic universality stuff is fun, but it is not necessarily relevant to practical implementations. Sometimes I am more of a mathematician than a computer scientist. However, there are some recent indications that the theory of universal intelligence might actually guide practical implementations: a working, practically applicable, asymptotically universal approximation of AIXI, and a Levin-search-based automatic programmer that works on some toy problems.

In any case! The main point is, in probabilistic relational systems, truth maintenance gets replaced by some form of belief revision plus some way of dealing with time. (In OpenCog, I understand that part of the strategy will be to have the truth values of time-sensitive statements decay gradually as they become more probably out-of-date.)

The other issue to address is how a goal system for a probabilistic-relational version should work, but, I guess that's too big a topic for the moment... though honestly I started writing this post to talk about that :) Such is blogging.

SOAR workshop so far

Daniel and I have just come back from the pre-workshop dinner. Our ride (another attendee) had a delayed flight, and we had to call a taxi; we ended up being about 45 minutes late for dinner. Daniel and I ended up getting seats at a separate table, so we didn't talk to anyone right away; eventually, though, we got some good discussions.

My primary thesis has always been the importance of expressive power in AI. This has been a reaction to the overwhelming majority of AI research being done with propositional methods.  However, this method tends to fall on deaf ears for several reasons.

1. If I don't phrase myself carefully, it sounds like I'm arguing the anti-AI position that many people abuse Gödel's theorem to argue. This is thanks, for example, to my use of words like "uncomputability" (and if I invoke Gödel's theorem, of course, that just makes it worse). If I say "system X can't represent uncomputable mathematical concepts, but humans can," it really makes people think that I mean "computers can't handle uncomputable mathematical concepts, but humans can." I don't mean that. Rather, I want to soundly answer the anti-AI position via a formal theory of which systems are capable of climbing the Tarski hierarchy on their own (and how they do it).
2. John Laird and the other fellow in the front seat when he was giving me a ride back to the hotel (sorry, don't remember the name! EDIT: Paul Rosenbloom) pointed out that worrying about expressive completeness is far less common than trying to find less-expressive subsets of existing systems which are more efficiently manipulated. Daniel put it another way: one shouldn't just worry about what a system can do in principle but about what it can do in reasonable amounts of time. Systems which are "more expressive" might be able to do far less in practice. My response to this is just to say that I prefer systems which use heuristics to stay in the space of efficient reasoning, rather than reduced expressiveness... this is a weak-sounding point, though I do think it is the right response...
3. If I'm already talking to someone who believes that expressive completeness is an important issue, then the remainder of my pet theory consists of ways of generalizing from a propositional system to more expressive models. This typically becomes a situation of singing to the quire, because the person will already be past propositional models and into at least first-order. All I have left to argue is the seemingly reversed position that most reasoning should actually take place at the sub-first-order level (say, 1/2 n-tuple markov models, 1/4 context-free, 1/8 context-sensitive, 1/16 first-order, 1/32 2nd-order...). This is related to the response for the 2nd point.
4. My project is really quite an abstract one, because at present my best guess is that so long as a system is doing probabilistic relational learning (ie, at least 1st order), and so long as it approximates Solomonoff induction in its ability to discover hidden relations in data, then it satisfies the requirements to climb the Tarski hierarchy. Because of this, I can't argue that there is a pitfall of expressive incompleteness waiting to trap anyone who isn't careful. So, it seems I should only be arguing for those basic requirements rather than arguing that a general theory telling us how to climb the Tarski hierarchy must be found. If I can argue for those points on separate grounds, a general theory saying that those are sufficient is more a nice factoid for those worried about the foundations of mathematics than a guiding principle for AI. (Though, there's still the possibility that the required structure for a system is significantly more specific than Solomonoff induction, in which case the theory may have definite value.)

So, should I give up what has been my primary thesis for 4 years? The banner "Expressive completeness is the central problem!" may not be the best way of organizing and presenting my ideas at present... in any case, it's clear that I need to think about my arguments more carefully.

Action Logic

Continuing a thought in this post.

A normal axiomatic logic pins down which inferences are permissible, but makes no comment on how these inferences are to be made. For real implementations, we've come up with a plethora of inference strategies-- however, the axiomatic system is always treated as separate from the inference strategies. My idea of action logic is to merge the two, hopefully in order to do nifty things like letting the system reason about its own inference strategies in a smooth way.

In other words, what we want is to nicely integrate logic and programming.


Several attempts to do this already exist. One example is Prolog. Prolog does not, however, satisfy the desire to allow deductive reasoning to determine flow of inference; Prolog just performs a backtracking resolution algorithm on horn clauses, paying some heed to meta-logical control flow statements that can be inserted.

However, I think we can take some inspiration from a predecessor of Prolog, known as Planner. Planner worked through a backtracking mechanism similar to that of Prolog, but more expressive. It used a separate notion of "goal" and "fact" to drive reasoning: if a goal is present, then the system starts reasoning about how to achieve that goal. This can involve the creation of subgoals which drive more reasoning, the execution of programs, and performance of inference steps.

One could argue that Prolog makes this distinction, but it is much less explicit: since programs and statements are the same thing, the creation of subgoals always just corresponds to the conditions in an if-then. (In PLANNER one can specify arbitrary advice for what subgoal to create at a given step; it is not so strongly tied to the form of the logical assertions in the knowledge base.)

PLANNER also has the feature that facts can be removed from the knowledge base when they become false, ie, the system does not need to index facts to time in order to model facts changing; this is important for efficiency, though it is less "logically pure" than the alternative.

This is a good overview of Planner for the interested. More recent systems such as SOAR, SCREAMER, ACL2, et cetera have many of the same features; I am really picking out PLANNER mainly for its historical significance.

In any case. I said that I was trying to merge declarative and procedural, yet I am praising PLANNER's explicit goal system over Prolog's implicit way of dealing with goals. Why? Because it is more powerful: we can provide more inference guidance in PLANNER than in Prolog.

In any case, I am not saying that Planner is a sufficient action logic, either! In fact, I'd say, let's question the basic mechanism which it shares with Prolog: if the system has goal G, and knows a statement of the form "S implies G," then it will automatically make a subgoal S. (For the curious: Both PLANNER and Prolog will select out of several statements "X implies G", try that X, give up if that subgoal turns out infeasible, and try the next. This technique is applied recursively, creating sub-sub goals, et cetera. In Prolog this is the only mechanism at play; in PLANNER there are more conditions to be met for this to happen, there are other mechanisms at work, and the programmer can add arbitrary mechanisms.)

What happens when we vary this mechanism? Well, there are a lot of options. We could create a reinforcement-type agent which attempted to learn what inferences to draw and what subgoals to create and when, getting rewarded whenever it meets a goal specified by the programmer. We could create a brute-force system which keeps proving theorems until it happens upon one of the form "P implies G" where P is a fully specified sequence of actions, rather than just a subgoal-- the system then does P. We could produce a system like Hutter's asymptotically optimal algorithm by creating a mechanism which searches for plans of action, replacing the current plan when the system finds a proof that switching to a different plan will result in a better outcome.

The weakest choice is to just require that if the goal "do X" is asserted, and X is a sequence of actions, the system does them immediately. This just means that the system is programmable. (X can be an arbitrary program because it can include branching goto type statements.) Any other choice of system can be modeled in this one by telling it to behave in that way.

Stronger choices will provide more built-in useful behavior, but will also have more built-in assumptions.

My desire is to create an abstract framework, not something that pins things down to a specific implementation. So, it seems like what I'm looking for is an abstract "should-ness" concerning what inferences to draw when, and what subgoals to make when.

Much of the logic discussed under the title of action logic in the Stanford Encyclopedia is somewhat relevant here, though the logics there are definitely not action logics in the sense I intend: they are just normal axiomatic systems, which must rely on outside inference procedures.

In general, my approach to AI is very much in the line of probabilistic relational methods: I advocate a move to probabilistic reasoning where just boolean reasoning is present, and to relational methods where just propositional methods are present. In this case, that means that what I see as the logical next step is to research probabilistic generalizations of PLANNER... it seems this would force many of the simplistic methods employed in PLANNER to be "broken open," so to speak, getting out the chaff and determining what can be salvaged and improved for the probabilistic setting.

Postmodernism

I've been thinking for a while about why postmodernism might be a tempting intellectual position. There are certain logically sound logical arguments that support particular assertions associated with postmodernism, as well as certain practical issues which might make it tempting. I will try to illustrate my position against postmodernism by giving the best arguments I can muster for it-- the intention is to show why we can get this far, but no further.

I won't be too surprised if someone reads this and says "but postmodernism doesn't try to go any further than that with the argument,"or further, "that's not what postmodernism is at all;" these arguments are based on my impression of postmodernist thought, not based on a formal education in the subject.

Since this thing would be tl/dr (or worse, tl/dw) if I did it as one post, I'll just post an outline for now; the points below will become links as I write individual posts. (I may also come back and add/delete/edit points, of course.)

Practical Reasons

-making room for others to doubt your beliefs
-the intellectual proliferation of hypotheticals
-Flexibility of language and definitions; anti-prescriptivism
-disagreements are often based on matters of language (differing definitions) rather than matters of fact
-such things as tables, chairs, etc don't exist (strictly speaking)
-Scientific theories are approximations

Logical Reasons

-loeb's theorem
-algorithmic complexity is relative
-We can always "interpret" talk in any logical system or system of axioms as just hypothetical first-order talk (by throwing out the naturalness constraint on interpretations)