my axioms for the "semantic" turnstile |=

[gusl]

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.

Comments

[ekorber.livejournal.com]

I didn't say it was ok, I said it was common and would probably be understood. :)

[easwaran.livejournal.com]

I guess I'm used to seeing SET_OF_SENTENCES |= SENTENCE. That's why an empty left side generally means "true in all models". Of course, there's a natural duality between sets of sentences and models, so there's a natural translation here.

I think the primary reason for having sentences on both sides is just that sentences are naturally syntactic objects, while models aren't, so it's awkward to have names for arbitrary sets of models except through sentences.

[gustavolacerda.livejournal.com]

When you have soundness and completeness, |- and |= are interchangeable.

I don't like SET_OF_SENTENCES |= SENTENCE. Is it ever the case that you can't write SET_OF_SENTENCES |- SENTENCE instead? (I suppose this may happen before you come up with rules for your logic, when talking about the territory that we want the logic to cover).

[easwaran.livejournal.com]

Yeah, that's the way I always think of it. The interesting relation between sentences is really the semantic one - the syntactic one is just a heuristic for finding when the semantic relationship holds, but soundness and completeness show that it's in fact coextensive.

[gustavolacerda.livejournal.com]

I agree with your assessment of interestingness: semantics gives us the specification with which to design the syntax.

I wonder if there are combinatorialist/proof-theorist types who like to start with syntax, and look at the semantics later... or perhaps design semantics (plural) in order to fit an existing syntax.

[easwaran.livejournal.com]

One thing that might be interesting to consider is when we'd be interested in classes of models that aren't described by sentences (I believe "non-elementary classes" is the model-theoretic term for that?) For instance, are we ever interested in the question of what sentences are true in all models that are prime for their complete theory, or that satisfy some other model-theoretic property?

[gustavolacerda.livejournal.com]

...skims some Wikipedia articles...

It seems to me that you can't have a "prime" predicate in your language. As soon as you add it, the meaning of prime changes (I'm not sure this predicate how adding would work in the models: would the model-checking involve an algorithm for primality-checking? That sounds too complex.). I imagine you can get a Feferman-hierarchy sort of thing, where you're adding predicates instead of axioms, i.e. we have a never-ending chain, in which model equivalence classes are getting finer.

[gustavolacerda.livejournal.com]

What is the natural translation?

It can't be simply replacing the |= for |-.

In SET_OF_SENTENCES |= SENTENCE notation (which I dislike), the more things on the LHS, the smaller the class of models the sentence is about.

In SET_OF_MODELS |= SENTENCE notation, the more things on the LHS, the bigger the class of models that the sentence is about.

Here's a translation I thought of:

phi_1, ..., phi_n |= psi

should be translated into

M(phi_1) ^ ... ^ M(phi_n) |= psi

where M(alpha) is the class of models where alpha holds (would you know standard notation for this?) and "^" means intersection.

This is all not to mention commas on the RHS!