Next: Options, Previous: Introduction, Up: Top

## 2 Terms

Biconditional
  A biconditional is a connective that connects two sentences, denoted by ‘`<->`’. A biconditional claims that ‘`sentence a if and only if sentence b`’ is a new sentence. A biconditional can be inserted in Aris using the key combination `CTRL+5` (see Keyboard Shortcuts).
Conclusion
  A conclusion is a sentence that is derived from a combination of other sentences and a rule. A focused conclusion will be highlighted in cyan. A conclusion has a set of references associated with it, which are highlighted in violet.
Conditional
  A conditional is a connective that connects two sentences, denoted by ‘`→`’. A conditional claims that ‘`if sentence a, then sentence b`’ is a new sentence. A conditional can be inserted in Aris using the key combination `CTRL+4` (see Keyboard Shortcuts).
Conjunction
  A conjunction is a connective that connects two or more sentences, denoted by ‘`^`’. A conjunction claims that ‘`sentence a and sentence b`’ is a new sentence. A conjunction can be inserted in Aris using the key combination `CTRL+7` (see Keyboard Shortcuts).
Connective
  A connective is a logical symbol that connects one or more sentences. The connectives used in system psi are conjuction (‘`^`’), disjunction (‘`v`’), negation, (‘`~`’), conditional (‘`→`’), and biconditional (‘`<->`’). In addition, system psi recognizes the one-place connectives of the tautology (‘`T`’) and the contradiction (‘`!`’).
Contradiction
  A contradiction is a zero-place connective that stands on its own, denoted by ‘`!`’. A contradiction represents something that is always false. A contradiction is only used with the boolean rules (see Boolean Rules), and can be inserted using the key combination `CTRL+6`.
Disjunction
  A disjunction is a connective that connects two or more sentences, denoted by ‘`v`’. A disjunction claims that ‘`sentence a or sentence b`’ is a new sentence. A disjunction can be inserted in Aris using the key combination `CTRL+\` (see Keyboard Shortcuts).
Evaluate
  To evaluate a sentence means different things depending on the type of sentence. At the very least, evaluation checks the sentence for text errors, i.e. mis-matched parenthesis, etc. Evaluating a conclusion checks that the sentence's text logically follows from the given references and its rule. Evaluating a goal means checking the corresponding proof for a sentence with this exact same text. To evaluate a sentence use the key combination `CTRL+E` (see Keyboard Shortcuts).
Evaluation Value
  An evaluation value is the value that appears to the right of a sentence's text entry. It can either be ‘`` ’, ‘`T`’, ‘`F`’, ‘`*`’, ‘`#`’, or ‘`?`’. ‘`` ’ means that the sentence is awaiting evaluation, except in the case of premises, where this could also mean that there are no errors with it. ‘`T`’ means that either the conclusion logically follows from its references and rule, or that the goal has been found in the corresponding proof. ‘`F`’ means that either the conclusion does not logically follow from its references and rule, or that the goal has not been found in the corresponding proof. ‘`*`’ means that there is a text error with this sentence. ‘`?`’ means that one of the conclusion's references has a text error. ‘`#`’ means that the conclusion is missing a rule.
Existential
  An existential is a quantifier that precedes the rest of sentence, denoted by ‘`3`’. An existential claims that ‘`there exists at least on item that has property property P`’ is a new sentence, assuming that ‘`P`’ is a valid predicate. An existential quantifier can be inserted into Aris using the key combination `CTRL+3`.
Function Symbol
  A function symbol maps one object to another object. These are always lower case. Examples of a function symbol is seqlog's ‘`z`’ and ‘`s`’ symbols (see Sequence Logic).
Goal
  A goal is a sentence that the user is looking to meet in a certain proof. The goal window contains all of these sentences, and can be toggled by the key combination `CTRL+L` (see Keyboard Shortcuts). When a sentence in the proof matches a goal, the proof sentence's line number is highlighted in red, while the goal's line number is changed to match the proof sentence's line number.
Negation
  A negation is a connective that is inserted in front of a sentence, denoted by ‘`~`’. A neagion claims that the opposite of the negation is true. A negation can be inserted into Aris using the key combination `CTRL+`` (see Keyboard Shortcuts).
Null Object
  A null object is an object, denoted by ‘`nil`’. In Aris it resembles a null byte, ‘`\0`’, and represents an undefined object in a sequence. A null object can be inserted by using the key combination `CTRL+.`.
Predicate
  A predicate is a type of logical symbol that denotes a property of or relation between one or more objects. These always begin with capital letters, and generally use prefix notation. Exceptions of this are the identity predicate (‘`=`’), the less than predicate (‘`<`’), and the element of predicate.
Premise
  A premise is a sentence that is given. A premise has no rule associated with it, nor does it have an evaluation value, unless there is an error in it. Any variables introduced in a premise are not considered arbitrary.
Proof
  A proof is a set of sentences, beginning with a set of premises and ending with a set of conclusions, that the user is trying to derive something from. The proof window is the main window that appears when the user opens up a proof.
Quantifier
  A quantifier is a type of logical symbol that claims something about the amount, or quantity, of an object that holds a specific property. The quantifiers used in system psi are the universal (‘`V`’), and the existential (‘`3`’).
Reference
  A reference is a sentence that is being used to derive a conclusion. A reference is highlighted in violet, and can be added or removed from the current sentence by holding down `CTRL`, and left-clicking on the desired reference.
Rules
  The rules in Aris are a combination of inference rules, equivalence rules, and predicate rules that the user can use to derive sentences. The rules window (also referred to as the rules tablet) is shared amongst all of the proofs in Aris. It can be toggled by the key combination `CTRL+R` (see Keyboard Shortcuts) from any proof window. For the list of rules, Rules Index.
Sentence
  A sentence is a line in Aris. A sentence always consists of a text entry, a line number, and an evaluation value.
Subproof
  A proof within a proof. To begin a subproof in Aris, use the key combination `CTRL+B`, and to exit one, use the key combination `CTRL+D`.
Tautology
  A tautology is a zero-place connective that stands on its own, denoted by ‘`T`’. A tautology represents something that is always true. A tautology is only used with the boolean rules (see Boolean Rules), and can be inserted using the key combination `CTRL+1`.
Universal
  A universal is a quantifier that precedes the rest of sentence, denoted by ‘`V`’. A universal claims that ‘`for all items, they have property P`’ is a new sentence, assuming that ‘`P`’ is a valid predicate. A universal quantifier can be inserted into Aris using the key combination `CTRL+2`.
Variable
  A variable represents an object within a proof. A variable is introduced when it is first used. If the line that it is introduced in is a premise, the start of a subproof, or a line using existential instantiation (see ei), then it is not considered arbitrary. Otherwise, it is. Only the variables from lines that can be selected from the current line are taken into account when processing it. This means that after a subproof is ended, then lines after it don't worry about variables introduced within it.