Trade Logic 2

More on Trade Logic

Previously

Earlier I introduced Trade Logic. It's a form of logic that I designed to be suitable for connecting prediction markets. It is logic that "lives" within the system, not in individual traders' analyses.

I planned to define standard as an exercise. But when I started to write it, I realized that there were a number of preliminaries that I needed first.

I also realized I had to change a few things. In the places where this post differs from the previous, it supersedes it.

About definitions

Definitions cannot assert

Definitions in Trade Logic deliberately cannot assert facts. And it would be disastrous if they could. If traders could "prove" things by defining them to be true, the whole system would collapse and be useless.

Instead, definitions simply expand to parameterized formulas. Formulas cannot assert facts.¹

A "classical" definition of standard would have implicitly asserted that there is one unique predicate standard. But that implicit assertion is banned in Trade Logic. We (deliberately) wouldn't be able to construct a formula that asserts that.

Instead, we would define a predicate that is true just if its argument "behaves the same as" the predicate standard. That is, is-standard would be true if its argument is a predicate that satisfies the axioms of Internal Set Theory as standard would.

NB, this won't (and shouldn't) imply that is-standard's argument is defined in the system. It doesn't neccessarily have a global name in the system.

Definitions cannot raise error

Definitions in Trade Logic are not allowed to error. If they could, that would wreak havoc on the system.

They can be undecidable, which causes no great problems for wise bettors. They are also total, meaning that each of their arguments can be of any type. So our definition won't be able to lean on a strong typechecking mechanism.

Definitions are statically simply type-correct

However, there is a weak typechecking mechanism in Trade Logic. It is a well-formedness condition for formulas and predicates and thus for bettable issues. I'm largely borrowing the mechanism from the simply typed lambda calculus. But the simply typed lambda calculus is functional while Trade Logic is relational, and Trade Logic manages modes as well. So I adapt it slightly.

The exposed primitive types are:

• thing
• type
• predicate

The type definitions are:

thing

Everything is a thing. For expressive purposes, either:

• A variable.
• Any object of any of the other types.
• Extensibly, any other literal the system accepts.

type

Either:

• One of the exposed primitive types
• A type literal naming a definition of a type in the system
• A list of types
• A dotted list of types
• Dynamically, anything satisfying is-type

call

Not an exposed type. Of the form (P . Args) where:

• P is a predicate
• Args is a (possibly empty) tree of things, ie a Herbrand term.

acceptable call

Not an exposed type. Either:

• A call where Args is statically accepted by P. Ie, where we can prove that beforehand and using only local information.
• Dynamically, a call satisfying (accepts-argobject P Args)
• Dynamically, a call satisfying both
  • (accepts-type P T)
  • (satisfies-type Args T)

wff

Not an exposed type. Either:

• Any issue (ie, predicate with empty argtree)
• A combination of wffs as defined in the previous post.
• An acceptable call.

predicate

Either:

• A predicate literal naming a built-in predicate in the system
• A predicate literal naming a definition of a predicate in the system
• A lambda term - a call where:
  • P is the built-in literal pred
  • Args is a list of 2 elements
  • The first argument is a wff
  • The second argument is a mode-spec
  • The whole is mode-correct, as defined in the previous post.
• Dynamically, anything satisfying is-predicate

Type acceptance

Type acceptance

A predicate P accepts a type T just if T is the type of P's parameter list or is subsumed by it.

The built-in predicate accepts-type

(accepts-type A B) is a binary predicate. It has two modes:

• (accepts-type - -)
• (accepts-type - +)

It is true just if:

• A is a predicate
• B is a type
• B is a type that A accepts. In the second mode, B is exactly the given type of A's argobject.

The built-in predicate satisfies-type

(satisfies-type A B) is a binary predicate. It has one mode:

• (satisfies-type - -)

It is true just if:

• B is a type
• A is of type B.

The built-in predicate accepts-argobject

(accepts-argobject A B) is effectively the conjunction of (accepts-type A C) and (satisfies-type B C)

Dynamic checking

Sometimes we don't know a thing's type statically, but we still want to use it or reason about how to use it. This often occurs when we use higher-order logic.

The clauses that say "Dynamically" are interpreted as allowing formulas to be conjunctions of type-checking operators and sub-formulas that require a specific type. Such formulas are interpreted as false if the type is incorrect, rather than erroneous. It is as if the type-check was examined first and the erroneous clause was skipped. (But in general, Trade Logic formulas do not have a particular order in which sub-terms are examined except as dictated by the mode system)

Definitions, redone

Types and predicates can be given names, ie defined in the system. Some trivial constructions of predicates deliberately can't be given names because it would be silly:

• The predicate literals - they already have names.
• The dynamic construction. "This predicate is something that satisfies is-predicate" would be pointless.

I might require a checkable proof for places in a construction that require static correctness. That would add an extra argument to acceptable-call and the pred call.

A named predicate can be bet on just if it accepts the empty type (null).

Footnotes:

¹ In particular, Trade Logic does not have functions, it has predicates. This rules out Skolemization.