∀I

Logical methods for AI

Lecture 7

Logical proofs

This work is licensed under CC BY 4.0

https://forms.gle/JiXXM9eysAZaJMja9

Logical proofs

Proof systems

Model of step-wise inference:

Ada is either in the study or on the Philosopher’s Walk, and if she’s on the Philosopher’s Walk, she’s thinking about mathematics. Ada is not in the study, so she must be thinking about mathematics.

Proofs

Sequence of formulas, where each is either:

assumption/axiom
derived from earlier formulas via an inference rule

Final formula = conclusion.

Inference rule

$$\begin{array}{ccc} A_1 & \dots & A_n \\ \hline & C \end{array}$$

$$\mathsf{STUDY}\lor\mathsf{WALK},\mathsf{WALK}\to\mathsf{MATH},\neg\mathsf{STUDY}\vdash\mathsf{MATH}$$

Proof systems

Hilbert systems

Axioms: Basic truths
Inference rules: as few as possible

Axioms:

$$ A\to ( B\to A)$$ $$( A\to ( B\to C))\to(( A\to B)\to ( A\to C))$$ $$(\neg A\to \neg B)\to ( B\to A)$$

Inference rule: $$A,A\to B\vdash B$$

$((\mathsf{RAIN} \to ((\mathsf{RAIN} \to \mathsf{RAIN}) \to \mathsf{RAIN})) \to ((\mathsf{RAIN} \to (\mathsf{RAIN} \to \mathsf{RAIN})) \to (\mathsf{RAIN} \to \mathsf{RAIN})))$
Axiom 2. with $A=\mathsf{RAIN}, B=(\mathsf{RAIN}\to \mathsf{RAIN}),$ and $C=\mathsf{RAIN}$
$(\mathsf{RAIN} \to ((\mathsf{RAIN} \to \mathsf{RAIN}) \to \mathsf{RAIN}))$
Axiom 1. with $A=\mathsf{RAIN}$ and $B=(\mathsf{RAIN}\to \mathsf{RAIN})$)
$((\mathsf{RAIN} \to (\mathsf{RAIN} \to \mathsf{RAIN})) \to (\mathsf{RAIN} \to \mathsf{RAIN}))$
From 1. and 2. by MP.
$(\mathsf{RAIN} \to (\mathsf{RAIN} \to \mathsf{RAIN}))$
Axiom 1. with $A=\mathsf{RAIN}$ and $B=\mathsf{RAIN}$.
$(\mathsf{RAIN} \to \mathsf{RAIN})$
From 3. and 4. by MP.

$$( A\land B)\leadsto \neg( A\to\neg B)$$ $$( A\lor B)\leadsto(\neg A\to B)$$ $$( A\leftrightarrow B)\leadsto(( A\to B)\land( B\to A))$$

$$\mathsf{STUDY}\lor\mathsf{WALK},\mathsf{WALK}\to\mathsf{MATH},\neg\mathsf{STUDY}\vdash\mathsf{MATH}$$ $$\mathsf{STUDY}\lor\mathsf{WALK}\leadsto\neg\mathsf{STUDY}\lor\mathsf{WALK}$$ $$\leadsto\neg\mathsf{STUDY}\to\mathsf{WALK},\mathsf{WALK}\to\mathsf{MATH},\neg\mathsf{STUDY}\vdash\mathsf{MATH}$$

$\neg \mathsf{STUDY}\to\mathsf{WALK}$ (Assumption)
$\neg \mathsf{STUDY}$ (Assumption)
$\mathsf{WALK}$ (1.,2. MP)
$\mathsf{WALK}\to\mathsf{MATH}$ (Assumption)
$\mathsf{MATH}$ (3.,4. MP)

Natural deduction

No axioms
Only inference rules
Try to model "natural" deduction

Discharging assumptions: $$\vdash \neg(\mathsf{RAIN}\land\neg\mathsf{RAIN})$$

$$\mathsf{STUDY}\lor\mathsf{WALK},\mathsf{WALK}\to\mathsf{MATH},\neg\mathsf{STUDY}\vdash\mathsf{MATH}$$

Resolution-based systems

No axioms
One rule

Resolution rule

$l_{i},k_{j}$ literals:

$$\begin{array}{ccc} l_1\lor l_2\lor \dots\lor p & & \neg p\lor k_1\lor k_2\lor\dots \\ \hline & l_1\lor l_2\lor \dots k_1\lor k_2\lor\dots \end{array}$$ $$\begin{array}{ccc} p & & \neg p \\ \hline & \bot \end{array}$$

$$\mathsf{STUDY}\lor\mathsf{WALK},\mathsf{WALK}\to\mathsf{MATH},\neg\mathsf{STUDY}\vdash\mathsf{MATH}$$ $$\mathsf{WALK}\to\mathsf{MATH}\leadsto\neg\mathsf{WALK}\lor\mathsf{MATH}$$

Problem

$$\mathsf{RAIN}\vDash\mathsf{RAIN}\lor\mathsf{SNOW}?$$

(Re)Solution

$$A_1,A_2,\dots\vdash C\Leftrightarrow $$ $$CNF(A_1),CNF(A_2),\dots,CNF(\neg C)\vdash \bot$$

$$\mathsf{RAIN}\vdash \mathsf{RAIN}\lor\mathsf{SNOW}\leadsto$$ $$\mathsf{RAIN},\neg\mathsf{RAIN},\neg\mathsf{SNOW}\vdash\bot$$ $$\begin{array}{ccc} \mathsf{RAIN} & & \neg \mathsf{RAIN} \\ \hline & \bot \end{array}$$

Applications

Metalogic

Soundness: All derivable inferences are valid
Completeness: All valid inferences are derivable
Soundness and completeness: $$P_1,P_2,\dots\vDash C\ \Leftrightarrow \ P_1,P_2,\dots\vdash C$$
Computationally tractable model of valid inference

Proof verification

Interactive theorem prover (ITP): program that checks inferences in formal language
Distribution of epistemic burden.

Example


      variable {p : Prop}
      variable {q : Prop}
      variable {r : Prop}
      open Classical
      
      theorem hilbert_1 : p → (q → p) := by
        intro h
        intro _
        exact h
      
      theorem hilbert_2: (p → (q → r))→ ((p → q) → (p → r)) := by
        intros h1 h2 hp
        apply h1 hp
        apply h2
        assumption
      
      theorem hilbert_3 : (¬p → ¬q) → (q → p) := by
        intros h hq
        by_cases hp : p
        · -- Case when p is true
          exact hp
        · -- Case when p is false (¬p)
          have hnq := h hp
          contradiction
      
      #print hilbert_1
      #print hilbert_2
      #print hilbert_3

Lean 4 Life