Connectives

Logical connectives create new sentences from two or more constituent sentences. There are five logical connectives in CORE: ~, &, |, ->, and <->.

Negation

The logical connective ~ represents negation. Unlike the other four connectives, this is a unary connective. If A represents a well formed sentence, then ~A is a well formed sentence. The sentence ~A should be interpreted to mean that A is not true.

Sentences composed with the ~ connective can be proven using the not command. A sentence of the form ~A is logically equivalent to the sentence A -> false. Given A and ~A, one can deduce false.

Note

Since CORE uses a kind of intuitionistic logic, it is not true in general that A | ~A for any sentence of the form A. Additionally, ~~A is generally weaker than the sentence A. One can model classical logic by adding the law of excluded middle as an axiom.

And

The logical connective & represents “and.” If {A} and {B} represent well formed sentences, then {A} & {B} is a well formed sentence. {A} & {B} is interpreted to be true if and only if {A} is true and {B} is true.

Sentences composed with the & logical connective can be constructed using the built-in function and. A sentence composed with the & connective can be deconstructed into its constituent sentences using variable assignment. A sentence {C} is stronger than the sentence {A} & {B} if {C} is stronger than both {A} and {B}. The sentence {A} & {B} is stronger than a sentence {C} if either {A} or {B} is stonger than {C}. See Trivial Implication for more information.

Or

The logical connective | represents “or.” If {A} and {B} represent well formed sentences, then {A} | {B} is a well formed sentence. {A} | {B} is interpreted to be true if and only if {A} is true or {B} is true.

Sentences composed with the | logical connective can be constructed using the built-in function or. A sentence composed with the | connective can be used in a proof to branch an argument. A sentence {C} is stronger than the sentence {A} | {B} if {C} is stronger than either {A} or {B}. The sentence {A} | {B} is stronger than a sentence {C} if both {A} and {B} are stronger than {C}. See Trivial Implication for more information.

Implies

The logical connective -> represents implication. If {A} and {B} represent well formed sentences, then {A} -> {B} is a well formed sentence. {A} -> {B} is interpreted to be true if and only if whenever one can prove {A}, one can prove {B}.

Verified sentences {A} -> {B} and {A} can be used to deduce the verified sentence {B}.

Biconditional

The logical connective <-> represents the biconditonal connective. If {A} and {B} represent well formed sentences, then {A} <-> {B} is a well formed sentences. {A} <-> {B} is logically equivalent to ({A} -> {B}) & ({B} -> {A}).

Sentences composed with the <-> logical connective can be constructed from implications using the built-in function iff. Verified sentences {A} <-> {B} and {A} can be used to deduce the verified sentence {B}. In addition, verified sentences {A} <-> {B} and {B} can be used to deduce {A}.

Connective Precedence

Connectives are associated according to precedence. Connectives are in the following list in order from highest precedence to lowest precedence:

  1. &

  2. |

  3. ->

  4. <->

For example, the sentence

A | B & C <-> D -> E

Is parsed as:

(A | (B & C)) <-> (D -> E)

Due to connective precedence.