Logical connective

A logical connective forms a compound proposition from one or more propositions.

Logical implication forms the proposition $A\to B$. In intuitionistic logic its proof consists of a construction that transforms any proof of $A$ into a proof of $B$.

The conjunction $A\wedge B$ holds when both $A$ and $B$ hold.

The disjunction $A\vee B$ holds when at least one of $A$ and $B$ holds. Constructively, a proof records which disjunct holds and provides its proof.

Logical truth is the nullary connective that is always true.

Logical falsity is the nullary connective with no proof.