# 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@@

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

## Connectives

• implies: Statement, Statement

implies(x, y) = if x then y

• forall: Statement, variable

forall(x, v) = x holds for all v; aka v is universally quantified in x

## 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

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)

Dan Connolly
\$Revision: 1.21 \$ of \$Date: 2000/08/01 16:32:41 \$ by \$Author: connolly \$