Logic

Formal Logic Role

Backbone of specification and verification. Provides framework for what can be claimed (language) and how claims are justified (logic). Much older than computer science.

Language Components

Terms (variables x, constants c, functions f). Atoms (truth-valued terms). Logical constants (⊤ true, ⊥ false). Propositional connectives (

, ∧, ∨, ⇒, ≡). Quantifiers (∀ for all, ∃ there exists). Modalities (□, ♢ for knowledge/time/possibility). Higher-order constructs (λ, ∀, ∃).

Logic Definition

Logic tells what follows from premises: Γ ⊢ F ("Γ entails F" or "F is a theorem of Γ"). Specifies consequences of given assumptions.

Calculus Purpose

Method to calculate all consequences of axioms in a fixed language and logic. Expressed as collection of inference rules. Enables systematic derivation.

Inference Rule Form

Premises above line, conclusion below: P₁ P₂ … Pₙ / C. If all premises hold, conclusion can be derived.

Natural Deduction Conjunction Rules

Conjunction introduction: from P and Q, infer P ∧ Q. Conjunction elimination: from P ∧ Q, infer P; from P ∧ Q, infer Q.

Natural Deduction Disjunction Rules

Disjunction introduction: from P, infer P ∨ Q; from Q, infer P ∨ Q. Disjunction elimination: from P ∨ Q, P ⇒ R, Q ⇒ R, infer R.

Natural Deduction Implication Rules

Implication introduction: assuming P, derive Q, then infer P ⇒ Q. Implication elimination (modus ponens): from P and P ⇒ Q, infer Q.

Falsity and Negation

⊥ represents contradiction. Negation defined as ¬P ≜ P ⇒ ⊥. From ⊥, any proposition can be derived (principle of explosion).

Commutativity of Conjunction Proof

Assume A ∧ B. By conjunction elimination, derive A and B. By conjunction introduction, B ∧ A. Therefore A ∧ B ⇒ B ∧ A.

Double Negation Introduction Proof

Assume P. Assume (P ⇒ ⊥) (¬P). From P and ¬P, derive ⊥. Therefore ¬P ⇒ ⊥ (¬¬P). Hence P ⇒ ¬¬P.

Classical Logic

Adds law of excluded middle (P ∨¬P) as theorem or double negation elimination rule: ¬¬

P / P. Enables proof by contradiction where intuitionistic logic cannot.

Intuitionistic Logic

Does not assume P ∨¬P or double negation elimination. Proofs must be constructive - existence proved by explicit construction. More restrictive than classical logic.

First-Order Logic Rules

Universal introduction: from F[x] (with x arbitrary), infer ∀x. F[x]. Universal elimination: from ∀x. F[x], infer F[t] for any term t.

Curry-Howard Correspondence

Connection between logic and computation. Propositions correspond to types, proofs correspond to programs. Rocq implements this correspondence