|
|
Monday, April 30th, 2007
|
3:54p - my axioms for the "semantic" turnstile |=
What are the axioms of the "semantic" turnstile |=?
In the spirit of Locus Solum, I want the freedom to define my symbols to mean anything I want. I like using semantic turnstiles as shorthand for "has property": if I want to say that a class of things has property phi, I will turn it into a class of models (see the second half of this post).
I want the freedom to define my own turnstiles (i.e. my own interpretations), even if that makes model-checking undecidable (e.g. let M |= phi iff phi is true of the output of Turing Machine M). But still, I want the symbol |= to carry some meaning.
The basic syntax I define is:
TURNSTILE_SENTENCE ::= SET_OF_MODELS |= SENTENCE
And as syntactic sugar:
SET_OF_MODELS ::= MODEL
(because it looks dumb to write {M} |= phi)
Axiom 1: definition of what it means for phi to hold in a set of models
M |= phi and N |= phi <=> {M, N} |= phi
|= phi conventionally means that phi is true of every model, i.e. "universal set |= phi", rather than "empty set |= phi". I would like to banish this abuse of notation, by requiring the use of a symbol like "U" for universal set.
Axiom 2: definition of what |/= means
S |/= phi means not S |= phi.
Since I (and all working mathematicians) believe in excluded middle (and non-contradiction), this means that forall S and phi, either S |= phi or S |/= phi, but not both.
As I mentioned earlier, some of the things I like to do with semantic turnstiles might be considered abuse, e.g. introducing mathematical symbols that can't readily be interpreted without importing a theory (which is left implicit in my treatment).
Does this objection apply to my example:
forall n ( exists f_n ( Gaussian |= ( E(X^n) = f_n ( E(X^2) , E(X) ) ) ) ?
The symbols n and f_n are going to disappear before the |= gets interpreted, so this is no problem. On the other hand, the "=" does not disappear. By using "=", I am a assuming a theory of real numbers in which we have equality. I guess this is ok as long as everyone agrees about when the equality holds. To be strict, I might need to plug-in an "implementation" of equality if I am going to say that I have a logic here.
Maybe this is a design issue, though: I can define a model (i.e. probability distribution) as a sequence of moments and deal with them as such. (Since all my queries are about moments, this representation is enough). So instead of E(X^2), we define a (parametric) property of the models, nth-moment(2). In order to check for equality, the model-checker would take the real numbers in some normal form, so it's not so easy afterall...
...or I can bring math into my logic, and define models as real probability distributions. If I do this, things get worse: the model-checker needs to know calculus in order to compute E(X^n).
But why should I need an implementation of equality? I'm just trying to express a definition: Gaussians are defined by first two moments, so it's no surprise that the first two moments uniquely determine the distribution.
![[info]](http://l-stat.livejournal.com/img/userinfo.gif) ekorber says that it's ok to mess around with "|=" even if I don't have everything strictly defined, because mathematicians do sloppy things with it all the time.
(8 comments  |comment on this)
|
10:53p - summer school settled ; lease signed
Today has brought me a lot of welcome closure.
It was decided that I am going to the Summer School on Probabilistic Models of Cognition in LA, and that this will count as work time (it's relevant training, since my project is about using machine learning to get cognitive models), so I will be paid. Sweet! Not enough to pay LA rent, but I really can't complain.
At 7pm, chrisamaphone (and gwillen) and Cemllyn came over to sign the lease, so now it's all formally settled.
I don't know if it's worth subletting my room for July. I can probably get a good $250 for it, if I can find someone who is compatible enough with the housemates at the time. On the other hand, I will most likely spend a few days of July in Pittsburgh, either at the beginning or at the end.
(2 comments |comment on this)
|
|
|
|
