CSE 472/572, Spring 2002 http://www.cse.buffalo.edu/∼rapaport/572.html

AN F.O.L. NATURAL-DEDUCTION EXAMPLE

Show ¬∀x[α(x)] ⊢ ∃x[¬α(x)]:

1. ¬∀x[α(x)] // assumption

/∗

Show ∃x[¬α(x)]:

Show ¬α(t), for some t & use ∃-Intro: /∗

∗2. α(t)  // temporary assumption (with arbitrary t)
∗3. ∀x[α(x)] // 2, ∀-Intro
∗4. ¬∀x[α(x)] // send 1
∗5. ¬α(t)  // 2,3,4, ¬-Intro
6. ¬α(t)  // return 5
7. ∃x[¬α(x)] // ∃-Intro

Exercise for the reader: Use ∀-Intro to show: ¬∃x[α(x)] ⊢ ∀x[¬α(x)]

\begin{matrix}c \\ ◯ \end{matrix}2002, William J. Rapaport, rapaport@cse.buffalo.edu file: 572/S02/natded.fol.20mr02.tex