Polimi CS - Notes

0 - References

6 min read

Chapter 1

Proposition 1.39: Product and Boolean structure

The product of relations is compatible with the Boolean structure of , in the sense that the following formulas hold when the operations are defined.

Proposition 1.48

For every relation the following formula holds:

Proposition 1.49

The opposite operation is compatible with inclusion, in the sense that the following formula holds for relations ,

Proposition 1.50

The opposite operation is compatible with the Boolean structure of relations in the sense that the following formulas hold.

Proposition 1.51

The opposite relation operation is compatible with the multiplicative structure, in the sense that the following formulas hold.

Proposition 1.59

If is a binary relation, then

  1. has at least one element for every if and only if ;
  2. has at most one element for every if and only if .

Thus, is a function if and only if

Proposition 1.72

Let be a function. Then

  1. is surjective if and only if ,
  2. is injective if and only if .

Therefore is a function if and only if is an isomorphism and in this case .

Proposition 1.84

Let be a property of relations on . Assume that:

  • For every relation on , there exists a relation containing .
  • is closed under intersections. Then, every relation on has -closure.

Lemma 1.145: Mono factorization

Assume, in the diagram below, that is an arbitrary function and a monomorphism. Then factors through if and only if . In this case is unique and

Chapter 2

Theorem 2.76: Induction for Uniform Notation

Let be a propositional language in the uniform set of connectives and let be a property of the formulas of . Then if and only if the following conditions are satisfied for every formula .

  1. If is atomic, then .
  2. If , then .
  3. If is an -formula and , then .
  4. If is a -formula and , then .

Definition 2.108

A Hintikka set is a set of formulas satisfying the following conditions:

  1. If is a propositional variable and , then ;
  2. ;
  3. If , then ;
  4. If then ;
  5. If , then or .

Corollary 2.114

Every element of a consistency poset is satisfiable.

Theorem 2.135

Assume ⊢ is an inference relation on .

  1. is sound if and only if every satisfiable set is consistent.
  2. is complete if and only if every consistent set is satisfiable.

Therefore, is sound and complete if and only if satisfiable and consistent sets coincide.

Proposition 2.136

Assuming the other properties of an inference rule, composition is equivalent to each of the following conditions.

Corollary 2.137

The following formulas hold for every inference relation.

Lemma 2.142: Lindenbaum

For a completely regular inference, every consistent set is contained in a complete consistent set.

Proposition 2.143

If is a completely regular inference and is a complete consistent set, then

Definition 2.147

An inference relation is regular if it satisfies the following conditions.

Proposition 2.149

For a regular inference, the class

of consistent sets is a consistency poset.

Definition 2.172

The following inference rules, in which ᵢ and ⱼ are generalized clauses, are allowed in the resolution calculus.

  • Falsehood. From a clause in which occurs, one can derive by omitting the occurrence of . Likewise, if occurs in one can derive by omitting .
  • Double negation. From a clause in which If occurs, one can derive by replacing the occurrence of with .
  • -expansion. From a clause in which a conjunctive formula occurs, one can derive by replacing the occurrence of with either or .
  • -expansion. From a clause in which a disjunctive formula occurs, one can derive the clause by replacing with the two components and .
  • Resolution. If the component occurs in and occurs in , one can infer the clause by omitting from from and then forming the union of the remaining components.
  • Cut. If is any formula, the clause can always be derived.

Lemma 2.182

A set has a closed expansion if and only if .

Backlinks

Graph View