2020-06-18 8:41:45 (GMT)
I'm looking for a good expression for the following. I'd like to say something like "clause set N is compatible with theory T if whenever N is satisfiable, so is N T." I'm guessing "compatible with" is not standard (and perhaps even confusing). What would be the best term?
2020-06-18 8:45:41 (GMT)
N is T-satisfiable?
2020-06-18 8:47:7 (GMT)
(but that might be terminology used in SMT context only)
2020-06-18 8:49:26 (GMT)
I think what Jasmin wants is the reverse, in which case, if I understand the problem correctly, T is simply a consequence of N.
2020-06-18 8:50:16 (GMT)
No, not all models of N need to be models of T, only some of them.
2020-06-18 8:50:18 (GMT)
How about "T is consistent with N"?
2020-06-18 8:52:25 (GMT)
For example, the axiom of choice is consistent with Zermelo–Fraenkel set theory.
2020-06-18 8:55:45 (GMT)
Right, what Alex said. :)
2020-06-18 8:56:1 (GMT)
I had "T is independent with N" at some point but that was too strong.
2020-06-18 8:56:33 (GMT)
But my only worry is that "consistent" is by many (most?) people a syntactic/proof-theoretic property.
2020-06-18 8:57:5 (GMT)
That's how I learned it, and that's also how e.g. Jeremy Avigad uses it (I recently had the discussion with him).
2020-06-18 8:57:58 (GMT)
Mathias's N is T-satisfiable makes sense.
2020-06-18 8:58:17 (GMT)
In my case my theory is a single axiom, so it might sound a bit strange unless I define the termology.
2020-06-18 9:3:13 (GMT)
Wouldn't it be "T is N-satisfiable" e.g. T is true in all models of N? In your setting it seems that you don't care about the case where N is unsatisfiable. In my understanding "N is T-satisfiable" means that whenever T is satisfiable so is N U T. Or am I getting things mixed up.
2020-06-18 9:7:15 (GMT)
Giles, you're right. :)
2020-06-18 9:7:55 (GMT)
For the record, it took me several hours to converge towards the right formulation (in my original post). I'm not too surprised to see wrong variants emerge (and confuse me again).
2020-06-18 9:8:18 (GMT)
Wait, no, Giles, that's not right. :S
2020-06-18 9:8:38 (GMT)
I don't want T to be true in all models of N; it's enough if it's true in some. That's the point Alex made.
2020-06-18 9:9:11 (GMT)
But Mathias's version is right only if we phrase it as follows "N is T-satisfiable whenever N is satisfiable".
2020-06-18 9:13:46 (GMT)
Chat is a very thought-provoking tool. Unfortuately, for me, the thoughts always occur five seconds after I've posted something. ;)
2020-06-18 9:33:56 (GMT)
But I miswrote... I think... I meant to write 'some' instead of 'all'... I'm just used to T having one model so it doesn't matter!
2020-06-18 9:35:57 (GMT)
Right. I guess it makes sense, but it really messes with my brain to put the N as the theory. :S