Formal Rules of Syntactic Implication

Syntactic implication utilizes deductive inference rules to transform premise sets into target conclusions. In what is also called a Sequent-style Calculus or Natural Deduction framework, let $\Gamma$ represent a set of formulas acting as premises(a.k.a. hypotheses), let $\phi ,\psi ,\theta$ represent individual formulas, and let the turnstile symbol $⊢$ denote “syntactically derives.”

Basic Proofs (Axioms)

These foundational rules establish the starting points for any formal derivation.

• Assumption ($Assum{e}_{\mathcal{L}}$): If a formula is already present within your active set of hypotheses, it is derived trivially.

  $\Gamma ⊢\phi \text{if }\phi \in \Gamma$

• Equality Reflexivity ($EqRefl$): Every valid term is inherently equal to itself.

  $\Gamma ⊢t=t\text{for all }t\in {\text{Term}}_{\mathcal{L}}$

Proof Rules (Connectives)

These inference rules dictate how to introduce new logical connectives into a derivation or eliminate existing ones to extract substructures.

Conjunction

• Elimination ($\wedge EL$ and $\wedge ER$): If a compound conjunction is derived, either constituent proposition can be extracted individually.

  $\frac{\Gamma ⊢\phi \wedge \psi }{\Gamma ⊢\phi }\text{and}\frac{\Gamma ⊢\phi \wedge \psi }{\Gamma ⊢\psi }$

• Introduction ($\wedge I$): If independent derivations exist for two separate formulas, they can be unified into a single conjunction.

  $\frac{\Gamma ⊢\phi \Gamma ⊢\psi }{\Gamma ⊢\phi \wedge \psi }$

Disjunction

• Introduction ($\vee IL$ and $\vee IR$): If a formula is derived, it can be disjoined with any arbitrary proposition while preserving validity.

  $\frac{\Gamma ⊢\phi }{\Gamma ⊢\phi \vee \psi }\text{and}\frac{\Gamma ⊢\psi }{\Gamma ⊢\phi \vee \psi }$

• Proof by Cases ($\vee PC$): If two distinct hypotheses independently derive the identical consequent $\theta$, then the disjunction of those hypotheses also derives $\theta$.

  $\frac{\Gamma \cup \{\phi \}⊢\theta \Gamma \cup \{\psi \}⊢\theta }{\Gamma \cup \{\phi \vee \psi \}⊢\theta }$

Implication

• Elimination / Modus Ponens ($\to E$): If a conditional implication and its operational antecedent are both derived, the consequent necessarily follows.

  $\frac{\Gamma ⊢\phi \to \psi \Gamma ⊢\phi }{\Gamma ⊢\psi }$

• Introduction / Deduction Theorem ($\to I$): If assuming a provisional hypothesis successfully derives a target formula, the overarching implication is established.

  $\frac{\Gamma \cup \{\phi \}⊢\psi }{\Gamma ⊢\phi \to \psi }$

Negation and Contradiction

• Proof by Contradiction ($\neg PC$): If assuming a hypothesis yields a structural contradiction (deriving both a formula and its explicit negation), the hypothesis is refuted.

  $\frac{\Gamma \cup \{\psi \}⊢\phi \Gamma \cup \{\psi \}⊢\neg \phi }{\Gamma ⊢\neg \psi }$

• Contradiction Rule / Reductio ad Absurdum ($Contr$): If assuming the negation of a proposition yields a logical contradiction, the foundational proposition is affirmed as true.

  $\frac{\Gamma \cup \{\neg \phi \}⊢\psi \Gamma \cup \{\neg \phi \}⊢\neg \psi }{\Gamma ⊢\phi }$

Equality Rules

• Substitution ($=Sub$): If a formula holds true for a specific term $t$, and an explicit identity mapping establishes that $t$ equals $u$, the formula remains valid when $t$ is replaced by $u$.

  $\frac{\Gamma ⊢{\phi }_t^x\Gamma ⊢t=u}{\Gamma ⊢{\phi }_u^x}$

Quantifier Rules

Quantifier rules govern the systematic introduction and elimination of operational scope variables across domains.

Existential Quantifiers

• Introduction ($\exists I$): Proving that a specific instantiated term satisfies a target property confirms that there exists at least one element satisfying that property.

  $\frac{\Gamma ⊢{\phi }_t^x}{\Gamma ⊢\exists x\phi }$

• Existential Elimination / Proof ($\exists P$): If an arbitrary placeholder $y$ can derive a conclusion $\psi$ from an existential statement, the derivation holds universally, provided $y$ remains unbound within the surrounding context.

  $\frac{\Gamma \cup \{{\phi }_y^x\}⊢\psi }{\Gamma \cup \{\exists x\phi \}⊢\psi }\text{if }y\notin \text{FreeVar}(\Gamma \cup \{\exists x\phi ,\psi \})$

Universal Quantifiers

• Elimination ($\forall E$): If a property is universally quantified across an entire domain, it holds valid for any specific instantiated term $t$.

  $\frac{\Gamma ⊢\forall x\phi }{\Gamma ⊢{\phi }_t^x}$

• Introduction ($\forall I$): If a property can be derived for a completely arbitrary, unconstrained placeholder $y$, it is formally established for all elements in the domain.

  $\frac{\Gamma ⊢{\phi }_y^x}{\Gamma ⊢\forall x\phi }\text{if }y\notin \text{FreeVar}(\Gamma \cup \{\forall x\phi \})$

Superset Rule

• Monotonicity ($Super$): Classical deduction is monotonic. Adding supplementary hypotheses to a valid derivation context never invalidates the previously established conclusion.

  $\frac{\Gamma ⊢\phi }{{\Gamma }^{\prime }⊢\phi }\text{if }{\Gamma }^{\prime }\supseteq \Gamma$