First-Order Predicate Calculus Flashcards
AC
What are the logical axioms?
For all variables x and y, terms t, and wff A and B (write A(x) to indicate free variable in A; if we write A, it may/not contain a free variable)
CP. All axiom schemata of propositional logic
L1. (Substitution) (∀x: A(x)) ⊃ A(t)
where A(t) arises by substituting t for all occurances of x in A for which t is free for x (i.e. A(t) = A(x)(t/x))
L2. (∀-Distrubution) (∀x: (A ⊃ B)) ⊃ (A ⊃ ∀x: B)
if A contains no free occurances of x.
AC
What are the axioms for equality?
E1. (x = x)
E2. (x = y) ⊃ (A(x) ⊃ A(y))
where A(y) arises from A(x) by replacing some, not necessarily all, free occurances of x by y, and y is free for the occurances of x which it replaces
AC
What are the inference rules?
Modus Ponens: From A and A⊃B infer B
Generalization: For A infer ∀x:A (add universal quantifiers)
Substitution Rule: Any wff can be substituted for the metalogical variables A and B
AC
What is ∃-Introduction?
(a) If t is free for x in A(x), then ⊢ A(t) ⊃ ∃x: A(x)
(b) If ⊢ A ⊃ B, then ⊢ (∃x: A) ⊃ Bwhenever x is not free in B
AC
What are the properties of “=”?
(a) For any term t,⊢ t = t
(b) ⊢ (t = u) (A(t) ⊃ A(u))
(c) ⊢ t = u ⊃ u = t
(d) ⊢ t = u ⊃ (u = v ⊃ t = v)
NDC
What are the univeral inference rules for first-order logic?
NDC
What are the inference rules for the existential quantifier in first-order logic?
NDC
What are the restrictions for the inference rules
∀Intro and ∃Elim: The free variable a must be free for x in A
∀Intro: a must not occur free in A(x), nor in any hypothesis which derivation depends
∃Elim: free variable a may not occur free in Ax) nor in C, nor any hypothesis on which derivation depends
∀Elim and ∃Intro: Term t must be free for x in A
NDC
How can ∀Elim and ∃Intro be substituted of terms for some occurances?
NDC
Prove: ∀x: A(x) ⊢ ∃x: A(x)
NDC
Prove: ∀x1: ∀x2: A(x1,x2) ⊢ ∀x2: ∀x1: A(x1,x2)
Soundness and completeness in FOL?
NDC
What are the natural deduction rules for equality?
