1 Propositional Logic¶

Propositional logic and natural deduction

Propositional logic as a formal language: syntax and semantics

Normal forms

SAT solvers

1.0 Introduction¶

We can define a computer language by rules.

\[Rule: Name \frac{Premise}{Conclusion} \]

Propositional logic, prediction logic and C/C++ are all formal languages (形式语言).

Mathematical logic and computer science logic are different. The logic in computer science teaches us how to use logic in programmig.

Formal argument: If p and not q, thne r. Not r. p. Therefore, q.

1.1 Declarative sentences¶

Declarative sentences
Formalize declarative sentences
- Symbolic
- Automatic manipulations
Strategy of formalization
- atomic, indecomposable
- code up in compositional way
Composition rule: $(p \land q) \to ((\neg r) \lor q)$
- negation: $\neg$
  - symbolic: $\neg$
  - semantic: negation
- disjunction: $\lor$
- conjunction: $\land$
- implication: $\to$

1.2 Natural deduction¶

more rules, less axioms

Formal System
- syntax
- semantics
- axioms $\phi \to \phi$
- rules $Name \frac{Premise}{Conclusion}$
Proof calculus 推导规则
- Natural deduction
- Hilbert system
Reasoning
- How to establish validity of declarative sentences?
- a calculus for reasoning propositions
Proof rules
- Nature deduction contains a collection of proof rules
- infer formulas from other formulas
- infer a conclusion from a set of premises $\implies $proof
Sequent 矢列
- A sequent is valid if there is a proof to draw the conclusion
Rules for conjunction
- And-introduction rule $\land +$
  - $\frac{\phi \quad \psi}{\phi \land \psi} \land i$
- And-elimination rule $\land -$
  - $\frac{\phi \land \psi}{\phi} \land e_1$
  - $\frac{\phi \land \psi}{\psi} \land e_2$
- Example
  - $p \land q, r \vdash q \land r$
Rules for disjunction
- Introduction rule
  - $\frac{\phi}{\phi \lor \psi} \lor i_1$
  - $\frac{\psi}{\phi \lor \psi} \lor i_2$
- Elimination rule
  - $\frac{\phi \lor \psi \ \boxed{\phi \dots \chi} \ \boxed{\psi \dots \chi}}{\chi} \lor e$
- Example
  - $p \lor q \vdash q \lor p$
    - See in images
  - $q \to r \vdash (p \lor q) \to (p \lor r)$
    - See in images
  - $(p \lor q) \lor r \vdash p \lor (q \lor r)$
    - See in images
Rules for double negation
- Introduction rule
  - $\frac{\phi}{\neg\neg\phi}\neg\neg i$
- Elimination rule
  - $\frac{\neg\neg\phi}{\phi}\neg\neg e$
Rules for eliminating implication
- $\frac{\phi \quad \phi \to \psi}{\psi} \to e$
- $\frac{\phi \to \psi \quad \neg\psi}{\neg \phi} MT$
- Examples
  - $p, p \to q, p \to (q \to r) \vdash r$
    - $1 \quad p \to (q \to r) \quad premise$
    - $2 \quad p \to q \quad premise$
    - $3 \quad p \quad premise$
    - $4 \quad q \to r \quad \to e 1, 3$
    - $5 \quad q \quad \to e 2, 3$
    - $6 \quad r \quad \to e 4, 5$
  - $p \to (q \to r), p, \neg r \vdash \neg q$
    - $1 \quad p \to (q \to r) \quad premise$
    - $2 \quad p \quad premis$
    - $3 \quad \neg r \quad premise$
    - $4 \quad q \to r \quad \to e1, 2$
    - $5 \quad \neg q \quad MT3,4$
Rule implies introduction
- $1 \quad p \to q \quad premise$
- $2 \quad \neg q \quad assumption$
- $3 \quad \neg p \quad MT1,2$
- $4 \quad \neg q \to \neg p \quad \to i2,3$
Formulation of $\to i$
- $- \frac{\phi \dots \psi}{\phi \to \psi} \to i$
Theorems
- $p \vdash p $ is valid
- Example
  - $\vdash (q \to r) \to ((\neg q \to \neg p) \to (p \to r))$
  - See in images
Observation
- transform any proof of $\phi_1, \phi_2, \dots, \phi_n \vdash \psi $into a proof of the theorem $\vdash \phi_i \to (\phi_2 \to (\dots \to (\phi_n \to \psi)\dots))$
- Example
  - $p \land q \to r \vdash p \to (q \to r)$
    - See in images
  - $p \to (q \to r) \vdash p \land q \to r$
  - $p \land q \to r \dashv \vdash p \to (q \to r)$
  - $p \land (q \lor r) \vdash (p \land q) \lor (p \land r)$
    - See in images
Rules for negation
- contraction
  - expressions of the form $\neg \phi \land \phi$or $\phi \land \neg \phi$
- can't infer $\neg \phi $from given $\phi$
- Bottom-elimination: $\frac{\bot}{\phi} \bot e$
- Not-elimination: $\frac{\phi \quad \neg \phi}{\bot} \neg e$
- PBC: $\frac{\boxed{\phi \dots \bot}}{\neg \phi} \neg i$
- Example
  - $\neg p \lor q \vdash p \to q$
    - See in images
  - $p \to q, p \to \neg q \vdash \neg p$
  - $p \land \neg q \to r, \neg r, p\vdash q$
derived rules
- MT: modus Tollens is a derived rule
Provable equivalence

Hilbert System: less rules, more axioms only one rule: modus ponens: $\frac{\phi \to \psi \quad \phi}{\psi}$

Model a 2-bit additive device

1.3 Propositional logic as a formal language¶

Example: Lambda calculus
- Syntax, semantics, and typing rules
- important!!!
Well-formed formulas
Backus Naur form (BNF)

1.4 Semantics of propositional logic¶

The defination of truth table:

Let $E(\phi)$be the evaluation of $\phi$

$E(\top)=T$, $E(\bot)=F$

If $E(\phi)=T$, then $E(\neg \phi)=F$

Hilbert System
- Axioms
- Rules
- Example: Prove that $x \to x$
Soundness
- Semantic entailment: $\phi_1, \phi_2, \dots, \phi_n \vDash \psi$
  - If for all valuations in which all $\phi_1, \phi_2, \dots, \phi_n$evaluate to T, $\psi$evaluates to T as well, we say that $\phi_1, \phi_2, \dots, \phi_n \vDash \psi$ holds.
- Semantic correct
- Sequent: $\phi_1, \phi_2, \dots, \phi_n \vdash \psi$
- Soundness of propositional logic
  - Theorem (Soundness): Let $\phi_1, \phi_2, \dots, \phi_n$and $\psi$be propositional logic formulas. If $\phi_1, \phi_2, \dots, \phi_n \vdash \psi$is valid, $\phi_1, \phi_2, \dots, \phi_n \vDash \psi$holds.
  - Proof (mathematical induction 数学归纳法)
    - Base: length = 1
    - Step: If any $\phi_1, \phi_2, \dots, \phi_n \vdash \psi$with a proof where lengthe is less that k, $\phi_1, \phi_2, \dots, \phi_n \vDash \psi$. For any $\phi_1, \phi_2, \dots, \phi_n \vdash \psi$ with a k-step proof, it is sound as well.
    - Eliminating assumption boxes
Completeness
- Completeness of propositional logic
  - Whenever $\phi_1, \phi_2, \dots, \phi_n \vDash \psi$holds, does there exist a natural deduction proof for the sequent $\phi_1, \phi_2, \dots, \phi_n \vdash \psi$?
  - Defination: A formula $\phi$ is called a tautology iff it evalutes to T under all its evaluation, i.e., $\vDash \phi$ (which implies step1)
  - Proof: Assuming $\phi_1, \phi_2, \dots, \phi_n \vDash \psi$ holds, the argument proceeds in three steps:
    - Step1, $\vDash \phi_1 \to (\phi_2 \to \dots (\phi_n \to \psi))$ holds
      - verify the truth table
    - Step2, $\vdash \phi_1 \to (\phi_2 \to \dots (\phi_n \to \psi))$ holds
      - Theorem: if $\vDash \eta$ holds, $\vdash \eta$ is valid
        
        Proof: see in PPT30
        
        Core idea:
        
        transform to $p \lor \neg p, q \lor \neg q \vDash \phi$
        
        generate each line of the true table, encode each line in the table into sequent => each line can be proved
        
        Proposition
        
        proof: induction on the structure of the fomula $\phi$(structural induction)
        
        $\phi$can be $p$, $\neg \phi$, $\phi_1 \to \phi_2$, $\phi_1 \land \phi_2$
        
        the detail of proof can be seen in PPT31
    - Step3, $\phi_1, \phi_2, \dots, \phi_n \vdash \psi$ holds.
Soundness and Completeness
- $\phi_1, \phi_2, \dots, \phi_n \vDash \psi$ holds iff $\phi_1, \phi_2, \dots, \phi_n \vdash \psi$ is valid.

$\phi_1, \phi_2, \dots, \phi_n \vdash \psi$: syntactic method

$\phi_1, \phi_2, \dots, \phi_n \vDash \psi$: sematic approach, the $\vDash$ means sematic entailment

1.5 Normal Forms¶

Deciding $\vDash$ may vary in different ways.

1.5.1 Semantic equivalence¶

Definition

Let $\phi$ and $\psi$ be formulas. We say that $\phi$ and $\psi$ are semantically equivalent iff $\phi \vDash \psi$ and $\psi \vDash \phi$ hold. In this case we write $\phi \equiv \psi$.

Further, we call $\phi$ is valid if $\vDash \phi$ holds.

Transforming formulas

Conjunctive normal form (CNF)

Satisfiable

Satisfiability Problem

Example: Sudoku problem

Pycosat Code

Article: Sudoku as a SAT Problem

Horn clauses and satisfiability