W3C HyperRDF

First Order Predicate Calculus

obsoletes 23 Jun FOPC stuff

see also: CS 540 Lecture Notes: First-Order Logic by Charles R. Dyer dyer@cs.wisc.edu, larch@@, algernon@@

see also: Glossary of First-Order Logic

also: Swell trait, a specification of this logic using larch as a metalogic, (background formal system trait)

Generators

• implication: List -> Statement

  implication(l, s) = s is the implication of the statements in l (i.e l[1] -> (l[2] -> (l[3] -> l[4]))))

  implication(empty, true)

  implication(A.L, x)

  if

  • first(A.L, A)
  • rest(A.L, L)
  • implication(L, Limp)
  • predicate(x, implies)
  • subject(x, A)
  • object(x, Limp)

• negation: Statement -> Statement

  negation(x, y) ::= y is the negation of x

  negation(x, y)

  if

  • predicate(y, implies)
  • subject(y, x)
  • object(y, false)

• conjunction: List -> Statement

  conjunction(l, s) ::= s is the conjunction of the statements in the list s

  conjuction(empty, true)

  conjuction(A.L, notAimpliesNotLc)

  if

  • first(A.L, A)
  • rest(A.L, L)
  • conjunction(L, Lc)
  • negation(Lc, notLc)
  • implication(notLc.AimpliesNotLc, A)
  • first(notLc.AimpliesNotLc, notLc)
  • second(notLc.AimpliesNotLc, AimpliesNotLc)
  • negation(AimpliesNotLc, notAimpliesNotLc)

Level-breaking Rules

whence comes the raging debate as to whether this is actually first-order logic or higher-order logic. See also: TimBL's design notes on logic, Hilog in XSB.

p(s, o)

if

• implies(true, x)
• subject(x, s)
• predicate(x, p)
• object(x, o)

Tim pointed out that this rule, combined with the liar's paradox and the "p or not p" axiom leads to inconsistency.

The liars paradox can be expressed as x such that subject(x, x), predicate(x, implies), object(x, false).

We can prevent this if we assume/assert that subject/predicate/object are acyclic. In particular: that the partOfSentence(x, y) property which is defined as subject(x, y) \/ predicate(x, y) \/ object(x,y) is acyclic.

Hmm... KIF seems to have this mechanism too:

As we have seen, it is possible in KIF to write expressions that describe KIF sentences. As it turns out, there is also a way to write sentences that assert the truth of the sentences so described. The effect of adding such metalevel sentences to a knowledge base is the same as directly including the (potentially infinite) set of described sentences in the knowledge base.

-- 10.3 Changing Levels of Denotation of Knowledge Interchange Format

Their wtr mechanism is nifty. I think I'll try another RDF logic based on KIF.

Definition of true:

negation(false, true)