Proving logical arguments based on syntax rather than semantics

Why? Easier for a computer (which cannot logically deduce things) to verify and prove statements

$Σ⊢A$: $A$ is formally deducible/provable from $Σ$.

Can we use a set of formulas (the premises, $Σ$) to prove another formula (the conclusion, $A$)?

For any set of formulas $Σ’$, we denote $Σ∪Σ’$ as $Σ, Σ’$

Rules are in the reference sheet.