N3 Syntax and Semantics

Following the conventional terminology of mathematical logic:

N3 Abstract syntax

• Terms
  • ground terms
    • URIs n (with notational abbreviations such as = for owl:sameAs and => for log:implies)
    • literals
      • strings, integers, decimals, floats, and booleans (true/false)
      • typed literals s^^n a la function terms n(s) hmm... what of ill-typed literals?
  • variables (?x, _:x and statitically distinguished URIs; also [] notation)
  • function symbols for quotation of a formula F, written { F }:
    • uri(string)
    • variable(string)
    • statement(ts, tp, to)
    • conjuction(list of term) # list may be empty.
    • generalization(tv, tf)
    • existential(tv, tf)

    Note that the quoted form of a literal is itself.

    Note that the result may have free variables, e.g. statement(?x, uri("http://example/vocab#t1), uri("http://example/vocab#t2))

• Formulas
  • Primitive formulas
    • holds(t1, t2, t3) writen t2 t1 t3.

      in particular:

      • t1 = t3
      • t1 owl:differentFrom t3
    • true (no concrete syntax, but can be quoted as {} )
  • Complex formulas (inductively defined)
    • conjunction finite set of formulas F1...n
    • implication from F to G (no concrete syntax, though {F} => {G} is analagous; see axiom schema 1 below)
    • existential quantification: @forSome _:x. F (with notational abbreviations that allow @forSome ?x. to be ommitted in certain cases)
    • universal quantification: @forAll ?x. F. (with notational abbreviations that allow @forAll ?x. to be ommitted in certain cases)

Well-formed formulas have no free variables.

Note that for each term there is a corresponding quoted term, and for each formula F there is a corresponding term for the quotation of the forumla, which we'll write here as { F }.

Semantics: Satisfaction

As usual, for a domain A, a structure/interpretation U maps each URI to A and maps holds to a subset of AxAxA, and each function symbol to a function over A.

The domain contains all strings of Unicode characters. The quoting functions (uri, variable, statement, ...) functions are 1-1; i.e. for any strings s1 and s2, if U(uri)(s1) = U(uri)(s2), then s1 = s2. The conjuction function is commutative and associative.

This is a start at discussing the semantics of quoting function symbols; need to keep goingto justify the axiom schema below.

Semantic extensions constrain interpretations further; for example, owl adds the constraint that for all x, y in D with x!=y, holds contains (U(owl:sameAs), x, x) and (U(owl:differentFrom), x, y) and does not contain (U(owl:differentFrom), x, x) nor (U(owl:sameAs), x, y).

Axiom Schemas

1. implication from holds({ F }, log:implies, { G }) to (implication from F to G).

Inference Rules

conjuction elimination (CE)

for any finite sets of formulas A and B, from conjunction A union B derive conjunction A. From conjunction {F} derive F.

conjuction introduction (CI)

from F, G, H, ... derive conjuction {F, G, H, ...}

existential introduction (EI)

from F/t derive @forSome _:x. F/t->_:x

modus ponens (MP)

from F and implication from F to G derive G

universal elimination (AE)

for any ground (or existential?) t, from @forAll ?x. F/?x derive F/t

Example

1. { ?x a Man } => { ?x a Mortal }
2. socrates a Man.
3. Show: socrates a Mortal
4. { socrates a Man } => { socrates a Mortal }
   • 1, AE ?x/socrates
5. implication from { socrates a Man } => { socrates a Mortal } to (implication from socrates a Man to socrates a Mortal)
   • schema 1
6. implication from socrates a Man to socrates a Mortal
   • 5, 4, MP
7. socratese a Mortal
   • 6, 2, MP

Example 2

1. { ?x parent [ brother ?y ] } => { ?x uncle ?y }.
2. mother s:subPropertyOf parent
3. { ?s [ rdfs:subPropertyOf ?p ] ?o } => { ?s ?p ?o }.
4. mary mother lorrie
5. lorrie brother joe
6. Show: mary uncle joe
7. { ?s [ rdfs:subPropertyOf parent ] ?o } => { ?s parent ?o }.
   • 3, AE ?p -> parent
8. { mary [ rdfs:subPropertyOf parent ] ?o } => { mary parent ?o }.
   1. 7, AE ?s -> mary
9. { @forSome _:p. mary _:p lorrie. _:p rdfs:subPropertyOf parent } => { mary parent lorrie }.
   • 7, AE ?o -> lorrie
10. implication from @forSome _:p. mary _:p lorrie. _:p rdfs:subPropertyOf parent to mary parent lorrie
    • schema 1, line 9, MP
11. mary mother lorrie. mother s:subPropertyOf parent.
    • 4, 2, CI
12. @forSome _:p. mary _:p lorrie. _:p rdfs:subPropertyOf parent
    • 11, EI
13. mary parent lorrie
    • 10, 12, MP
14. { mary parent [ brother ?y ] } => { mary uncle ?y }.
    • 1, AE ?x -> mary
15. { mary parent [ brother joe ] } => { mary uncle joe }.
    • 14, AE ?y -> joe
16. mary parent lorrie. lorrie brother joe
    • 13, 5, CI
17. @forSome _:x. mary parent _x. _:x brother joe.
    • 16, EI
18. implication from @forSome _:x. mary parent _x. _:x brother joe. to mary uncle joe
    • schema 1, line 15, MP
19. mary uncle joe
    • 18, 17, MP

Appendix: Truth Predicate and Quoting Axioms

Axioms

1. implication from (implication from F to bottom) to { F } a log:Falsehood.
2. implication from {F} a log:Truth to F. # truth predicate dequoting
3. log:Truth owl:disjointFrom log:Falsehood.
4. {[ is rdf:type of ?x ] owl:disjointWith [ is rdf:type of ?y ]} => { ?x owl:differentFrom ?y } # defn owl:disjointWith
5. ( ) log:conjuction { }. # quoting conjunction, base case.

Schemas

1. if ?L log:conjunction { F } then [ rdf:first F; rdf:rest ?L ] log:conjuction { F G } #@@
2. ( [ log:quote t1] [log:quote t2] [log:quote t3] ) log:statement { t1 t2 t3 }. #hmm... `t`
3. ( [log:quote v] { F } ) log:generalizaztion { @forAll ?v. F }
4. ( [log:quote _:v] { F } ) log:existential { @forSome _:v. F }

Appendix: Literals and Equality

While not necessary for the basic inference mechanisms above, we do assume the domain contains the integers, rationals (which decimal literals denote), floating point numbers, and strings of Unicode characters. We require that the integers are distinct from each other, but we don't constrain whether integers are equal to rationals (or strings, for that matter) for all interpretations.

Start with FOL (with equality).

• Drop LEM to avoid paradox
• Add formulas as terms. (how? quoting? HOL?)
  • quoting
  • HOL, intuitionistic type theory
    • strongly normalizing? not turing complete; e.g. coq/calculus of constructions
  • impredicative? (not constructive enough for the intuitionists?)