Logic

Zvi Berger

Details

• Authors: Aaron R. Bradley, Zohar Manna
• From: Stanford University, USA
• Publisher: Springer Science+Business Media
• Year: 2007

​

• Sections: 1.1--1.3, 2.1 -- 2.3, 3.1 -- 3.3

Lecture outline

• Propositional Logic (PL)
• Syntax
• Semantics
• Satisfiability and Validity
• Proof System – Lyndom
• Completeness and Soundness

​

​

​

​

​

• First Order Logic (FOL)
• Syntax
• Semantics
• Satisfiability and Validity
• Proof System
• Completeness and Soundness
• Gödel's Incompleteness

​

​

​

Logic

Syntax

Example

Precedence of Logical Operators

Precedence of Logical Operators

Subformula

• Formula G is a subformula of formula F if it occurs syntactically within G.

Subformula

• Formula G is a subformula of formula F if it occurs syntactically within G.

​

• the only subformula of P is P;
• the subformulae of ¬F are ¬F and the subformula of F;
• the subformula of F1 ∧ F2, F1∨F2, F1 → F2, F1 ↔ F2 are the formula itself and the subformula of F1 and F2.

​

​

Subformula

• Example:

F : (P ∧ Q) → (P ∨ ¬Q)

• Subformula:

F , P ∧ Q , P ∨ ¬Q , P , Q, ¬Q

​

​

​

Subformula

• Example:

F : (P ∧ Q) → (P ∨ ¬Q)

• Subformula:

F , P ∧ Q , P ∨ ¬Q , P , Q, ¬Q

​

• The strict subformulae of a formula are all its subformulae except itself.

​

​

semantic

p /\ q

p \/ q

Semantic – True Table

• Consider the formula:

F : P ∧ Q → P ∨ ¬Q

and the interpretation:

I : {P → true, Q → false}

To evaluate the truth value of F under I, construct the following table:

Semantic – Inductive Definition

Semantic – Inductive Definition

Semantic – Inductive Definition

• Consider the formula:

F : P ∧ Q → P ∨ ¬Q

and the interpretation:

I : {P → true, Q → false}

Satisfiability and Validity

Satisfiability and Validity

Validity Proofs – True Table

• Consider the formula:

F : P ∧ Q → P ∨ ¬Q

​

​

​

​

• The final column, which represents the truth value of F under the possible interpretations, is filled entirely with true. F is valid.

Proof System -Lyndon

Axioms (tautologies):

A1 (ϕ 🡪(ψ🡪ϕ))

A2 ((ϕ 🡪(ψ🡪η))🡪((ϕ 🡪ψ)🡪(ϕ 🡪η)))

A3 (((ϕ 🡪F)🡪F)🡪ϕ)

Inference Rule:

ϕ🡪ψ MP-Modus Ponens

ϕ

ψ

Proof System -Lyndon

Definition (Σ ⊢ φ): φ is provable from Σ if there is a derivation using sentences of Σ, the axioms A1, A2, A3 and M.P., ending in φ.

• ⊢ is syntactic (symbol manipulation); ⊨ is semantic (every assignment satisfying Σ satisfies φ).

Proof System -Lyndon

Example: from false, everything follows — F ⊢ φ:

1. F (assumption from Σ)

2. F → ((φ → F) → F) (A1 with ψ = φ → F)

3. (φ → F) → F (M.P. 1, 2)

4. ((φ → F) → F) → φ (A3)

5. φ (M.P. 3, 4)

FOL - First Order Logic

• Now, we extends the machinery of propositional logic to first-order logic (FOL), also called both predicate logic and the first-order predicate calculus.
• FOL extends PL with predicates, functions, and quantifiers.
• All formulae of PL evaluate to true or false. FOL is not so simple. In FOL, terms evaluate to values other than truth values such as integers, people, or cards of a deck.

​

​

FOL - Syntax

FOL - Quantifier

FOL - Quantifier

• A variable is free in formula F[x] if there is an occurrence of x that is not bound by any quantifier.

Denote by free(F) the set of free variables of a formula F.

​

• . A variable is bound in formula F[x] if there is an occurrence of x in the scope of a binding quantifier ∀x or ∃x.

Denote by bound(F) the set of bound variables of a formula F

​

• A formula F is closed if it does not contain any free variables.

FOL - Examples

Semantic - Domain

Semantic - Assignment

FOL - Semantic

FOL – Interpreted Example

FOL - Satisfiability and Validity

F : (∀x. p(x)) → (∀y. p(y))

​

PL Proof System - Lyndon

Axioms (tautologies):

A1 (ϕ 🡪(ψ🡪ϕ))

A2 ((ϕ 🡪(ψ🡪η))🡪((ϕ 🡪ψ)🡪(ϕ 🡪η)))

A3 (((ϕ 🡪F)🡪F)🡪ϕ)

Inference Rule:

ϕ🡪ψ MP-Modus Ponens

ϕ

ψ

FOL Proof System - Lyndon

Extend the propositional system with quantifier and equality axioms:

4. (∀v (φ → ψ) → (φ → ∀v ψ)) — v not free in φ.

5. (∀v φ(v) → φ(t)) — no variable of t becomes bound in φ.

6. ∀v: v = v.

7. (v = w) → (A(v) → A(w)) — A(w) is A(v) with (some) v replaced by w.

Two inference rules:

Generalization (Gen): from φ(v) infer ∀x φ(x) — v not free in any assumption of Σ.

Modus Ponens (M.P.): from φ → ψ and φ infer ψ

Completeness and Soundness

Soundness: A sound system proves only correct entailments: Σ ⊢ φ → Σ ⊨ φ.

Soundness: any sentence that can be proved have a satisfying model.

Completeness: A complete system proves every entailment: Σ ⊨ φ → Σ ⊢ φ.

Completeness: any sentence with a satisfying model can be proved.

​

Theorem: Propositional Logic and First-Order Logic is sound and complete:

Σ ⊢ φ ⇔ Σ ⊨ φ.

​

Peano Arithmetic

Peano Theory - Example

Peano Theory – Non Equal

Gödel's Incompleteness

Theorem: if PA is consistent, there is a sentence G such that neither G nor ¬G can be proved from PA.

​

Incompleteness: some sentences cannot be proved from PA's axioms.

​

Presburger Arithmetic

Presburger Theory – Negative Numbers

• Assume we have this formula with negative numbers:

​

​

• we transform the formula to formula with natural numbers:

​

Presburger Theory – Negative Numbers

​

​

• Now transform the formula to formula without - operator:

​

​

Presburger Theory – Negative Numbers

​

​

• Finally transform the formula to formula without multiplication operator:

​

​

Theory of Integers

​

​

Theory of Integers - Example

​

​

Thank you for listening