2
$\begingroup$

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.

$\endgroup$
5
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ @DavidRicherby Added some detail, I hope enough to convey the idea. $\endgroup$ – user48832 Apr 7 '16 at 18:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.