Expressions

Expressions allow the programmer to combine expression values to obtain new expression values. Expression operations include deduction rules.

• Expression Values
• Variables
• Object Substitution
• Pipe Operator
• Deduction
• Sentence Constants
• Predicate Definitions
• Expression Brackets
• Built-in Functions
  • left
  • right
  • and
  • or
  • iff
  • trivial
  • expand
  • substitute
  • branch

Expression Values

Expressions evaluate to expression values. There are three types of expression values: verified sentences, unverified sentences, and object values.

Verified sentences represent results that the programmer has proven to be true. Verified sentences can generally only be deduced from other verified sentences. Verified sentences may have unbound predicates (see Axiom Schema and Proof Schema), but will never have unbound variables.

Unverified sentences are generally substituted as a predicate in a sentence with unbound predicates. An expression value containing any unverified sentence can be created using sentence constants.

Object expression values are used for object substitution. These expression values only store a reference to an object. The object refered by an object expression value will never be an object bound by a quantifier in a sentence. An object expression value is created by referring to the object by name. For example, if an object named OBJ belongs to a context called con, then the expression con.OBJ evaluates to an object expression value referencing that object.