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)

**implies**: Statement, Statementimplies(x, y) = if x then y

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

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

- implication(
`A.L`,`x`) - if

- implication(
**negation**: Statement -> Statementnegation(x, y) ::= y is the negation of x

**conjunction**: List -> Statementconjunction(l, s) ::= s is the conjunction of the statements in the list s

- 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`)

- first(

- conjuction(

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.

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.

- negation(false, true)

Dan Connolly

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