Next: Options, Previous: Introduction, Up: Top [Contents]
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 Other Key Shortcuts).
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. Both of these colors can be changed using customization (see Customization).
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 Other Key Shortcuts).
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 Other Key Shortcuts).
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 (‘!’).
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.
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 Other Key Shortcuts).
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 Proof Windows).
An evaluation value is the value that appears to the right of a sentence’s text entry. It can either be a square, a light green check, an X, an X polygon, a pointer box, or a dark green check icon. The square means that the sentence is awaiting evaluation. The light gren check means that either the conclusion logically follows from its references and rule, or that the goal has been found in the corresponding proof. In the case of premises, this means that the premise has no syntactic errors. The red X 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. The X polygon means that there is a text error with this sentence. The green check means that one of the conclusion’s references has a text error. The pointer box means that the conclusion is missing a rule.
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.
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).
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 Proof Windows). 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.
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 Other Key Shortcuts).
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+..
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.
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.
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.
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’).
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.
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 Proof Windows) from any proof window. For the list of rules, Rules Index.
A sentence is a line in Aris. A sentence always consists of a text entry, a line number, and an evaluation value.
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.
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.
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.
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.
Next: Options, Previous: Introduction, Up: Top [Contents]