Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
I have seen use of , and somewhere use of ; when defining context :
$$\dfrac{\phi \ , \ \Gamma \ \vdash } {} $$
somewhere else i have seen :
$$\dfrac{\phi \ ; \ \Gamma \ \vdash } {} $$
What is the difference between both. I have read something like extension of context. Then what second one means.
You'd have to check whatever you're reading, but the way I've most commonly seen it used is to separate different contexts. The rules will then behave differently if a variable or formula is in one context versus another. mobileink mentioned substructural logics which are often formulated with a context for linear variables and a different context for non-linear variables.
However, ; could simply be being used to separate other things so you don't confuse it with context extension. Or it could just be part of a term. Or it could be some operator on contexts distinct from context extension. Or it could just be this author decided to use ; instead of , for context extension. Again, what it means is whatever it is defined to mean, which may be nothing on its own. For example, used to separate different contexts, it's just part of the syntax of a judgement, e.g. the judgement may be 3-ary relation $(-);(-)\vdash (-)$ in which case it makes no more sense to ask what ; means than it would to ask what $.$ means in $\forall x.P(x)$. See my answer to a similar question for more elaboration on this.
They can express different ideas of what "together with" means. See Substructural Logics
For example, in many logics, there is a structural rule that says you can go from $A;B\vdash C$ to $B;A\vdash C$ (often call the rule of Exchange). Another rule says you can go from $A;A\vdash B$ to $A\vdash B$ (rule of Contraction). Etc. They're called structural rather than logical rules because they set the meaning of (non-logical) punctuation marks like ";" in these examples. Real-world analogs: suppose A and B represent events in the first example, and $A;B$ means "event A, then event B", and the rule of Exchange does not hold. Note that we could add a second mark $A,B$ to express that both events occurred in either order.
In the second example, suppose A means "one dollar" and B means "cup of coffee", so $A;A\vdash B$ means that two dollars will get you a cup of coffee, and the rule of Contraction does not hold. So in this case the informal notion of a resource that can be consumed can be expressed as a purely formal Structural Rule.
By defining different punctuation marks and selecting various structural rules you get lots of different ways of interpreting "A together with B"; logics that can be used to model lots of different things.
