## Overview

For the moment, please treat this as a kind of proof-of-concept. It's intended to have enough detail to make the design concept clear, without bogging down too much in details at this point. For example, I'm disregarding literals for now, because they are inessential to the basic deductive system. I guess the basic idea is that we ought to be able to use some variation of Natural Deduction to express just about everything needed to define RDF and RDFS clearly and concisely. Among other things this should allow us to eliminate stuff like "instance of a graph" and "lean graph" (described in RDF Semantics); the former is just not needed (being handled by derivation rules involving variables), while the latter seems to correspond to the concept of normalization, in the sense of a set (sequence) of independent triads, no one of which can be derived from the others. To get started I'm just sketching out a basic calculus to suggest what shape the final thing would have.

Also, the notes amount to a sort of tutorial/cry-for-help in that I try to explain what I'm doing and why, rather than just stating definitions as one might do in a formal definition.

Also, the notes amount to a sort of tutorial/cry-for-help in that I try to explain what I'm doing and why, rather than just stating definitions as one might do in a formal definition.

## Meta-language

- Constants:
- All constants in the object language are also constants in the meta-language.
- \(\exists\): existential quantifier
- \(\land\): logical and
- \(\phi\): a formula
- \(\Phi\): set of formulae
- \(\vdash\): derivation relation
- \(\models\): entailment (logical consequence) relation
- \(\leadsto\); informal justification
- \(\Rightarrow\): rewrite relation; like derivation, only from object language to meta-language.
- Formulae
- Quantification
- \(\exists x.\!x\phi\) has its usual FOL meaning.
- Inference. We treat inference as a genus with three species:
- \(\Phi \vdash \phi\): the formulae \(\Phi\)
*derives*the formula \(\phi\); \(\phi\) is*derivable*or*deducible*from \(\Phi\) - \(\Phi \models \phi\): the formulae \(\Phi\)
*entail*the formula \(\phi\); \(\phi\) is a (logical)*consequence*of \(\Phi\). - \(\Phi \leadsto \phi\): the meanings of \(\Phi\)
*justify*or*lead to*the meaning \(\phi\); \(\phi\)*follows from*of \(\Phi\) (semantically). (**NB**: this is an informal notion we will use to explicate the consequence relation.)

Note that the meta-language contains a few constants from First-Order Logic (FOL): \(\exists, \land, \vdash, \models\). They allow us to say useful things about object languages and how they work.

*As it stands it is not complete; this is just enough to get the ideas across.*

##
**\(\displaystyle\mathbb{T}_\varnothing\) (T-null)**

**Symbols****Constants**: \(\{A\ldots Z\} \cup \{a,\ldots z\}\cup \{., ``,"\}\)**Term calculus**: every symbol is a term.**Formula calculus**:- If \(A\), \(B\), and \(C\) are terms, then \(ABC\) is a formula.
- If \(A\), \(B\), and \(C\) are terms, then each of the following is a formula:
- \(xBC\), \(AxC\), \(ABx\)
- \(xyC\), \(xBy\), \(Axy\)
- \(xyz\)
- If \(ABC\) and \(DEF\) are formulae, then \(ABC, DEF.\) is a formula.

So far, \(\mathbb{T}_\varnothing\) - call it

*T-null*- is a minimal language to say the least. It has a very limited number of forms, and it has no semantics whatsoever. In other words, it's not really a language at all; we could call it an uninterpreted*calculus*, except that you can't do any calculating in it. However we care to classify it, we can attach any semantics we care to it by assigning meanings to its symbols, but since no such assignments are*fixed*the result has no stability - you can always change any assignment, so there isn't much point in making one in the first place.
We can express this in terms of expressive

*strength*in a way that will turn out to be useful as we proceed. \(\mathbb{T}_0\) is the*weakest*possible language, because it has no expressive stability. You can't say anything in it that is guaranteed to mean the same thing under different interpretations.
\(\mathbb{T}_\varnothing\) corresponds to RDF without blank nodes and literals.

Formulae like \(ABC\) obviously correspond structurally to RDF triples; to maintain a clean separation between this language and RDF languages, we will call such forms

*triads*. We might occasionally be tempted to call the constants*trions*, but we hope not.##
**\(\displaystyle\mathbb{T}_0\) (T-basic)**

What can we do to remedy this sorry state of affairs? Let's start by giving the speakers of this little language the ability to express things like "somebody killed Caesar" and "Cicero said something". While we're at it, let's allow them to say "Somebody killed Caesar and Cicero said something".

As to "somebody" ("something", etc.): the usual way this is done is by

But since we want to track RDF, whose symbol set does not include anything corresponding to \(\exists\), we will take a different tack, one that corresponds to the way things are done in the RDF ecology: instead of

There are two ways to do this. One is to pick some constants that are already in the language and give them a fixed meaning. This is the technique we will use later on when we accomodate the various "entailment regimes" of RDF. This kind of strengthening is equivalent to extending the set of constants in the language with fixed meanings (call them the

The other way to strengthen a language, which we will now use, is to

The new meta-language rules fixing the meanings of formulae containing variables will be expressed as

As to "somebody" ("something", etc.): the usual way this is done is by

*extending*the language. One adds some symbols and the axioms that fix their meanings. In this case, we could add the existential quantifier \(\exists\) to the object language and, if we wanted to be fastidious, define rules in the meta-language to determine its meaning ("there exists"). This would allow users of the language to "say" things of the form \(\exists x.\!xBC\); if you set B = killed and C = Caesar, and this expresses "somebody killed Caesar".But since we want to track RDF, whose symbol set does not include anything corresponding to \(\exists\), we will take a different tack, one that corresponds to the way things are done in the RDF ecology: instead of

*extending*the language, we*strengthen*it.Note: there's more to say about extending/strengthening; in particular such changes must be conservative, that is, they cannot break what is already there. More generally: we have a language, a world, and a stable but partial interpretation. Fix any two and vary the third.

There are two ways to do this. One is to pick some constants that are already in the language and give them a fixed meaning. This is the technique we will use later on when we accomodate the various "entailment regimes" of RDF. This kind of strengthening is equivalent to extending the set of constants in the language with fixed meanings (call them the

*fixed constants*for short). Having more fixed constants means more expressive power; it allows the speaker to say more (kinds of) things.The other way to strengthen a language, which we will now use, is to

*reclassify*some subset of its constants. Notice that \(\mathbb{T}_\varnothing\) contains only one kind of symbol. We will change the language not by adding symbols, but by reclassifying the symbols \(x, y,\) and \(z\) into a new class of*Variables.*Unfortunately, that alone would have no effect; something additional needs to be introduced in order to make such reclassification meaningful. In this case, that means adding rules to the meta-language that fix the meanings of the formulae in which they appear. That last clause - "meanings of the formulae" - is critical, since with this technique we do*not*fix the meanings of the variable symbols themselves. On the contrary, quantified variables of this sort will*never*be assigned a determinate meaning. Their meaning is essentially tied up with the meaning of quantification, which in turn is essentially connected with the composite forms in which the variables appear.The new meta-language rules fixing the meanings of formulae containing variables will be expressed as

*rewrite*rules. A rewrite rule is essentially the same as a syntactic derivation or transformation rule; it says how one form can be mapped to another. The difference is that derivation rules work*within*the object language (i.e. they're closed), whereas rewrite rules take forms from the object language to forms in the metalanguage.

**Symbols****Constants**: \(\{A\ldots Z\} \cup \{a,\ldots z\}\!\setminus\!\{x, y, z\} \cup \{., ``,"\}\)**Variables**: \(\{x, y, z\}\)**Meta-language**~~Rewrite~~Sublimation Rules- \(ABC\Rightarrow ABC\)
- \(, \Rightarrow\land\)
- \(xBC \Rightarrow \exists x.\!xBC\) and similarly for AxC and ABx. We treat any formula in the object language that contains variables as an existentially quantified formula.
- \(xyC \Rightarrow \exists x\exists y.\!xyC\).
- \(xyz \Rightarrow \exists x\exists y\exists z.\!xyz\).
- \(xBC, xEF \Rightarrow \exists x.\!(xBC\land xEF)\) and similar for two and three variables.
- \(xBC, yEF \Rightarrow \exists x\exists y.\!(xBC\land yEF)\) and similar for two and three variables.
- etc. (existential rewrites shown by example rather than general rule)

CAVEAT:it may be tempting to view the rewrite rules as a kind of semantic interpretation. That would be a tragic mistake. They are purely syntactic rules.

For example, if we have \(ABC, xEF\), rewrite rules 1-3 ``sublimate'' this to \(ABC\land\exists x.\!xEF\).

Note: as it stands this calculus is not complete, because it does not handle the scope of quantification for all cases. For example it does not tell us how to get from \(xBC, DEF, GHy\) to \(\exists x\exists y.\!(xBC\land~DEF\land~GHy)\). But I hope what's there is sufficient to get the idea across.

This is a stronger language, but it still lacks a highly desirable bit of logic: it does not yet support any form of inference. We cannot go from a premise to a conclusion. In particular, even though we know how to construct (legal) formulae containing ',' and \(\land\), nothing tells us when it is appropriate to do so. For example, if you know that grass is green, and you also know (separately, as it were) that snow is white, then you ought to be able to package those two bits of knowledge into a single whole and say "grass is green and snow is white". Intuitively that's obviously what we do; but for a calculus, we need an explicit rule. Similarly for \(\exists\): if we know the specific person (thing) that exists, then we can say that

*some*person or thing exists. But we need a formal rule for this.
We could strengthen \(\mathbb{T}_0\) and call it a new language, but in the interest of conciseness let's just define \(\mathbb{T}_0\) as including support for a basic form of inference. It is intuitively obvious that if "Brutus killed Caesar" is true, then so is "somebody killed Caesar". Going from the former to the latter is a basic species of inference. Similarly, if you know "Somebody killed Caesar", and you also know (perhaps you were told) that Brutus killed Caesar, then you no longer need "Somebody killed Caesar". Since Brutus is somebody, you lose nothing if you discard "Somebody killed Caesar" and retain "Brutus killed Caesar". This too is a form of inference.

To support this in \(\mathbb{T}_0\) we add inference rules governing the

To support this in \(\mathbb{T}_0\) we add inference rules governing the

*introduction*and*elimination*of terms like "somebody". To start, we have only two such terms: \(\exists\) ("there exists") corresponding to "somebody" (or "something", etc.) and \(\land\) ("and")*.*[In the case of \(\exists\) we're abusing the terminology a little bit, since \(\exists\) is not part of the object language. Our introduction rule will actually license introduction of variables in triad constructions, which in turn are mapped to \(\exists\) expressions in the meta-language.**\(\land\)-Introduction: \(\displaystyle{\Phi\quad \phi\over \Phi,\ \phi}\)****\(\land\)-Elimination:****\(\displaystyle{\Phi,\ \phi\over\Phi}\)****\(\displaystyle{\Phi,\ \phi\over\phi}\)****\(\exists\)-Introduction**- \(ABC\vdash xBC\) ...similar for \(AxB, ABx\) etc.
- \(ABC\vdash xyC\) ...
- \(ABC\vdash xyz\)
**\(\exists\)-Elimination**- \({ABC\quad xBC\over ABC}\qquad or\qquad {\Phi\quad \Phi x\over\Phi} \)

RDF: \(\exists\)-Elimination is basically the counterpart to "instancing" in RDF-Semantics.

**
**NOTE: I'm not sure how to write \(\exists\)-Elimination yet. Maybe something like one of these?TODO: explicate significance of elimination rules for readers unfamiliar with this style of logic.

[NB: if we were being really fastidious we would give each of these rules a distinct name, but that seems like too much bother for now. And why not just call them \(\exists\)\!I rules, since that's what they mean?]

Alternative format:CAVEAT: this works fine for one triad, but does not work for a sequent of triads. The single triad rule would allow e.g. \(ABC,ADE\vdash xBC,yDE\). We need a rule to express the requirement of uniform substitution, e.g. \(ABC,ADE\vdash xBC,xDE\).

\(ABC\over xBC\) \(ABC\over AxC\) \(ABC\over ABx\) \(ABC\over xyC\) \(ABC\over Axy\) \(ABC\over xBy\) \(ABC\over xyz\)

[NB: can we generalize? E.g. \(\Phi a\over\Phi x\) , reading \(\Phi a\) to mean a collection of triads containing one or more constants a so the rule says replace 'em all with a variable. For a single triad, \(\phi a\over\phi x\).]

The intuitive way to interpret such rules is simple: if you have \(ABC\), then you are licensed to

*introduce*a var in place of any of the constants. So "introduce a var" is the formal counterpart of "say 'somebody' (instead of 'Brutus')". [NB: "Var-introduction" actually doesn't quite work, since it involves substitution, but it's close enough.]
[TODO: explicate: are the inference rules part of the language definition, or are they in the meta-language? Intuitively they seem to be like the rules of the formula calculus; but they use the symbol \(\vdash\), which we do not want to admit to the language. So they must be part of the meta-language. Remember, the meta-language "includes" the object language.]

Historical note: this rule is cribbed directly from the great Gerhard Gentzen, who first came up with the idea of introduction and elimination rules as determining the meanings of the logical constants. But his \(\exists\)-Introduction rule is different than our

*Var-Introduction*rule, since his object language included they symbol \(\exists\) and ours does not. His looked like something this: \[{Pa\over\exists x.Px}\ {\scriptstyle\!\exists\!-\!I}\]
where the \(\exists\!-\!I\) on the right names the rule.

Normal Form

Informally, a collection of triads is in normal form if the triads are independent; that is, if none of them can be derived from the others.Normal Form

RDF: as far as I can tell, the concept of "leanness" introduced in RDF-Semantics boils down to normal form. It is expressed in terms of graphs, instances, and proper subgraphs, but what a "lean" graph amounts to is one whose triples are independent - the semantic domain counterpart of normal form.

**Literals**

**If we want our little Triad calculus to reflect RDF, we obviously need to support literals. I'll get to it eventually.**

##
**\(\displaystyle\mathbb{T}_1\) (RDF-entailment)**

##
**...todo**

##
**\(\displaystyle\mathbb{T}_2\) (RDFS-entailment)**

**...todo**

## Commentary:

So far, this has nothing to do with RDF per se, except insofar as it reflects its structure. But the symbol set has been chosen with an eye toward the RDF family of languages we will define using this calculus. Informally:

- Our set of constant symbols \(\{A, B,\ldots\}\cup \{a, b,\ldots\}\) corresponds to the set of IRIs
- To define a logical language corresponding to RDFS, OWL, etc. we will fix the meanings of subsets of the constants, e.g. \(t\) corresponds to \(\mathrm{rdf:type}\)
- Variable symbols will be used to capture the RDF concept of ``blank node''.

We intentionally limit the symbol set so that we can write triads concisely. If we our term calculus allow e.g. "Foo" as a term, we would need to be able to write "Foo Bar Baz". Which isn't all that bad, but ABC is a whole lot more concise, and since we're only concerned with inference we don't need to be able to construct human-readable terms like "Brutus". This is supposed to be a meta-language, after all.

- \(AtB, BkC\vdash AtC\).

Hi Gregg,

ReplyDeleteLove it! Suggestion: use "sublimation rule" instead of "rewrite rule", since it lifts up to the meta level. Also more amusing.

-Gregg

Also, "extending the set of fixed constants" suggests adding new symbols to the language; at the least, it's ambiguous, and could lead to "which sense of 'expanding' do you mean?" questions in dialog. Try "enlarging" or "expanding" by including/incorporating existing non-fixed constants.

Delete