Hello, dear friend, you can consult us at any time if you have any questions, add WeChat: daixieit

Proof System for Propositional Logic

Proofs

In mathematics, we like to prove things. In a mathematical proof, we generally begin with some facts that we take as given. We then provide a sequence of reasoning, ultimately reaching a conclusion that follows from the facts.

It is our goal to describe a formal proof system in the setting of propositional logic. We want to make sure that our proof system only allows us to prove things that are true. It would also be nice if whenever one statement followed from others, there would be a proof of this in our system.

Proof System for Propositional Logic

Definition

For any propositional formulas ϕ, ψ, and χ, the following formulas will be axioms of our proof system:

(1) (ϕ → (ψ → ϕ))

(2) ((ϕ → (ψ → χ)) → ((ϕ → ψ) → (ϕ → χ)))

(3) ((¬ϕ → ¬ψ) → (ψ → ϕ))

Definition

Our proof system will have one rule, known as Modus Ponens (MP):

For propositional formulas ϕ and ψ, from ϕ and (ϕ → ψ), we conclude ψ.

The rule Modus Ponens is often represented as

ϕ

(ϕ → ψ)

ψ

Definition

For Γ a set of propositional formulas and ϕ a propositional formula, we say ϕ is provable from Γ and write Γ ` ϕ if there exists a finite list of propositional formulas ϕ1, ϕ2, . . . , ϕn with ϕn = ϕ such that for each 1 ≤ i ≤ n either

(1) ϕi ∈ Γ (we say ϕi is a premiss),

(2) ϕi is an axiom, or

(3) there are l, m < i such that ϕi follows from ϕl and ϕm using the rule MP. That is, ϕm = (ϕl → ϕi).

We call the sequence ϕ1, . . . , ϕn a derivation of ϕ from Γ.

Proof System for Propositional Logic

Notation: If ϕ is a formula such that ∅ |- ϕ, we simply write |- ϕ.

Note that if Θ is a set of formulas and ϕ is a formula such that Θ |- ϕ, then for any set of formulas Γ, Γ ∪ Θ |- ϕ. In particular, if |- ϕ, then for any set of formulas Γ, Γ |- ϕ.

Soundness of Our Proof System

Soundness of Our Proof System

Now we want to check that our proof system only proves things that are true. More formally, we wish to show that if Γ ` ϕ, then Γ |= ϕ.

Theorem (Soundness)

For any set of propositional formulas Γ and any propositional formula ϕ, if Γ |- ϕ, then Γ |= ϕ.

To prove the Soundness Theorem, we will first check that all our axioms are tautologies. We will then check that our rule MP preserves truth in the sense that {ϕ, (ϕ → ψ)} |= ψ. The result will then follow from the definitions of |= and |- .

Theorem (Soundness)

For any set of propositional formulas Γ and any propositional formula ϕ, if Γ ` ϕ, then Γ |= ϕ.

Proof: We have the following truth tables.

So we see that all the axioms of our system are tautologies.