\(A : B\) means “\(A\) is a \(B\)”.
\(\prop\) is the type of propositions.
\(\context\) is the type of contexts.
\(\judgment\) is the type of judgments.
\(\frac{A \quad B \quad \ldots}{C}\) means “from \(A, B, \ldots\) infer \(C\)”. This is called an inference rule.
\(A, B, \ldots\) are the premises.
\(C\) is the conclusion.
\(A [x / B]\) means “\(A\) with \(x\) replaced by \(B\)”. This is called a substitution.
\(\varnothing\) is a context.
If \(\Gamma\) is a context and \(A\) is a proposition, then \(\Gamma, A\) is a context.
Thus a context is a list of propositions, which are called assumptions.
\[ \frac{}{\varnothing : \context} \]
\[ \frac{\Gamma : \context \qquad A : \prop}{\Gamma, A : \context} \]
If \(\Gamma\) is a context and \(A\) is a proposition, then \(\Gamma \vdash A\) is a judgment.
\[ \frac{\Gamma : \context \qquad A : \prop}{(\Gamma \vdash A) : \judgment} \]
Restatement: \[ \frac{}{\Gamma, A \vdash A} \]
Weakening: \[ \frac{\Gamma \vdash A}{\Gamma, B \vdash A} \]
Contraction: \[ \frac{\Gamma, B, B \vdash A}{\Gamma, B \vdash A} \]
Exchange: \[ \frac{\Gamma, A, B, \Delta \vdash C}{\Gamma, B, A, \Delta \vdash C} \]
\(\top\) means “true”.
Top formation: \[ \frac{}{\Gamma \vdash \top : \prop} \]
Top introduction: \[ \frac{}{\Gamma \vdash \top} \]
\(\bot\) means “false”.
Bottom formation: \[ \frac{}{\Gamma \vdash \bot : \prop} \]
\(A \Rightarrow B\) means “\(A\) implies \(B\)”. This is called an implication.
Implication formation: \[ \frac{\Gamma \vdash A : \prop \qquad \Gamma \vdash B : \prop}{\Gamma \vdash A \Rightarrow B : \prop} \]
Implication introduction: \[ \frac{\Gamma, A \vdash B}{\Gamma \vdash A \Rightarrow B} \]
Implication elimination: \[ \frac{\Gamma \vdash A \Rightarrow B \qquad \Gamma \vdash A}{\Gamma \vdash B} \]
\(A \land B\) means “\(A\) and \(B\)”. This is called a conjunction.
Conjunction formation: \[ \frac{\Gamma \vdash A : \prop \qquad \Gamma \vdash B : \prop}{\Gamma \vdash A \land B : \prop} \]
Conjunction introduction: \[ \frac{\Gamma \vdash A \qquad \Gamma \vdash B}{\Gamma \vdash A \land B} \]
Conjunction elimination (left): \[ \frac{\Gamma \vdash A \land B}{\Gamma \vdash A} \]
Conjunction elimination (right): \[ \frac{\Gamma \vdash A \land B}{\Gamma \vdash B} \]
\(A \lor B\) means “\(A\) or \(B\)”. This is called a disjunction.
Disjunction formation: \[ \frac{\Gamma \vdash A : \prop \qquad \Gamma \vdash B : \prop}{\Gamma \vdash A \lor B : \prop} \]
Disjunction introduction (left): \[ \frac{\Gamma \vdash A}{\Gamma \vdash A \lor B} \]
Disjunction introduction (right): \[ \frac{\Gamma \vdash B}{\Gamma \vdash A \lor B} \]
Disjunction elimination: \[ \frac{\Gamma \vdash A \lor B \qquad \Gamma, A \vdash C \qquad \Gamma, B \vdash C}{\Gamma \vdash C} \]
\(\forall x . A\) means “for all \(x\), \(A\)”. This is called a universal quantification.
Universal formation: \[ \frac{\Gamma \vdash A : \prop}{\Gamma \vdash \forall x . A : \prop} \qquad \text{\(x\) not free in \(\Gamma\)} \]
Universal introduction: \[ \frac{\Gamma \vdash A}{\Gamma \vdash \forall x . A} \qquad \text{\(x\) not free in \(\Gamma\)} \]
Universal elimination: \[ \frac{\Gamma \vdash \forall x . A}{\Gamma \vdash A [x / B]} \]
\(\exists x . A\) means “there exists an \(x\) such that \(A\)”. This is called an existential quantification.
Existential formation: \[ \frac{\Gamma \vdash A : \prop}{\Gamma \vdash \exists x . A : \prop} \qquad \text{\(x\) not free in \(\Gamma\)} \]
Existential introduction: \[ \frac{\Gamma \vdash A [x / B]}{\Gamma \vdash \exists x . A} \]
Existential elimination: \[ \frac{\Gamma \vdash \exists x . A \qquad \Gamma, A \vdash B}{\Gamma \vdash B} \qquad \text{\(x\) not free in \(\Gamma, B\)} \]
\(A = B\) means “\(A\) is identical to \(B\)”. This is called an identity.
Identity formation: \[ \frac{}{\Gamma \vdash A = B : \prop} \]
Identity introduction: \[ \frac{}{\Gamma \vdash A = A} \]
Identity elimination: \[ \frac{\Gamma \vdash A = B \qquad \Gamma \vdash C [x / A]}{\Gamma \vdash C [x / B]} \]
\(A \Leftrightarrow B\) means “\(A\) if and only if \(B\)”. This is called a bi-implication.
\(A \Leftrightarrow B\) is equivalent to \((A \Rightarrow B) \land (B \Rightarrow A)\).
Bi-implication formation: \[ \frac{\Gamma \vdash A : \prop \qquad \Gamma \vdash b : \prop}{\Gamma \vdash A \Leftrightarrow B : \prop} \]
Bi-implication introduction: \[ \frac{\Gamma, A \vdash B \qquad \Gamma, B \vdash A}{\Gamma \vdash A \Leftrightarrow B} \]
Bi-implication elimination (left): \[ \frac{\Gamma \vdash A \Leftrightarrow B \qquad \Gamma \vdash A}{\Gamma \vdash B} \]
Bi-implication elimination (right): \[ \frac{\Gamma \vdash A \Leftrightarrow B \qquad \Gamma \vdash B}{\Gamma \vdash A} \]
\(\neg A\) means “not \(A\)”. This is called a negation.
\(\neg A\) is equivalent to \(A \Rightarrow \bot\).
Negation formation: \[ \frac{\Gamma \vdash A : \prop}{\Gamma \vdash \neg A : \prop} \]
Negation introduction: \[ \frac{\Gamma, A \vdash \bot}{\Gamma \vdash \neg A} \]
Negation elimination: \[ \frac{\Gamma \vdash \neg A \qquad \Gamma \vdash A}{\Gamma \vdash \bot} \]