Probabilistic HOL

Where We Are: 
The formalism we will be using for the horn-clause subset of first-order probabilistic reasoning will be something close to the following. (Propositions may end up being either crisp or fuzzy or both in the initial version. For stating crisp propositions, we have predicates which are boolean predicates, and boolean truth functions (at least and) to make sentences. For stating fuzzy propositions, we have continuous functions which are predicates, and fuzzy truth functions (at least and) for combining them. The choice between the two will not matter in what follows.)

1. Predicates, or more generally sentences with free variables, can have probabilities associated with them. These represent the probability that they will be true on random arguments (random instantiations of their variables). I call these "unconditional probabilities" since the system will also store conditional probabilities. They are also called "marginal probabilities." We can specify ahead of time this prior probability for some predicates, and explicitly conditional probabilities, elsewhere. Together, these probabilities can be thought of as the probabilistic version of universal quantification that will be employed.
2. Existential quantification could be represented by allowing statements to the effect that the probability of a predicate is nonzero; however, we will be using skolem functions in any case, and it seems (to me) more reasonable to always represent existential quantification with skolem functions. (Eliminating zero from the range does not eliminate places arbitrarily close to zero, so the meaning of such a statement is unclear to me. Perhaps existential statements could be generalized to say "the probability is not below x" for typically-small x, but that introduces interval probabilities.)
3. Conditional probabilities will be employed, which will allow the construction of Bayesian networks (along with the unconditional probabilities, which get used for the initial nodes in the network). Predicates, variables, constants, skolem functions, &, and a conditional put together give the capability to express Horn clauses. Conditional assertions play the role of rules, and unconditional assertions (which can be seen as just assertions with empty conditions) play the role of ground information which the rules act upon; note, however, that since unconditional assertions can still have variables, lifted inference (inference which reaches general conclusions rather than only ground conclusions) can take place via the same algorithm that would do the ground inference. Lifted inference can be approximated to get the marginal probabilities for predicates and partial instantiations of predicates which we might otherwise not have marginal probabilities for (ie, when we did ground reasoning later we'd be forced to instantiate more bayes net than we might want to for efficiency, because some predicate needs more information to generate a probability estimate for it).

 Where We May Go:
We will eventually want to move on to full first-order logic (FOL) and higher-order logic (HOL). These are some speculations on how.

1. In the resulting system, skolem functions and skolem constants are treated as always existing, but not necessarily meaningful: they may not be equal to any entities in the domain that we are actually interested in, ie, they may have an "undefined" value. (This happens when they exist in an uncertain generalization; if the generalization turns out to be false in some particular case, the skolem-function entities are "stranded" and do not take place in further meaningful reasoning.) This is consistent with  the HOL approach we want to take, ie, resolving paradoxes by accepting that some expressions have an undefined value.
2. For FOL, it is sufficient to generalize the above treatment from Horn clauses to general clauses.  If we add negation to the mix, then we've got general FOL clauses on our hands. This is the case even if we give up conditionals, though, which may indicate that we're adding too much power; we want most of the reasoning to stay within probabilistic conditionals so that it can be performed by Bayes nets. Restricting this, we can allow negated predicates but not arbitrary negations of larger compounds. This still corresponds to general clauses in the crisp (p=1) case, and Bayesian networks can easily handle negation of individual variables. However, it becomes unclear that the same reasoning method is complete for the expanded logic. So, I need to think about this more, as well as the several other ways to generalize away from strict Horn clauses.
3. Right now, I am trying to come up with a higher-order logic without going into higher-order probabilities. (2-level PZ is not what I'm worried about; I'm worried about unbounded levels.) Essentially, what's desired is probabilistic reasoning about HOL. This means that although we may speak of a HOL statement having a probability as a value, it does not have that "value" in the HOL sense. Otherwise, the existence of higher-order functions would practically force us to encode higher-order probabilities. Maybe this is the right way to go in the long run, but for this round I'm trying to come up with a relatively simple system...
4. The "ascent" strategy for designing the HOL is to first decide on the best way to generalize the present formalism to FOL, and then perhaps start considering SOL, TOL, et cetera until the pattern is clear enough to generalize to HOL. The "descent" strategy is to skip even the full FOL step and instead just try to figure out how to apply lifted bayesian network style reasoning to HOL directly. My approach is somewhere in between, trying to think about both in parallel so that I might apply constraints from the top to the bottom, and from the bottom to the top, until both meet.
5. One "descent" constraint is the idea that expressions do not always have truth values as their values. Predicates are just functions that map to truth values, and there are other types of functions. Bayesian networks can certainly deal with this! It might be good to use type reasoning to determine the sets of possible values for the bayes-net variables. (Even untyped HOL does type reasoning, after all.) This is not a difficult one.

Lots more to think about... but I might as well post this now.