#$implies implies **COMMENT NOT REVIEWED** **GAFs NOT REVIEWED**

A #$LogicalConnective that represents the material implication relation in #$CycL. It is a #$FixedArityRelation, taking two #$ELSentence-Assertibles as arguments. (#$implies ANTE CONSEQ) means that either the sentence ANTE is false, or the sentence CONSEQ is true (possibly both); equivalently, it is not the case that ANTE is true and CONSEQ is false. Cyc assertions that begin with #$implies are used during inference: both modus ponens and modus tollens. (Cf. by contrast #$sentenceImplies -- a mere predicate primarily intended to be used for rules that quantify over #$CycL formulas.

guid: bd5880f8-9c29-11b1-9dad-c379636f7270

direct instance of: #$MacroRelation #$BinaryRelation #$LogicalConnective #$Individual

#$not not

An instance of both #$LogicalConnective and #$UnaryRelation. which takes an instance of #$ELSentence-Assertible as its argument. (#$not SENT) is true if and only if SENT is false (and false if and only if SENT is true).

guid: bd5880fb-9c29-11b1-9dad-c379636f7270

direct instance of: #$UnaryRelation #$LogicalConnective #$Individual

#$and and (relationship) (mathematical concept)

A #$LogicalConnective that represents conjunction in #$CycL. It is a #$VariableArityRelation, taking an arbitrary number of #$ELSentence-Assertibles as arguments. (#$and P Q ... Z) is true if and only if all of the sentences P, Q, ..., and Z are true.

guid: bd5880f9-9c29-11b1-9dad-c379636f7270

direct instance of: #$AssociativeRelation #$CommutativeRelation #$VariableArityRelation #$LogicalConnective #$Individual

#$or or

A #$LogicalConnective that represents disjunction in #$CycL. It is a #$VariableArityRelation, taking an arbitrary number of #$ELSentence-Assertibles as arguments. (#$or P Q ... Z) is true if and only if at least one of the sentences P, Q, ..., or Z is true.

guid: bd5880fa-9c29-11b1-9dad-c379636f7270

direct instance of: #$AssociativeRelation #$CommutativeRelation #$VariableArityRelation #$LogicalConnective #$Individual

#$forAll for all **COMMENT NOT REVIEWED** **GAFs NOT REVIEWED**

The predicate #$forAll is Cyc's version of the universal quantifier of predicate calculus (i.e., the operator symbolized in one common notation by an upside-down `A'). As its two arguments, #$forAll takes a variable (which is an instance of #$ELVariable) and an instance of #$ELSentence-Assertible, respectively. (#$forAll VAR FORM) means that FORM is true whenever all the occurrences of the variable VAR in the formula FORM are replaced by any object in the Cyc universe. For example, to say that every person is a mammal, we could assert: (#$forAll ?X (#$implies (#$isa ?X #$Person) (#$isa ?X #$Mammal). In addition, CycL follows a convention that allows #$forAll to be omitted; that is, when no explicit quantifier is used, seemingly unbound variables inside formulas are assumed to be universally quantified. With that convention, the sample assertion could be written more compactly as: (#$implies (#$isa ?X #$Person) (#$isa ?X #$Mammal). [Developer-level footnote: There are many `flavors' of quantification `on the market' these days; here is how the Cyc system currently handles axioms that involve #$forAll: When processing an FI-ASK about whether an assertion of the form (#$forAll VAR FORM) is true or not, Cyc determines extensionally whether or not any known VAR (anything in the knowledge base) could make FORM false. When processing an FI-PROVE about whether an assertion of the form (#$forAll VAR FORM) is true or not, Cyc tries to construct an intensional proof (at least at a default-true level) that FORM must be true regardless of what VAR is ever inserted therein. When processing an FI-ASSERT in which a user or program tells Cyc that an assertion of the form (#$forAll VAR FORM) is true, Cyc records it intensionally so that it can later serve as part of an intensional proof, when some future FI-PROVE request is processed.]

guid: bd5880f7-9c29-11b1-9dad-c379636f7270

direct instance of: #$BinaryRelation #$Quantifier #$Individual

#$thereExists there exists **COMMENT NOT REVIEWED** **GAFs NOT REVIEWED**

The predicate #$thereExists is Cyc's version of the existential quantifier of predicate calculus (i.e., the operator symbolized in one common notation by a backwards 'E'). As its two arguments, #$thereExists takes a variable (which is an instance of #$ELVariable) and an instance of #$ELSentence-Assertible, respectively. (#$thereExists VAR FORM) means that FORM is true in at least one case (and possibly more) in which all occurrences of the variable VAR in FORM are replaced by an object in the Cyc universe. For example, to say that every person has a mother, we could assert: (#$forAll ?PER (#$implies (#$isa ?PER #$Person) (#$thereExists ?MOM (#$mother ?MOM ?PER)))). [Developer-level footnote: There are many `flavors' of quantification `on the market' these days; here is how the Cyc system currently handles axioms that have #$thereExists in the arg0 position: When processing an FI-ASK about whether (#$thereExists VAR FORM) is true or not, Cyc determines extensionally whether or not any known VAR (anything in the knowledge base) satisfies FORM (makes it true.) When processing an FI-PROVE about whether (#$thereExists VAR FORM) is true or not, Cyc tries to construct an intensional proof (at least at a default-true level) that there must exist some value of VAR --- which may or may not already be known in the KB -- for which FORM must be true. When processing an FI-ASSERT in which a user or program tells Cyc that (#$thereExists VAR FORM) is true, Cyc records the assertion intensionally so that it can later serve as part of an intensional proof, when some future FI-PROVE request is processed. It does this by creating a new #$SkolemFunction (q.v.). When modus ponens is used with a rule of the form (#$implies ANTECEDENT (#$thereExists VAR FORM)), and the formula ANTECEDENT is true, then Cyc will generate a new term for VAR, add that to its language, and assert that the new term satisfies FORM.]

guid: bd5880f6-9c29-11b1-9dad-c379636f7270

direct instance of: #$ExistentialQuantifier #$BinaryRelation #$Individual

#$thereExistAtLeast there exist at least **COMMENT NOT REVIEWED** **GAFs NOT REVIEWED**

An #$ExistentialQuantifier and a specialized (albeit higher #$arity) form of #$thereExists (q.v.). (#$thereExistAtLeast NUM VAR SENT) means that there are at least NUM distinct objects which, when taken as the value of the #$ELVariable VAR in the #$ELSentence-Assertible SENT, make SENT true (where NUM is an instance of #$PositiveInteger). If VAR does not in fact appear in SENT, then (#$thereExistAtLeast NUM VAR SENT) will have the same truth value as SENT (whatever that is). See also #$thereExistAtMost, #$thereExistExactly.

guid: c10af5e7-9c29-11b1-9dad-c379636f7270

direct instance of: #$ExistentialQuantifier #$TernaryRelation #$Individual

#$thereExistAtMost there exist at most

An #$ExistentialQuantifier and a specialized (albeit higher #$arity) form of #$thereExists (q.v.). (#$thereExistAtMost NUM VAR SENT) means that there are at most NUM distinct objects which, when taken as the value of the #$ELVariable VAR in the #$ELSentence-Assertible SENT, make SENT true (where NUM is an instance of #$PositiveInteger). If VAR does not in fact appear in SENT, then (#$thereExistAtMost NUM VAR SENT) will have the same truth value as SENT (whatever that is). See also #$thereExistAtLeast, #$thereExistExactly.

guid: c10af932-9c29-11b1-9dad-c379636f7270

direct instance of: #$ExistentialQuantifier #$TernaryRelation #$Individual

#$thereExistExactly there exist exactly

An #$ExistentialQuantifier and a specialized (albeit higher #$arity) form of #$thereExists (q.v.). (#$thereExistExactly NUM VAR SENT) means that there are exactly NUM distinct objects which, when taken as the value of the #$ELVariable VAR in the #$ELSentence-Assertible SENT, make SENT true (where NUM is an instance of #$PositiveInteger). If VAR does not in fact appear in SENT, then (#$thereExistExactly NUM VAR SENT) will have the same truth value as SENT (whatever that is). See also #$thereExistAtLeast, #$thereExistAtMost.

guid: c10ae7b8-9c29-11b1-9dad-c379636f7270

direct instance of: #$TernaryRelation #$ExistentialQuantifier #$Individual

#$True true (mathematical concept) **COMMENT NOT REVIEWED** **GAFs NOT REVIEWED**

An instance of #$TruthValue. #$True is logical truth in Cyc; this is the abstract logical notion--not to be confused with Lisp's T, nor with the English word `true'.

guid: bd5880d9-9c29-11b1-9dad-c379636f7270

direct instance of: #$TruthValue #$Individual

#$False false **COMMENT NOT REVIEWED** **GAFs NOT REVIEWED**

An instance of #$TruthValue. #$False is logical falsehood in Cyc; this is the abstract logical notion--not to be confused with Lisp's NIL, nor with the English word `false'.

guid: bd5880d8-9c29-11b1-9dad-c379636f7270

direct instance of: #$TruthValue #$Individual

#$equals equals

The binary identity relation. (#$equals THING1 THING2) means that THING1 and THING2 are numerically (as opposed to qualitatively ) identical, i.e. they are one and the same thing. A sentence of the above form is true if and only if the terms occupying the two argument-places of `#$equals' denote the same thing.

guid: bd5880c9-9c29-11b1-9dad-c379636f7270

direct instance of: #$StrictlyFunctionalSlot #$DefaultMonotonicPredicate #$EquivalenceRelation

#$evaluate evaluate (binary predicate) (CycL predicate) (relationship) **COMMENT NOT REVIEWED** **GAFs NOT REVIEWED**

If the arg1 of #$evaluate is a variable, (#$evaluate VAR EXPRESSION) is satisfied by an HL module which evaluates EXPRESSION and binds VAR to the result. For example, (#$evaluate ?SUM (#$PlusFn 1 2)) would bind ?SUM to 3. If the arg1 is a fully-bound expression, then the HL module checks to see if the arg2 evaluates to the arg1. For example, asking (#$evaluate 3 (#$PlusFn 1 2)) returns #$True.

guid: c03afa6d-9c29-11b1-9dad-c379636f7270

direct instance of: #$BinaryPredicate

#$different having a distinct identity from

A variable-arity predicate (see #$VariableArityRelation) that is used to state the non-identity of two or more things. (#$different THING1..THINGn) means that for any THINGi and THINGj (where 0 <= i <= n, 0 <= j <= n, and i =/ j), THINGi is not identical with THINGj. That is, each of THING1, ..., THINGn is distinct from all of the others. Cf. #$equals.

guid: bd63f343-9c29-11b1-9dad-c379636f7270

direct instance of: #$EvaluatablePredicate #$ComparisonPredicate #$CommutativeRelation #$VariableArityRelation

direct specialization of: #$differentSymbols