(Natural Deduction & Resolution)

A variable 𝒙 in a WFF 𝝓 and a term 𝒕: [𝒕/𝒙] is a substitution. Applying a substitution on 𝝓— 𝜙[𝑡/𝑥] is the WFF obtained from 𝜙 by replacing all free occurrences of 𝒙 with t

when applying multiple substitutions: order is important

for two substitutions 𝒔𝒖𝒃𝟏 and 𝒔𝒖𝒃𝟐: 𝒔𝒖𝒃𝟏 ∘ 𝒔𝒖𝒃𝟐 is the composition of the substitutions and applies 𝑠𝑢𝑏2, then 𝑠𝑢𝑏1

substitution example 𝜙 = (∀𝑥 𝑃 𝑥 ∨ Q 𝑦 ) → 𝑆(𝑥, 𝑦): 𝜙[𝑡/𝑥] = (∀𝑥 𝑃 𝑥 ∨ Q 𝑦 ) → 𝑆(𝒕, 𝑦) ….. 𝜙 [𝑓(𝑧)/𝑦] = (∀𝑥 𝑃 𝑥 ∨ Q 𝒇 𝒛 ) → 𝑆(𝑥, 𝒇(𝒛))

substitution problem: The bound variable conflicts with the substitute variable

substitution solution: Rename the bound variable before substitution

Rename 𝑥 to 𝑧 and then apply the substitution: 𝜙[𝑥/𝑦] = ∀𝑧 𝑆(𝑧, 𝑥)

A WFF 𝜙 in prenex normal form: A sequence of quantifiers and variables followed by a quantifier-free sub-formula

The quantifier-free sub-formula is called: the matrix of 𝜙

∀𝑥 ∃𝑦 (𝑃 𝑥, 𝑦 → 𝑆 𝑧 ) is in: prenex normal form

(𝑃 𝑥, 𝑦 → 𝑆 𝑧 ) is: its matrix

∀𝑥∃𝑦 𝑃 𝑥, 𝑦 → ∃𝑧 𝑆(𝑧) is: not in prenex normal form

PNF Theorem: Every WFF can be converted to prenex normal form

¬∀𝑥∃𝑦∃𝑧 𝑆(𝑥, 𝑦, 𝑧) : ∃𝑥∀𝑦∀𝑧 ¬𝑆(𝑥, 𝑦, 𝑧)

(∀𝑥 𝑃 𝑥, 𝑦 ∨ ∃𝑧 𝑄 𝑧 ) : ∀𝑥∃𝑧 (𝑃 𝑥, 𝑦 ∨ 𝑄 𝑧 )

¬∀x 𝜙 𝑥 : ∃¬𝜙(𝑥)

¬∃x 𝜙 𝑥 : ∀¬𝜙(𝑥)

Skolemization: Converting WFFs to WFFs without existential quantifiers

Skolem normal form: The result of Skolemization of a formula in prenex normal form

MGU: A unifier 𝑠𝑢𝑏1 is called a most general unifier (MGU) if every unifier 𝑠𝑢𝑏2 is equal to 𝑠𝑢𝑏 ∘ 𝑠𝑢𝑏1 for some substitution 𝑠𝑢b. e.g. 𝑠𝑢𝑏1 = [𝑓 (𝑧) Τ𝑥] is a MGU for {𝑃 (x), 𝑃 (𝑓 (z))}

Robinson’s Theorem: Every set of unifiable clauses has a MGU

MGUs are not unique, but they differ only in variable names

For WFFs 𝜙 and 𝜓, we follow these steps to prove 𝝓 ⊢ 𝝍 using resolution: 1. Convert 𝝓 ∧ ¬𝝍 to prenex Skolem form with a matrix 𝑭. 2. Convert 𝐹 to a set of clauses 𝑭. 3. Apply resolution steps on clauses in 𝐹. 4. Stop and return True if □ is reached

Equisatisfiable: WFFs 𝜙 and 𝜓 are equisatisfiable if 𝜙 is satisfiable if and only if 𝜓 is satisfiable

Two logically equivalent formulas are also equisatisfiable, but: two equisatisfiable formulas are not always equivalent

Theorem: A WFF in predicate logic is equisatisfiable to its Skolem form