Introduction of Logic | xiaojuan’s blog

type

status

date

slug

summary

Proposition Logic

1. Logic Sentence

proposition constants: A propositional vocabulary is a set/sequence of primitive symbols, called proposition constants. eg. raining, r32aining

propositional sentence: a member of the vocabulary or a compound expression using logical operators.

Negations
Conjunctions
Disjunctions
Implications
Biconditionals

Precedence: ¬, ∧, ∨, ⇒, ⇔

∧ or ∨: left; ⇒ or ⇔: right

propositional language: the set of all propositional sentences that can be formed from a propositional vocabulary.

2. Semantics

propositional interpretation: an association between the propositional constants in a propositional language and the values T or F

sentential interpretation: an association between the sentences in a propositional language and the truth values T or F.

Semantics of different 连接词 (略）

3. Evaluation

根据对proposition constant的interpretation，evaluate the truth of compound Sentence. For example:

4. Satisfaction

Evaluation versus Satisfaction

根据sentence truth来找出proposition constant的interpretation，可以使用truth table

Truth Tables: a table of all possible interpretations for the propositional constants in a language.

Propositional Analysis

1. Properties of Sentences

valid: A sentence is valid if and only if every interpretation satisfies it.(satisfiablez)

contingent: A sentence is contingent if and only if some interpretation satisfies it and some interpretation falsifies it. (satisfiable) (falsifiable)

unsatisfiable: A sentence is unsatisfiable if and only if no interpretation satisfies it. (falsifiable)

2. Relationships Between Sentences

logically equivalent: have the same value for every propositional interpretation

logically entails (|=) : every interpretation that satisfies ϕ also satisfies ψ.

Sets of Premises/conclusion: ,等价于/\

Validities: If {} ⊨ ϕ , then ϕ is valid.

Vacuity: If Δ is unsatisfiable, then Δ ⊨ ϕ for all ϕ.

Monotonicity: If Γ ⊨ ϕ and Γ ⊆ Δ, then Δ ⊨ ϕ.

Ramification: If Ω ⊨ Δ and Γ ⊆ Δ, then Ω ⊨ Γ.

Logical Consistency: A sentence φ is consistent with a sentence ψ if and only if there is a truth assignment that satisfies both φ and ψ.

3. Connections (metatheorems)

Monotonicity Theorem

Ramification Theorem

Equivalence Theorem: A sentence φ and a sentence ψ are logically equivalent if and only if the sentence (φ ⇔ ψ) is valid.

Substitution Theorem: If(ϕ ⇔ ψ) is valid, then the sentence χϕ←ψ is logically equivalent to χ.

Deduction Theorem: A sentence φ logically entails a sentence ψ if and only if (φ ⇒ ψ) is valid

Unsatisfiability Theorem: Δ ⊨ ϕ if and only if Δ ∪ {¬ϕ} is unsatisfiable.

Consistency Theorem: A sentence φ is logically consistent with a sentence ψ if and only if the sentence (φ ∧ ψ) is satisfiable.

Direct Proofs (Hilbert)

1. Direct Proof

Schemas / Schemata

for example:

instance: substituting sentences for the metavariables in the rule

valid schema: an infinite set of sentences, all of which are valid

rule of inference: a pattern of reasoning consisting of zero or more schemas, called premises, and one or more additional schemas, called conclusions.

proof:

2. Proof Systems

A proof system is a finite set of (usually valid) axiom schemata and (usually sound) rules of inference.

3. Soundness and Completeness

The Hilbert System is sound and complete for Propositional Logic.

Natural Deduction (Fitch system)

1. rules of inference

Implication Introduction

Implication Elimination

Negation Introduction (NI):

Negation Elimination (NE)

And Introduction (AI):

And Elimination (AE):

Or Introduction (OI):

Or Elimination (OE):

Biconditional Introduction (BI):

Biconditional Elimination (BE):

2. Soundness and Completeness

Fitch is sound and complete for Propositional Logic.

3. Reasoning tips

Given a goal (φ ⇒ ψ), it is often good to assume φ, prove ψ, and then use Implication Introduction.

Given a goal (φ ∧ ψ), prove φ, prove ψ, and then use And Introduction to derive (φ ∧ ψ).

Given a goal (φ ∨ ψ), try to prove φ or prove ψ (only one is needed), then use Or Introduction to disjoin with anything else.

Given a goal of the form ¬φ, assume φ and derive the sentence (φ ⇒ ψ), assume φ again and derive the sentence ¬ψ leading to (φ ⇒ ¬ψ), and use Negation Introduction to derive ¬φ.

Given a goal φ, assume ¬φ, prove a contradiction, thereby deriving ¬¬φ, and then apply Negation Elimination to get φ. ¬p ⇒ q, ¬p ⇒ ¬q, ¬¬p

Given a premise of the form (φ ⇒ ψ) and a goal ψ, try proving φ and then use Implication Elimination to derive ψ.

Given a premise (φ ∨ ψ) and a goal χ, try proving (φ ⇒ χ) and (ψ ⇒ χ) and use Or Elimination to derive χ

Refutation Proofs (Robinson)

A refutation proof is a proof by contradiction

Propositional Resolution is a refutation proof system.

Just one rule of inference - the Resolution Principle.

Propositional Resolution is sound and complete.

but works only on expressions in clausal form

1. Clausal Form

literal: either an atomic sentence or a negation of an atomic sentence

clausal sentence: either a literal or a disjunction of literals

clause: A clause is a set of literals

Clauses are Disjunctions

Conversion to Clausal Form:

Implications Out:
Negations In:
Distribution
Operators Out

2. Resolution Principle

3. Resolution Reasoning

A resolution derivation of a conclusion from a set of premises is a finite sequence of clauses terminating in the conclusion in which each clause is either a premise or the result of applying the resolution principle to earlier elements of the sequence.

Unsatisfiability Determination: If a set of clauses is unsatisfiable, it is possible to derive the empty clause using the Resolution Principle.

Unsatisfiability Theorem: Δ ⊨ ϕ if and only if Δ ∪ {¬ϕ} is unsatisfiable.

Thus, Resolution Method: To prove that a set Δ of sentences logically entails a conclusion φ, write Δ ∪ {¬φ} in clausal form and derive the empty clause.

Relational Logic

1. Syntax

Constants: object constants; Relation constants

Vocabularies: A vocabulary / signature consists of a finite, non-empty set of object constants and a finite, non-empty set of relation constants together with a specification of arity for the relation constants.

term: either (1) a variable or (2) an object constant.

sentences:

relational sentence: an expression formed from an n-ary relation constant and n terms enclosed in parentheses and separated by commas. (called atoms or atomic sentences) eg. q(ay)

Logical sentences: (p(a) ∧ p(b))

Quantified Sentences

ground: An expression is ground if and only if it contains no variables.

An occurrence of a variable is bound if and only if it in in the scope of a quantifier of that variable. Else, free.

A sentence is open if and only if it has free variables. Otherwise, it is closed.

2. Semantics

Truth Assignment: an association between ground atomic sentences and the truth values true or false.

Sentential truth assignment

An instance of an expression is an expression in which all free variables have been consistently replaced by ground terms.

A truth assignment satisfies a sentence with free variables if and only if it satisfies every instance of that sentence

Relational Analysis

Propositional Metatheorems

Common Quantifier Reversal

Distributing Existentials over Universals but not Distributing Universals over Existentials !!!

Distributing Quantifiers over Operators

Distributing Quantifiers over Implications

Distributing Operators over Quantifiers

Determining Logical Entailment

Relational Proofs

Fitch is sound and complete for Relational Logic.

Functional Logic

1. Syntax

Constants

Function constants (constructors) represent functions.
Object constants (symbols) represent objects.
Relation constants (predicates) represent relations.

arity: The arity of a function constant or a relation constant is the number of arguments it takes.

Unary function or relation constant
…
n-ary function or relation constant

Signatures: A signature consist of a set of object constants, a set of function constants, and a set of relation constants together with a specification of arity for the function constants and relation constants.

term: either a variable, an object constant, or a functional term (defined shortly).

A functional term is an expression consisting of an n-ary function constant and n terms enclosed in parentheses and separated by commas.

Sentences

Relational sentences: an expression formed from an n-ary relation constant and n terms enclosed in parentheses and separated by commas but not terms and cannot be nested inside terms or relational sentences.
Logical sentences
Quantified sentences

2. Semantics

Resolution

1. Clausal Form

Implications Out

Negations In

Standardize variables: ∀x. p(x) ∨ ∀x.q(x)→ ∀x. p(x) ∨ ∀y.q(y)

Existentials Out (Outside in): ∃x. p(x)→ p(a)

Alls Out: ∀x.( p(x) ∧ q(x, y, f (x, y)))→ p(x) ∧ q(x, y, f (x, y))

Distribution

Operators Out

2. Unification

Unification is the process of determining whether two expressions can be unified

Composition of Substitutions

most general unifier

If two expressions are unifiable, then they have an mgu that is unique up to variable permutation.

Unification procedure

3. Resolution Principle

simple version

improved version

4. Resolution Reasoning

If empty clause generated, the original set is unsatisfiable.

5. Logical Entailment

A sentence ϕ is provable from a set of sentences Δ by resolution if and only if there is a derivation of the empty clause from the clausal form of Δ∪{¬ϕ}

A resolution proof is a derivation of the empty clause from the clausal form of the premises and the negation of the desired conclusion.

Proposition Logic

1. Logic Sentence

2. Semantics

3. Evaluation

4. Satisfaction

Propositional Analysis

1. Properties of Sentences

2. Relationships Between Sentences

3. Connections (metatheorems)

Direct Proofs (Hilbert)

1. Direct Proof

2. Proof Systems

3. Soundness and Completeness

Natural Deduction (Fitch system)

1. rules of inference

2. Soundness and Completeness

3. Reasoning tips

Refutation Proofs (Robinson)

1. Clausal Form

2. Resolution Principle

3. Resolution Reasoning

Relational Logic

1. Syntax

2. Semantics

Relational Analysis

Relational Proofs

Functional Logic

1. Syntax

2. Semantics

Resolution

1. Clausal Form

2. Unification

3. Resolution Principle

4. Resolution Reasoning

5. Logical Entailment

6. Answer Extraction