Natrual Deduction for FOL part 1

FOL Natrual Deduction Rules

Still includes all the TFL rules, but more

ⱯI and ⱯE

▪ Key idea: arbitrary names effectively stand in for any name at all(for Intro one)

▪ ∃I and ∃E

more for the elimination:

kinda like disjunctions

easy to make true , hard to derive from

use arbitrary names

The basic idea: replace the bound variable with an arbitrary name, then see what we can de

▪ Quantifier Conversion Rules

▪ =I and =E

Proof Theoretic Concepts for FOL

Proof Theoretic and Semantic Consepts