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.^{1}
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,
isstandard
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 isstandard
'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 typecorrect
However, there is a weak typechecking mechanism in Trade Logic. It is a wellformedness 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 istype
 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 byP
. Ie, where we can prove that beforehand and using only local information. 
Dynamically, a call satisfying
(acceptsargobject P Args)

Dynamically, a call satisfying both

(acceptstype P T)

(satisfiestype Args T)


A call where
 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 builtin 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 builtin literalpred

Args
is a list of 2 elements  The first argument is a wff
 The second argument is a modespec
 The whole is modecorrect, as defined in the previous post.

 Dynamically, anything satisfying ispredicate
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 builtin predicate acceptstype
(acceptstype A B)
is a binary predicate. It has two modes:

(acceptstype  )

(acceptstype  +)
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 builtin predicate satisfiestype
(satisfiestype A B)
is a binary predicate. It has one mode:

(satisfiestype  )
It is true just if:
 B is a type
 A is of type B.
The builtin predicate acceptsargobject
(acceptsargobject A B)
is effectively the conjunction of
(acceptstype A C)
and (satisfiestype 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 higherorder logic.
The clauses that say "Dynamically" are interpreted as allowing formulas to be conjunctions of typechecking operators and subformulas that require a specific type. Such formulas are interpreted as false if the type is incorrect, rather than erroneous. It is as if the typecheck was examined first and the erroneous clause was skipped. (But in general, Trade Logic formulas do not have a particular order in which subterms 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 ispredicate" 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
acceptablecall and the pred
call.
A named predicate can be bet on just if it accepts the empty type (null).
Footnotes:
^{1} In particular, Trade Logic does not have functions, it has predicates. This rules out Skolemization.
No comments:
Post a Comment