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

8.5 KiB
Raw Blame History

title TARGET DECK FILE TAGS tags
Quantification Obsidian::STEM logic::quantification
logic
quantification

Overview

A quantifier refers to an operator that specifies how many members of a set satisfy some formula. The most common quantifiers are \exists and \forall, though others (such as the counting quantifier) are also used.

%%ANKI Basic What are the most common first-order logic quantifiers? Back: \exists and \forall Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What term refers to operators like \exists and \forall? Back: Quantifiers. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

  • Existential quantification (\exists) asserts the existence of at least one member in a set satisfying a property.

%%ANKI Basic What symbol denotes existential quantification? Back: \exists Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic How many members in the domain of discourse must satisfy a property in existential quantification? Back: At least one. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic \exists x : S, P(x) is shorthand for what? Back: \exists x, x \in S \land P(x) Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What term refers to S in \exists x : S, P(x)? Back: The domain of discourse. Reference: Oscar Levin, Discrete Mathematics: An Open Introduction, 3rd ed., n.d., https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf.

END%%

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

END%%

  • Universal quantification (\forall) asserts that every member of a set satisfies a property.

%%ANKI Basic What symbol denotes universal quantification? Back: \forall Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic How many members in the domain of discourse must satisfy a property in universal quantification? Back: All of them. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic \forall x : S, P(x) is shorthand for what? Back: \forall x, x \in S \Rightarrow P(x) Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

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

END%%

%%ANKI Cloze {1:\exists} is to {2:\lor} as {2:\forall} is to {1:\land}. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic How is \forall x : S, P(x) equivalently written in terms of existential quantification? Back: \neg \exists x : S, \neg P(x) Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI How is \exists x : S, P(x) equivalently written in terms of universal quantification? Back: \neg \forall x : S, \neg P(x) Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. END%%

  • Counting quantification (\exists^{=k} or \exists^{\geq k}) asserts that (at least) k (say) members of a set satisfy a property.

%%ANKI Basic What symbol denotes counting quantification (of exactly k members)? Back: \exists^{=k} Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What symbol denotes counting quantification (of at least k members)? Back: \exists^{\geq k} Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic How is \exists x : S, P(x) written in terms of counting quantification? Back: \exists^{\geq 1} x : S, P(x) Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic How is \forall x : S, P(x) written in terms of counting quantification? Back: Assuming S has k members, \exists^{= k} x : S, P(x) Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

Identifiers

Identifiers are said to be bound if they are parameters to a quantifier. Identifiers that are not bound are said to be free. A first-order logic formula is said to be in prenex normal form (PNF) if written in two parts: the first consisting of quantifiers and bound variables (the prefix), and the second consisting of no quantifiers (the matrix).

%%ANKI Basic When is an identifier said to be bound? Back: When it is specified as a parameter to a quantifier. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic When is an identifier said to be free? Back: When it isn't specified as a parameter to a quantifier. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Cloze An identifier that is not {bound} is instead {free}. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Prenex normal form consists of what two parts? Back: The prefix and the matrix. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic How is the prefix of a formula in PNF formatted? Back: As only quantifiers and bound variables. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic How is the matrix of a formula in PNF formatted? Back: Without quantifiers. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Which identifiers in the following are bound? \exists x, P(x) \land P(y) Back: Just x. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Which identifiers in the following are free? \exists x, P(x) \land P(y) Back: Just y. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic How is the following rewritten in PNF? (\exists x, P(x)) \land (\exists y, P(y)) Back: \exists x \;y, P(x) \land P(y) Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

References