r
/
notebook
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
notebook/notes/logic/equiv-trans.md

20 KiB
Raw Blame History

title TARGET DECK FILE TAGS tags
Equivalence Transformation Obsidian::STEM logic::equiv-trans
logic
equiv-trans

Overview

Equivalence-transformation refers to a class of calculi for manipulating propositions derived from negation (\neg), conjunction (\land), disjunction (\lor), implication (\Rightarrow), and equality (=). Gries covers two in "The Science of Programming": a system of evaluation and a formal system. The system of evaluation mirrors how a computer processes instructions, at least in an abstract sense. The formal system serves as a theoretical framework for reasoning about propositions and their transformations without resorting to "lower-level" operations like substitution.

%%ANKI Basic Who is the author of "The Science of Programming"? Back: David Gries Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What are the constant propositions? Back: T and F Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What are the basic propositional logical operators? Back: \neg, \land, \lor, \Rightarrow, and \Leftrightarrow/= Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Cloze Gries replaces logical operator {\Leftrightarrow} in favor of {=}. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic How does Lean define propositional equality? Back: Expressions a and b are propositionally equal iff a = b is true. Reference: Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d. Tags: lean

END%%

%%ANKI Basic How does Lean define propext? Back:

axiom propext {a b : Prop} : (a ↔ b) → (a = b)

Reference: Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d. Tags: lean

END%%

%%ANKI Basic What Lean theorem justifies Gries' choice of = over \Leftrightarrow? Back: propext Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. Tags: lean

END%%

%%ANKI Basic What name is given to \land operands? Back: Conjuncts Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What name is given to \lor operands? Back: Disjuncts Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What name is given to operand a in a \Rightarrow b? Back: The antecedent Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What name is given to operand b in a \Rightarrow b? Back: The consequent Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Is (b \land c) well-defined in \{(b, T), (c, F)\}? Back: Yes Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Is (b \lor d) well-defined in \{(b, T), (c, F)\}? Back: No Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What C operator corresponds to \neg? Back: ! Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. Tags: c

END%%

%%ANKI Basic What C operator corresponds to \land? Back: There isn't one. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. Tags: c

END%%

%%ANKI Basic What C operator corresponds to \lor? Back: There isn't one. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. Tags: c

END%%

%%ANKI Basic What C operator corresponds to \Rightarrow? Back: There isn't one. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. Tags: c

END%%

%%ANKI Basic What C operator corresponds to \Leftrightarrow? Back: == Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. Tags: c

END%%

%%ANKI Basic What proposition represents states \{(b, T)\} and \{(c, F)\}? Back: b \lor \neg c Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What set of states does a \land b represent? Back: The set containing just state \{(a, T), (b, T)\}. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What is sloppy about phrase "the states in b \lor \neg c"? Back: b \lor \neg c is not a set but a representation of a set (of states). Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What is the weakest proposition? Back: T Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What set of states does T represent? Back: The set of all states. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What is the strongest proposition? Back: F Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What set of states does F represent? Back: The set of no states. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What does a proposition represent? Back: The set of states in which it is true. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic When is p stronger than q? Back: When p \Rightarrow q. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic When is p weaker than q? Back: When q \Rightarrow p. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic A proposition is well-defined with respect to what? Back: A state to evaluate against. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Why is b \land c stronger than b \lor c? Back: The former represents a subset of the states the latter represents. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What is a state? Back: A function mapping identifiers to values. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What are the two calculi Gries describes equivalence-transformation with? Back: A formal system and a system of evaluation. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

Equivalence Schemas

A proposition is said to be a tautology if it evaluates to T in every state it is well-defined in. We say propositions E1 and E2 are equivalent if E1 = E2 is a tautology. In this case, we say E1 = E2 is an equivalence.

%%ANKI Basic What does it mean for a proposition to be a tautology? Back: That the proposition is true in every state it is well-defined in. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic The term "equivalent" refers to a comparison between what two objects? Back: Propositions. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What does it mean for two propositions to be equivalent? Back: Given propositions E1 and E2, it means E1 = E2 is a tautology. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What is an equivalence? Back: Given propositions E1 and E2, tautology E1 = E2. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

  • Commutative Laws
    • (E1 \land E2) = (E2 \land E1)
    • (E1 \lor E2) = (E2 \lor E1)
    • (E1 = E2) = (E2 = E1)

%%ANKI Basic Which of the basic logical operators do the commutative laws apply to? Back: \land, \lor, and = Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What do the commutative laws allow us to do? Back: Reorder operands. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What is the commutative law of e.g. \land? Back: E1 \land E2 = E2 \land E1

END%%

  • Associative Laws
    • E1 \land (E2 \land E3) = (E1 \land E2) \land E3
    • E1 \lor (E2 \lor E3) = (E1 \lor E2) \lor E3

%%ANKI Basic Which of the basic logical operators do the associative laws apply to? Back: \land and \lor Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What do the associative laws allow us to do? Back: Remove parentheses. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What is the associative law of e.g. \land? Back: E1 \land (E2 \land E3) = (E1 \land E2) \land E3 Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

  • Distributive Laws
    • E1 \lor (E2 \land E3) = (E1 \lor E2) \land (E1 \lor E3)
    • E1 \land (E2 \lor E3) = (E1 \land E2) \lor (E1 \land E3)

%%ANKI Basic Which of the basic logical operators do the distributive laws apply to? Back: \land and \lor Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What do the distributive laws allow us to do? Back: "Factor" propositions. Reference: Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What is the distributive law of e.g. \land over \lor? Back: E1 \land (E2 \lor E3) = (E1 \land E2) \lor (E1 \land E3) Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

  • De Morgan's Laws
    • \neg (E1 \land E2) = \neg E1 \lor \neg E2
    • \neg (E1 \lor E2) = \neg E1 \land \neg E2

%%ANKI Basic Which of the basic logical operators do De Morgan's Laws apply to? Back: \land and \lor Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What is De Morgan's Law of e.g. \land? Back: \neg (E1 \land E2) = \neg E1 \lor \neg E2 Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

  • Law of Negation
    • \neg (\neg E1) = E1

%%ANKI Basic What does the Law of Negation say? Back: \neg (\neg E1) = E1 Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

  • Law of the Excluded Middle
    • E1 \lor \neg E1 = T

%%ANKI Basic Which of the basic logical operators does the Law of the Excluded Middle apply to? Back: \lor Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What does the Law of the Excluded Middle say? Back: E1 \lor \neg E1 = T Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Which equivalence schema is "refuted" by sentence, "This sentence is false." Back: Law of the Excluded Middle Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

  • Law of Contradiction
    • E1 \land \neg E1 = F

%%ANKI Basic Which of the basic logical operators does the Law of Contradiction apply to? Back: \land Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What does the Law of Contradiction say? Back: E1 \land \neg E1 = F Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Cloze The Law of {1:the Excluded Middle} is to {2:\lor} whereas the Law of {2:Contradiction} is to {1:\land}. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

Gries lists other "Laws" but they don't seem as important to note here.

%%ANKI Basic How is \Rightarrow written in terms of other logical operators? Back: p \Rightarrow q is equivalent to \neg p \lor q. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic How is \Leftrightarrow/= written in terms of other logical operators? Back: p \Leftrightarrow q is equivalent to (p \Rightarrow q) \land (q \Rightarrow p). Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

Equivalence Rules

  • Rule of Substitution
    • Let P(r) be a predicate and E1 = E2 be an equivalence. Then P(E1) = P(E2) is an equivalence.
  • Rule of Transitivity
    • Let E1 = E2 and E2 = E3 be equivalences. Then E1 = E3 is an equivalence.

%%ANKI Basic What two inference rules make up the equivalence-transformation formal system? Back: Substitution and transitivity. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What does the rule of substitution say in the system of evaluation? Back: Let P(r) be a predicate and E1 = E2 be an equivalence. Then P(E1) = P(E2) is an equivalence. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic How is the rule of substitution written as an inference rule (in standard form)? Back:


\begin{matrix}
E1 = E2 \\
\hline P(E1) = P(E2)
\end{matrix}

END%%

%%ANKI Basic What does the rule of transitivity state in the system of evaluation? Back: Let E1 = E2 and E2 = E3. Then E1 = E3. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic How is the rule of transitivity written as an inference rule (in standard form)? Back:


\begin{matrix}
E1 = E2, E2 = E3 \\
\hline E1 = E3
\end{matrix}

END%%

%%ANKI Cloze The system of evaluation has {equivalences} whereas the formal system has {theorems}. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

Normal Forms

Every proposition can be written in disjunctive normal form (DNF) and conjunctive normal form (CNF). This is evident with the use of truth tables. To write a proposition in DNF, write its corresponding truth table and \lor each row that evaluates to T. To write the same proposition in CNF, apply \lor to each row that evaluates to F and negate it.

\neg (a \Rightarrow b) \Leftrightarrow c

It's truth table looks like

\begin{array}{c|c|c|c|c|c}
\neg & (a & \Rightarrow & b) & \Leftrightarrow & c \\
\hline
F & T & T & T & F & T \\
F & T & T & T & T & F \\
T & T & F & F & T & T \\
T & T & F & F & F & F \\
F & F & T & T & F & T \\
F & F & T & T & T & F \\
F & F & T & F & F & T \\
F & F & T & F & T & F
\end{array}$$

and it's DNF looks like

(a \land b \land \neg c) \lor (a \land \neg b \land c) \lor (\neg a \land b \land \neg c) \lor (\neg a \land \neg b \land \neg c)



It's CNF results from applying De Morgan's Law to the truth table's "complement":

\neg( (a \land b \land c) \lor (a \land \neg b \land \neg c) \lor (\neg a \land b \land c) \lor (\neg a \land \neg b \land c) )



%%ANKI
Basic
What construct is used to prove every proposition can be written in DNF or CNF?
Back: Truth tables
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707311868994-->
END%%

%%ANKI
Basic
Where are $\land$ and $\lor$ found within a proposition in DNF?
Back: $\lor$ separates disjuncts containing $\land$.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707311868998-->
END%%

%%ANKI
Basic
What is DNF an acronym for?
Back: **D**isjunctive **N**ormal **F**orm.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707311869000-->
END%%

%%ANKI
Basic
What is CNF an acronym for?
Back: **C**onjunctive **N**ormal **F**orm.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707311869002-->
END%%

%%ANKI
Basic
Where are $\land$ and $\lor$ found within a proposition in CNF?
Back: $\land$ separates conjuncts containing $\lor$.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707311869003-->
END%%

## References

* Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
* Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.