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.
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.
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.
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.