Logic

Propositional Logic

Propositional logic is based on Propositions, statements about the world that can be either true or false.

All binary logical connectives are right associative. $a\vee b\vee c\text{ means }a\vee (b\vee c)$ $a⟹b⟹c\text{ means }a⟹(b⟹c)$

Checking that a formula is a Tautology

If you remember, from the definition of Tautology, it’s that a “propositional formula $P$ is a tautology (or valid) if $[P]=T$ for all Boolean valuations”. You can check that with a Tautology, it’s that a “propositional formula $P$ is a tautology (or valid) if $[P]=T$ for all Boolean valuations”. You can check that with a Truth Table. However, that truth table grows exponentially with the number of propositional symbols.

Another way we can determine whether a formula is a Tautology is by using a Tautology is by using a Proof Theory!

Proof Theory for Propositional Logic:

• Transformational Proof (sideways proof, statement algebra,$<->$)
• Natural Deduction (forward proof, $⊢$)
• Semantic Tableaux (backward proof, $⊢$)
• Hilbert Systems (axiom systems)
• Resolution
• DPLL (Davis Putnam Logeman Loveland)
• Binary Decision Diagrams

The only condition is that we need to make sure that our Proof Theory is Sound.

Related

• Formalization