The Open Logic Project PKGMM3P5QY

URI	`m2://res/PKGMM3P5QY`
Kind	textbook
Creators	The Open Logic Project
Date	2026-08-14
MSC	03-01
Scope	in

Expressions

e1: edition

Language	en
Date	2026-08-14

Contents

section 1: Bisimulations
chapter 1: aml
section 1.1: Introduction
section 1.2: The Language of Epistemic Logic
section 1.3: Accessibility Relations and Epistemic Principles
section 1.4: Public Announcement Logic
section 1.5: Semantics of Public Announcement Logic
section 1.6: Relational Models
section 1.7: Truth at a World
section 1.8: Additional Operators for Temporal Logic
section 1.9: Introduction
section 1.10: Possible Histories
section 1.11: Properties of Temporal Frames
section 1.12: Semantics for Temporal Logic
chapter 2: aml
section 2.1: Applying the Fixed-Point Theorem
section 2.2: Computably Enumerable Sets are Closed under Union and Intersection
section 2.3: Computably Enumerable Sets
section 2.4: Coding Computations
section 2.5: Computably Enumerable Sets not Closed under Complement
section 2.6: Complete Computably Enumerable Sets
chapter 3: cmp
section 3.1: Computable Sets
section 3.2: Defining Functions using Self-Reference
section 3.3: Equivalent Defininitions of Computably Enumerable Sets
section 3.4: The Fixed-Point Theorem
section 3.5: The Halting Problem
section 3.6: Introduction
section 3.7: An Example of Reducibility
section 3.8: No Universal Computable Function
section 3.9: There Are Non-Computable Sets
section 3.10: The Normal Form Theorem
section 3.11: Properties of Reducibility
section 3.12: Reducibility
section 3.13: Rice's Theorem
section 3.14: Comparison with Russell's Paradox
section 3.15: The $s$-$m$-$n$ Theorem
section 3.16: Totality is Undecidable
section 3.17: The Universal Partial Computable Function
section 3.18: Bounded Minimization
section 3.19: Composition
section 3.20: Examples of Primitive Recursive Functions
section 3.21: General Recursive Functions
section 3.22: The Halting Problem
section 3.23: Introduction
section 3.24: Non-Primitive Recursive Functions
section 3.25: The Normal Form Theorem
section 3.26: Primitive Recursion Notations
section 3.27: Other Recursions
section 3.28: Partial Recursive Functions
section 3.29: Primitive Recursive Functions are Computable
section 3.30: Primitive Recursion Functions
section 3.31: Primitive Recursive Relations
section 3.32: Primes
section 3.33: Primitive Recursion
chapter 4: cmp
section 4.1: Sequences
section 4.2: Trees
section 4.3: Counterfactuals
chapter 5: cnt
section 5.1: The Material Conditional
section 5.2: Paradoxes of the Material Conditional
section 5.3: The Strict Conditional
section 5.4: Antecedent Strengthening
section 5.5: Contraposition
section 5.6: Introduction
chapter 6: cnt
section 6.1: Sphere Models
section 6.2: Transitivity
section 6.3: Truth and Falsity of Counterfactuals
chapter 7: fol
chapter 8: pl
section 8.1: Axioms and Rules for the Propositional Connectives
section 8.2: Axioms and Rules for Quantifiers
section 8.3: The Deduction Theorem with Quantifiers
section 8.4: The Deduction Theorem
section 8.5: \usetoken{P}{derivation} with \usetoken{S}{identity}
section 8.6: Proof-Theoretic Notions
section 8.7: \usetoken{S}{derivability} and Consistency
section 8.8: \usetoken{S}{derivability} and the Propositional Connectives
section 8.9: \usetoken{S}{derivability} and the Quantifiers
section 8.10: Properties of \usetoken{S}{derivability}
section 8.11: \usetoken{P}{derivation} with Quantifiers
section 8.12: Examples of \usetoken{P}{derivation}
section 8.13: Rules and \usetoken{P}{derivation}
section 8.14: Soundness
chapter 9: fol
section 9.1: Higher-Order logic
section 9.2: Overview
section 9.3: Intuitionistic Logic
section 9.4: Many-Sorted Logic
section 9.5: Modal Logics
section 9.6: Other Logics
section 9.7: Second-Order logic
section 9.8: A Direct Proof of the Compactness Theorem
section 9.9: The Compactness Theorem
section 9.10: Complete Consistent Sets of \usetoken{P}{sentence}
section 9.11: The Completeness Theorem
chapter 10: fol
chapter 11: pl
section 11.1: Construction of a Model
section 11.2: The L\"owenheim--Skolem Theorem
section 11.3: Henkin Expansion
section 11.4: Identity
section 11.5: Introduction
section 11.6: Lindenbaum's Lemma
section 11.7: Maximally Consistent Sets of \usetoken{P}{sentence}
section 11.8: Outline of the Proof
section 11.9: First-Order Logic
section 11.10: \usetoken{P}{formula}
chapter 12: fol
section 12.1: Models and Theories
section 12.2: Satisfaction
section 12.3: Semantic Notions
section 12.4: \usetoken{P}{sentence}
section 12.5: Soundness and Completeness
section 12.6: Substitution
section 12.7: Syntax
section 12.8: Expressing Properties of \printtoken{P}{structure}
section 12.9: Expressing Relations in \article{structure} \printtoken{S}{structure}
section 12.10: Introduction
chapter 13: fol
section 13.1: The Theory of Sets
section 13.2: Expressing the Size of \printtoken{P}{structure}
section 13.3: Examples of First-Order Theories
section 13.4: \usetoken{P}{derivation}
section 13.5: \usetoken{P}{derivation} with \usetoken{S}{identity}
chapter 14: fol
chapter 15: pl
section 15.1: Proof-Theoretic Notions
section 15.2: Propositional Rules
subsection 15.2.1: Rules for $\land$
subsection 15.2.2: Rules for $\lor$
subsection 15.2.3: Rules for $\lif$
subsection 15.2.4: Rules for $\lnot$
subsection 15.2.5: Rules for $\lfalse$
section 15.3: \usetoken{S}{derivability} and Consistency
section 15.4: \usetoken{S}{derivability} and the Propositional Connectives
section 15.5: \usetoken{S}{derivability} and the Quantifiers
section 15.6: \usetoken{P}{derivation} with Quantifiers
section 15.7: Examples of \usetoken{P}{derivation}
section 15.8: Quantifier Rules
subsection 15.8.1: Rules for $\lforall$
subsection 15.8.2: Rules for $\lexists$
section 15.9: Rules and \usetoken{P}{derivation}
section 15.10: Soundness with \usetoken{S}{identity}
section 15.11: Soundness
section 15.12: Axiomatic \usetoken{P}{derivation}
section 15.13: Introduction
section 15.14: Natural Deduction
chapter 16: fol
chapter 17: pl
section 17.1: The Sequent Calculus
section 17.2: \usetoken{P}{tableau}
section 17.3: \usetoken{P}{derivation}
section 17.4: \usetoken{P}{derivation} with \usetoken{S}{identity}
section 17.5: Proof-Theoretic Notions
section 17.6: Propositional Rules
subsection 17.6.1: Rules for $\lnot$
subsection 17.6.2: Rules for $\land$
subsection 17.6.3: Rules for $\lor$
subsection 17.6.4: Rules for $\lif$
section 17.7: \usetoken{S}{derivability} and Consistency
section 17.8: \usetoken{S}{derivability} and the Propositional Connectives
section 17.9: \usetoken{S}{derivability} and the Quantifiers
section 17.10: \usetoken{P}{derivation} with Quantifiers
section 17.11: Examples of \usetoken{P}{derivation}
section 17.12: Quantifier Rules
subsection 17.12.1: Rules for $\lforall$
subsection 17.12.2: Rules for $\lexists$
section 17.13: Rules and \usetoken{P}{derivation}
chapter 18: fol
chapter 19: pl
section 19.1: Soundness with \usetoken{S}{identity}
section 19.2: Soundness
section 19.3: Structural Rules
subsection 19.3.1: Weakening
subsection 19.3.2: Contraction
subsection 19.3.3: Exchange
section 19.4: Variable Assignments
section 19.5: Covered \printtoken{P}{structure} for First-order Languages
section 19.6: Extensionality
section 19.7: First-Order Languages
section 19.8: Formation Sequences
section 19.9: Free \printtoken{P}{variable} and \printtoken{P}{sentence}
section 19.10: Introduction
section 19.11: Introduction
section 19.12: Introduction
section 19.13: \printtoken{S}{main operator} of a Formula
section 19.14: Satisfaction of \article{formula} \printtoken{S}{formula} in \article{structure} \printtoken{S}{structure}
section 19.15: Semantic Notions
chapter 20: fol
section 20.1: \printtoken{P}{structure} for First-order Languages
section 20.2: \printtoken{P}{subformula}
section 20.3: Substitution
chapter 21: fol
chapter 22: fol
section 22.1: Terms and \printtoken{P}{formula}
section 22.2: Unique Readability
section 22.3: \usetoken{P}{tableau}
section 22.4: \usetoken{P}{tableau} with \usetoken{S}{identity}
section 22.5: Proof-Theoretic Notions
section 22.6: Propositional Rules
subsection 22.6.1: Rules for $\lnot$
subsection 22.6.2: Rules for $\land$
subsection 22.6.3: Rules for $\lor$
subsection 22.6.4: Rules for $\lif$
subsection 22.6.5: The Cut Rule
section 22.7: \usetoken{S}{derivability} and Consistency
section 22.8: \usetoken{S}{derivability} and the Propositional Connectives
section 22.9: \usetoken{S}{derivability} and the Quantifiers
section 22.10: \usetoken{P}{tableau} with Quantifiers
section 22.11: Examples of \usetoken{P}{tableau}
section 22.12: Quantifier Rules
subsection 22.12.1: Rules for $\lforall$
subsection 22.12.2: Rules for $\lexists$
section 22.13: Rules and \usetoken{P}{tableau}
section 22.14: Soundness with \usetoken{S}{identity}
section 22.15: Soundness
chapter 23: fol
chapter 24: pl
section 24.1: Alan Turing
section 24.2: Alfred Tarski
section 24.3: Alonzo Church
section 24.4: Bertrand Russell
chapter 25: his
section 25.1: Emmy Noether
section 25.2: Ernst Zermelo
section 25.3: Georg Cantor
section 25.4: Gerhard Gentzen
section 25.5: Julia Robinson
section 25.6: Kurt G\"odel
section 25.7: R\'ozsa P\'eter
section 25.8: Cantor on the Line and the Plane
section 25.9: Appendix: Hilbert's Space-filling Curves
section 25.10: Infinitesimals and Differentiation
section 25.11: Rigorous Definition of Limits
section 25.12: More Myth than History?
section 25.13: Pathologies
chapter 26: his
chapter 27: inc
section 27.1: Coding \printtoken{P}{formula}
section 27.2: Coding Symbols
section 27.3: Coding Terms
section 27.4: Introduction
section 27.5: Axiomatic \usetoken{P}{derivation}
section 27.6: \usetoken{P}{derivation} in $\Log{LK}$
section 27.7: \usetoken{P}{derivation} in Natural Deduction
section 27.8: Substitution
section 27.9: The First Incompleteness Theorem
section 27.10: The Fixed-Point Lemma
section 27.11: Comparison with G\"odel's Original Paper
chapter 28: inc
section 28.1: Introduction
section 28.2: L\"ob's Theorem
section 28.3: The \usetoken{S}{derivability} Conditions for $\Th{PA}$
section 28.4: Rosser's Theorem
section 28.5: The Second Incompleteness Theorem
section 28.6: The Undefinability of Truth
section 28.7: Definitions
section 28.8: Historical Background
chapter 29: inc
section 29.1: Overview of Incompleteness Results
section 29.2: Undecidability and Incompleteness
section 29.3: Basic Functions are Representable in~$\Th{Q}$
section 29.4: The Beta Function Lemma
section 29.5: Functions in $C$ are Representable in $\Th{Q}$
section 29.6: The Functions $C$
section 29.7: Computable Functions are Representable in $\Th{Q}$
section 29.8: Composition is Representable in $\Th{Q}$
section 29.9: Introduction
section 29.10: Regular Minimization is Representable in $\Th{Q}$
section 29.11: Simulating Primitive Recursion
chapter 30: inc
section 30.1: Functions Representable in $\Th{Q}$ are Computable
section 30.2: Representing Relations
section 30.3: \texorpdfstring{$\Sigma_1$}{Sigma-1} completeness
section 30.4: Undecidability
section 30.5: \printtoken{S}{axiomatizable} Complete Theories are Decidable
section 30.6: \printtoken{S}{axiomatizable} Theories
section 30.7: Theories Consistent with $\Th{Q}$ are Undecidable
section 30.8: Consistent Extensions of $\Th{Q}$ are Undecidable
section 30.9: $\Th{Q}$ has no Complete, Consistent, !!^{axiomatizable} Extensions
section 30.10: Sentences Provable and Refutable in $\Th{Q}$ are Computably Inseparable
section 30.11: Theories in which $\Th{Q}$ is Interpretable are Undecidable
section 30.12: Introduction
section 30.13: $\omega$-Consistent Extensions of $\Th{Q}$ are Undecidable
section 30.14: $\Th{Q}$ is \printtoken{S}{c.e.}-Complete
chapter 31: inc
section 31.1: Axiomatic \usetoken{P}{derivation}
section 31.2: The Brouwer--Heyting--Kolmogorov Interpretation
section 31.3: Constructive Reasoning
chapter 32: int
section 32.1: Natural Deduction
subsection 32.1.1: Conjunction
subsection 32.1.2: Conditional
subsection 32.1.3: Disjunction
subsection 32.1.4: Absurdity
subsection 32.1.5: Rules for $\lnot$
subsection 32.1.6: Examples of \usetoken{P}{derivation}
section 32.2: Syntax of Intuitionistic Logic
section 32.3: Introduction
section 32.4: Propositions
section 32.5: \usetoken{P}{relational model}
section 32.6: Semantic Notions
chapter 33: int
section 33.1: Topological Semantics
section 33.2: The Canonical Model
section 33.3: The Completeness Theorem
section 33.4: Decidability
section 33.5: Lindenbaum's Lemma
section 33.6: Soundness of Axiomatic \usetoken{P}{derivation}
chapter 34: int
section 34.1: Soundness of Natural Deduction
section 34.2: The Truth Lemma
section 34.3: Introduction
section 34.4: \usetoken{P}{tableau} for Intuitionistic Logic
section 34.5: Rules for Intuitionistic Logic
section 34.6: Soundness for Intuitionistic \usetoken{P}{tableau}
chapter 35: int
section 35.1: $\beta\eta$-reduction
section 35.2: $\beta$-reduction
chapter 36: lam
section 36.1: Definition and Properties
section 36.2: Parallel $\beta\eta$-reduction
section 36.3: Parallel $\beta$-reduction
section 36.4: The Basic Primitive Recursive Functions are \usetoken{S}{lambda definable}
section 36.5: The Church--Rosser Property
section 36.6: The \usetoken{S}{lambda definable} Functions are Closed under Composition
section 36.7: Computable Functions are \usetoken{S}{lambda definable}
section 36.8: Currying
section 36.9: Fixed-Point Combinators
chapter 37: lam
section 37.1: \usetoken{S}{lambda definable} Functions are Computable
section 37.2: \usetoken{S}{lambda definable} Arithmetical Functions
section 37.3: The \usetoken{S}{lambda definable} Functions are Closed under Minimization
section 37.4: Overview
section 37.5: \usetoken{S}{lambda definable} Functions are Closed under Primitive Recursion
section 37.6: Reduction of Lambda Terms
section 37.7: The Syntax of the Lambda Calculus
section 37.8: \usetoken{S}{lambda definable} Arithmetical Functions
section 37.9: Fixpoints
section 37.10: Introduction
chapter 38: lam
section 38.1: \usetoken{S}{lambda definable} Functions are Recursive
section 38.2: Lists
section 38.3: Minimization
section 38.4: Pairs and Predecessor
section 38.5: Partial Recursive Functions are \usetoken{S}{lambda definable}
section 38.6: Primitive Recursive Functions are \usetoken{S}{lambda definable}
section 38.7: Truth Values and Relations
section 38.8: Abbreviated Syntax
section 38.9: $\alpha$-Conversion
section 38.10: $\beta$-reduction
section 38.11: Conversion and Reduction
section 38.12: The De Bruijn Index
section 38.13: $\eta$-conversion
section 38.14: Free Variables
section 38.15: Substitution
chapter 39: lam
section 39.1: Terms as $\alpha$-Equivalence Classes
section 39.2: Terms
section 39.3: Unique Readability
section 39.4: G\"odel logics
chapter 40: mvl
section 40.1: Introduction
section 40.2: \L ukasiewicz logic
section 40.3: Introduction
section 40.4: Proof-Theoretic Notions
section 40.5: Propositional Rules for Selected Logics
subsection 40.5.1: Rules for $\lnot$
subsection 40.5.2: Rules for $\land$
subsection 40.5.3: Rules for $\lor$
subsection 40.5.4: Rules for $\lif$
section 40.6: Rules and \usetoken{P}{derivation}
chapter 41: mvl
section 41.1: Structural Rules
section 41.2: Languages and Connectives
section 41.3: \usetoken{P}{formula}
section 41.4: Introduction
section 41.5: Matrices
section 41.6: Semantic Notions
section 41.7: Many-valued logics as sublogics of~$\LogCL$
chapter 42: mvl
section 42.1: \usetoken{P}{valuation} and Satisfaction
section 42.2: G\"odel logics
section 42.3: Introduction
section 42.4: Kleene logics
section 42.5: \L ukasiewicz logic
section 42.6: Designating not just $\True$
chapter 43: mvl
section 43.1: Induction on~$\Nat$
chapter 44: mth
section 44.1: Inductive Definitions
section 44.2: Introduction
section 44.3: Relations and Functions
section 44.4: Strong Induction
section 44.5: Structural Induction
section 44.6: I Can't Do It!{}
section 44.7: An Example
section 44.8: Another Example
section 44.9: Inference Patterns
subsection 44.9.1: Using a Conjunction
subsection 44.9.2: Proving a Conjunction
subsection 44.9.3: Proving a Disjunction
subsection 44.9.4: Conditional Proof
subsection 44.9.5: Universal Claims
subsection 44.9.6: Proof by Cases
subsection 44.9.7: Proving an Existence Claim
subsection 44.9.8: Using Existence Claims
section 44.10: Introduction
section 44.11: Proof by Contradiction
chapter 45: mth
section 45.1: Reading Proofs
section 45.2: Other Resources
subsection 45.2.1: Motivational Videos
section 45.3: Starting a Proof
section 45.4: Using Definitions
chapter 46: mod
section 46.1: Dense Linear Orders
section 46.2: Isomorphic Structures
section 46.3: Non-standard Models of Arithmetic
section 46.4: Overspill
section 46.5: Partial Isomorphisms
section 46.6: Reducts and Expansions
section 46.7: Sub\printtoken{p}{structure}
section 46.8: The Theory of a \printtoken{S}{structure}
section 46.9: The Definability Theorem
section 46.10: Craig's Interpolation Theorem
chapter 47: mod
section 47.1: Introduction
section 47.2: Separation of \printtoken{P}{sentence}
section 47.3: Abstract Logics
section 47.4: Introduction
section 47.5: Lindstr\"om's Theorem
chapter 48: mod
section 48.1: Compactness and L\"owenheim--Skolem Properties
section 48.2: Computable Models of Arithmetic
section 48.3: Introduction
chapter 49: mod
section 49.1: Models of $\Th{PA}$
section 49.2: Models of $\Th{Q}$
section 49.3: Non-Standard Models
section 49.4: Standard Models of Arithmetic
chapter 50: nml
section 50.1: Consistency
section 50.2: Derived Rules
section 50.3: Dual \usetoken{P}{formula}
section 50.4: Introduction
section 50.5: \usetoken{P}{derivation} and Modal Systems
section 50.6: More Proofs in \Log{K}
section 50.7: Normal Modal Logics
section 50.8: Proofs in \Log{K}
section 50.9: Proofs in Modal Systems
section 50.10: \usetoken{S}{derivability} from a Set of \usetoken{P}{formula}
section 50.11: Properties of \usetoken{S}{derivability}
section 50.12: Soundness
section 50.13: Showing Systems are Distinct
section 50.14: Canonical Models
section 50.15: Complete $\Sigma$-Consistent Sets
section 50.16: Determination and Completeness for \Log{K}
chapter 51: nml
section 51.1: Frame Completeness
section 51.2: Introduction
section 51.3: Lindenbaum's Lemma
section 51.4: Modalities and Complete Consistent Sets
section 51.5: The Truth Lemma
section 51.6: \Log{S5} is Decidable
section 51.7: \Log{K} and \Log{S5} have the Finite Model Property
section 51.8: Filtrations of Euclidean Models
section 51.9: Examples of Filtrations
section 51.10: Filtrations
chapter 52: nml
section 52.1: Filtrations are Finite
section 52.2: Introduction
section 52.3: Filtrations and Properties of Accessibility
section 52.4: Preliminaries
section 52.5: Frame Definability
section 52.6: Equivalence Relations and \Log{S5}
section 52.7: First-order Definability
chapter 53: nml
section 53.1: Frames
section 53.2: Introduction
section 53.3: Properties of Accessibility Relations
section 53.4: Second-order Definability
section 53.5: Introduction
section 53.6: Rules for Other Accessibility Relations
section 53.7: Sequent \usetoken{P}{derivation} for \Log{K}
section 53.8: Rules for \Log{K}
chapter 54: nml
section 54.1: Entailment
section 54.2: Introduction
section 54.3: The Language of Basic Modal Logic
section 54.4: Validity
section 54.5: Normal Modal Logics
section 54.6: Relational Models
section 54.7: Schemas and Validity
section 54.8: Simultaneous Substitution
chapter 55: nml
section 55.1: Tautological Instances
section 55.2: Truth at a World
section 55.3: Truth in a Model
section 55.4: Completeness for \Log{K}
section 55.5: Countermodels from \usetoken{P}{tableau}
section 55.6: Introduction
section 55.7: Rules for Other Accessibility Relations
section 55.8: Soundness for Additional Rules
section 55.9: \usetoken{P}{tableau} for \Log{K}
section 55.10: Rules for \Ax{K}
section 55.11: Simple \usetoken{P}{tableau} for \Log{S5}
section 55.12: Soundness for \Log{K}
chapter 56: nml
chapter: About the Open Logic Project
section 56.1: Removing Largest Cuts
section 56.2: Removing Topmost Cuts
chapter 57: pt
section 57.1: Maehara's Lemma and Craig's Interpolation Theorem
section 57.2: Introduction
section 57.3: The Midsequent Theorem and Herbrand's Theorem
section 57.4: Grafting \usetoken{P}{proof}
section 57.5: Introduction
chapter 58: pt
section 58.1: Regular \usetoken{P}{proof} and Substitution
section 58.2: Rules and \usetoken{P}{proof}
section 58.3: Natural Deduction with Sequents: \Log{N2c} and~\Log{N2i}
section 58.4: Translating from \Log{G2i} to \Log{N2i}
section 58.5: Translating from \Log{N2} to \Log{G2}
section 58.6: Introduction
section 58.7: The Normalization Theorem
chapter 59: pt
section 59.1: Permutation Conversions
section 59.2: Reduction Conversions
section 59.3: Segments and Cuts
section 59.4: Translating Between Normal \Log{N2i}-\usetoken{P}{proof} and \Log{G2i}
section 59.5: Completeness
section 59.6: Introduction
chapter 60: pt
section 60.1: Search Algorithm for \Log{G3c}
section 60.2: Tableaux
section 60.3: Introduction
section 60.4: Normalization
section 60.5: Proof Terms
section 60.6: Converting \usetoken{P}{derivation} to Proof Terms
chapter 61: int
section 61.1: Reduction
section 61.2: Sequent Natural Deduction
section 61.3: Recovering \usetoken{P}{derivation} from Proof Terms
section 61.4: Type Preservation
section 61.5: Types
section 61.6: Admissible and Derivable Rules
section 61.7: Interpretation of Rules
section 61.8: Introduction
section 61.9: Invertibility of Rules
section 61.10: Examples of Proofs
section 61.11: Regular Proofs and Substitution
section 61.12: Rules and \usetoken{P}{proof}
chapter 62: pt
section 62.1: Translating between \Log{G1c} and \Log{G3c}
section 62.2: Completeness of Propositional Logic
section 62.3: Formation Sequences
section 62.4: Propositional \usetoken{P}{formula}
section 62.5: Introduction
section 62.6: Preliminaries
section 62.7: Semantic Notions
section 62.8: Soundness of Propositional Logic
chapter 63: pl
section 63.1: \usetoken{P}{valuation} and Satisfaction
chapter 64: ref
chapter 65: ref
section 65.1: Second-order Logic is not Compact
section 65.2: Introduction
section 65.3: The L\"owenheim--Skolem Theorem Fails for Second-order Logic
chapter 66: sol
section 66.1: Second-order Arithmetic
section 66.2: Second-order Logic is not Axiomatizable
section 66.3: Cardinalities of Sets
section 66.4: Comparing Sets
section 66.5: Introduction
section 66.6: The Power of the Continuum
chapter 67: sol
section 67.1: Expressive Power
section 67.2: Describing Infinite and \usetoken{S}{enumerable} \usetoken{P}{domain}
section 67.3: Introduction
section 67.4: The Language of Second-Order Logic
section 67.5: Satisfaction
section 67.6: Semantic Notions
chapter 68: sol
section 68.1: Terms and \printtoken{P}{formula}
chapter 69: sth
section 69.1: The Continuum Hypothesis
section 69.2: Some Simplification with Cardinal Exponentiation
section 69.3: $\aleph$-Fixed Points
section 69.4: Defining the Basic Operations
section 69.5: Simplifying Addition and Multiplication
chapter 70: sth
section 70.1: Cardinals as Ordinals
section 70.2: Finite, \usetoken{S}{enumerable}, \usetoken{S}{nonenumerable}
section 70.3: Cantor's Principle
section 70.4: Appendix: Hume's Principle
section 70.5: $\ZFC$: A Milestone
section 70.6: The Banach--Tarski Paradox
chapter 71: sth
section 71.1: Countable Choice
section 71.2: Comparability and Hartogs' Lemma
section 71.3: Introduction
section 71.4: Intrinsic Considerations about Choice
section 71.5: The Tarski--Scott Trick
section 71.6: Appendix: Vitali's Paradox
section 71.7: The Well-Ordering Problem
section 71.8: Ordinal Addition
section 71.9: Ordinal Exponentiation
section 71.10: Introduction
section 71.11: Ordinal Multiplication
chapter 72: sth
section 72.1: Using Ordinal Addition
section 72.2: Basic Properties of the Ordinals
section 72.3: The General Idea of an Ordinal
section 72.4: Introduction
section 72.5: Order-Isomorphisms
section 72.6: $\ZFminus$: a milestone
section 72.7: Successor and Limit Ordinals
chapter 73: sth
section 73.1: Ordinals as Order-Types
section 73.2: Replacement
section 73.3: Von Neumann's Construction of the Ordinals
section 73.4: Well-Orderings
section 73.5: Replacement and ``Absolute Infinity''
section 73.6: Extrinsic Considerations about Replacement
section 73.7: Appendix: Finite axiomatizability
section 73.8: Introduction
section 73.9: Limitation-of-size
section 73.10: Replacement and Reflection
section 73.11: Appendix: Results surrounding Replacement
chapter 74: sth
section 74.1: The Strength of Replacement
section 74.2: Foundation
section 74.3: Defining the Stages as the $V_\alpha$s
section 74.4: Rank
section 74.5: The Transfinite Recursion Theorem(s)
chapter 75: sth
section 75.1: Basic Properties of Stages
section 75.2: $\Z$ and $\ZF$: A Milestone
section 75.3: The Cumulative-Iterative Approach
section 75.4: Extensionality
section 75.5: Appendix: Frege's Basic Law V
section 75.6: Predicative and Impredicative
section 75.7: Russell's Paradox (again)
chapter 76: sth
section 76.1: Urelements or Not?
section 76.2: Appendix: Closure, Comprehension, and Intersection
section 76.3: Infinity
section 76.4: $\Z^-$: a Milestone
section 76.5: Selecting our Natural Numbers
section 76.6: Pairs
section 76.7: Powersets
section 76.8: Separation
section 76.9: The Story in More Detail
section 76.10: Union
chapter 77: sth
chapter 78: sfr
section 78.1: Appendix: the Reals as Cauchy Sequences
section 78.2: Ordered Rings and Fields
section 78.3: From $\Rat$ to $\Real$
section 78.4: From $\Nat$ to $\Int$
section 78.5: From $\Int$ to $\Rat$
section 78.6: The Real Line
section 78.7: Some Philosophical Reflections
section 78.8: Composition of Functions
section 78.9: Basics
section 78.10: Kinds of Functions
section 78.11: Functions as Relations
chapter 79: sfr
section 79.1: Inverses of Functions
section 79.2: Isomorphism
section 79.3: Partial Functions
section 79.4: Introduction
section 79.5: Appendix: Proving Schr\"oder-Bernstein
section 79.6: Dedekind Algebras
section 79.7: Dedekind Algebras and Arithmetical Induction
section 79.8: Dedekind's ``Proof'' of the Existence of an Infinite Set
section 79.9: Hilbert's Hotel
chapter 80: sfr
section 80.1: Equivalence Relations
section 80.2: Graphs
section 80.3: Operations on Relations
section 80.4: Orders
section 80.5: Philosophical Reflections
section 80.6: Relations as Sets
chapter 81: sfr
chapter 82: sfr
section 82.1: Special Properties of Relations
section 82.2: Trees
section 82.3: Extensionality
section 82.4: Some Important Sets
section 82.5: Pairs, Tuples, Cartesian Products
section 82.6: Proofs about Sets
section 82.7: Russell's Paradox
chapter 83: sfr
section 83.1: Subsets and Power Sets
section 83.2: Unions and Intersections
section 83.3: Sets of Different Sizes, and Cantor's Theorem
section 83.4: Enumerations and \usetoken{S}{enumerable} Sets
section 83.5: Enumerations and \usetoken{S}{enumerable} Sets
section 83.6: Equinumerosity
section 83.7: Introduction
section 83.8: \printtoken{S}{nonenumerable} Sets
section 83.9: \printtoken{S}{nonenumerable} Sets
section 83.10: An Alternative Pairing Function
section 83.11: Pairing Functions and Codes
section 83.12: Reduction
section 83.13: Reduction
section 83.14: The Notion of Size, and Schr\"oder-Bernstein
chapter 84: sfr
chapter 85: sfr
section 85.1: Cantor's Zig-Zag Method
section 85.2: The Church--Turing Thesis
section 85.3: Combining Turing Machines
section 85.4: Configurations and Computations
section 85.5: Disciplined Machines
section 85.6: Halting States
section 85.7: Introduction
chapter 86: tur
section 86.1: Representing Turing Machines
section 86.2: Turing Machines
section 86.3: Unary Representation of Numbers
section 86.4: Variants of Turing Machines
section 86.5: The Decision Problem
section 86.6: Enumerating Turing Machines
section 86.7: The Halting Problem
section 86.8: Introduction
section 86.9: Representing Turing Machines
section 86.10: Trakhtenbrot's Theorem
chapter 87: tur
section 87.1: Universal Turing Machines
section 87.2: The Decision Problem is Unsolvable
section 87.3: Verifying the Representation

Items in this resource

The mentions of the inventory that name this resource. Each name links to the card of its inventory row.

Item	Kind	Where	Source
10KEYYD2EP	proof	proof, section 59.5	open_logic
11CSGZMN38	statement	prop, section 80.4	open_logic
11GAAKS9M6	proof	proof, section 34.6	open_logic
Consistency	definition	defn, section 15.1	open_logic
12GAHE0V7Q	statement	cor, section 83.5	open_logic
134BDD3BRZ	example	ex, section 83.5	open_logic
Scheme of Separation	statement	axiom, section 76.8	open_logic
13ZC9X463D	statement	prop, section 22.8	open_logic
14GJ0DQZAR	proof	proof, section 70.1	open_logic
14NQ9Y10NV	statement	lem, section 36.3	open_logic
15MZCFRWFZ	definition	defn, section 28.7	open_logic
15SJWZ33HG	proof	proof, section 55.1	open_logic
16JPC35VE1	statement	prop, section 62.1	open_logic
16KM45FN2S	proof	proof, section 83.3	open_logic
16M4QE5ECY	statement	prop, section 85.5	open_logic
16Z3A1MDSR	statement	prop, section 55.8	open_logic
17T1ND15E6	definition	defn, section 1.2	open_logic
180ZXFEJW6	statement	lem, section 38.9	open_logic
18AZTQVX4V	statement	prop, section 49.1	open_logic
18FZEM9PMR	definition	defn, section 46.3	open_logic
1996D6MNJT	statement	thm, section 38.9	open_logic
19EP2K9GQV	statement	prop, section 62.1	open_logic
1AVVRMYBZP	statement	thm, section 69.5	open_logic
1AY71ZGACC	proof	proof, section 71.8	open_logic
1BQYQ0F5YQ	statement	prop, section 19.4	open_logic
1BS4KX47VJ	proof	proof, section 30.3	open_logic
1C1479BS5W	statement	thm, section 78.3	open_logic
1C5A55HB8H	definition	defn, section 79.1	open_logic
1CQBV4JENZ	proof	proof, section 62.3	open_logic
1D6JG314AN	exercise	prob, section 34.1	open_logic
1D7NHQBYF2	exercise	prob, section 78.2	open_logic
1DSZ0BYRX4	exercise	prob, section 38.9	open_logic
1EMERXQ70N	definition	defn, section 46.5	open_logic
1FEVZDKAT6	proof	proof, section 66.4	open_logic
1FJ5QWAGQ7	example	ex, section 8.11	open_logic
1GA6YBQAEQ	proof	proof, section 15.1	open_logic
Soundness	statement	thm, section 62.8	open_logic
Kleene's Normal Form Theorem	statement	thm, section 3.25	open_logic
1J39VJG4BS	exercise	prob, section 36.3	open_logic
Reflexivity	statement	prop, section 17.5	open_logic
1K324ZX9R7	proof	proof, section 71.2	open_logic
!!^{derivability}	definition	defn, section 15.1	open_logic
1KCGZWYV80	proof	proof, section 76.8	open_logic
1KFA1F3PR5	proof	proof, section 8.8	open_logic
1KZT384F7Z	definition	defn, section 38.13	open_logic
1M6TQ6NS51	exercise	prob, section 19.4	open_logic
1MDRK7AGDC	statement	thm, section 30.11	open_logic
Linear order	definition	defn, section 80.4	open_logic
1MZ67A7788	definition	defn, section 48.1	open_logic
1N4908S3T5	definition	defn, section 61.9	open_logic
1N8E1NA76D	statement	prop, section 50.6	open_logic
1NABB2AZKR	proof	proof, section 49.1	open_logic
1NW6ST8KT5	statement	thm, section 51.1	open_logic
1P4HFEJF1D	proof	proof, section 76.8	open_logic
1PEYTNZ7QF	statement	prop, section 76.8	open_logic
1PVJHHMC5C	proof	proof, section 3.5	open_logic
1PW6YVA41Q	proof	proof, section 44.9.5	open_logic
Cartesian product	definition	defn, section 82.5	open_logic
1QNJ8221ZM	example	ex, section 83.5	open_logic
1R3QN46G4P	exercise	prob, section 83.12	open_logic
1RCJ47JF0S	exercise	prob, section 6.2	open_logic
1RRFEHZS4S	exercise	prob, section 86.1	open_logic
1S20RTZ5P5	statement	prop, section 19.8	open_logic
1S81WGE6AN	proof	proof, section 19.8	open_logic
1SCJTEV49B	proof	proof, section 56.2	open_logic
1T2TNT9T69	example	ex, section 82.4	open_logic
1T4MVDGBFT	exercise	prob, section 62.6	open_logic
1TBYGJGFN2	example	ex, section 55.11	open_logic
1TH587AC3Z	proof	proof, section 22.7	open_logic
1TYC9ETC1R	definition	defn, section 2.3	open_logic
1V356F6QV3	exercise	prob, section 9.8	open_logic
1VD0HZST98	proof	proof, section 19.15	open_logic
1VE228KWJH	statement	cor, section 72.2	open_logic
1VJCX2FD34	example	ex, section 80.4	open_logic
1W0PR2HWA6	proof	proof, section 39.4	open_logic
1W5XNWHZZK	statement	prop, section 27.7	open_logic
1WV1N35WYS	proof	proof, section 72.5	open_logic
1XWJ1FZC6E	statement	cor, section 86.10	open_logic
1YSCCGSD3K	exercise	prob, section 72.1	open_logic
1YXGHN19EP	statement	lem, section 71.8	open_logic
1Z472BFGN8	statement	prop, section 32.5	open_logic
203EK7VX7R	exercise	prob, section 83.6	open_logic
209K7H7MGN	exercise	prob, section 2.6	open_logic
20XVAKH2A6	statement	prop, section 44.9.7	open_logic
Russell's Paradox	statement	thm, section 82.7	open_logic
22FGRJBT89	exercise	prob, section 38.10	open_logic
22M2ZYYMSE	definition	defn, section 55.2	open_logic
23A8M6C3N8	statement	thm, section 36.1	open_logic
23C5E1WAT7	proof	proof, section 51.4	open_logic
23MS6M4WEQ	proof	proof, section 3.20	open_logic
23SBZXG696	proof	proof, section 58.7	open_logic
23TASTFE8H	definition	defn, section 56.2	open_logic
23ZKWZG18X	example	ex, section 80.1	open_logic
26ZCE8F8JW	statement	prop, section 72.7	open_logic
27BC0MHQXA	proof	proof, section 78.1	open_logic
27H0J3Q9GH	statement	cor, section 8.14	open_logic
27QVFP2WYT	definition	defn, section 83.3	open_logic
27TRBJD38K	proof	proof, section 49.3	open_logic
28N6GKZPXZ	proof	proof, section 50.7	open_logic
Strong Generalization on Constants	statement	thm, section 8.10	open_logic
29GSBPKZQR	proof	proof, section 42.6	open_logic
2BFSTW9X8A	statement	prop, section 51.4	open_logic
Anti-symmetry	definition	defn, section 82.1	open_logic
2CDVA6FPTR	proof	proof, section 71.8	open_logic
2CHNT4SXK8	definition	defn, section 11.3	open_logic
2D4HD2QPA1	proof	proof, section 8.9	open_logic
2DVGHBG0HP	definition	defn, section 1.10	open_logic
2E9656XCQG	statement	cor, section 83.5	open_logic
2E9MT84A2N	example	ex, section 20.1	open_logic
2EDE5JGQXQ	proof	proof, section 8.7	open_logic
2EE7BF580M	exercise	prob, section 4.1	open_logic
2EFB9ESWZQ	statement	prop, section 29.3	open_logic
2EJJ049ANC	definition	defn, section 50.16	open_logic
2EJNBF6GMA	example	ex, section 83.1	open_logic
2EKQBCB096	proof	proof, section 27.7	open_logic
2EKSBX94J0	example	ex, section 83.10	open_logic
2F0J2Q5F7S	proof	proof, section 30.3	open_logic
2FDKMJ1SEE	statement	cor, section 41.7	open_logic
2FGSJKR4G5	exercise	prob, section 17.10	open_logic
2G93DR30HW	statement	thm, section 36.5	open_logic
2GP7837H14	proof	proof, section 3.11	open_logic
2HAJGBT65M	definition	defn, section 28.7	open_logic
2HEAYAFGEM	definition	defn, section 55.3	open_logic
2HEVYC1FMH	proof	proof, section 75.5	open_logic
2HRXX3PS6D	statement	prop, section 4.1	open_logic
2JFN8KKG0X	statement	thm, section 65.1	open_logic
2JHFBMAEYF	proof	proof, section 22.2	open_logic
2JJ7YHGE3V	proof	proof, section 86.6	open_logic
2K2FZE72A5	statement	lem, section 70.1	open_logic
2K40WDYW5R	exercise	prob, section 50.6	open_logic
2K54TD2AFD	definition	defn, section 1.8	open_logic
2KB91QZKKR	exercise	prob, section 86.9	open_logic
2M8NHSC1CP	statement	prop, section 3.20	open_logic
2MGM6PJMYV	statement	cor, section 72.2	open_logic
2NQ4SEDQE6	proof	proof, section 62.7	open_logic
2NVCX1WA5V	exercise	prob, section 8.7	open_logic
2P297HQPYR	proof	proof, section 74.2	open_logic
2PQB0WQ1F2	definition	defn, section 1.5	open_logic
2Q6K8QEKGF	exercise	prob, section 9.11	open_logic
2QJXDXTHTH	statement	prop, section 79.3	open_logic
2QPF2M3KDY	exercise	prob, section 19.5	open_logic
Reflexivity	definition	defn, section 82.1	open_logic
2V5ABWKF05	proof	proof, section 11.1	open_logic
Kleene's Normal Form Theorem	statement	thm, section 3.10	open_logic
2X30EVY0QP	definition	defn, section 79.4	open_logic
2XERJVJ7RE	statement	prop, section 27.1	open_logic
2YB4J5CSRR	example	ex, section 12.9	open_logic
2Z9JKWRFET	proof	proof, section 50.6	open_logic
$x$-Variant	definition	defn, section 19.14	open_logic
2ZQHJX2T3Q	proof	proof, section 72.2	open_logic
30NG7Q1ND9	statement	prop, section 17.7	open_logic
312G2PX709	proof	proof, section 59.4	open_logic
3203R7TAD4	definition	defn, section 53.1	open_logic
33HNJCT7VV	statement	prop, section 69.3	open_logic
33X2PS1QMJ	exercise	prob, section 17.11	open_logic
34GD9BY3SR	definition	defn, section 61.5	open_logic
34PJX1QTSZ	exercise	prob, section 33.3	open_logic
34R9ZSFPK9	statement	prop, section 4.1	open_logic
352A89ER3M	statement	prop, section 3.20	open_logic
359XS28AGP	definition	defn, section 59.3	open_logic
Compactness Theorem	statement	prop, section 62.2	open_logic
37A4DFBQXA	example	ex, section 9.9	open_logic
38VVARR69B	proof	proof, section 30.2	open_logic
394SNBPD8G	statement	lem, section 30.6	open_logic
396QGRRTG9	proof	proof, section 66.6	open_logic
3983SE3T6H	proof	proof, section 11.4	open_logic
3A2H72EHSB	proof	proof, section 55.12	open_logic
3A7Y3PTKD6	exercise	prob, section 19.9	open_logic
3AGWVDCSMN	statement	prop, section 40.2	open_logic
3B9WTWW8EK	exercise	prob, section 53.3	open_logic
3BARKY9ZEH	exercise	prob, section 40.2	open_logic
3BB727ZAMN	proof	proof, section 56.1	open_logic
3BSK3E7EPC	statement	cor, section 59.4	open_logic
3BTJ2MCR5P	statement	prop, section 29.3	open_logic
3CJYMYDATB	proof	proof, section 49.4	open_logic
3CS5NZ8K9Q	statement	lem, section 35.2	open_logic
3CT5K2QNXC	exercise	prob, section 38.6	open_logic
3E5EASDG1V	proof	proof, section 36.3	open_logic
3E9HX49YYX	exercise	prob, section 76.6	open_logic
3EPT6602GG	definition	defn, section 46.2	open_logic
3FBF4EPKRZ	exercise	prob, section 50.13	open_logic
3FE12B9H4M	proof	proof, section 58.1	open_logic
3FN3KKVCX5	proof	proof, section 36.2	open_logic
3FQ78KN9E2	statement	cor, section 75.1	open_logic
3FZ1MHQQQW	statement	prop, section 66.3	open_logic
3FZGRBTVBT	statement	thm, section 30.3	open_logic
$\beta\eta$-complete development	definition	defn, section 36.2	open_logic
3G9734M5KJ	statement	prop, section 73.4	open_logic
3GKT8C3DR9	proof	proof, section 74.4	open_logic
3GSEN0F5QC	exercise	prob, section 22.10	open_logic
3H19SY28D7	exercise	prob, section 38.2	open_logic
3H6EXX8MCV	proof	proof, section 15.4	open_logic
3JHDB8D6V3	example	ex, section 60.6	open_logic
3K85JKQAD7	statement	prop, section 53.4	open_logic
3KDQF6BKXE	definition	defn, section 9.9	open_logic
3KVW8GDSC9	exercise	prob, section 8.3	open_logic
3M4BWP9917	exercise	prob, section 78.5	open_logic
Simple Transfinite Induction	statement	thm, section 72.7	open_logic
3MTD63SW5W	definition	defn, section 28.7	open_logic
3NA829X2QG	statement	thm, section 46.5	open_logic
3NARDM6FRZ	statement	cor, section 36.5	open_logic
3NE03NH7SH	definition	defn, section 62.4	open_logic
3NEQQVNBP5	statement	prop, section 66.4	open_logic
3NVXRZ62EQ	proof	proof, section 17.9	open_logic
3PJBHFHY3V	statement	thm, section 28.2	open_logic
3PXB8JC1H0	exercise	prob, section 86.10	open_logic
3Q4DA10R9F	proof	proof, section 11.6	open_logic
3QNS23M2EH	exercise	prob, section 79.1	open_logic
Extensionality	definition	defn, section 82.3	open_logic
3R9C25SNWT	statement	lem, section 72.1	open_logic
3RGFA836K3	proof	proof, section 11.7	open_logic
Composition	definition	defn, section 78.8	open_logic
3S9T29ET66	statement	cor, section 50.16	open_logic
3SF1TQ0ZT2	exercise	prob, section 19.2	open_logic
3SGR4M1H4H	definition	defn, section 27.2	open_logic
3SJTY2A29V	proof	proof, section 83.5	open_logic
3TGFW4H4DJ	definition	defn, section 61.10	open_logic
3TXZQHB4K5	definition	defn, section 71.5	open_logic
3TZMM3406D	example	ex, section 86.1	open_logic
3VER5PJP56	proof	proof, section 72.2	open_logic
3WEZVZVYHN	example	ex, section 17.10	open_logic
3WPCPTZA1K	proof	proof, section 38.6	open_logic
3X99ZYZZQR	proof	proof, section 17.7	open_logic
3XMCCM6VS2	statement	prop, section 44.11	open_logic
3XNJPVP027	proof	proof, section 74.4	open_logic
3YAACNE572	example	ex, section 31.2	open_logic
3YDAXXHP6V	statement	prop, section 8.5	open_logic
3ZKY8EJPRC	exercise	prob, section 62.7	open_logic
406TYVX5YX	statement	prop, section 54.7	open_logic
4074EV81C6	example	ex, section 78.9	open_logic
Enumeration, informally	definition	defn, section 83.5	open_logic
40ZGVQE4FX	proof	proof, section 11.2	open_logic
42D4C9GCYD	statement	thm, section 50.13	open_logic
42E4F6WZW1	proof	proof, section 27.1	open_logic
Free and bound occurrence	definition	defn, section 38.14	open_logic
43JY09RF8S	example	ex, section 78.9	open_logic
44EYZXT7NQ	proof	proof, section 29.5	open_logic
4595CBFHK3	statement	prop, section 76.8	open_logic
$\beta$-reduction, $\bred$	definition	defn, section 38.10	open_logic
45WJRQ4F7V	exercise	prob, section 27.1	open_logic
45ZW21B3YX	proof	proof, section 51.9	open_logic
$\beta$-normal	definition	defn, section 38.10	open_logic
46DJEH25AW	definition	defn, section 59.3	open_logic
46G2EXMA4V	exercise	prob, section 33.3	open_logic
46QZWJ65YB	statement	cor, section 22.15	open_logic
Re-proof of Schr\"oder-Bernstein	proof	proof, section 70.1	open_logic
47HBN3K2FE	statement	prop, section 3.7	open_logic
4945NDTZKF	statement	prop, section 22.7	open_logic
497V6ZTVEF	exercise	prob, section 22.4	open_logic
Theorems	definition	defn, section 8.6	open_logic
49RQZFRNZM	exercise	prob, section 20.2	open_logic
4AEQ4ZKP1N	example	ex, section 37.8	open_logic
4B2RGHKVJR	proof	proof, section 78.3	open_logic
4BHQ5Y5DBY	definition	defn, section 27.2	open_logic
Truth Lemma	statement	prop, section 51.5	open_logic
4BNK5HFB19	definition	defn, section 3.28	open_logic
4BR1DN4JHF	statement	prop, section 50.15	open_logic
4C7103SCHR	statement	cor, section 46.5	open_logic
4CGZKSV0ZP	statement	prop, section 83.5	open_logic
4CQVG303A7	proof	proof, section 71.6	open_logic
4CZAAGB4Y8	exercise	prob, section 38.9	open_logic
4D27DEAP62	statement	prop, section 29.3	open_logic
$\eta$-contraction, $\eredone$	definition	defn, section 38.13	open_logic
4DA7RYTKV2	proof	proof, section 31.1	open_logic
4DAAX8VNT9	statement	prop, section 80.4	open_logic
4DDF7BZ8D8	statement	prop, section 11.4	open_logic
4DJZSW5TP7	proof	proof, section 71.6	open_logic
4DPMM08YMA	statement	prop, section 8.12	open_logic
4DRBM1BXKB	exercise	prob, section 38.15	open_logic
4DSWV80BEP	definition	defn, section 1.6	open_logic
4DYB36ZVQE	exercise	prob, section 22.11	open_logic
4DZ3EKV0SG	statement	lem, section 39.3	open_logic
4DZQVE0YXQ	statement	thm, section 28.5	open_logic
Reflexivity	statement	prop, section 15.1	open_logic
4FBNBKW0B6	statement	cor, section 22.15	open_logic
4FGSH5MVPP	exercise	prob, section 54.7	open_logic
4FPEZHW79C	statement	prop, section 45.4	open_logic
4GHAXXPAGB	statement	lem, section 51.4	open_logic
Satisfaction	definition	defn, section 19.14	open_logic
4GY6076NV6	statement	cor, section 53.4	open_logic
4GYFZ8PCYZ	proof	proof, section 82.7	open_logic
4HE4ZR45WA	exercise	prob, section 11.4	open_logic
Theorems	definition	defn, section 40.4	open_logic
4HQZSF9MM8	statement	lem, section 29.10	open_logic
4HZQHBD5MV	exercise	prob, section 8.6	open_logic
4J0HJ8AQ8D	exercise	prob, section 55.8	open_logic
4JFW4925JD	exercise	prob, section 55.2	open_logic
Induction on !!{formula}s	definition	defn, section 79.4	open_logic
4JVNM6FJGT	proof	proof, section 55.8	open_logic
4KR8RRE6JW	definition	defn, section 59.3	open_logic
4KXND2QKS4	proof	proof, section 44.5	open_logic
4M7WM65VXB	proof	proof, section 75.1	open_logic
4MQFAB5S20	exercise	prob, section 17.10	open_logic
!!^{derivability}	definition	defn, section 40.6	open_logic
4N9P8FAR72	statement	prop, section 13.2	open_logic
4NYGKJ648X	proof	proof, section 50.12	open_logic
4P4T7QH955	proof	proof, section 44.3	open_logic
Maehara's Lemma	statement	lem, section 57.1	open_logic
4QDR1PMYAW	statement	lem, section 38.9	open_logic
4QHY91VXZT	statement	prop, section 46.8	open_logic
4QK7236GCR	definition	defn, section 83.5	open_logic
4R9NK3SBN6	example	ex, section 82.2	open_logic
in $\Zminus + \text{Countable Choice}$	statement	thm, section 71.1	open_logic
4S2WHJYX0G	exercise	prob, section 8.4	open_logic
4TJVQEKGBM	proof	proof, section 32.1.6	open_logic
4TXQB4K340	definition	defn, section 69.1	open_logic
4VJDZFK7ZG	proof	proof, section 35.1	open_logic
4W3XYPFMBY	statement	prop, section 52.6	open_logic
4WKJVK60TR	proof	proof, section 47.2	open_logic
4WPSW07MFX	exercise	prob, section 42.5	open_logic
4WPWX1V9EV	proof	proof, section 29.10	open_logic
4X006N7NJJ	statement	prop, section 83.6	open_logic
4Y0K5NHVVK	statement	prop, section 55.4	open_logic
4YKE73KD1Y	exercise	prob, section 38.14	open_logic
Beth Definability Theorem	statement	thm, section 46.9	open_logic
4ZCMP5W51V	proof	proof, section 41.7	open_logic
4ZHZX5KJB8	proof	proof, section 87.2	open_logic
50WQXNY881	statement	prop, section 32.6	open_logic
50YRA720PN	proof	proof, section 71.1	open_logic
50ZM69G9X9	statement	prop, section 19.8	open_logic
512XDAYFNS	exercise	prob, section 51.7	open_logic
Vitali	statement	cor, section 71.6	open_logic
51FA7EDM11	proof	proof, section 3.31	open_logic
51PQ3S1BKY	statement	prop, section 83.1	open_logic
52J3DYM1PX	proof	proof, section 70.2	open_logic
52MFH2YC9W	exercise	prob, section 38.2	open_logic
53F4EZV01X	proof	proof, section 36.6	open_logic
53NFXJ595F	exercise	prob, section 42.6	open_logic
54GJKFJYVF	exercise	prob, section 22.2	open_logic
54TF1YJ7NQ	statement	prop, section 43.1	open_logic
Partial order	definition	defn, section 80.4	open_logic
555TDV7ZEF	proof	proof, section 29.3	open_logic
56B0EZQ8RQ	exercise	prob, section 30.3	open_logic
\emph{Principle of induction on !!{formula}s}	statement	thm, section 62.6	open_logic
56FNSE4YB0	statement	lem, section 30.3	open_logic
56RARC9WK3	statement	lem, section 38.14	open_logic
56YM3XPRDX	definition	defn, section 27.7	open_logic
574WPVXY9R	definition	defn, section 62.7	open_logic
57TX651VXM	definition	defn, section 72.5	open_logic
585PGR4Y63	exercise	prob, section 27.7	open_logic
586WNZHZ5G	statement	prop, section 46.6	open_logic
Axioms	definition	defn, section 8.1	open_logic
5940RNBHR7	statement	prop, section 19.14	open_logic
595Q9NFHZQ	proof	proof, section 19.8	open_logic
5AAX336WAP	proof	proof, section 19.4	open_logic
5B84X5M4K3	proof	proof, section 49.1	open_logic
5B88ZW0T9C	statement	prop, section 82.5	open_logic
5BJA9NPFA5	definition	defn, section 74.4	open_logic
5C8A7ZWPCW	exercise	prob, section 38.15	open_logic
Cut	definition	defn, section 78.3	open_logic
5CF8WRANG9	exercise	prob, section 17.11	open_logic
5CW8FA9D8J	example	ex, section 17.4	open_logic
5D1WEG56M6	example	ex, section 22.4	open_logic
5D2351YKDD	definition	defn, section 85.4	open_logic
Proper !!^{subformula}	definition	defn, section 20.2	open_logic
5DYVJ90AXY	proof	proof, section 52.5	open_logic
5E3WS3Z544	statement	lem, section 86.7	open_logic
Transitive closure	definition	defn, section 80.3	open_logic
Theorems	definition	defn, section 8.13	open_logic
Syntactic identity	definition	defn, section 22.1	open_logic
5FQBJXGWP1	statement	prop, section 9.10	open_logic
Consistency	definition	defn, section 40.4	open_logic
5H6Y065RQ4	statement	lem, section 35.1	open_logic
5HP0Y011MF	statement	prop, section 29.8	open_logic
5K07CY9QSA	exercise	prob, section 9.9	open_logic
5KD6WM8MVV	example	ex, section 15.6	open_logic
5M36DMFS65	proof	proof, section 44.9.8	open_logic
5NBJBGATDB	statement	prop, section 70.2	open_logic
5NGA8SCNJV	definition	defn, section 50.15	open_logic
5NMJCJ65TP	proof	proof, section 38.3	open_logic
5P6QP6A0R5	definition	defn, section 28.7	open_logic
5PBY7FSCQ1	exercise	prob, section 72.5	open_logic
5PK147R14F	proof	proof, section 39.3	open_logic
5PVPH576PA	proof	proof, section 19.4	open_logic
5QWT3GD53H	exercise	prob, section 54.1	open_logic
5R5B0SRWBD	proof	proof, section 72.2	open_logic
5RC01GC3DZ	statement	prop, section 50.2	open_logic
5RGFZZVPSG	exercise	prob, section 28.6	open_logic
5RGWV5FG6B	exercise	prob, section 44.1	open_logic
5SENAAPZ2Y	statement	thm, section 38.9	open_logic
5SGXX5DFA2	statement	lem, section 30.1	open_logic
5TA27Z6128	exercise	prob, section 19.8	open_logic
Binary relation	definition	defn, section 80.6	open_logic
5TJZCHQDVW	exercise	prob, section 86.10	open_logic
5V0R4NJ798	exercise	prob, section 49.2	open_logic
Graph of a partial function	definition	defn, section 79.3	open_logic
5V8D41QT9T	exercise	prob, section 83.3	open_logic
5VG381AY0M	proof	proof, section 62.1	open_logic
5VJAAMXRHE	statement	prop, section 19.4	open_logic
5WDHAR5DQX	statement	prop, section 78.4	open_logic
5WMTPRDD7X	example	ex, section 15.6	open_logic
5XG7Y4E0ZN	exercise	prob, section 79.1	open_logic
5XP1E5KXSK	statement	thm, section 33.4	open_logic
5XS2QWMYCT	statement	prop, section 3.30	open_logic
5XZ43Y4KPA	exercise	prob, section 67.2	open_logic
5Y5DJSYPJB	statement	lem, section 87.3	open_logic
5YKGJPQWGT	exercise	prob, section 80.2	open_logic
5Z6RJ060Z3	exercise	prob, section 46.1	open_logic
5ZVK7MSAWN	example	ex, section 67.5	open_logic
60F8H2SN01	example	ex, section 48.2	open_logic
615X69MN0S	statement	prop, section 20.2	open_logic
61YRPD0W9P	example	ex, section 53.6	open_logic
61ZAX2BWB5	definition	defn, section 19.2	open_logic
62DC2YMB78	definition	defn, section 72.7	open_logic
62DXFD36Z5	statement	prop, section 49.1	open_logic
Substitution in a term	definition	defn, section 20.3	open_logic
63QXNWSCV8	proof	proof, section 38.15	open_logic
Compactness	statement	prop, section 15.1	open_logic
Proof of \olref{thm:interpolation}	proof	proof, section 57.1	open_logic
650DN7G9Z7	definition	defn, section 52.5	open_logic
656CFQSN0T	example	ex, section 53.6	open_logic
658VJJF6YC	proof	proof, section 52.6	open_logic
65YK1HPR5X	proof	proof, section 17.8	open_logic
662WENYB3F	exercise	prob, section 36.2	open_logic
Soundness	statement	thm, section 33.6	open_logic
675EQZFNP7	exercise	prob, section 8.7	open_logic
Trakhtenbrot's Theorem	statement	thm, section 86.10	open_logic
68W7AKXBMP	exercise	prob, section 83.9	open_logic
Completeness Theorem	statement	thm, section 9.11	open_logic
Reflexivity	statement	prop, section 22.5	open_logic
6ARTQM73SR	exercise	prob, section 22.7	open_logic
6AW254NN4S	definition	defn, section 61.12	open_logic
6B4TC0AASY	proof	proof, section 74.2	open_logic
6BAM655C0T	statement	lem, section 69.5	open_logic
6BMFDQQ8SP	exercise	prob, section 32.6	open_logic
\emph{Principle of induction on !!{formula}s}	statement	lem, section 22.1	open_logic
6DCD80H3GB	proof	proof, section 58.3	open_logic
6EFTQPXSKE	definition	defn, section 85.4	open_logic
6FC4DMG14H	proof	proof, section 59.4	open_logic
6FWA43VP26	example	ex, section 54.5	open_logic
6FZ1WMWCP6	statement	prop, section 50.11	open_logic
6G2DDJ3F0J	exercise	prob, section 86.3	open_logic
6G38B2GYC7	statement	thm, section 48.1	open_logic
6GEQJT566P	statement	thm, section 83.8	open_logic
Lindstr\"om's Theorem	statement	thm, section 47.5	open_logic
6GZG9AD3MK	statement	lem, section 86.10	open_logic
6HDQB5Z088	proof	proof, section 37.1	open_logic
6J9K6E2PFB	statement	prop, section 44.5	open_logic
6JE3KEX4RY	statement	thm, section 46.3	open_logic
6JJ90BSSMM	example	ex, section 41.2	open_logic
6JRK2T9AG3	definition	defn, section 44.3	open_logic
6K5MDYKG0M	exercise	prob, section 54.4	open_logic
6KBW08YMZQ	exercise	prob, section 65.1	open_logic
6MA50AT55S	statement	lem, section 69.4	open_logic
6MTB6WNQ3G	exercise	prob, section 49.1	open_logic
Formula	definition	defn, section 62.4	open_logic
6N4WDPNSZ8	exercise	probtag, section 55.2	open_logic
6N7YVY9TFM	proof	proof, section 62.7	open_logic
6P97Y99AAF	proof	proof, section 19.14	open_logic
Weak Church-Rosser Property	statement	prop, section 60.4	open_logic
6QH9PRBX89	statement	prop, section 49.3	open_logic
6R1M3HSMWF	definition	defn, section 54.6	open_logic
6RDXJ5KE30	statement	cor, section 51.10	open_logic
6RKAP4HZ88	statement	prop, section 29.10	open_logic
6RRGRJ8QR0	proof	proof, section 44.11	open_logic
6SV296JAD1	exercise	prob, section 36.3	open_logic
Initial Sequent	definition	defn, section 17.13	open_logic
6SYQ1W06WA	proof	proof, section 51.4	open_logic
6T3NCNK2ED	statement	prop, section 27.7	open_logic
6TG8E5N14W	exercise	prob, section 86.7	open_logic
6TYRFESHR4	statement	lem, section 71.6	open_logic
6VRDTV94ES	proof	proof, section 47.5	open_logic
Equivalence relation	definition	defn, section 80.1	open_logic
6VXQF4PKBF	proof	proof, section 15.1	open_logic
6WBH9CRGBW	proof	proof, section 83.5	open_logic
6WMMCA1PAD	proof	proof, section 47.5	open_logic
6WT9FPAR4J	statement	prop, section 58.5	open_logic
6X9B2ZBRK2	definition	defn, section 1.7	open_logic
6XAPETEMBH	proof	proof, section 83.8	open_logic
6Y4GKQX60Z	example	ex, section 20.3	open_logic
6YKA2B4913	proof	proof, section 78.2	open_logic
6YYDWG2VMV	example	ex, section 55.5	open_logic
6Z427TA77T	statement	lem, section 35.1	open_logic
6ZXHGZY911	statement	thm, section 17.9	open_logic
Difference	definition	defn, section 83.2	open_logic
70W8PZHFWT	exercise	prob, section 57.1	open_logic
711TF5FN6K	exercise	prob, section 73.5	open_logic
71P0Q43RCV	example	ex, section 17.11	open_logic
71QAH94GWV	definition	defn, section 83.2	open_logic
72KADK269P	definition	defn, section 50.7	open_logic
72P4MT7CTD	statement	thm, section 37.2	open_logic
73DT1R5PC9	exercise	prob, section 50.9	open_logic
73GY4XSG7T	proof	proof, section 19.4	open_logic
73M5RYT8R4	definition	defn, section 48.2	open_logic
73MV4DDBQ2	exercise	prob, section 42.6	open_logic
73WMXRKF89	definition	defn, section 46.2	open_logic
746RP5QCSA	exercise	prob, section 9.8	open_logic
74ABEEHKVR	definition	defn, section 54.5	open_logic
74PWP5C0W2	proof	proof, section 35.2	open_logic
74TFT3AQ4Z	exercise	prob, section 83.6	open_logic
74WH5J0KA1	proof	proof, section 28.6	open_logic
75E6AW9Q58	exercise	prob, section 46.3	open_logic
75EA2T24G0	exercise	prob, section 39.4	open_logic
75QDGX0MW6	proof	proof, section 55.12	open_logic
769K64F44D	statement	prop, section 19.6	open_logic
76GC5AMFBX	statement	prop, section 3.20	open_logic
76YC18BNSV	statement	prop, section 19.8	open_logic
77353JJEMC	proof	proof, section 76.3	open_logic
Determination	statement	thm, section 50.16	open_logic
77BP1ABQWD	proof	proof, section 62.6	open_logic
77NFEC7SSF	statement	prop, section 27.6	open_logic
77TM75NRYF	statement	prop, section 27.5	open_logic
78QR8J5WZW	statement	prop, section 52.6	open_logic
79APC5Y78E	definition	defn, section 38.7	open_logic
79MM9F2KMB	statement	prop, section 61.6	open_logic
79Q9GMDVCF	statement	thm, section 66.2	open_logic
7A5F75TX50	statement	cor, section 62.8	open_logic
7AG9SMH1EQ	definition	defn, section 55.4	open_logic
7AWFH2ACHR	example	ex, section 79.3	open_logic
7BJ09QCD4C	definition	defn, section 60.5	open_logic
7CD6KBCEN3	exercise	prob, section 3.32	open_logic
7CG5Z2QSFS	proof	proof, section 29.10	open_logic
7DEHJ1T596	proof	proof, section 69.1	open_logic
Transitivity	statement	prop, section 17.5	open_logic
7E9A1ZJBNC	exercise	probtag, section 51.9	open_logic
7ENZDS96WP	definition	defn, section 42.2	open_logic
7FE229HZWX	proof	proof, section 87.3	open_logic
$\beta$-complete development	definition	defn, section 36.3	open_logic
7GCRQ91F41	statement	thm, section 66.2	open_logic
7GD4RA93DT	statement	lem, section 61.11	open_logic
7GSTKN01R7	statement	cor, section 22.15	open_logic
7HK9MVM6E2	statement	thm, section 38.1	open_logic
7HKMCBPAN1	definition	defn, section 38.12	open_logic
7HPYFRNWPC	exercise	prob, section 38.14	open_logic
Compactness	statement	prop, section 8.6	open_logic
7JEKG6962E	proof	proof, section 69.1	open_logic
7JSS2972CZ	example	ex, section 53.6	open_logic
7JZHAVZFZM	definition	defn, section 28.7	open_logic
7KJRS9EC3R	definition	defn, section 53.4	open_logic
7M3BXSWKVP	example	ex, section 85.5	open_logic
Soundness Theorem	statement	thm, section 50.12	open_logic
7MJ1ANN8GV	proof	proof, section 38.6	open_logic
7N2C62WTJ7	proof	proof, section 32.6	open_logic
Strings	example	ex, section 82.4	open_logic
7NNNAWZ0QZ	proof	proof, section 58.4	open_logic
7P98MQMZHQ	statement	prop, section 8.4	open_logic
7PWGV60YA4	exercise	prob, section 22.5	open_logic
!!^{surjective} function	definition	defn, section 78.10	open_logic
7Q7655B61T	proof	proof, section 40.4	open_logic
7Q8QDHZGQB	proof	proof, section 53.4	open_logic
7RMN4Q2VKQ	proof	proof, section 31.3	open_logic
7RP3C8FS2F	proof	proof, section 56.2	open_logic
Change of bound variable, $\aconvone$	definition	defn, section 38.9	open_logic
7SBD2293A7	example	ex, section 13.3	open_logic
7SPARRRFC1	example	ex, section 17.11	open_logic
$\alpha$-conversion, $\aconv$	definition	defn, section 38.9	open_logic
7T13TJ3S9V	exercise	prob, section 27.3	open_logic
7T8A8Y4W0C	exercise	probtag, section 19.4	open_logic
7TC17EP3WT	proof	proof, section 15.3	open_logic
7TGP2Z6YVX	example	ex, section 53.6	open_logic
7TK3AWCW42	statement	thm, section 36.2	open_logic
7TXQE75BK7	statement	prop, section 85.1	open_logic
7VAYC6XDW6	exercise	prob, section 86.7	open_logic
7VDGS2GDG9	proof	proof, section 57.1	open_logic
7VMZ5ECMEF	proof	proof, section 69.4	open_logic
7VR387ZCX6	exercise	prob, section 11.4	open_logic
7VSH10CDCM	exercise	prob, section 78.2	open_logic
7VX45JPPXY	exercise	prob, section 22.11	open_logic
7VXJNA5TCS	proof	proof, section 67.2	open_logic
7W5583S1RF	definition	defn, section 1.2	open_logic
7W5Q20NBJP	proof	proof, section 49.3	open_logic
Unique Readability	statement	prop, section 62.6	open_logic
7X7B5C8177	exercise	prob, section 78.1	open_logic
7X9ZZXZBB8	statement	prop, section 61.10	open_logic
7XJZG5XEX7	statement	prop, section 29.3	open_logic
7XKE964N35	proof	proof, section 8.7	open_logic
7XP5EZNXNN	proof	proof, section 46.9	open_logic
7XPTRN1204	proof	proof, section 69.2	open_logic
7YHBZ1T00H	example	ex, section 83.1	open_logic
7Z17C01NA7	proof	proof, section 9.8	open_logic
7Z2WHN21B0	statement	prop, section 50.8	open_logic
801MKCEYAS	proof	proof, section 29.2	open_logic
$\in$-Induction Scheme	statement	thm, section 74.4	open_logic
82233NB7SW	proof	proof, section 27.9	open_logic
8239M2KX1E	definition	defn, section 63.1	open_logic
82EJD7RSR4	statement	prop, section 83.5	open_logic
82HXJBRAZ4	proof	proof, section 76.7	open_logic
82Y0CGX0RX	statement	lem, section 71.11	open_logic
82YGXRTZPD	statement	prop, section 17.5	open_logic
83474VRC4P	example	ex, section 13.5	open_logic
83BS3YTVK3	statement	thm, section 87.2	open_logic
83K0HTPYC6	statement	lem, section 47.2	open_logic
83WBSC07CB	statement	lem, section 37.5	open_logic
8410AXF31P	proof	proof, section 30.9	open_logic
841EAH0E6X	exercise	prob, section 9.8	open_logic
84N8C43Q7J	statement	thm, section 38.9	open_logic
84TGA7W2VT	statement	prop, section 70.2	open_logic
84XYH221SP	statement	prop, section 70.2	open_logic
851BGYCDA6	proof	proof, section 71.11	open_logic
854A0T4MJY	statement	lem, section 61.9	open_logic
Satisfaction	definition	defn, section 63.1	open_logic
85PD40J0CC	proof	proof, section 3.4	open_logic
8621N0WXVD	statement	prop, section 72.5	open_logic
869MT8KP26	example	ex, section 13.4	open_logic
869P34HYCZ	proof	proof, section 65.3	open_logic
Satisfaction	definition	defn, section 42.1	open_logic
86M0W2R861	proof	proof, section 52.6	open_logic
86MFPV0ZYE	exercise	prob, section 76.7	open_logic
$\alpha$-conversion, $\aconv$	definition	defn, section 38.9	open_logic
8792CMWETD	definition	defn, section 42.6	open_logic
87VAFERG3N	proof	proof, section 3.22	open_logic
880JTJFHPK	proof	proof, section 43.1	open_logic
88HZ8AQ5ZS	statement	thm, section 30.13	open_logic
88QXKEDQFR	definition	defn, section 27.5	open_logic
Power Set	definition	defn, section 83.1	open_logic
89PGS7AS8K	proof	proof, section 15.4	open_logic
Assumption	definition	defn, section 15.9	open_logic
8A2NN21MSQ	proof	proof, section 19.6	open_logic
8ADJ0X9GD1	exercise	prob, section 73.7	open_logic
8B4AQS7TRJ	exercise	prob, section 71.11	open_logic
8B4EV1DQEA	example	ex, section 3.30	open_logic
8B58NFAE79	example	ex, section 13.3	open_logic
8BC9N4P3Z6	proof	proof, section 51.1	open_logic
8BT7JBWNK4	proof	proof, section 40.2	open_logic
8BXT2T011F	proof	proof, section 19.8	open_logic
8CBBH1QMHS	statement	cor, section 70.2	open_logic
8CYGG09BGR	proof	proof, section 15.3	open_logic
8D4NKJM0E8	statement	prop, section 49.1	open_logic
8DAMYNW1Q0	definition	defn, section 74.3	open_logic
8E7948FXX5	statement	thm, section 53.3	open_logic
8EHMXX6R0F	statement	lem, section 59.5	open_logic
8EM9YJD8GY	statement	lem, section 71.6	open_logic
8EVW9236DN	definition	defn, section 79.9	open_logic
8FVM3DWPWV	statement	lem, section 29.10	open_logic
8G2WXDM229	exercise	prob, section 83.13	open_logic
8GBYQBADQ2	proof	proof, section 44.7	open_logic
8GG8FRYTJ5	proof	proof, section 30.3	open_logic
8GPQAPHNHQ	proof	proof, section 57.3	open_logic
Bounded Recursion	statement	lem, section 74.5	open_logic
8HHVYERQ62	exercise	prob, section 78.5	open_logic
Theorems	definition	defn, section 31.1	open_logic
8JQD4J298B	proof	proof, section 22.5	open_logic
8K08EKK9XV	proof	proof, section 54.4	open_logic
8KGHZ96EJ4	proof	proof, section 61.11	open_logic
8M6AEZRQZ4	definition	defn, section 61.5	open_logic
8MJNRAY44Y	definition	defn, section 46.6	open_logic
Infinity	statement	axiom, section 76.3	open_logic
8N38ZSX3JJ	exercise	prob, section 83.13	open_logic
8N4K221848	proof	proof, section 46.5	open_logic
8PVX6RQBXD	example	ex, section 51.9	open_logic
8QFQD2DEBA	exercise	prob, section 79.1	open_logic
8QRM5ZR7WT	proof	proof, section 76.8	open_logic
8QV7KBGJVZ	example	ex, section 55.9	open_logic
8RD4R4RMHX	statement	cor, section 29.2	open_logic
8RK33N0QC4	statement	thm, section 29.9	open_logic
8RQ6638J2E	statement	cor, section 59.5	open_logic
8RSE93QCG6	statement	thm, section 35.1	open_logic
8S0YRSRQAK	definition	defn, section 51.9	open_logic
Proof of {\olref[nen-alt]{thm:nonenum-pownat}} by reduction	proof	proof, section 83.12	open_logic
8THHMTAXRX	exercise	prob, section 82.5	open_logic
8TX66E0B72	definition	defn, section 19.4	open_logic
in $\ZF$	statement	thm, section 71.7	open_logic
8V5CV4XDNH	proof	proof, section 60.4	open_logic
8VT9MTEZ0S	exercise	prob, section 55.8	open_logic
8W80RZ9TYB	proof	proof, section 51.1	open_logic
8WM0ZXRZB9	exercise	prob, section 69.4	open_logic
8WW3JF7TX1	statement	thm, section 2.5	open_logic
8WZN3PN2WY	definition	defn, section 46.1	open_logic
8X21TM24MM	proof	proof, section 46.4	open_logic
8X675NG6XZ	proof	proof, section 17.5	open_logic
8XH7KNE370	exercise	prob, section 19.15	open_logic
8XQZ0JPNN6	proof	proof, section 3.11	open_logic
8YD5XPJ01V	statement	thm, section 30.4	open_logic
8YVYEA5037	proof	proof, section 11.1	open_logic
8Z440DYMWE	statement	prop, section 27.6	open_logic
Extensionality for !!^{sentence}s	statement	cor, section 19.6	open_logic
91QNX2JFMF	definition	defn, section 30.13	open_logic
92E1F2HYQZ	exercise	prob, section 34.6	open_logic
Uniform Substitution	definition	defn, section 62.6	open_logic
92MMMX79JD	exercise	prob, section 3.20	open_logic
92YT3DV8KW	statement	prop, section 62.6	open_logic
931PCSVCSC	statement	cor, section 62.2	open_logic
9487VB6XK1	exercise	prob, section 78.8	open_logic
94NT30TKJJ	statement	prop, section 27.7	open_logic
955DPPDD8R	definition	defn, section 42.4	open_logic
95WJ31Y4B0	definition	defn, section 37.2	open_logic
966QE4TDQM	exercise	prob, section 73.7	open_logic
983Q0G0N8M	proof	proof, section 63.1	open_logic
983SQBFA4X	statement	thm, section 46.4	open_logic
98RF28Q803	definition	defn, section 83.3	open_logic
992KYS3909	proof	proof, section 87.1	open_logic
Monotonicity	statement	prop, section 8.10	open_logic
99Q7YJR56Y	exercise	prob, section 32.5	open_logic
9A5T78SJ13	proof	proof, section 15.1	open_logic
9AEP6R09TG	proof	proof, section 34.6	open_logic
9B979N2P9Q	exercise	prob, section 22.2	open_logic
Sequent	definition	defn, section 61.8	open_logic
9CP37P4FHM	proof	proof, section 22.7	open_logic
9CWAGPN65D	example	ex, section 20.1	open_logic
9DJBNJ9Y8M	proof	proof, section 44.9.6	open_logic
9DR5Y8HEBZ	proof	proof, section 30.6	open_logic
9EA419SMNB	proof	proof, section 27.10	open_logic
9F3W4Y5MDZ	statement	prop, section 15.1	open_logic
9FKKJV0XDE	statement	thm, section 72.5	open_logic
9FYYGG37TH	statement	cor, section 15.11	open_logic
Strict order	definition	defn, section 80.4	open_logic
Pairs	statement	axiom, section 76.6	open_logic
9GQSJYWHAN	statement	lem, section 38.9	open_logic
9H9YXV1TD1	exercise	prob, section 29.3	open_logic
General Recursion	statement	thm, section 74.5	open_logic
\emph{Principle of induction on terms}	statement	lem, section 22.1	open_logic
9JAQSEKGMG	statement	prop, section 22.5	open_logic
9JY82G1A1N	exercise	prob, section 22.11	open_logic
9K259K97GK	statement	lem, section 38.6	open_logic
9K57KKRFXN	statement	prop, section 44.9.5	open_logic
9K65YJYH45	example	ex, section 28.7	open_logic
9KTMANAS6G	definition	defn, section 75.2	open_logic
9KXT0DHGNV	statement	prop, section 66.6	open_logic
9M0XMH8C9N	proof	proof, section 67.2	open_logic
9M3WHZRKYN	proof	proof, section 50.1	open_logic
9MB6CEARWK	statement	thm, section 3.5	open_logic
9MC95YDXYX	example	ex, section 83.2	open_logic
9MNFQVQ7GZ	proof	proof, section 15.1	open_logic
9MS2K4WP43	proof	proof, section 87.3	open_logic
9N3AHZ158G	statement	lem, section 28.1	open_logic
9N752555EJ	exercise	prob, section 3.20	open_logic
9NN7FE9ZQV	proof	proof, section 28.6	open_logic
9NPBCYQS03	statement	prop, section 50.7	open_logic
Formation sequences for terms	definition	defn, section 19.8	open_logic
9Q5CBNEDK6	definition	defn, section 55.12	open_logic
9QBZ1FK1CH	statement	thm, section 46.2	open_logic
9QKXJ6GF88	proof	proof, section 4.2	open_logic
Entailment	definition	defn, section 67.6	open_logic
9T5GAPTWC7	statement	prop, section 9.8	open_logic
9TFN16K1R0	exercise	prob, section 34.4	open_logic
9TRWSAEG1W	exercise	prob, section 13.5	open_logic
9V082YV9NY	proof	proof, section 29.10	open_logic
9W9TJ01P6X	definition	defn, section 61.11	open_logic
9WHDHG7YSG	proof	proof, section 3.7	open_logic
9WNFRRAP21	proof	proof, section 62.7	open_logic
9WY9M6BNBW	proof	proof, section 34.6	open_logic
Change of Bound Variable	statement	lem, section 8.10	open_logic
9XSGSTNN1Z	proof	proof, section 83.6	open_logic
9XVYH9YGF5	statement	thm, section 3.17	open_logic
9Y9N1D25TW	proof	proof, section 72.2	open_logic
9YEFR4TZD2	exercise	prob, section 86.3	open_logic
9Z18BN8224	exercise	prob, section 61.9	open_logic
9ZGCHY79QV	statement	prop, section 29.3	open_logic
9ZN1P1CFCP	statement	lem, section 11.3	open_logic
9ZZWSQX0ZG	proof	proof, section 71.11	open_logic
A0MFN9D7NM	statement	prop, section 82.2	open_logic
A0YBN82Z62	example	ex, section 86.3	open_logic
A10HF44E02	statement	prop, section 3.16	open_logic
A19CGPB0RF	definition	defn, section 28.7	open_logic
A1W65ZFZJ1	exercise	prob, section 49.2	open_logic
A222DNGB17	proof	proof, section 38.9	open_logic
A28KBDRB7T	exercise	prob, section 39.2	open_logic
A2J9GFJRTT	proof	proof, section 17.7	open_logic
A34APSDZR7	definition	defn, section 19.14	open_logic
Proper prefix	definition	defn, section 22.2	open_logic
A652K6BKG3	proof	proof, section 30.3	open_logic
A68KDF9FB3	exercise	prob, section 85.1	open_logic
Completeness Theorem, Second Version	statement	cor, section 9.11	open_logic
A778E7W69V	definition	defn, section 78.5	open_logic
A7HY1T903G	proof	proof, section 52.4	open_logic
A7R5QSZBD3	exercise	prob, section 39.4	open_logic
A82J44JNXD	statement	cor, section 59.5	open_logic
A8WGRAFSNY	exercise	prob, section 66.1	open_logic
A9G9PSZSZW	exercise	prob, section 9.8	open_logic
Transitivity	statement	prop, section 22.5	open_logic
ABAK83CT2H	proof	proof, section 9.11	open_logic
ABFCRSV5M8	statement	thm, section 51.1	open_logic
ABHRE3BKC6	statement	lem, section 3.4	open_logic
ABWS2DF67C	definition	defn, section 41.2	open_logic
AC4WW0RFKW	exercise	prob, section 71.8	open_logic
AC5DSZ6WTT	statement	cor, section 59.4	open_logic
ACEAHZZB70	statement	thm, section 70.2	open_logic
ADJAF0GE4V	statement	thm, section 46.5	open_logic
AE2WZC44DD	definition	defn, section 55.1	open_logic
AEEPMZN0HP	definition	defn, section 3.21	open_logic
AEM18Y8ZCZ	statement	cor, section 19.2	open_logic
AEYMKF8SEJ	statement	thm, section 36.3	open_logic
\emph{in $\ZF$}	statement	lem, section 71.2	open_logic
AFT4HK937B	proof	proof, section 69.5	open_logic
in $\ZF$	statement	thm, section 71.4	open_logic
AJ5DRV4P2N	proof	proof, section 9.9	open_logic
AJJN7JC602	statement	prop, section 50.13	open_logic
AJV63ZZCQY	statement	thm, section 58.7	open_logic
Connectivity	definition	defn, section 82.1	open_logic
AK7K2ZBZC8	statement	prop, section 54.7	open_logic
AKM5RQWBTA	proof	proof, section 8.14	open_logic
AKNT6Z8ME9	proof	proof, section 57.4	open_logic
AMHCM7JNX4	proof	proof, section 29.8	open_logic
AMREX0B9Z0	statement	cor, section 8.14	open_logic
Generalization	statement	thm, section 8.10	open_logic
ANYT9R3KZY	proof	proof, section 19.15	open_logic
APCSGVBSXZ	exercise	prob, section 44.11	open_logic
$\beta$-equivalence, $\equal$	definition	defn, section 38.10	open_logic
APGM2KHF0R	definition	defn, section 39.1	open_logic
APVD9PDRDY	proof	proof, section 51.6	open_logic
APZC6ZEJ90	definition	defn, section 3.12	open_logic
AQ5R0NBTVQ	statement	prop, section 38.3	open_logic
AQFGPT7Z2F	definition	defn, section 32.4	open_logic
Soundness	statement	thm, section 15.11	open_logic
AQV6852ZE4	example	ex, section 82.3	open_logic
AR1ZYQM4Q3	statement	thm, section 2.2	open_logic
ATYQAC8GQF	proof	proof, section 69.4	open_logic
AV21HA8A13	proof	proof, section 72.2	open_logic
AVCTDG0Y5D	exercise	prob, section 32.5	open_logic
AVF3VQZ87D	proof	proof, section 38.9	open_logic
AVPCGTCPVR	exercise	prob, section 85.3	open_logic
AVWJM757RM	exercise	prob, section 52.5	open_logic
AX9M9WEK44	statement	cor, section 30.11	open_logic
AXG7EYPHWP	proof	proof, section 27.7	open_logic
AXRPBSC2D5	proof	proof, section 53.4	open_logic
AXSTHCYEK1	proof	proof, section 71.6	open_logic
AXTC1QE80H	definition	defn, section 53.4	open_logic
AXY3KEYYD5	example	ex, section 53.6	open_logic
AYC2G31S3F	statement	lem, section 35.1	open_logic
AYNB7RWS9E	exercise	prob, section 8.12	open_logic
AZ4HVJ3ZJ1	exercise	prob, section 54.1	open_logic
AZS6DVD3F4	definition	defn, section 51.7	open_logic
AZX4KZG2H2	statement	thm, section 56.1	open_logic
B053NZNKJG	exercise	prob, section 83.11	open_logic
B06C6MSEFK	exercise	prob, section 49.3	open_logic
B17HG0NFGE	proof	proof, section 22.9	open_logic
B1Y36V3PY9	statement	prop, section 85.1	open_logic
B2HYVABHY2	statement	prop, section 15.3	open_logic
B344HNX4JZ	proof	proof, section 22.2	open_logic
B35CCQ7753	proof	proof, section 38.15	open_logic
B3EQS5422E	statement	lem, section 58.1	open_logic
B3H133D40W	statement	cor, section 62.2	open_logic
B3N8YNQHHZ	exercise	prob, section 4.1	open_logic
B3PXY0F4AA	statement	prop, section 51.4	open_logic
B4M5QRQSH6	example	ex, section 61.6	open_logic
B4MBF9SWW3	exercise	prob, section 56.2	open_logic
B4YB4GBY90	exercise	prob, section 54.7	open_logic
B58Q8HA4AH	definition	defn, section 28.6	open_logic
B6GE026JZP	proof	proof, section 3.4	open_logic
B6NY3XK1GF	exercise	prob, section 83.1	open_logic
B6PA2KG5JB	statement	thm, section 51.8	open_logic
B6XHYEGMA4	proof	proof, section 79.6	open_logic
B83GEZET1S	definition	defn, section 71.8	open_logic
B8E2E8SFHV	proof	proof, section 73.1	open_logic
B8JE3H99HT	proof	proof, section 17.5	open_logic
B8M0J1NES7	statement	prop, section 72.2	open_logic
B8S9H1ZD94	exercise	prob, section 73.7	open_logic
B8TFPB4T12	exercise	prob, section 61.6	open_logic
Closed term, combinator	definition	defn, section 38.14	open_logic
B8Z3JAR7T4	statement	prop, section 17.8	open_logic
B95GRZ1QZZ	proof	proof, section 61.10	open_logic
B9D5HT1YMW	exercise	prob, section 62.7	open_logic
Initial sequents for $\eq$	definition	defn, section 17.4	open_logic
BAESC08BZS	proof	proof, section 61.11	open_logic
BAH6E9DWB6	proof	proof, section 17.8	open_logic
BC3MFF7WEH	proof	proof, section 27.7	open_logic
BD1P0SMGBX	statement	prop, section 58.4	open_logic
BD9Q18K4D5	proof	proof, section 73.4	open_logic
BDMGDSJYZF	exercise	probtag, section 50.15	open_logic
BDRC6X20HG	statement	thm, section 9.3	open_logic
BET1KKVQD4	exercise	prob, section 42.6	open_logic
BF0X385P2C	proof	proof, section 4.1	open_logic
BFBFTDCRE8	exercise	prob, section 5.3	open_logic
BFBQ0X8F4A	proof	proof, section 50.13	open_logic
BFVM1AFFT2	exercise	prob, section 83.5	open_logic
BGXKRQBAE8	statement	prop, section 54.4	open_logic
BGYH89Y7TT	exercise	prob, section 27.9	open_logic
BHACVRHNDR	proof	proof, section 44.11	open_logic
BHRDYC25K2	proof	proof, section 44.1	open_logic
BHXXRZPQVP	statement	lem, section 79.5	open_logic
Rice's Theorem	statement	thm, section 3.13	open_logic
BJCEF1FT2Q	definition	defn, section 66.6	open_logic
BK7GF7RTQT	proof	proof, section 35.1	open_logic
BKFJ472ZNA	definition	defn, section 67.1	open_logic
BKZBWXG4KB	statement	prop, section 46.8	open_logic
BKZC64QFNK	exercise	prob, section 41.6	open_logic
BM4SACK74Z	exercise	prob, section 46.2	open_logic
BME3PDA7SF	exercise	prob, section 42.6	open_logic
BMXQWRBXJV	proof	proof, section 50.13	open_logic
BMZ4GTHCTM	proof	proof, section 69.3	open_logic
BN2V0EHT0B	statement	lem, section 87.3	open_logic
BND7SFRVF8	statement	thm, section 38.5	open_logic
BP2XXSPH01	example	ex, section 82.3	open_logic
BPB5DZ0TJ1	statement	lem, section 29.10	open_logic
BQ9PT7YZ0K	definition	defn, section 46.7	open_logic
BQ9T6P1G91	statement	thm, section 9.3	open_logic
BQDM7ZRBNH	example	ex, section 71.1	open_logic
Sentence	definition	defn, section 19.9	open_logic
BRPWM7ZYE0	proof	proof, section 70.2	open_logic
BS77PGEZCC	proof	proof, section 2.1	open_logic
BS84E8S9X2	proof	proof, section 27.6	open_logic
BSG66QF3XB	statement	lem, section 47.5	open_logic
BSGX87K0S2	definition	defn, section 42.5	open_logic
BSM7AF2YMK	statement	lem, section 86.10	open_logic
BT3PKFT8E5	proof	proof, section 9.11	open_logic
BTNJH644ZZ	proof	proof, section 72.5	open_logic
BVMQ0E8XR3	statement	prop, section 53.4	open_logic
BVNWVEMZ2Q	proof	proof, section 79.1	open_logic
BVX6C223XJ	definition	defn, section 87.3	open_logic
BW0775BZPJ	exercise	prob, section 20.2	open_logic
BWDAA4KQ0M	statement	prop, section 27.8	open_logic
BWGQNGTB3N	statement	prop, section 49.1	open_logic
BWSJH6PBWF	definition	defn, section 6.1	open_logic
BWXYHJW65Q	proof	proof, section 3.20	open_logic
BX1B1Z55RZ	definition	defn, section 22.1	open_logic
BXC4AK22TF	definition	defn, section 25.9	open_logic
BXP12APHDS	example	ex, section 9.9	open_logic
BXWZMYP9R7	definition	defn, section 50.14	open_logic
BY3DD8ZJ14	exercise	prob, section 33.4	open_logic
Halting problem	definition	defn, section 86.7	open_logic
BYA4Z9Q0NJ	definition	defn, section 50.4	open_logic
Herbrand's Theorem	statement	thm, section 57.3	open_logic
BYEWH0VCRX	statement	prop, section 52.1	open_logic
BYGJRXD2TT	statement	prop, section 3.20	open_logic
BZ70BXRNAG	statement	cor, section 55.4	open_logic
!!^{valuation}s	definition	defn, section 63.1	open_logic
BZWPNHS4VJ	statement	cor, section 73.1	open_logic
Bisimulation	definition	defn, section 1	open_logic
C194JKQWP1	proof	proof, section 22.9	open_logic
C2864BYEM9	statement	prop, section 11.1	open_logic
C2AGNVVFFR	proof	proof, section 11.2	open_logic
C2JVZ2BJE1	proof	proof, section 22.5	open_logic
C2SAN20BYM	exercise	prob, section 76.6	open_logic
Absorption	statement	prop, section 45.1	open_logic
C3RZGB93YQ	definition	defn, section 32.5	open_logic
C3S47RZQ2E	proof	proof, section 82.6	open_logic
Pairing function	definition	defn, section 83.11	open_logic
C4P2VJRZRB	proof	proof, section 27.3	open_logic
C512A1PBXQ	statement	prop, section 9.8	open_logic
C567VW50YP	exercise	prob, section 83.2	open_logic
C5WE1Q90VT	proof	proof, section 61.10	open_logic
C5Z0JB59C9	statement	prop, section 71.8	open_logic
C6J3DXEN58	statement	prop, section 34.6	open_logic
C6MEQGXDX9	statement	prop, section 85.3	open_logic
C6NZ7PMQN9	exercise	prob, section 48.2	open_logic
C6RCC321XA	proof	proof, section 8.10	open_logic
C6TD2M3EXS	proof	proof, section 28.4	open_logic
C6Z2WV7C3D	proof	proof, section 29.10	open_logic
C8M6JM2ENV	statement	prop, section 40.2	open_logic
Subset	definition	defn, section 83.1	open_logic
C9EFX7RGSY	proof	proof, section 39.4	open_logic
C9ZM4DRM74	proof	proof, section 59.5	open_logic
C9ZPXCPBPY	statement	lem, section 56.2	open_logic
CAKDKXJD76	exercise	prob, section 51.9	open_logic
Free variables of a term	definition	defn, section 38.14	open_logic
CAMXSSPRVG	exercise	prob, section 19.4	open_logic
Matrix	definition	defn, section 41.5	open_logic
CAWAMQ550C	proof	proof, section 82.2	open_logic
CB9SD9Z7WG	statement	thm, section 51.6	open_logic
CBMDSFVDC9	proof	proof, section 17.7	open_logic
Transitivity	statement	prop, section 8.6	open_logic
Asymmetry	definition	defn, section 82.1	open_logic
CBVN1GJVHW	exercise	prob, section 46.3	open_logic
CCM9E1AA2B	exercise	prob, section 9.9	open_logic
CD42HEBXYG	definition	defn, section 3.28	open_logic
CDFC821PYA	exercise	prob, section 54.7	open_logic
CDRM91C3TK	proof	proof, section 78.6	open_logic
CE4H0EZQD3	statement	prop, section 3.20	open_logic
CFHECDK6GN	definition	defn, section 70.1	open_logic
CGCM73JYPB	exercise	prob, section 22.15	open_logic
CGNZSDJ4QP	proof	proof, section 8.10	open_logic
CGVDYADJJW	definition	defn, section 37.10	open_logic
CGZ10ZEXY3	statement	thm, section 36.7	open_logic
CH1319C5RS	exercise	prob, section 3.30	open_logic
CH3QVY6PQM	statement	prop, section 66.4	open_logic
Formula	definition	defn, section 32.2	open_logic
CHNKZ8TRKY	statement	prop, section 44.11	open_logic
CJ959RPT8Y	proof	proof, section 44.11	open_logic
CJG32QQH1N	exercise	prob, section 78.2	open_logic
CK99JR77NX	example	ex, section 31.2	open_logic
CKBSW94V6N	exercise	prob, section 3.27	open_logic
CKBYWJAKHC	definition	defn, section 28.7	open_logic
CKF5ZB7BFH	statement	prop, section 40.4	open_logic
CKPRGYAAYP	statement	prop, section 27.7	open_logic
Extensionality	definition	defn, section 38.13	open_logic
CMJ946F668	statement	thm, section 74.2	open_logic
CMY9AVHA58	example	ex, section 79.4	open_logic
CN4F4HWJJK	proof	proof, section 17.5	open_logic
CN899YV8RT	proof	proof, section 8.12	open_logic
CNKCEW3EMB	proof	proof, section 50.8	open_logic
CNKX4YNV4V	statement	thm, section 3.15	open_logic
CPG58QSE04	proof	proof, section 60.4	open_logic
CPNR0SWMRR	statement	prop, section 42.6	open_logic
Trichotomy	statement	thm, section 72.2	open_logic
CPR2VBS232	proof	proof, section 4.1	open_logic
CQBQ6E1XAQ	statement	cor, section 49.1	open_logic
CQSK0ECX32	statement	prop, section 71.11	open_logic
CR48BFQV65	example	ex, section 22.11	open_logic
CRJ35EQVPS	exercise	prob, section 80.3	open_logic
Monotonicity	statement	prop, section 40.4	open_logic
CSM2NMMEAT	proof	proof, section 3.3	open_logic
CT8AYXMN8C	statement	prop, section 38.12	open_logic
CVE4G2QJTM	example	ex, section 38.14	open_logic
CVWW6R20WQ	statement	cor, section 70.2	open_logic
CVZAFQ0TVY	proof	proof, section 30.10	open_logic
CW8ZAJD5KH	exercise	prob, section 55.4	open_logic
Strict linear order	definition	defn, section 80.4	open_logic
CWDB1HMZRV	proof	proof, section 73.11	open_logic
CWHV10KF1M	example	ex, section 61.6	open_logic
CWM68A3AN8	proof	proof, section 38.9	open_logic
Scheme of Replacement	statement	axiom, section 73.2	open_logic
CWQ71VRK0N	example	ex, section 83.1	open_logic
CX858HZ664	proof	proof, section 8.3	open_logic
CXM6NQSYPW	proof	proof, section 42.6	open_logic
CYC2YPHBEK	proof	proof, section 19.4	open_logic
CZN5DHYW69	statement	prop, section 22.7	open_logic
CZSKMERTMR	exercise	prob, section 40.2	open_logic
Validity	definition	defn, section 67.6	open_logic
D1NBZCGTXE	example	ex, section 55.5	open_logic
D277T6YFQS	exercise	prob, section 9.10	open_logic
D2DNKPX3S7	exercise	prob, section 86.3	open_logic
D2DVKQY10K	statement	prop, section 55.2	open_logic
D2GJKB222N	exercise	prob, section 19.4	open_logic
D2H56ZD5XQ	proof	proof, section 3.5	open_logic
D2YWRS3TZ2	proof	proof, section 15.5	open_logic
D3J202W0JW	proof	proof, section 60.4	open_logic
D40VN2J0ZP	statement	lem, section 22.2	open_logic
D495BGNJ24	definition	defn, section 1.2	open_logic
D4C7VZ80PG	exercise	prob, section 83.13	open_logic
Proof sketch	proof	proof, section 78.1	open_logic
Change of bound variable, $\aconvone$	definition	defn, section 38.9	open_logic
D4XGCGBDQX	exercise	prob, section 42.5	open_logic
D4YC1GQ10Q	proof	proof, section 49.1	open_logic
Terms	definition	defn, section 22.1	open_logic
D5FFSFYT4K	statement	lem, section 72.5	open_logic
D69SFZXAQ4	exercise	prob, section 83.13	open_logic
Cantor	statement	thm, section 83.3	open_logic
D81XX6MC09	proof	proof, section 38.15	open_logic
D8S5TQRE3N	definition	defn, section 37.10	open_logic
D8YN7HCQY1	exercise	prob, section 17.4	open_logic
D91B88HPKR	statement	lem, section 87.3	open_logic
D98HGQADZ4	exercise	prob, section 83.2	open_logic
D993YNDD0F	proof	proof, section 48.1	open_logic
DA84NCFK5P	exercise	prob, section 51.10	open_logic
DAH1AS6C91	statement	thm, section 15.5	open_logic
Completeness	statement	thm, section 62.2	open_logic
DCWGEHDEFY	statement	prop, section 57.4	open_logic
DE39AM8180	proof	proof, section 9.3	open_logic
DET0HFS2C4	definition	defn, section 83.4	open_logic
Proof	proof	proof, section 73.11	open_logic
DGYSS3XTNA	exercise	prob, section 30.2	open_logic
DH2HWB4AYD	example	ex, section 80.4	open_logic
DHTWZG3KS9	exercise	prob, section 51.8	open_logic
DHXY3FV3M4	exercise	prob, section 29.8	open_logic
DHZPNHMVBA	statement	prop, section 27.6	open_logic
DJ21DEVPMH	definition	defn, section 54.3	open_logic
DJN9YZNKTH	statement	prop, section 55.8	open_logic
DJVDVDT30M	proof	proof, section 49.1	open_logic
DK05HXQX2Y	exercise	prob, section 53.6	open_logic
DK9Y5HAS7D	statement	thm, section 28.5	open_logic
DKGJ6NB73W	definition	defn, section 67.5	open_logic
DKXG468JT3	definition	defn, section 54.7	open_logic
Consistency	definition	defn, section 8.6	open_logic
DN02HH9H96	statement	prop, section 80.4	open_logic
DNM4HGY2YN	statement	lem, section 71.8	open_logic
DNR9VXEF88	proof	proof, section 69.2	open_logic
DP0ZK5H15Q	statement	lem, section 27.10	open_logic
DPDJ0XMD81	proof	proof, section 27.1	open_logic
DPK97F6558	definition	defn, section 86.7	open_logic
DPPDEFG5E9	definition	defn, section 71.11	open_logic
DQR0A7K3PC	definition	defn, section 54.8	open_logic
DQWKH0YFJF	exercise	prob, section 80.1	open_logic
DR067BFZSZ	statement	lem, section 71.6	open_logic
DR5M1Z7HAW	proof	proof, section 71.11	open_logic
DR78EGFC6P	statement	cor, section 55.12	open_logic
DRGABKC0RH	proof	proof, section 8.14	open_logic
DTDEJ6D6V2	proof	proof, section 46.8	open_logic
DV75KNABX2	statement	thm, section 22.9	open_logic
DWAAM61MPT	proof	proof, section 74.4	open_logic
DWH9ZTESJB	proof	proof, section 35.2	open_logic
DY0G2AX59R	proof	proof, section 15.3	open_logic
\emph{in $\ZF$}	statement	thm, section 71.2	open_logic
DY447EJM15	proof	proof, section 46.2	open_logic
DY90MHK3N7	definition	defn, section 54.3	open_logic
DYDYZGRHAB	example	ex, section 55.7	open_logic
DZA2462TH2	exercise	probtag, section 51.5	open_logic
DZC2HFYC1G	statement	thm, section 3.4	open_logic
DZZAA5TQEX	definition	defn, section 61.6	open_logic
E1GB8MH080	exercise	prob, section 52.5	open_logic
E1NFRH6JED	definition	defn, section 87.1	open_logic
E1SVCKNWF5	exercise	prob, section 78.4	open_logic
E2B7XHE62K	proof	proof, section 74.5	open_logic
E2WD66MPCK	exercise	prob, section 9.11	open_logic
E3274AWQXS	proof	proof, section 3.9	open_logic
E3AN4M7EE4	proof	proof, section 3.17	open_logic
Tree	definition	defn, section 82.2	open_logic
E41X6Y734Y	proof	proof, section 71.2	open_logic
E4CN9CATWE	proof	proof, section 79.7	open_logic
E4KVCVHW52	statement	cor, section 19.2	open_logic
Foundation	statement	axiom, section 74.2	open_logic
E65P8STK61	definition	defn, section 78.2	open_logic
E6TNKE9TVW	proof	proof, section 29.3	open_logic
E7DTC32AY3	proof	proof, section 72.7	open_logic
E7RG3JSVB0	definition	defn, section 3.30	open_logic
E8ZF3F0NDA	statement	cor, section 51.3	open_logic
E91PJTKMPW	proof	proof, section 51.8	open_logic
E9F2GJPT9F	proof	proof, section 70.2	open_logic
Completeness	statement	thm, section 55.4	open_logic
E9HS4C4C95	proof	proof, section 29.3	open_logic
EASRJM5VWR	definition	defn, section 39.1	open_logic
EBMCTCBK2P	proof	proof, section 41.6	open_logic
EBMNCZP7DP	statement	cor, section 70.2	open_logic
EC01ZD00TP	definition	defn, section 33.1	open_logic
EC059BR05V	proof	proof, section 76.6	open_logic
ECKS63MJ1C	example	ex, section 17.3	open_logic
!!^{derivation}	definition	defn, section 13.4	open_logic
ED8DS3V5XD	exercise	prob, section 9.8	open_logic
EDC2YHFCNT	proof	proof, section 80.4	open_logic
!!^{derivability}	definition	defn, section 31.1	open_logic
EDFV7ZCJYA	example	ex, section 67.1	open_logic
Substitution in !!a{formula}	definition	defn, section 20.3	open_logic
EEBT1KAWTC	statement	prop, section 50.2	open_logic
EEH9H550HN	exercise	prob, section 27.1	open_logic
EEKR0ZXS20	proof	proof, section 58.1	open_logic
Transfinite Induction	statement	thm, section 72.2	open_logic
EFTXPJW6MW	proof	proof, section 38.3	open_logic
EG7HN62QPW	proof	proof, section 71.6	open_logic
EG8MEZC11T	exercise	prob, section 55.8	open_logic
EGHYDTTP84	definition	defn, section 30.3	open_logic
EH0KVTZAY9	proof	proof, section 69.2	open_logic
EH4EHR3CHD	statement	prop, section 11.4	open_logic
EHAS44MQ4J	definition	defn, section 19.4	open_logic
EHNRGQ8222	exercise	prob, section 3.11	open_logic
EJ32DVECZE	proof	proof, section 45.1	open_logic
EJBVNYWFJB	statement	lem, section 22.2	open_logic
EJDJX2M8JK	statement	lem, section 19.8	open_logic
Russell's Paradox	statement	thm, section 75.7	open_logic
EK9X0DZ268	statement	prop, section 49.1	open_logic
EN2ZYE0STK	proof	proof, section 66.1	open_logic
ENHXYQ7H4M	proof	proof, section 49.1	open_logic
ENPN6JT949	example	ex, section 17.11	open_logic
EP9TV5DR2G	exercise	prob, section 8.6	open_logic
EQ4V3KB7S1	statement	prop, section 50.7	open_logic
in $\Z + \text{Weak-Reflection}$.	statement	lem, section 73.11	open_logic
EQPE1SZF5Z	proof	proof, section 19.14	open_logic
ERV6VW2JY9	statement	prop, section 51.1	open_logic
!!^{main operator}	definition	defn, section 19.13	open_logic
ES1GXHAHTK	exercise	prob, section 83.11	open_logic
ESRP8A1NXR	exercise	prob, section 85.5	open_logic
ET548GCJDR	definition	defn, section 3.31	open_logic
ETHX88YXXX	proof	proof, section 69.5	open_logic
Nice terms	definition	defn, section 44.1	open_logic
EVFT5XNBCW	proof	proof, section 80.4	open_logic
EW19CXVJY2	proof	proof, section 22.5	open_logic
EX2RQN5XNN	example	ex, section 86.3	open_logic
EX5CR0EVAN	statement	prop, section 49.1	open_logic
EX79S7EPRK	exercise	prob, section 83.8	open_logic
Branches	definition	defn, section 82.2	open_logic
EYKV9KXWSN	proof	proof, section 38.6	open_logic
Semantic Deduction Theorem	statement	thm, section 19.15	open_logic
EZ8M40SPYK	proof	proof, section 58.5	open_logic
F04WW77JSB	exercise	prob, section 17.7	open_logic
F04YSZ7GM3	exercise	prob, section 13.1	open_logic
F0D0JGKP78	proof	proof, section 60.6	open_logic
F0GTQWA4JZ	proof	proof, section 11.4	open_logic
F10NPNKJBV	definition	defn, section 80.1	open_logic
F19HHMSVHP	statement	lem, section 72.5	open_logic
F1DSKC75PV	definition	defn, section 47.3	open_logic
Term model	definition	defn, section 11.1	open_logic
Vitali's Paradox (in $\ZFC$)	statement	thm, section 71.6	open_logic
F264EBXX57	example	ex, section 19.7	open_logic
F2XB5M5A9P	proof	proof, section 71.1	open_logic
F3QMFFS6YS	example	ex, section 31.2	open_logic
Scope	definition	defn, section 19.9	open_logic
Extensionality	statement	axiom, section 75.4	open_logic
F4EJ0CJGZG	proof	proof, section 52.1	open_logic
F4KKK7HD9M	example	ex, section 82.5	open_logic
F5C1W7C9KW	statement	thm, section 30.8	open_logic
F5EPBNAAZ3	proof	proof, section 50.5	open_logic
F5JJEKFR1Z	proof	proof, section 36.3	open_logic
F5WQ6ASC6C	statement	prop, section 15.3	open_logic
F5Z656E1AQ	proof	proof, section 86.7	open_logic
F67GXHFDMY	statement	lem, section 72.5	open_logic
F6GPS1REFM	proof	proof, section 73.11	open_logic
F7FAYM1FQ2	example	ex, section 78.8	open_logic
F7SPN8JHCH	proof	proof, section 61.4	open_logic
F87VBGGAQH	exercise	prob, section 42.4	open_logic
F8A4FXYGPD	proof	proof, section 36.5	open_logic
F8G1GGRXT4	proof	proof, section 71.8	open_logic
F8JYMK17HF	statement	lem, section 29.10	open_logic
F8R66YJWS5	exercise	prob, section 61.6	open_logic
F98HJAPEAT	exercise	prob, section 39.4	open_logic
F9ZT6Q9Z44	statement	prop, section 50.2	open_logic
FA4DQ5AA1F	definition	defn, section 79.6	open_logic
FAHE999M30	statement	prop, section 69.3	open_logic
FBA03Z38JB	example	ex, section 83.2	open_logic
Union	definition	defn, section 83.2	open_logic
FC1467AJFS	proof	proof, section 3.20	open_logic
FCB15G0M9Z	proof	proof, section 45.1	open_logic
FCDQZK1536	definition	defn, section 61.12	open_logic
FCK4MJQNZD	proof	proof, section 45.1	open_logic
FD1Q2PKAJC	statement	cor, section 73.2	open_logic
FEBPE9CN6A	statement	lem, section 36.4	open_logic
FEH1MFQZ50	proof	proof, section 3.8	open_logic
FFDDG3XC6N	example	ex, section 80.4	open_logic
FFDREFZH6T	proof	proof, section 29.8	open_logic
FFEKMTZ3W6	exercise	prob, section 9.9	open_logic
FFR1DJ663X	statement	thm, section 1	open_logic
FFV1XVZWYD	statement	thm, section 29.2	open_logic
Formula	definition	defn, section 41.3	open_logic
FG6A1RKKAM	proof	proof, section 79.7	open_logic
FGNE30F8XJ	exercise	prob, section 22.5	open_logic
FJ1F91KE6B	definition	defn, section 79.3	open_logic
FJHWCXYHEJ	statement	prop, section 22.8	open_logic
FJJB77HYBM	proof	proof, section 3.20	open_logic
FK4HGWXZ8F	proof	proof, section 83.6	open_logic
FK6NWF7VKP	statement	lem, section 35.2	open_logic
FMYA24SBY4	statement	prop, section 3.20	open_logic
FN0RJVWZV6	proof	proof, section 46.6	open_logic
FND30B4Z3R	definition	defn, section 42.1	open_logic
FQ36ZS8CRT	proof	proof, section 30.13	open_logic
FQ7DSA7S52	definition	defn, section 73.3	open_logic
FR0Q1X9AB2	exercise	prob, section 38.7	open_logic
FRTDEBNCPX	proof	proof, section 29.5	open_logic
FS47P53NTR	example	ex, section 80.2	open_logic
FSFEA6265F	definition	defn, section 57.4	open_logic
FSNHRXSS3D	statement	prop, section 55.3	open_logic
FTS8DTB81S	proof	proof, section 52.3	open_logic
FV906J2ZBY	exercise	prob, section 49.2	open_logic
FWSDGWR4FP	exercise	prob, section 42.5	open_logic
FX6Y2DF8SH	proof	proof, section 72.7	open_logic
FYWSBTKDYH	proof	proof, section 58.3	open_logic
FZ6SFMZDSD	statement	prop, section 27.1	open_logic
FZ95T1Y1ZS	statement	prop, section 8.5	open_logic
FZ9KE4TPBX	proof	proof, section 34.1	open_logic
G0F8PFVWH7	proof	proof, section 83.5	open_logic
Proof: first part.	proof	proof, section 25.8	open_logic
G1FTZ1V8TJ	proof	proof, section 15.5	open_logic
G1XD3DVRHH	example	ex, section 78.9	open_logic
G2984T1DCT	exercise	prob, section 59.1	open_logic
G39EPQ2E06	example	ex, section 83.10	open_logic
G3BG57XFRA	statement	thm, section 46.1	open_logic
G3CJYDBSNE	proof	proof, section 62.8	open_logic
G3DJKP15XH	statement	prop, section 66.6	open_logic
G3GHCP4AJ5	proof	proof, section 54.7	open_logic
G4VYSVDH0D	statement	prop, section 52.5	open_logic
G52GWKES8N	definition	defn, section 12.10	open_logic
G5ASZ332AF	statement	lem, section 35.2	open_logic
G5CJSG7NTN	proof	proof, section 62.6	open_logic
G5SG8VNQSQ	exercise	prob, section 74.4	open_logic
G5X5B6DQHA	definition	defn, section 41.6	open_logic
G6MGP8G9HY	exercise	prob, section 57.3	open_logic
G6PRYF1WPX	definition	defn, section 28.7	open_logic
G6RBEFZEQP	proof	proof, section 71.7	open_logic
G777KS6CVM	proof	proof, section 49.1	open_logic
Proof skeleton	proof	proof, section 69.4	open_logic
G7KWM7PG08	exercise	prob, section 3.18	open_logic
G9JBYXPDDR	example	ex, section 27.2	open_logic
GAVY1NY3BK	definition	defn, section 20.3	open_logic
GBB3BYCSGN	exercise	prob, section 59.1	open_logic
GBD7MMMQZQ	proof	proof, section 50.6	open_logic
in \emph{Grundgesetze}	statement	lem, section 75.5	open_logic
GBME3DDGW7	proof	proof, section 50.16	open_logic
GC5F9EZP7Q	statement	prop, section 15.10	open_logic
K\H{o}nig's lemma	statement	prop, section 82.2	open_logic
GCWXEYEN4A	proof	proof, section 8.10	open_logic
Initial Sequent	definition	defn, section 40.6	open_logic
GEJPEZZ5R6	statement	prop, section 54.7	open_logic
Deduction Theorem	statement	thm, section 8.3	open_logic
GGKRDZGMPN	exercise	prob, section 67.1	open_logic
GH076J8K8P	statement	lem, section 87.3	open_logic
GH333M3Z30	proof	proof, section 46.5	open_logic
GHDXSES0PP	statement	prop, section 55.8	open_logic
GHHRPAFAWV	statement	lem, section 38.6	open_logic
GJ8NYZZPXW	exercise	prob, section 3.11	open_logic
GJ96VQTJJV	proof	proof, section 87.2	open_logic
GK6ZP6A7P6	statement	thm, section 70.2	open_logic
GM4Z6XF4HP	proof	proof, section 72.2	open_logic
GM5A9Z51T6	statement	prop, section 19.15	open_logic
GM9V7QF04K	statement	thm, section 78.6	open_logic
GNYA57SY5Q	proof	proof, section 30.7	open_logic
GP82G7TWZZ	statement	thm, section 38.15	open_logic
GP8ZV5EZNR	exercise	prob, section 49.1	open_logic
GPT0NFAVH8	statement	prop, section 19.4	open_logic
GQEY8GQ5KK	statement	thm, section 87.2	open_logic
GQHF033K4J	statement	lem, section 36.6	open_logic
Lindenbaum's Lemma	statement	lem, section 33.5	open_logic
GQTZFW4MY1	statement	prop, section 51.7	open_logic
GR4V7A771N	proof	proof, section 32.4	open_logic
GRA7C80P1M	statement	thm, section 52.5	open_logic
GRBP70YG7J	statement	thm, section 36.2	open_logic
GS0TWXGEWE	proof	proof, section 19.15	open_logic
GS17HZSQP4	exercise	prob, section 27.5	open_logic
Theorems	definition	defn, section 40.6	open_logic
GT9A55B7MM	statement	prop, section 74.4	open_logic
GTANQBACNQ	definition	defn, section 83.6	open_logic
GTDNPWDGG2	statement	prop, section 50.13	open_logic
GVB7EAJ1D1	exercise	prob, section 3.26	open_logic
GVGAT89P68	statement	thm, section 3.3	open_logic
Soundness	statement	thm, section 34.1	open_logic
GVVS4C3JRQ	proof	proof, section 50.2	open_logic
GWQED7MN7S	statement	thm, section 76.8	open_logic
GWSF2RCXM7	definition	defn, section 50.4	open_logic
GWV1X8MAVY	definition	defn, section 54.5	open_logic
GXSEMDV3N6	statement	lem, section 36.3	open_logic
Compactness	statement	prop, section 40.4	open_logic
GYTE7NRX29	exercise	prob, section 51.7	open_logic
GYVYF3TTC4	definition	defn, section 72.7	open_logic
GZF4XXD028	proof	proof, section 36.7	open_logic
GZPQHYPNA5	example	ex, section 67.5	open_logic
GZQHTXXVV1	statement	prop, section 41.6	open_logic
H05RVBJYKF	example	ex, section 71.1	open_logic
H0HKAGRW4E	proof	proof, section 72.5	open_logic
H0M5REPBHN	proof	proof, section 36.2	open_logic
H1EH82YZX6	statement	prop, section 3.11	open_logic
H1GKSDB8CJ	definition	defn, section 30.3	open_logic
!!^{injective} function	definition	defn, section 78.10	open_logic
H2MT9ERM91	proof	proof, section 69.3	open_logic
!!^{structure}s	definition	defn, section 20.1	open_logic
H3GEJ3QM7J	proof	proof, section 11.4	open_logic
H3P8BTMBC9	proof	proof, section 79.1	open_logic
H42TR7JA0M	proof	proof, section 51.4	open_logic
H44SEP9WQ9	statement	prop, section 52.4	open_logic
H4CJ6EAC93	exercise	prob, section 27.10	open_logic
H4JFH34ARW	statement	prop, section 67.2	open_logic
H4RWTGZ72X	exercise	prob, section 87.3	open_logic
H5CVVFYMCP	definition	defn, section 29.4	open_logic
H606K4CXYM	example	ex, section 49.2	open_logic
H6NVHY2TBW	proof	proof, section 22.14	open_logic
H75PB4S57P	proof	proof, section 79.5	open_logic
H853Y3CBSJ	proof	proof, section 74.2	open_logic
H8G37FVP15	example	ex, section 78.10	open_logic
H8KFDSGXSV	exercise	prob, section 15.7	open_logic
H92Q93S8H6	exercise	prob, section 51.4	open_logic
H9AKB8KSM6	statement	prop, section 27.8	open_logic
H9FR37NFA3	example	ex, section 22.10	open_logic
H9SNW79E9T	definition	defn, section 27.6	open_logic
H9TP3JQPCM	proof	proof, section 3.18	open_logic
H9YB3QYWP9	exercise	prob, section 59.2	open_logic
H9YMSWRHN7	statement	prop, section 32.6	open_logic
HA3W4QVQ7P	statement	prop, section 79.1	open_logic
HAAXG3EZTE	exercise	prob, section 38.4	open_logic
HADR3C585K	statement	prop, section 42.6	open_logic
HAGFD65W3Q	proof	proof, section 55.8	open_logic
HAJREKS3AX	exercise	prob, section 86.1	open_logic
HAMY4P15BH	exercise	prob, section 69.4	open_logic
HAQX4MPN09	exercise	prob, section 9.8	open_logic
HATDCR3KZ9	proof	proof, section 71.6	open_logic
HAV19VWGAH	proof	proof, section 2.2	open_logic
HAZXETCC8D	proof	proof, section 22.8	open_logic
HBDRN09E85	statement	prop, section 3.20	open_logic
HBGF6EMMAQ	statement	thm, section 70.2	open_logic
HC1FTD2G26	proof	proof, section 62.1	open_logic
HC38JD6T9S	example	ex, section 83.4	open_logic
HC8JEJC8KT	definition	defn, section 54.3	open_logic
HCPPFCGTDF	statement	prop, section 74.4	open_logic
HCS842FQ4F	statement	lem, section 36.2	open_logic
HCYFG5AQER	statement	prop, section 13.2	open_logic
HDRRN1H4R3	proof	proof, section 35.1	open_logic
HDWR8AB3BP	proof	proof, section 38.9	open_logic
HE960XTKCT	definition	defn, section 46.6	open_logic
HEY5XN2CQY	proof	proof, section 8.7	open_logic
Irreflexivity	definition	defn, section 82.1	open_logic
HG1WVVZ3S8	proof	proof, section 74.4	open_logic
HG75CXCRR4	proof	proof, section 43.1	open_logic
Soundness	statement	thm, section 8.14	open_logic
HGPN1K082A	exercise	prob, section 13.5	open_logic
HH04WX1JJS	statement	prop, section 62.3	open_logic
HH6ZDAJZ0S	exercise	prob, section 82.1	open_logic
HHQ1H0G2ET	proof	proof, section 15.10	open_logic
HJ2H11SV4X	statement	prop, section 39.3	open_logic
Compactness	statement	prop, section 22.5	open_logic
HJKB4E234M	statement	prop, section 76.8	open_logic
HJM3J51E4X	example	ex, section 8.12	open_logic
HJQXCFZQ3W	proof	proof, section 38.13	open_logic
HK5J4YSQQF	exercise	prob, section 54.7	open_logic
HK5MZHQ27X	statement	cor, section 34.6	open_logic
HK66D4800A	statement	cor, section 69.3	open_logic
HKB2GGZCT1	proof	proof, section 27.9	open_logic
HKZFYKHRHE	statement	prop, section 4.1	open_logic
HM74H6JWST	definition	defn, section 50.1	open_logic
HMMJ4NVWE2	example	ex, section 86.3	open_logic
HMS0RFX4WY	proof	proof, section 22.5	open_logic
HMX298QQDJ	statement	thm, section 78.1	open_logic
HNCXFSDTCG	statement	prop, section 4.1	open_logic
HNHHH9G213	definition	defn, section 1.12	open_logic
HNMJACHFGT	statement	prop, section 27.5	open_logic
HPCQSZ2EVX	example	ex, section 5.5	open_logic
HPQHJFR6C4	definition	defn, section 33.5	open_logic
HPZR3431GY	proof	proof, section 22.8	open_logic
HREGJASN5R	statement	prop, section 49.4	open_logic
HS8K5RQJW5	statement	prop, section 31.1	open_logic
HSC4XN15Q2	exercise	prob, section 28.4	open_logic
HT3P8AEV4E	proof	proof, section 3.20	open_logic
HT4GJW3WQS	statement	thm, section 8.10	open_logic
HV19V0838X	definition	defn, section 29.9	open_logic
Choice	statement	axiom, section 71.7	open_logic
HV6DNPMEBV	statement	prop, section 66.6	open_logic
HVD24QP957	statement	prop, section 76.6	open_logic
HWNEZH31AX	proof	proof, section 78.2	open_logic
HWRBCP7413	proof	proof, section 38.9	open_logic
HX9E9K978J	exercise	prob, section 44.3	open_logic
HXA1YABCRH	proof	proof, section 17.7	open_logic
HXBBQNVHTY	example	ex, section 79.2	open_logic
HXG2JPPYS4	exercise	prob, section 46.5	open_logic
HXSRFA285Q	statement	prop, section 69.2	open_logic
HYJ3YEC6VQ	exercise	prob, section 55.8	open_logic
$\Log{LK}$ !!{derivation}	definition	defn, section 17.3	open_logic
HYVZZ8NQW7	proof	proof, section 51.5	open_logic
HZ55ZPMPB5	statement	prop, section 46.5	open_logic
HZGRHTVMFZ	definition	defn, section 52.4	open_logic
J08V62QD6T	statement	cor, section 30.11	open_logic
Enumeration, set-theoretic	definition	defn, section 83.4	open_logic
J0VTXJRMJK	proof	proof, section 50.8	open_logic
J1475Y5HEC	exercise	prob, section 52.6	open_logic
J1GF7P1CEW	exercise	prob, section 50.8	open_logic
J1RR4CZWY5	statement	prop, section 8.4	open_logic
J1V0CS4DKP	example	ex, section 49.2	open_logic
J2AC5KDEYQ	proof	proof, section 76.8	open_logic
J2RZD1HXN3	exercise	prob, section 19.8	open_logic
J3CC9PNRNY	statement	prop, section 62.7	open_logic
J3DWGJVGG7	exercise	prob, section 54.7	open_logic
Hausdorff's Paradox (in $\ZFC$)	statement	thm, section 71.6	open_logic
J3QXQP1VXF	exercise	prob, section 39.3	open_logic
J3XVC2W8WE	proof	proof, section 9.10	open_logic
J4NBH4BZY8	proof	proof, section 53.3	open_logic
J5DZC9BWH7	statement	prop, section 66.1	open_logic
J5JBBYC9Q2	proof	proof, section 19.4	open_logic
J61BE5XS59	definition	defn, section 78.4	open_logic
Craig's Interpolation Theorem	statement	thm, section 46.10	open_logic
Free occurrences of !!a{variable}	definition	defn, section 19.9	open_logic
J7KN679BXD	example	ex, section 85.6	open_logic
J7YBRJC6J6	definition	defn, section 50.7	open_logic
Preorder	definition	defn, section 80.4	open_logic
J81TAEW1T6	proof	proof, section 27.1	open_logic
J8H21W5XH6	exercise	prob, section 86.1	open_logic
J928Q31YZN	proof	proof, section 87.3	open_logic
J94XDPJ7JC	exercise	prob, section 44.5	open_logic
J99HV3EZPD	exercise	prob, section 49.4	open_logic
J9WE2SMXBJ	proof	proof, section 75.5	open_logic
Proof of \olref{thm:lob}	proof	proof, section 28.2	open_logic
Proof of {\olref[nen]{thm:nonenum-pownat}} by reduction	proof	proof, section 83.13	open_logic
JB58K264DB	exercise	prob, section 22.10	open_logic
JCC8P2Q69S	exercise	prob, section 19.14	open_logic
JCMCMG8YYP	exercise	prob, section 83.4	open_logic
JD67VD1XPB	exercise	prob, section 62.6	open_logic
JDKHCK9EEF	proof	proof, section 8.5	open_logic
JE6DYTJKG4	exercise	prob, section 11.7	open_logic
JE97VB0BPT	proof	proof, section 50.9	open_logic
JESF92NWXN	exercise	prob, section 27.6	open_logic
JEV7A17XAV	statement	prop, section 39.4	open_logic
JEY55GVYE0	exercise	prob, section 37.8	open_logic
Truth Lemma	statement	lem, section 62.2	open_logic
JF89X4WKMZ	exercise	prob, section 30.3	open_logic
JFK2R5BPY4	definition	defn, section 1.4	open_logic
JGAKYR5TDH	proof	proof, section 19.6	open_logic
JGF1M462WR	example	ex, section 80.4	open_logic
Configuration	definition	defn, section 85.4	open_logic
JHR6XVSTQ1	statement	prop, section 61.9	open_logic
JHYBXZVH2W	statement	prop, section 66.6	open_logic
Well-Ordering	statement	axiom, section 70.1	open_logic
JK677XNNSQ	statement	cor, section 34.6	open_logic
JKGFPKSGBZ	proof	proof, section 11.3	open_logic
JMEADM3VXQ	statement	prop, section 11.3	open_logic
JMMDBYKJQN	exercise	prob, section 52.3	open_logic
JMS25W1TRZ	statement	thm, section 30.9	open_logic
JPA7AKV2PX	definition	defn, section 78.11	open_logic
JPYYDWCRJZ	statement	lem, section 29.5	open_logic
JQ3PAMQG4S	proof	proof, section 40.4	open_logic
JQ8AQMT12D	exercise	prob, section 72.2	open_logic
JQ8FYPKSHF	statement	lem, section 29.3	open_logic
JRDKRCA2E7	statement	thm, section 86.6	open_logic
JRPAHS6E94	statement	lem, section 29.4	open_logic
JSPHZECS4Y	statement	prop, section 50.1	open_logic
Newman's Lemma	statement	lem, section 60.4	open_logic
Formation sequences for formulas	definition	defn, section 19.8	open_logic
JV4ZM8M6XY	exercise	prob, section 62.6	open_logic
Satisfaction	definition	defn, section 67.5	open_logic
Midsequent Theorem	statement	thm, section 57.3	open_logic
JVR68DA6BW	statement	thm, section 37.9	open_logic
JW6DJ722HH	exercise	prob, section 61.7	open_logic
JWG15G50C1	proof	proof, section 3.20	open_logic
JWM4599X72	example	ex, section 34.4	open_logic
JXPG36RWXD	proof	proof, section 19.6	open_logic
!!^{derivability}	definition	defn, section 22.5	open_logic
JYRCJ4A51W	exercise	prob, section 12.9	open_logic
JYSSCRNNE5	exercise	prob, section 46.3	open_logic
Monotonicity	statement	prop, section 17.5	open_logic
JZXE0MRGZZ	statement	lem, section 38.6	open_logic
K04DD342SA	definition	defn, section 46.5	open_logic
K0A44DPG55	exercise	prob, section 83.12	open_logic
K0QJNQ75VC	exercise	prob, section 22.15	open_logic
K123ZZCRWA	proof	proof, section 49.1	open_logic
K13CR7VWS8	example	ex, section 9.9	open_logic
K1DK1NG88V	proof	proof, section 30.8	open_logic
K1NHYRRTKN	statement	prop, section 27.3	open_logic
K1PDBYH7C8	statement	prop, section 74.4	open_logic
K1Q97AAS2Q	exercise	prob, section 83.4	open_logic
K1ZA8K762M	statement	prop, section 72.2	open_logic
K232EKJEFF	proof	proof, section 85.1	open_logic
K286BMVEEP	proof	proof, section 8.7	open_logic
K2A7E9XTRH	statement	thm, section 60.4	open_logic
K2N729828P	definition	defn, section 28.7	open_logic
K3ZA3VZJQC	exercise	probtag, section 19.15	open_logic
K40G5S41A5	exercise	prob, section 38.8	open_logic
K4MAKCZWP7	statement	prop, section 50.9	open_logic
K4TKCE21QK	statement	prop, section 50.2	open_logic
Complete set	definition	defn, section 9.10	open_logic
K5JB4HH9MP	proof	proof, section 8.9	open_logic
K5VTA6GR3A	statement	thm, section 35.2	open_logic
K643A1GNB7	statement	thm, section 73.1	open_logic
K6BCCDAQX6	proof	proof, section 36.1	open_logic
K75HBZG5C4	proof	proof, section 80.1	open_logic
K7QH6YQFYD	statement	prop, section 69.2	open_logic
K7YKMF43MP	proof	proof, section 3.31	open_logic
K83NDS5ZZV	proof	proof, section 30.7	open_logic
K8CNC5PM8P	proof	proof, section 78.4	open_logic
K8W5G53JT0	proof	proof, section 50.2	open_logic
Deduction Theorem	statement	thm, section 8.4	open_logic
!!^{derivability}	definition	defn, section 17.5	open_logic
KBJH53G8W9	statement	prop, section 66.4	open_logic
KBKX8NJMVN	statement	prop, section 42.4	open_logic
KCCXZ70TND	statement	lem, section 79.6	open_logic
Transitivity	statement	prop, section 40.4	open_logic
KCM5QDGS8S	proof	proof, section 27.5	open_logic
KEBEJCDMBJ	definition	defn, section 58.1	open_logic
KEDDP85C7B	definition	defn, section 46.2	open_logic
KEJDK85MGB	statement	lem, section 71.6	open_logic
KEMNE9A175	exercise	prob, section 49.1	open_logic
KF489HCSDC	proof	proof, section 46.1	open_logic
KFWXVZHDZF	statement	lem, section 29.11	open_logic
KG3Q1HA6AB	definition	defn, section 50.10	open_logic
Lindenbaum's Lemma	statement	thm, section 51.3	open_logic
KGTMG5J4Q2	statement	cor, section 38.9	open_logic
KGZY2N0ZKD	proof	proof, section 86.10	open_logic
KH1K8PTNZ4	proof	proof, section 40.4	open_logic
KHB93MDCM0	statement	lem, section 29.5	open_logic
KHBPZVMYYY	proof	proof, section 57.1	open_logic
KHGFM25XSK	definition	defn, section 27.9	open_logic
KHH1C9E6E5	proof	proof, section 19.2	open_logic
KHT1PZB8WF	proof	proof, section 17.9	open_logic
KJ30ATD73C	statement	prop, section 83.5	open_logic
KJ9CTFSFNR	statement	prop, section 44.9.8	open_logic
KJN89PSGFB	exercise	prob, section 38.15	open_logic
KJWRR5VZRS	proof	proof, section 37.8	open_logic
KJY2ZZ0620	statement	lem, section 74.2	open_logic
KK4QDR0RW4	example	ex, section 86.1	open_logic
KKQEY0KXNX	statement	thm, section 65.3	open_logic
KMY4YZ31W8	exercise	prob, section 33.3	open_logic
KNG7J7F3P2	proof	proof, section 8.6	open_logic
KNQCX4QJZA	statement	cor, section 19.2	open_logic
KNYE4K58EG	definition	defn, section 1.12	open_logic
Graph of a function	definition	defn, section 78.11	open_logic
KQB59PDTSR	statement	prop, section 80.1	open_logic
KQHPF6R31F	definition	defn, section 33.1	open_logic
KRH73E7Y79	proof	proof, section 8.10	open_logic
KS9P0TX1QK	definition	defn, section 50.3	open_logic
KSVAATQ1MR	exercise	prob, section 82.3	open_logic
KTCGBMGFX2	exercise	prob, section 5.3	open_logic
KTEENBR9E9	statement	prop, section 53.3	open_logic
KTZ3HA1BSG	proof	proof, section 37.3	open_logic
KV2J09H17D	definition	defn, section 46.5	open_logic
KVMQNATP7G	proof	proof, section 50.3	open_logic
KW7RB6HKF7	definition	defn, section 37.9	open_logic
KWDKRMXDF5	exercise	prob, section 30.3	open_logic
KWKKY36MSG	exercise	prob, section 8.7	open_logic
KWR6990M3H	statement	prop, section 3.31	open_logic
KX7ZPKDXB2	definition	defn, section 11.1	open_logic
KXK1TMGJKH	proof	proof, section 19.2	open_logic
Proof of Herbrand's Theorem	proof	proof, section 57.3	open_logic
$\beta$-contraction, $\bredone$	definition	defn, section 38.10	open_logic
KXQ9XM1RZW	statement	prop, section 17.7	open_logic
KY6NJTF51P	statement	prop, section 69.1	open_logic
KYJMZSF7PR	proof	proof, section 70.2	open_logic
KYPNGFKR34	proof	proof, section 44.11	open_logic
KZASCQ7HD5	proof	proof, section 19.1	open_logic
KZHZ5D19B0	example	ex, section 41.3	open_logic
KZKY47NG19	proof	proof, section 15.1	open_logic
KZXF98WEHC	definition	defn, section 46.3	open_logic
M06DAWM6W6	proof	proof, section 15.3	open_logic
M07PCFZE3S	exercise	prob, section 79.3	open_logic
M0G5K41YSK	statement	thm, section 37.1	open_logic
M1ARWV2AFA	proof	proof, section 35.2	open_logic
M2HBANQ2DK	proof	proof, section 69.3	open_logic
M35K1GAVZQ	proof	proof, section 51.9	open_logic
M3CWV7DENF	proof	proof, section 78.11	open_logic
M3KBY8H80J	example	ex, section 53.7	open_logic
M47BMKH3B2	statement	lem, section 37.5	open_logic
M4F89S27HM	statement	prop, section 22.7	open_logic
M5E1MRM67Q	statement	thm, section 33.3	open_logic
M5EQ0MWP5J	statement	prop, section 8.7	open_logic
M5W4E1PEB7	definition	defn, section 73.4	open_logic
M6G33XMSDE	example	ex, section 17.11	open_logic
M7CT4MYZ14	definition	defn, section 12.9	open_logic
Consistency	definition	defn, section 17.5	open_logic
M7PA152Z0F	proof	proof, section 46.10	open_logic
Unique Readability	statement	prop, section 39.3	open_logic
M8DAD23PTY	proof	proof, section 22.7	open_logic
M8WG52JFSK	exercise	prob, section 28.5	open_logic
M95WPB762R	statement	prop, section 32.6	open_logic
M9EXA8MC5T	proof	proof, section 86.9	open_logic
MA037V7KY3	exercise	prob, section 6.2	open_logic
MAQXEXWJZY	proof	proof, section 8.8	open_logic
MBK55VSTCP	statement	lem, section 11.4	open_logic
MC2V3ATX0A	definition	defn, section 42.4	open_logic
MC650G2W18	proof	proof, section 15.11	open_logic
MC9PJAJ6VJ	proof	proof, section 3.20	open_logic
MCQY3VACRC	statement	prop, section 69.4	open_logic
MDY2VCVBTH	statement	thm, section 30.7	open_logic
ME881TPNVW	statement	thm, section 38.15	open_logic
MEEBR801YB	statement	prop, section 19.15	open_logic
MFDH3DPW2X	proof	proof, section 55.4	open_logic
MG389BQWP4	proof	proof, section 51.7	open_logic
MGT2VE46Y0	statement	prop, section 46.4	open_logic
MH69856YWS	proof	proof, section 40.4	open_logic
MH7ADZW54F	statement	lem, section 69.5	open_logic
Turing machine	definition	defn, section 86.2	open_logic
MHV4QKQPG3	definition	defn, section 39.4	open_logic
MHXCT65YJQ	exercise	prob, section 83.1	open_logic
MJ4CF6H612	statement	lem, section 29.3	open_logic
MJ70F8A5T3	example	ex, section 8.12	open_logic
MJFXTZDVZ2	proof	proof, section 19.8	open_logic
MJYM0FYRYK	definition	defn, section 54.7	open_logic
MK6H5A867F	statement	prop, section 27.7	open_logic
MK6HNJE36Z	statement	prop, section 27.1	open_logic
MKAP28S3ND	statement	lem, section 37.3	open_logic
MKE5A9N70M	proof	proof, section 78.2	open_logic
MKKK0Q90Y4	exercise	prob, section 83.12	open_logic
MMCMTCNNR5	statement	prop, section 41.7	open_logic
MMQZV2G8N8	statement	thm, section 3.8	open_logic
MMYM7NX99S	proof	proof, section 8.6	open_logic
Formation sequences for formulas	definition	defn, section 62.3	open_logic
MN6ETV2R8C	statement	prop, section 22.2	open_logic
Axioms for quantifiers	definition	defn, section 8.2	open_logic
MP0MRT84YH	statement	prop, section 72.7	open_logic
MP2VMCBKY7	statement	lem, section 30.10	open_logic
MP6AT8SDEJ	exercise	prob, section 29.4	open_logic
Isomorphism	definition	defn, section 79.2	open_logic
Compactness	statement	prop, section 17.5	open_logic
MQ2MGPMGV1	definition	defn, section 46.5	open_logic
Strings	definition	defn, section 19.8	open_logic
MQB001MB1K	statement	thm, section 25.8	open_logic
MQZE8FB2C4	exercise	prob, section 54.4	open_logic
MSQ98DKRWH	exercise	prob, section 17.11	open_logic
MTD5E1HX7K	exercise	prob, section 78.1	open_logic
Infinite sequences	example	ex, section 82.4	open_logic
Entailment	definition	defn, section 19.15	open_logic
MVPE6Y9VVK	definition	defn, section 76.3	open_logic
MVRFE0Q66Z	statement	lem, section 75.1	open_logic
MVT7FXAG6N	statement	prop, section 50.3	open_logic
MVZPYXWWHN	proof	proof, section 29.2	open_logic
MW6RBQGB2T	exercise	prob, section 4.1	open_logic
MWHKEDGEZE	statement	thm, section 51.10	open_logic
MWM22AAYDP	exercise	prob, section 63.1	open_logic
MWPPYFKF0P	exercise	prob, section 85.5	open_logic
MWWRYKR35W	exercise	prob, section 19.14	open_logic
MWYMG21AMJ	statement	prop, section 59.4	open_logic
MX89FPTENZ	proof	proof, section 36.4	open_logic
MY2BSP8SMF	statement	prop, section 83.6	open_logic
MY37M034QA	exercise	prob, section 50.7	open_logic
MYFGVJBR4C	statement	prop, section 8.7	open_logic
MYNPJBQDDJ	statement	lem, section 9.8	open_logic
MYXHM25YQB	definition	defn, section 52.6	open_logic
Immediate !!^{subformula}	definition	defn, section 20.2	open_logic
MZ9E5FRTCW	definition	defn, section 76.4	open_logic
MZZCDBBB31	statement	thm, section 38.13	open_logic
Covered !!{structure}	definition	defn, section 19.5	open_logic
Truth Lemma	statement	lem, section 11.1	open_logic
N0MN5YXMRF	proof	proof, section 8.10	open_logic
N13ZQ1406B	statement	prop, section 69.3	open_logic
N1BCW0DMXG	statement	prop, section 79.5	open_logic
N1FDBH3Q13	statement	prop, section 15.4	open_logic
N1FXCG227X	proof	proof, section 15.4	open_logic
N1TPDTQ24W	statement	thm, section 29.7	open_logic
Variable Assignment	definition	defn, section 67.5	open_logic
N25SA6M623	statement	lem, section 51.4	open_logic
N2D6F3D7EN	statement	cor, section 69.4	open_logic
N2MJY2R5E7	proof	proof, section 8.8	open_logic
N2V8ATCHE1	statement	prop, section 86.9	open_logic
N32DSD2PJ2	statement	prop, section 44.7	open_logic
N37JVQ02AE	definition	defn, section 54.1	open_logic
N3HR20JFE3	statement	cor, section 55.12	open_logic
N41YDXWAA3	statement	lem, section 39.3	open_logic
Theorems	definition	defn, section 15.1	open_logic
N4YM8MBY40	exercise	prob, section 5.3	open_logic
N5DZ54YC00	exercise	prob, section 15.6	open_logic
N5FGQE4SAG	definition	defn, section 86.3	open_logic
N698416NJ6	statement	prop, section 60.1	open_logic
N6N4EGYSSB	proof	proof, section 30.8	open_logic
N6NN2KE5ME	proof	proof, section 50.8	open_logic
N6TW1PJJ47	proof	proof, section 33.3	open_logic
N7AP90EHSJ	exercise	prob, section 55.2	open_logic
N7QP8ZDHBS	exercise	prob, section 38.9	open_logic
N7XKD11Y05	exercise	prob, section 58.1	open_logic
N8G9HBRBNE	statement	lem, section 56.1	open_logic
N945RCWFB4	proof	proof, section 49.1	open_logic
N967J5SNMY	statement	thm, section 65.3	open_logic
NA5RV3AHXF	proof	proof, section 70.1	open_logic
NA63TC15YQ	statement	prop, section 13.2	open_logic
NAH2CFN0BY	definition	defn, section 61.6	open_logic
NB72BH38G4	statement	prop, section 63.1	open_logic
NBD38FMY7S	definition	defn, section 71.8	open_logic
NCESV563VJ	proof	proof, section 70.2	open_logic
ND4T283191	exercise	prob, section 87.3	open_logic
in $\Z$ + Weak-Reflection	statement	thm, section 73.11	open_logic
NEA3E6NV08	proof	proof, section 39.3	open_logic
NEGNCSVASC	exercise	prob, section 42.5	open_logic
Compactness Theorem	statement	thm, section 9.9	open_logic
NFBV8BMX5A	statement	lem, section 30.3	open_logic
NFK486416G	proof	proof, section 50.8	open_logic
NFKRKZB99G	proof	proof, section 51.7	open_logic
NFWSK759VW	proof	proof, section 70.2	open_logic
NGA7TV2VFX	proof	proof, section 62.3	open_logic
NGXV501GHG	proof	proof, section 30.1	open_logic
NHKPJX9NGX	statement	prop, section 55.12	open_logic
NHVE58P1E3	proof	proof, section 63.1	open_logic
NJMB6CFPPP	statement	lem, section 55.1	open_logic
NM383SMSJD	proof	proof, section 50.2	open_logic
NM5CBG00KY	proof	proof, section 32.5	open_logic
NMNKQY0H21	statement	lem, section 30.3	open_logic
NNCW8W5MBC	proof	proof, section 8.10	open_logic
NNT5GXHAEZ	definition	defn, section 80.3	open_logic
NNVACYMQH6	proof	proof, section 65.1	open_logic
NPAX29RZEN	proof	proof, section 27.3	open_logic
Change of bound variable, $\aconvone$	definition	defn, section 38.9	open_logic
NPGTNJYN0N	exercise	prob, section 71.9	open_logic
Computation	definition	defn, section 86.3	open_logic
Tarski--Scott	definition	defn, section 71.5	open_logic
NQJ17R80MS	statement	lem, section 9.8	open_logic
NQJE1180JK	proof	proof, section 3.3	open_logic
NQNBM83FKV	statement	prop, section 19.15	open_logic
NQNJ4YYMH7	statement	lem, section 8.10	open_logic
NRC3S6N0E2	statement	thm, section 3.3	open_logic
NRDC5E0T8N	example	ex, section 19.8	open_logic
NRGGN1ZYF5	proof	proof, section 37.8	open_logic
NSBNMEKANY	statement	thm, section 29.4	open_logic
NSN8Y3XHE1	statement	prop, section 44.1	open_logic
NSSNJ22EV4	statement	prop, section 42.5	open_logic
NTJZ71N18C	statement	thm, section 29.1	open_logic
NTSF0YC5QF	proof	proof, section 22.15	open_logic
NV5V86206F	statement	lem, section 36.2	open_logic
NVF09X8F2A	example	ex, section 58.2	open_logic
NVK6X8SSNK	statement	prop, section 66.4	open_logic
Proof of Rice's theorem	proof	proof, section 3.13	open_logic
Formulas	definition	defn, section 22.1	open_logic
Satisfiability	definition	defn, section 67.6	open_logic
NY06JD1NTK	exercise	prob, section 9.11	open_logic
NY87QHSHGV	statement	cor, section 72.2	open_logic
NYHDAYGQMM	example	ex, section 82.2	open_logic
NYX4QY40JY	statement	prop, section 17.7	open_logic
NZ56NZ12XX	statement	prop, section 51.7	open_logic
NZ96S975DN	statement	prop, section 61.4	open_logic
NZXPKD7JZJ	proof	proof, section 60.4	open_logic
P0DSF052KF	proof	proof, section 50.2	open_logic
P0MRV3CDQ4	exercise	prob, section 15.11	open_logic
P0P48V6332	statement	prop, section 73.4	open_logic
P0PEK7C60C	proof	proof, section 55.8	open_logic
P0WRDGWPZA	statement	prop, section 19.1	open_logic
P1AAZET082	example	ex, section 31.2	open_logic
P1NS7QN9GM	proof	proof, section 19.15	open_logic
P26HGNCKKC	proof	proof, section 69.4	open_logic
P2SNAYW3A7	statement	prop, section 71.8	open_logic
P38JRD3414	statement	prop, section 8.5	open_logic
!!^{derivability}	definition	defn, section 31.1	open_logic
P4XC19DE3F	proof	proof, section 27.5	open_logic
P50E62ZP1V	exercise	prob, section 15.3	open_logic
P5JF786P10	proof	proof, section 83.9	open_logic
P5TFPB389J	proof	proof, section 19.6	open_logic
P62DGGWS97	statement	thm, section 87.1	open_logic
P67DC3N5NW	proof	proof, section 78.2	open_logic
P6GDF8W7A5	proof	proof, section 51.7	open_logic
P6WD4SRY95	example	ex, section 86.1	open_logic
P7DEEQ7TQT	exercise	prob, section 37.8	open_logic
P822K7W66C	statement	prop, section 69.4	open_logic
P8AKRPXH9Z	proof	proof, section 3.31	open_logic
P8CY08604S	definition	defn, section 69.5	open_logic
P8ZCBE2T0Y	example	ex, section 83.4	open_logic
P9558PB5NF	proof	proof, section 8.14	open_logic
P9QCFBK1ZZ	statement	prop, section 69.1	open_logic
PANS62YY7E	definition	defn, section 78.2	open_logic
PBHTK2VQ76	exercise	prob, section 86.1	open_logic
Saturated set	definition	defn, section 11.3	open_logic
PCYTPJ4K4E	exercise	prob, section 83.11	open_logic
PD7ABEDKSA	proof	proof, section 87.2	open_logic
PDAF3GT9WP	statement	prop, section 50.5	open_logic
PDKNVV6JR9	exercise	prob, section 83.9	open_logic
PE8GVMRD8C	statement	prop, section 38.6	open_logic
PEP9JZ63MK	example	ex, section 67.1	open_logic
PF7TY0FQ50	example	ex, section 27.5	open_logic
PFEZSS5KPK	proof	proof, section 30.14	open_logic
PFHY65HA5V	definition	defn, section 58.2	open_logic
PG3NBD4HN1	proof	proof, section 62.2	open_logic
PJB0NJND94	proof	proof, section 59.4	open_logic
PJQB1FJRNE	proof	proof, section 22.2	open_logic
PK0B24SDK6	exercise	prob, section 34.1	open_logic
PKN63A2Y2S	statement	prop, section 19.4	open_logic
PKSWEZ791X	statement	lem, section 39.3	open_logic
PKZQSCTGSK	statement	prop, section 79.1	open_logic
PM50E4789D	statement	prop, section 19.6	open_logic
PMBHYJFQFP	proof	proof, section 51.3	open_logic
PNMGJMDWR5	statement	prop, section 66.3	open_logic
PP7Y6VV3N5	example	ex, section 15.7	open_logic
PPJ7XEAZP8	definition	defn, section 44.3	open_logic
PPMRJ5N6G0	exercise	prob, section 19.4	open_logic
PPP9QB2NN9	example	ex, section 19.14	open_logic
PQCY0FHP9C	statement	prop, section 37.8	open_logic
Skolem's Paradox	example	ex, section 11.2	open_logic
PS2CWTTDJG	statement	cor, section 30.11	open_logic
PT9SGCYA0T	statement	thm, section 36.3	open_logic
PTGD2JW8DT	proof	proof, section 72.5	open_logic
PTV3JM5M16	proof	proof, section 86.10	open_logic
PVDVK256WH	example	ex, section 12.8	open_logic
!!^{derivability}	definition	defn, section 40.4	open_logic
PWAYJ50EEH	proof	proof, section 61.5	open_logic
PWGAAG6BJC	exercise	prob, section 36.3	open_logic
PX22SMQZ8B	example	ex, section 31.2	open_logic
PX3BVVBD3A	proof	proof, section 70.2	open_logic
PX3F2YG6DY	statement	prop, section 49.1	open_logic
PX9AN68ABS	definition	defn, section 49.4	open_logic
Monotonicity	statement	prop, section 15.1	open_logic
PXYQM3A4X3	proof	proof, section 3.30	open_logic
Monotonicity	statement	prop, section 22.5	open_logic
PYQKMZN6QB	example	ex, section 80.6	open_logic
PYZ1713HK8	statement	prop, section 50.2	open_logic
Variable Assignment	definition	defn, section 19.14	open_logic
Q03E897HWC	statement	prop, section 69.2	open_logic
Q0J5VREK8S	statement	prop, section 52.6	open_logic
Q0VYYZXQJ9	proof	proof, section 71.1	open_logic
Q19GHFER24	proof	proof, section 29.5	open_logic
Q27ER9RF3K	definition	defn, section 38.12	open_logic
Q2CP7YTD3D	example	ex, section 83.4	open_logic
Q330NQDE9C	proof	proof, section 8.5	open_logic
Q3CFTVE3YV	proof	proof, section 32.6	open_logic
Q43708FFM2	statement	cor, section 70.2	open_logic
Q45E8DP74W	exercise	prob, section 42.2	open_logic
Q4CBN26AMY	proof	proof, section 72.2	open_logic
Q4TZCCEDEG	statement	prop, section 72.2	open_logic
Q5DJ3B02VP	definition	defn, section 38.12	open_logic
Q5K6PJ7J00	statement	prop, section 8.10	open_logic
Q5VY17K4SG	statement	thm, section 3.10	open_logic
Q68XEETVBE	statement	prop, section 32.4	open_logic
Q6G00AEA7C	exercise	prob, section 73.4	open_logic
Q6J4R48E8Z	example	ex, section 85.3	open_logic
Q6S58ZYVM3	statement	lem, section 30.1	open_logic
Q6XRDVWM2J	statement	thm, section 58.7	open_logic
Q6YD393JXZ	exercise	prob, section 83.2	open_logic
Q73D9BBMYK	statement	prop, section 61.10	open_logic
Q74FXATMF7	statement	prop, section 50.8	open_logic
Q74PYE5EFB	statement	thm, section 27.9	open_logic
Q84SGDGKDC	example	ex, section 22.10	open_logic
Q8PJZQE2P9	definition	defn, section 28.7	open_logic
Q8TQVJS6MJ	definition	defn, section 1.12	open_logic
Q8XDF9Y7ZQ	statement	prop, section 44.3	open_logic
QA865VQQPS	definition	defn, section 30.2	open_logic
QAE3VAGKXR	statement	prop, section 4.2	open_logic
QBEEYV4H0B	definition	defn, section 32.6	open_logic
QBPZDEJ2RT	exercise	prob, section 82.5	open_logic
QCF90G76T5	proof	proof, section 4.1	open_logic
QCRM2F2HV1	statement	cor, section 19.4	open_logic
QCYC1AQ2V8	exercise	prob, section 63.1	open_logic
QDCQ7T3X8T	exercise	prob, section 69.4	open_logic
QDVSDCGJ2Q	statement	prop, section 29.8	open_logic
Sequent	definition	defn, section 17.13	open_logic
QE3VRMSGT5	exercise	prob, section 83.11	open_logic
QEWK1QQCQM	proof	proof, section 35.2	open_logic
QG0X5S94GA	exercise	prob, section 82.6	open_logic
Halting function	definition	defn, section 86.7	open_logic
Theorems	definition	defn, section 17.5	open_logic
QGBRAYSJJQ	proof	proof, section 29.7	open_logic
Lindenbaum's Lemma	statement	lem, section 11.6	open_logic
QH2G77AS34	statement	prop, section 19.15	open_logic
Consistency	definition	defn, section 22.5	open_logic
QHGMH1G6PK	proof	proof, section 72.7	open_logic
QHNN00N9CM	statement	prop, section 60.6	open_logic
QHX3P5WKAG	exercise	prob, section 9.11	open_logic
QJ1AYE9G06	statement	thm, section 83.9	open_logic
QK0G01N5E1	statement	prop, section 15.3	open_logic
QKZNP7A12X	proof	proof, section 29.11	open_logic
QM8XYHKDRX	proof	proof, section 19.8	open_logic
QMAD2QPBZA	proof	proof, section 69.3	open_logic
QNQVS8JVHM	statement	prop, section 49.4	open_logic
QNSYF5A3SY	statement	thm, section 8.9	open_logic
QNX5ZMH4NQ	statement	cor, section 15.11	open_logic
QNYKMR8TMR	proof	proof, section 66.2	open_logic
QPA660W7YR	statement	prop, section 51.4	open_logic
QPGXY9Z1GP	proof	proof, section 50.2	open_logic
QQBW18HZ7E	definition	defn, section 1.4	open_logic
Church--Rosser property, CR	definition	defn, section 36.1	open_logic
QR4JV7JE8Y	statement	prop, section 8.8	open_logic
QR6DRCWHKJ	definition	defn, section 22.15	open_logic
QRC48HNED9	statement	prop, section 49.1	open_logic
QREHK015E2	proof	proof, section 75.1	open_logic
QS6VRSQJBG	statement	prop, section 3.11	open_logic
in \emph{Grundgesetze}.	statement	lem, section 75.5	open_logic
QSM622MW3R	exercise	prob, section 62.7	open_logic
QTB143K7AK	proof	proof, section 44.5	open_logic
QV2YNBH4B1	proof	proof, section 74.5	open_logic
QVPGNFA63Z	statement	cor, section 79.7	open_logic
QWCEPHM9GY	example	ex, section 19.8	open_logic
QX975A6JG8	exercise	prob, section 50.2	open_logic
QXHW9CTHQ2	statement	thm, section 29.2	open_logic
Transitivity	statement	prop, section 15.1	open_logic
QYG8J9D2D6	statement	prop, section 44.11	open_logic
QZ3Q4FGRDB	exercise	prob, section 80.6	open_logic
QZFHJ9T0GZ	proof	proof, section 8.4	open_logic
!!^{subformula}	definition	defn, section 20.2	open_logic
QZPBGRV25Y	exercise	prob, section 11.1	open_logic
R0KBJM0NSW	exercise	prob, section 38.9	open_logic
R0YQXEFYA2	proof	proof, section 8.6	open_logic
R1GA9D5949	exercise	prob, section 6.2	open_logic
Parallel $\beta\eta$-reduction, $\beredpar$	definition	defn, section 36.2	open_logic
Rule of inference	definition	defn, section 8.13	open_logic
R2B0FNJBCW	exercise	prob, section 4.2	open_logic
R2SGDPRCMM	proof	proof, section 35.1	open_logic
R391QNGMHX	statement	prop, section 76.3	open_logic
Rules for quantifiers	definition	defn, section 8.2	open_logic
R40XEQKP1W	exercise	prob, section 56.1	open_logic
R44JT8A3A9	definition	defn, section 1.7	open_logic
R4760ZZG6X	statement	lem, section 29.5	open_logic
R49M9RTG5C	statement	prop, section 8.8	open_logic
R4H61QJZCD	exercise	prob, section 83.5	open_logic
R4MA1PYP1B	exercise	prob, section 44.3	open_logic
R50Q16YJS9	proof	proof, section 61.9	open_logic
R514S0Y6QZ	example	ex, section 19.8	open_logic
R54GYGGTTN	definition	defn, section 74.2	open_logic
R57SGYVXRZ	proof	proof, section 61.9	open_logic
R59KM5E42K	example	ex, section 83.2	open_logic
R5BXS9V88C	proof	proof, section 40.2	open_logic
R5CPVSCQY0	statement	prop, section 44.9.6	open_logic
R5KTV66G3A	statement	thm, section 28.6	open_logic
R623ZKNRRW	statement	lem, section 72.5	open_logic
R66GKE7BKR	proof	proof, section 55.2	open_logic
in $\Zminus + \text{Countable Choice}$	statement	thm, section 71.1	open_logic
R6ME6K4Y37	proof	proof, section 72.2	open_logic
R7RY2BK8C3	exercise	prob, section 46.6	open_logic
in $\Zminus$	statement	lem, section 71.1	open_logic
R8KM63CQAT	statement	thm, section 52.3	open_logic
R8X2Y2625K	example	ex, section 80.4	open_logic
Extensionality	statement	prop, section 19.6	open_logic
RA1KCR6VMG	example	ex, section 86.1	open_logic
RA65EAC3ZM	exercise	probtag, section 55.2	open_logic
RAD6JWY0K0	statement	lem, section 28.6	open_logic
RARP73T50K	definition	defn, section 45.4	open_logic
RAWN1ZA2SD	exercise	prob, section 9.8	open_logic
RAYZHGK2YG	statement	prop, section 74.4	open_logic
RBGK1RT3F0	proof	proof, section 82.5	open_logic
RBT2TD6Q8R	proof	proof, section 27.7	open_logic
RC1W8WWTVF	statement	lem, section 71.11	open_logic
RC8WXGN9Q9	proof	proof, section 59.5	open_logic
RCJVM9Z7M2	statement	lem, section 61.9	open_logic
Scope	definition	defn, section 38.14	open_logic
RDVNPSW4HG	statement	thm, section 83.8	open_logic
REDAA4S3AV	statement	prop, section 8.14	open_logic
REPRQ4MD3D	proof	proof, section 73.7	open_logic
REYPNCWN5Z	exercise	prob, section 78.2	open_logic
RFBBPPP9EA	statement	cor, section 52.5	open_logic
RG79EXPZAF	exercise	prob, section 83.12	open_logic
RH7XT6Y8FN	example	ex, section 67.5	open_logic
RHH2HV056A	proof	proof, section 22.5	open_logic
RHQQS64SNK	exercise	prob, section 56.2	open_logic
Ordered pair	definition	defn, section 82.5	open_logic
RJ3PQ7PDXP	definition	defn, section 69.4	open_logic
RJEXJ7HJ9H	proof	proof, section 72.5	open_logic
RJF28RHBG6	definition	defn, section 46.8	open_logic
RJJWQA91EM	example	ex, section 15.6	open_logic
RK7JAJYWHT	proof	proof, section 87.3	open_logic
Soundness	statement	thm, section 22.15	open_logic
RM2XN0BR4S	proof	proof, section 37.8	open_logic
RMDRQMGGS2	statement	prop, section 66.6	open_logic
RMJJ5SK3EV	example	ex, section 27.7	open_logic
RPY0TSHK4G	example	ex, section 78.9	open_logic
RQ4XPYT7FE	definition	defn, section 58.2	open_logic
RQ9HHGAZ47	statement	lem, section 29.3	open_logic
RQG92HEQ7R	exercise	prob, section 83.2	open_logic
Schr\"oder-Bernstein	statement	thm, section 83.14	open_logic
RQT6YD5YVM	exercise	prob, section 3.31	open_logic
RQWZ26VWJY	statement	thm, section 11.2	open_logic
RQYAH7S8VN	definition	defn, section 34.6	open_logic
Successors	definition	defn, section 82.2	open_logic
RRQATMYJ14	definition	defn, section 37.2	open_logic
RRYWPNVP9X	proof	proof, section 73.2	open_logic
RSN7QRR8WB	proof	proof, section 54.7	open_logic
RSVQDW68Y1	definition	defn, section 47.2	open_logic
RSWZ7XGJBA	statement	cor, section 87.2	open_logic
RT0WKM65DK	statement	prop, section 73.7	open_logic
RTWHD0WC28	proof	proof, section 69.5	open_logic
RTXXS0PQQQ	definition	defn, section 85.5	open_logic
Soundness	statement	thm, section 55.12	open_logic
Soundness	statement	thm, section 34.6	open_logic
RW66D2DNP9	statement	lem, section 51.4	open_logic
RW691PZ6VA	statement	lem, section 60.4	open_logic
RX1Z3586M7	exercise	prob, section 42.2	open_logic
RXZA5KM9YX	exercise	prob, section 22.2	open_logic
RYQ35RH2KH	proof	proof, section 62.2	open_logic
Syntactic identity	definition	defn, section 62.4	open_logic
RZ8M97F78Y	statement	prop, section 62.7	open_logic
S07XM6BRNT	exercise	prob, section 83.13	open_logic
S0Q4Y6941Z	exercise	prob, section 15.11	open_logic
S0TSDYCVJF	statement	prop, section 29.8	open_logic
S0ZH111SSC	proof	proof, section 46.4	open_logic
S269CWFN1D	example	ex, section 82.3	open_logic
$\beta\eta$-reduction, $\bered$	definition	defn, section 38.13	open_logic
S3BXA5V5Y5	exercise	prob, section 62.6	open_logic
S3DVY7A19A	proof	proof, section 30.3	open_logic
S3M2ZJS297	exercise	prob, section 28.2	open_logic
S3RZ01MV3F	exercise	prob, section 55.3	open_logic
S493NEXH2B	example	ex, section 78.9	open_logic
S4HT2XRPMV	statement	prop, section 50.9	open_logic
S52R2FJP7G	definition	defn, section 42.6	open_logic
S5F2NNH3RH	proof	proof, section 85.3	open_logic
S5ZWJVDWKG	statement	lem, section 11.1	open_logic
S69M5KX9GZ	proof	proof, section 27.6	open_logic
S6YHSRAJJ3	statement	thm, section 83.9	open_logic
S7AMEFYDJ4	proof	proof, section 61.6	open_logic
S7SDGS371X	example	ex, section 54.8	open_logic
S81MJTN1NS	statement	prop, section 54.4	open_logic
S89288BYG4	proof	proof, section 86.10	open_logic
S8BCRYE765	statement	prop, section 11.3	open_logic
S8X7T89S99	proof	proof, section 71.6	open_logic
S8Y3A3N5Y1	proof	proof, section 11.3	open_logic
Church--Turing thesis	definition	defn, section 85.2	open_logic
S95BA5VD74	statement	lem, section 34.2	open_logic
S9EEK6M202	proof	proof, section 50.9	open_logic
SA429DTKZK	proof	proof, section 71.6	open_logic
SAWCM284W6	statement	cor, section 3.13	open_logic
SCDMXWBJ4C	exercise	prob, section 53.7	open_logic
SCKJY0RBFH	statement	thm, section 3.9	open_logic
SCXGETPZ2G	proof	proof, section 83.5	open_logic
SD248QN66M	exercise	prob, section 86.10	open_logic
SD3XK0FFTM	example	ex, section 15.7	open_logic
SD4PMGREVK	statement	cor, section 55.8	open_logic
SD6GBQRCHQ	definition	defn, section 48.1	open_logic
SDAYDBMDTY	statement	lem, section 72.1	open_logic
Reflection Schema	statement	thm, section 73.10	open_logic
SDM0PMDGK5	exercise	prob, section 87.3	open_logic
SDSQ45F95R	example	ex, section 80.3	open_logic
SDY7NJQHY2	statement	prop, section 76.7	open_logic
SED9C3BJMG	statement	prop, section 50.7	open_logic
SEQ1H6Y3F8	proof	proof, section 55.12	open_logic
SF26J1GJ99	proof	proof, section 75.1	open_logic
SFEAXXREPM	exercise	prob, section 42.4	open_logic
SFRZ55QA9M	exercise	prob, section 27.8	open_logic
SFTD8EADZY	definition	defn, section 73.1	open_logic
SG4RGTN61F	exercise	prob, section 86.7	open_logic
SG7QR37GXB	exercise	prob, section 15.1	open_logic
SGETF0NEXN	definition	defn, section 52.7	open_logic
SGF8G5C2Q8	example	ex, section 82.5	open_logic
SGYKH1WT2J	definition	defn, section 46.5	open_logic
Compactness	statement	thm, section 9.8	open_logic
SH3X6EF9S5	proof	proof, section 55.1	open_logic
SH9C0BKHGT	example	ex, section 61.12	open_logic
SHBM6J9KBS	exercise	prob, section 50.13	open_logic
SHGQHTP12N	example	ex, section 19.7	open_logic
SJ84Q3N2WF	statement	lem, section 38.3	open_logic
SJGVCWW3CQ	exercise	prob, section 61.9	open_logic
!!^{tableau}	definition	defn, section 22.3	open_logic
SJQ98NSE2S	exercise	prob, section 78.8	open_logic
SJQV0D4AQ3	definition	defn, section 53.1	open_logic
SM9GDBS0C7	statement	prop, section 20.2	open_logic
SN1ED3A81D	proof	proof, section 37.9	open_logic
SNG112VTG0	proof	proof, section 33.6	open_logic
SPP915CE76	exercise	prob, section 83.12	open_logic
$x$-Variant	definition	defn, section 67.5	open_logic
SRAAJPTFXX	proof	proof, section 3.16	open_logic
SRWV3JK91Q	proof	proof, section 38.9	open_logic
SRXSQC1D87	statement	prop, section 39.4	open_logic
Modus ponens	definition	defn, section 8.1	open_logic
SSJ072AQS1	definition	defn, section 71.8	open_logic
ST8K1JVRVP	proof	proof, section 44.9.7	open_logic
STHE0EK2FD	statement	thm, section 31.3	open_logic
SVC2447FTT	proof	proof, section 86.7	open_logic
SVENZMAJ6W	exercise	prob, section 32.1.6	open_logic
SVKH91K23R	example	ex, section 78.9	open_logic
SWCG4YD9E4	proof	proof, section 40.4	open_logic
SWFG0SYEHW	statement	prop, section 44.5	open_logic
SWJ2RZKSC2	proof	proof, section 55.8	open_logic
SWJFNHQG3W	proof	proof, section 66.1	open_logic
SXPKYEF3F6	proof	proof, section 72.2	open_logic
Proof of Schr\"oder-Bernstein	proof	proof, section 79.5	open_logic
SYGCXZMD4A	proof	proof, section 46.5	open_logic
SZ5HHEJ6JJ	exercise	prob, section 9.8	open_logic
SZ854CPR00	statement	prop, section 15.5	open_logic
T06EATFW17	statement	prop, section 27.2	open_logic
T13M0KAWQY	definition	defn, section 38.4	open_logic
T1F1B39C1J	exercise	prob, section 38.15	open_logic
T26RSRBM3A	statement	thm, section 69.4	open_logic
T26STA9F8M	exercise	prob, section 86.10	open_logic
T2JY1BA7HV	definition	defn, section 86.9	open_logic
T2QY9V3EGT	proof	proof, section 42.4	open_logic
T37F4KZMGW	exercise	prob, section 3.11	open_logic
!!^{bijection}	definition	defn, section 78.10	open_logic
T3QPCHKXQ7	exercise	prob, section 33.5	open_logic
T3WJHS9H5M	definition	defn, section 75.1	open_logic
T3X0W26QEK	definition	defn, section 74.5	open_logic
T4HK07B7ST	definition	defn, section 50.9	open_logic
T4PCNY9GMT	statement	prop, section 49.1	open_logic
Semantic Deduction Theorem	statement	thm, section 62.7	open_logic
T6M1M0YAPY	definition	defn, section 82.2	open_logic
T7CD4FP03N	statement	prop, section 49.4	open_logic
T7KFQ2CZ7R	exercise	prob, section 19.14	open_logic
T84JGJJ2CQ	exercise	prob, section 45.1	open_logic
T877BPVZN1	proof	proof, section 15.11	open_logic
T9B2826NHM	exercise	prob, section 38.9	open_logic
T9VEK2VDDP	definition	defn, section 51.9	open_logic
TAKN4S4XGY	statement	thm, section 38.15	open_logic
TAXWDBTA8P	exercise	prob, section 15.6	open_logic
TB21M5RQ13	statement	lem, section 56.1	open_logic
TBEQT874RD	statement	lem, section 27.9	open_logic
TBX1E04SXC	definition	defn, section 1.12	open_logic
TC058KG5Q2	proof	proof, section 8.4	open_logic
TC3NTAYRK9	example	ex, section 22.11	open_logic
TCABME6P5X	definition	defn, section 34.6	open_logic
TCBVX352KX	exercise	prob, section 40.4	open_logic
TDQZSPJF75	definition	defn, section 71.9	open_logic
TDRYDB8H41	proof	proof, section 70.2	open_logic
TDWMC8QJRZ	statement	lem, section 30.5	open_logic
TDWP1HJ4KC	definition	defn, section 79.6	open_logic
TE4BBSX06M	statement	prop, section 61.6	open_logic
TE82A44FRB	statement	lem, section 72.2	open_logic
TEKMYAX5PE	exercise	prob, section 55.12	open_logic
TF112SKF5W	statement	lem, section 75.1	open_logic
TF2TQX7012	statement	lem, section 73.11	open_logic
Unsolvability of the Halting Problem	statement	thm, section 86.7	open_logic
TGC87VG48X	proof	proof, section 50.15	open_logic
TGEKQV57FK	statement	prop, section 22.8	open_logic
TGSQGGYBGQ	statement	prop, section 27.3	open_logic
TGYBNFV05R	statement	cor, section 51.7	open_logic
TGZTW1RDRS	statement	prop, section 27.1	open_logic
Unique Readability	statement	prop, section 22.2	open_logic
THC9Z0FW3T	statement	lem, section 30.8	open_logic
!!^{value} of closed terms	definition	defn, section 19.5	open_logic
TKEKG85A8W	statement	prop, section 51.9	open_logic
TKXSRC5Y6K	proof	proof, section 44.8	open_logic
TKZ10GWHKQ	statement	prop, section 22.14	open_logic
TM68B4M789	example	ex, section 80.3	open_logic
TMBQ6BHMD2	proof	proof, section 38.15	open_logic
TMP2MX4VQG	statement	lem, section 71.6	open_logic
TMVKQE91RC	proof	proof, section 56.1	open_logic
TMVTHKKRAX	definition	defn, section 61.6	open_logic
TNA4QG76N0	exercise	prob, section 54.7	open_logic
TNESSVXKQP	statement	prop, section 37.8	open_logic
TNN0ERJBG6	statement	lem, section 11.4	open_logic
TPVBTF3MNA	example	ex, section 80.4	open_logic
TQMKNC3DFG	proof	proof, section 17.8	open_logic
TQTNXQJGQM	proof	proof, section 73.4	open_logic
TRE680VP3E	proof	proof, section 83.9	open_logic
Satisfiability	definition	defn, section 19.15	open_logic
TSXBWYGYR5	definition	defn, section 42.6	open_logic
TTE3KPWT8J	statement	prop, section 8.10	open_logic
TV2D0D3DRE	statement	prop, section 50.6	open_logic
parallel $\beta$-reduction, $\bredpar$	definition	defn, section 36.3	open_logic
TVWEDP1JKY	proof	proof, section 3.9	open_logic
TW37HD4B4Q	proof	proof, section 33.4	open_logic
Model of a set	definition	defn, section 12.8	open_logic
Reflexivity	statement	prop, section 40.4	open_logic
TWPCRQX5VQ	proof	proof, section 38.9	open_logic
TWQKKWBBQT	definition	defn, section 46.9	open_logic
TWSZCGNY0C	proof	proof, section 80.4	open_logic
TX1EKBM9EY	exercise	prob, section 86.6	open_logic
TXDGJE7KVS	proof	proof, section 73.11	open_logic
TXYBP57WH7	statement	thm, section 30.14	open_logic
Bound Variables	definition	defn, section 19.9	open_logic
TZDCGP80KR	exercise	prob, section 19.6	open_logic
V0ATTW7RJZ	definition	defn, section 51.4	open_logic
V0CDFJ4VTW	exercise	prob, section 83.11	open_logic
V142XDMA2Z	exercise	prob, section 1.7	open_logic
V15WV1GGFV	statement	thm, section 19.8	open_logic
Intersection	definition	defn, section 83.2	open_logic
V1RFQ42P7D	proof	proof, section 47.2	open_logic
V2DDDFXX7H	definition	defn, section 72.5	open_logic
V2P6MH7SR2	definition	defn, section 46.5	open_logic
V2YWH93868	example	ex, section 13.3	open_logic
V31XQN4KMZ	statement	prop, section 29.3	open_logic
V3HC9WZZEF	statement	prop, section 3.30	open_logic
V43Y2SHCZP	proof	proof, section 55.3	open_logic
V4BV5XWN9D	proof	proof, section 70.2	open_logic
Validity	definition	defn, section 19.15	open_logic
V4JQKWRHE8	statement	prop, section 58.3	open_logic
V4VB5PHCCW	proof	proof, section 50.16	open_logic
V5159FMDPS	proof	proof, section 17.5	open_logic
V53T3YJM31	exercise	prob, section 50.3	open_logic
V5G81NAGF2	example	ex, section 79.3	open_logic
V7CDBNSMYE	statement	prop, section 3.31	open_logic
Reflexivity	statement	prop, section 8.6	open_logic
V807K2QX9K	statement	prop, section 74.2	open_logic
V94RMV8QZP	statement	prop, section 17.7	open_logic
VABE7167PC	definition	defn, section 83.1	open_logic
VAJYNV89Y0	proof	proof, section 36.3	open_logic
VBF88Z2TAQ	statement	prop, section 8.7	open_logic
VBFTFS7DTZ	definition	defn, section 78.2	open_logic
VBMNAJMZKB	statement	prop, section 45.4	open_logic
VBTGGDHAQF	statement	thm, section 3.22	open_logic
VCCFY7MAJT	proof	proof, section 71.8	open_logic
VCRHH1R13Z	statement	lem, section 71.8	open_logic
VCTYAFJD1K	statement	thm, section 79.6	open_logic
VDFZMTDZ03	exercise	prob, section 53.3	open_logic
Proof of \olref{prop:rep-add}	proof	proof, section 29.3	open_logic
VDK5B1B90T	statement	prop, section 66.6	open_logic
VDQNQ52HN4	proof	proof, section 30.1	open_logic
VDTV3EH89V	proof	proof, section 46.3	open_logic
VERZQ5ZB7Z	statement	prop, section 58.1	open_logic
VF22HVTS16	statement	lem, section 30.3	open_logic
VG2H9R8E2R	proof	proof, section 11.4	open_logic
VGAE5AH3A9	proof	proof, section 33.5	open_logic
VHQV17J52Q	proof	proof, section 61.6	open_logic
VHYAKW59GT	proof	proof, section 54.7	open_logic
Proof: completed.	proof	proof, section 25.8	open_logic
VJY94TH5BH	statement	prop, section 15.4	open_logic
VK1RQBRCNT	definition	defn, section 39.1	open_logic
VKBXYG96X3	exercise	prob, section 86.7	open_logic
VKTAP66ZNE	exercise	prob, section 86.3	open_logic
VM8Q0WGS3J	statement	cor, section 52.5	open_logic
VMA8SHK7EB	proof	proof, section 65.3	open_logic
VNF5A88R37	proof	proof, section 53.4	open_logic
VNWZCY3D3D	proof	proof, section 27.8	open_logic
VP2V9M4TAR	exercise	probtag, section 8.10	open_logic
VPDHH45954	definition	defn, section 72.6	open_logic
VPGDZEK9AM	example	ex, section 22.10	open_logic
VPTEGEW5RJ	exercise	prob, section 86.3	open_logic
VPYH56508V	proof	proof, section 50.6	open_logic
VQ49BW1X64	statement	prop, section 4.1	open_logic
VQDGMWFYPT	exercise	prob, section 19.8	open_logic
VQDVB3ZS44	exercise	prob, section 12.9	open_logic
VQXW7M09AW	proof	proof, section 74.4	open_logic
Craig's Interpolation Theorem	statement	thm, section 57.1	open_logic
VRDHX46WJT	definition	defn, section 57.4	open_logic
VS5K0VWC75	exercise	prob, section 8.14	open_logic
Axioms for !!{identity}	definition	defn, section 8.5	open_logic
VSF1C8ZJF2	statement	prop, section 15.3	open_logic
VSH8AHQ0GG	exercise	prob, section 22.1	open_logic
Second-order Terms	definition	defn, section 68.1	open_logic
VSMP4FAZXC	exercise	prob, section 86.3	open_logic
VSPZYWSKZ6	exercise	prob, section 11.1	open_logic
VSZNRVVWW4	exercise	prob, section 8.5	open_logic
VTEVWPFZZD	definition	defn, section 47.3	open_logic
VV8JR13K4S	proof	proof, section 29.3	open_logic
VVBB2208TA	definition	defn, section 32.6	open_logic
Induction on $\Nat$	definition	defn, section 79.4	open_logic
VVVG5MT0ZN	statement	prop, section 79.1	open_logic
VW2MCVCEGV	exercise	prob, section 38.15	open_logic
VW3QF2M6QJ	statement	prop, section 32.1.6	open_logic
VWFRG23KC3	proof	proof, section 17.5	open_logic
VWRTC9191M	proof	proof, section 8.6	open_logic
VWX0JW4306	exercise	prob, section 62.2	open_logic
VX7C932KH3	statement	thm, section 30.2	open_logic
VXHB8F875Y	statement	prop, section 55.8	open_logic
VXHGCGAVQK	exercise	prob, section 8.4	open_logic
VXJ2XKY791	proof	proof, section 27.8	open_logic
Maximally consistent set	definition	defn, section 11.7	open_logic
!!^{value} of Terms	definition	defn, section 19.14	open_logic
VY47PKGQ4W	statement	prop, section 61.11	open_logic
VZ3NVK0V6Y	proof	proof, section 2.5	open_logic
VZF3W6YKKK	exercise	prob, section 55.8	open_logic
VZSTXWDZJ8	proof	proof, section 49.1	open_logic
W0JS7WT45W	proof	proof, section 71.11	open_logic
W0N333NJ1H	exercise	prob, section 83.11	open_logic
W14GC0CQNW	definition	defn, section 79.4	open_logic
W1KQZQJY63	definition	defn, section 55.12	open_logic
W2TPTMBA2D	definition	defn, section 3.1	open_logic
W3HGXN6H20	proof	proof, section 36.2	open_logic
W3NM409VEM	statement	prop, section 15.4	open_logic
W3YFXXN3DR	proof	proof, section 86.10	open_logic
Transitivity	definition	defn, section 82.1	open_logic
W4HY84P31W	exercise	prob, section 82.5	open_logic
W4SP0R3FRW	proof	proof, section 22.7	open_logic
W577TVR8H1	statement	cor, section 30.7	open_logic
W57TD3YJM5	proof	proof, section 36.3	open_logic
Union	statement	axiom, section 76.10	open_logic
\usetoken{S}{value} of a Term	definition	defn, section 67.5	open_logic
Absorption	statement	prop, section 82.6	open_logic
W7145DGJSX	statement	prop, section 8.9	open_logic
W7ZAZD930P	proof	proof, section 50.6	open_logic
working in $\ZFminus + \text{Regularity}$	statement	prop, section 74.4	open_logic
W9EF0PAWM4	definition	defn, section 29.4	open_logic
W9J36ZTZV0	proof	proof, section 38.6	open_logic
WA6CRKEN48	proof	proof, section 38.1	open_logic
WA7E9JWAB4	definition	defn, section 11.4	open_logic
WABQHPVTTH	statement	prop, section 55.8	open_logic
WAPHYCCKJ6	exercise	prob, section 12.9	open_logic
WAVTARH0D3	exercise	prob, section 61.9	open_logic
WBK6F604PT	definition	defn, section 40.2	open_logic
WBY3AZFSGH	statement	lem, section 60.4	open_logic
WCKK0FF2BW	proof	proof, section 30.4	open_logic
WD0ZK7RP22	exercise	prob, section 83.12	open_logic
Monotonicity	statement	prop, section 8.6	open_logic
WE8GQHG91D	statement	prop, section 79.1	open_logic
WEVH9YDPHE	statement	thm, section 9.3	open_logic
WFXQ0FWMZB	proof	proof, section 70.2	open_logic
WFYBKGW27G	proof	proof, section 79.3	open_logic
WHNDGXZQVK	proof	proof, section 30.5	open_logic
WJ1HF49N1Q	proof	proof, section 37.5	open_logic
WJ77KDCF05	proof	proof, section 74.5	open_logic
WJQHJZ3B8G	proof	proof, section 39.3	open_logic
WJSNSY2492	statement	prop, section 67.2	open_logic
WKD48GWB1G	statement	prop, section 3.31	open_logic
WKYRNA91R6	exercise	prob, section 56.2	open_logic
WMH64Y4X2V	proof	proof, section 69.2	open_logic
WMK6FWP4QC	statement	prop, section 17.9	open_logic
WMX3B7NPDX	exercise	prob, section 85.1	open_logic
WN93A0FF9A	definition	defn, section 47.3	open_logic
WNCTGVGHP5	proof	proof, section 27.1	open_logic
WNQRE2AXQD	statement	cor, section 30.4	open_logic
WPHXG4THWD	example	ex, section 19.7	open_logic
WPTWJ4ACS4	statement	prop, section 79.1	open_logic
WPX7TYH6AZ	exercise	prob, section 29.3	open_logic
WQ3PA685PR	definition	defn, section 6.1	open_logic
WQFNBK8X8Q	proof	proof, section 49.4	open_logic
WQWACQ74M3	statement	prop, section 55.1	open_logic
WR7E8XT3P1	statement	prop, section 8.6	open_logic
WRKXBTPEJV	definition	defn, section 50.7	open_logic
WRZX5FVE85	proof	proof, section 55.8	open_logic
WSBTQYWM9J	definition	defn, section 50.4	open_logic
WTJBPTWJ51	proof	proof, section 27.7	open_logic
WTRPMX1PFA	statement	prop, section 61.5	open_logic
WTX2225X6Q	definition	defn, section 1.10	open_logic
WV9DAZK5ZF	statement	thm, section 28.4	open_logic
WWX4DN2MMW	exercise	prob, section 83.5	open_logic
WWZJHF9ZB1	statement	prop, section 50.2	open_logic
WX34XXNFVQ	definition	defn, section 2.6	open_logic
WXAF983M2F	definition	defn, section 52.4	open_logic
WXX530GPZE	exercise	prob, section 29.2	open_logic
WYK44492SB	proof	proof, section 4.1	open_logic
WYRFCRYS5S	proof	proof, section 72.1	open_logic
Beth Definability Theorem	statement	lem, section 57.1	open_logic
Banach--Tarski Paradox (in $\ZFC$)	statement	thm, section 70.6	open_logic
WZE6HE9T7V	proof	proof, section 22.8	open_logic
WZX9GJPSK4	definition	defn, section 71.7	open_logic
WZXEDBNTXT	proof	proof, section 72.2	open_logic
WZYDV3PTQE	exercise	prob, section 83.5	open_logic
X085DH063S	definition	defn, section 74.1	open_logic
X16CCSDPCK	proof	proof, section 69.5	open_logic
X1C0W1E4WS	proof	proof, section 66.2	open_logic
Function	definition	defn, section 78.9	open_logic
X23QF9RPPB	proof	proof, section 66.1	open_logic
X270VP6ACT	statement	lem, section 27.9	open_logic
X2FKTEE2XP	proof	proof, section 51.4	open_logic
X2MHPS03W7	proof	proof, section 62.3	open_logic
X2PET93K1F	statement	prop, section 22.9	open_logic
X3ECTFQVFE	statement	prop, section 69.5	open_logic
X3ER0WTY0Z	statement	cor, section 30.8	open_logic
X3GGP9C24S	example	ex, section 38.9	open_logic
Tennenbaum's Theorem	statement	thm, section 48.2	open_logic
X4D7NAJWM1	statement	thm, section 11.2	open_logic
X4HMHZR32G	proof	proof, section 22.15	open_logic
X4TA2XAM2N	definition	defn, section 32.5	open_logic
X5CHCW53DW	proof	proof, section 36.2	open_logic
X5YRAXTEJJ	proof	proof, section 74.4	open_logic
X6C9J5QZ4Y	exercise	prob, section 74.4	open_logic
X6MC0BTV55	statement	lem, section 28.6	open_logic
X6VMYQR8G6	proof	proof, section 8.10	open_logic
Directed graph	definition	defn, section 80.2	open_logic
X7K9PC0K8J	exercise	prob, section 71.4	open_logic
Proof Sketch	proof	proof, section 3.10	open_logic
X8T0YKMED7	proof	proof, section 69.5	open_logic
X8T827EWMM	statement	prop, section 8.7	open_logic
X9KXN7FDKM	example	ex, section 15.7	open_logic
XA01RA712C	proof	proof, section 72.5	open_logic
XA114PF4ND	exercise	prob, section 46.2	open_logic
XA9YW3BDWK	statement	thm, section 73.7	open_logic
Compatibility of relation	definition	defn, section 38.9	open_logic
XBD7S1CPQ8	proof	proof, section 29.8	open_logic
XBZSQ2J0TQ	proof	proof, section 51.4	open_logic
XCKSS15MMY	example	ex, section 22.3	open_logic
XDFHJP9M32	proof	proof, section 49.1	open_logic
XEC3GMK7T4	statement	prop, section 69.5	open_logic
XF3WW7Y194	exercise	prob, section 53.3	open_logic
XFKSBKH1WG	definition	defn, section 49.3	open_logic
XGP8AD7DG3	proof	proof, section 37.5	open_logic
XGP9Z460YK	statement	prop, section 62.6	open_logic
XGWJVPD1Y5	statement	thm, section 2.6	open_logic
XH14EQ0YY0	example	ex, section 6.2	open_logic
XJ7C4XGMHW	example	ex, section 82.5	open_logic
XJTK8528EE	exercise	prob, section 79.1	open_logic
Minimal formation sequences	definition	defn, section 19.8	open_logic
XKR0T517E2	statement	prop, section 49.3	open_logic
XKX7V2H3R0	example	ex, section 83.5	open_logic
Terms	definition	defn, section 39.2	open_logic
XN63Q6648C	definition	defn, section 47.3	open_logic
!!^{derivability}	definition	defn, section 8.13	open_logic
XNMR8GGWWS	definition	defn, section 54.4	open_logic
XNV2FKEV39	exercise	prob, section 83.13	open_logic
XNVECPNN5K	statement	thm, section 66.1	open_logic
Theorems	definition	defn, section 22.5	open_logic
XPXNM2JQQ9	exercise	prob, section 61.10	open_logic
XQ0BZA49SP	statement	prop, section 3.18	open_logic
XQ7B6YSHZ8	definition	defn, section 46.9	open_logic
XQC8GD30QB	exercise	prob, section 62.7	open_logic
XR10QE7RSN	proof	proof, section 19.2	open_logic
XRKCSJNP0M	example	ex, section 55.9	open_logic
XRREGPS1Y6	proof	proof, section 75.7	open_logic
XRT4N4WKHP	definition	defn, section 22.13	open_logic
XRYXF3S0Y2	proof	proof, section 57.1	open_logic
!!^{derivability}	definition	defn, section 8.6	open_logic
!!^{derivability}	definition	defn, section 8.13	open_logic
XSY58BB36A	statement	cor, section 2.5	open_logic
XTE2Q3SS47	exercise	prob, section 83.4	open_logic
Soundness	statement	thm, section 19.2	open_logic
XV5FHZ3N1J	proof	proof, section 73.1	open_logic
!!^{valuation}s	definition	defn, section 42.1	open_logic
XVT35F2RKP	exercise	prob, section 55.9	open_logic
XVZ2HDDHDM	proof	proof, section 3.20	open_logic
XXHF5EE1TC	exercise	prob, section 15.7	open_logic
XXNDRC29DC	statement	prop, section 11.7	open_logic
Simple Recursion	statement	thm, section 74.5	open_logic
XYRQC4KTKV	proof	proof, section 34.2	open_logic
XYVK755FR0	proof	proof, section 22.15	open_logic
XYY6WRKS1H	definition	defn, section 28.7	open_logic
XZFX03T843	exercise	prob, section 83.11	open_logic
XZQ8B3M01B	statement	prop, section 69.2	open_logic
XZW7X4ZWH9	proof	proof, section 73.7	open_logic
Y0MXSWQ7XX	statement	prop, section 66.4	open_logic
Y212CTP0NK	exercise	prob, section 45.4	open_logic
Y2CE032WKH	exercise	prob, section 42.6	open_logic
Y2EB084QQ4	statement	thm, section 78.1	open_logic
Y2PRXQDQ2N	proof	proof, section 2.6	open_logic
Sequent	definition	defn, section 40.6	open_logic
Y2VK786TW2	exercise	prob, section 15.1	open_logic
Y3SE2S711H	exercise	prob, section 83.13	open_logic
Y3YKF03VHE	statement	cor, section 74.4	open_logic
Y4DZKMPGP1	statement	cor, section 66.1	open_logic
Y4EP5MARD9	statement	prop, section 51.9	open_logic
Y4WQAEHBC7	statement	lem, section 71.6	open_logic
Y4XP7KER2N	exercise	prob, section 72.2	open_logic
Y5HVMFBK6K	proof	proof, section 50.7	open_logic
Y5RJ2TC7W5	exercise	prob, section 78.8	open_logic
Y5W4FQ9DWM	statement	thm, section 8.10	open_logic
Y6AEQ3A9RV	definition	defn, section 11.4	open_logic
Y6EQ7ATH1A	exercise	prob, section 9.10	open_logic
Y7D2YG2WKC	definition	defn, section 11.10	open_logic
Powersets	statement	axiom, section 76.7	open_logic
Y86D8V7GHP	statement	prop, section 66.4	open_logic
Y9QW5GP62Y	statement	thm, section 62.3	open_logic
Y9WQ5GXSRB	statement	thm, section 2.1	open_logic
YA3YVR0Y8R	exercise	prob, section 56.2	open_logic
YA8C8SVDYK	exercise	prob, section 83.11	open_logic
YADMXHCVZD	exercise	prob, section 59.1	open_logic
YAF6XH9G9N	exercise	prob, section 42.2	open_logic
YAX80S9TGG	statement	lem, section 62.3	open_logic
YB6ZF5W049	proof	proof, section 49.4	open_logic
YBCSDXXKZ3	proof	proof, section 2.5	open_logic
YBR71T5PY7	example	ex, section 86.2	open_logic
YCASZC6CPT	statement	lem, section 71.11	open_logic
YCHMWXY76T	proof	proof, section 74.4	open_logic
YCW0YPQM9P	proof	proof, section 62.2	open_logic
YD2FNMX7SF	exercise	prob, section 32.4	open_logic
YE27Y2P92H	example	ex, section 19.9	open_logic
YE4F75D6AQ	proof	proof, section 78.2	open_logic
YEPZKG9R8R	definition	defn, section 50.5	open_logic
YFBWWP7AD1	statement	prop, section 78.11	open_logic
YGBH75B5T9	example	ex, section 13.3	open_logic
YGD0QMHD9M	proof	proof, section 27.9	open_logic
YGDYG9XR4P	statement	prop, section 17.8	open_logic
YGFYMHGDXM	statement	thm, section 3.9	open_logic
YGXMCY9E62	statement	thm, section 46.5	open_logic
YH4ETYTJ2Y	exercise	prob, section 83.4	open_logic
YH78AK5VQ1	proof	proof, section 29.10	open_logic
YHNQH2J7W6	proof	proof, section 79.1	open_logic
Symmetry	definition	defn, section 82.1	open_logic
YK0QDA37RQ	proof	proof, section 41.7	open_logic
YKHGDNKTK6	proof	proof, section 52.5	open_logic
YKSEBYE13R	proof	proof, section 79.1	open_logic
Proof of \olref{prop:rep-id}	proof	proof, section 29.3	open_logic
YM7R4PAZ6C	exercise	prob, section 17.5	open_logic
YMN0D7PBPY	exercise	prob, section 55.7	open_logic
YNCNY4PYHJ	statement	thm, section 43.1	open_logic
YNQEKFZBP4	example	ex, section 53.7	open_logic
YP71PH8H2V	statement	prop, section 19.14	open_logic
YPKWGF8GT5	proof	proof, section 30.4	open_logic
YPQ35B9AWH	definition	defn, section 62.2	open_logic
YPWG0Y19B5	example	ex, section 22.11	open_logic
YQJR5YTSKJ	definition	defn, section 3.30	open_logic
YQMN2N2718	exercise	prob, section 76.7	open_logic
YQWHFSB2MA	exercise	prob, section 61.10	open_logic
YRGMRFRAA7	example	ex, section 19.5	open_logic
YRHCPDENZJ	proof	proof, section 55.4	open_logic
YRMG9PBJVB	example	ex, section 8.12	open_logic
YSM77N949F	example	ex, section 13.3	open_logic
YSN1TMQJBY	statement	prop, section 22.7	open_logic
YT8Z6ZFP7D	definition	defn, section 44.3	open_logic
YTE0TGF0QV	statement	prop, section 50.6	open_logic
YXM50A6SPW	proof	proof, section 11.1	open_logic
YXRH37VS6V	example	ex, section 54.1	open_logic
YXYP1NTNP5	proof	proof, section 51.4	open_logic
YYPESRW8AA	exercise	prob, section 3.8	open_logic
YYZZC7EMS5	example	ex, section 53.6	open_logic
YZ03DER3SJ	statement	thm, section 9.3	open_logic
YZ6AN798BC	statement	prop, section 54.7	open_logic
YZ7WA6CJKF	statement	thm, section 56.2	open_logic
YZFJ83ANT3	exercise	prob, section 15.7	open_logic
YZJA4YQ0KS	statement	lem, section 70.1	open_logic
Z0E01664FF	proof	proof, section 3.13	open_logic
Z0PNZHRDR0	example	ex, section 41.5	open_logic
Z0PS2PNTGV	proof	proof, section 4.1	open_logic
Z17DJVX0NZ	proof	proof, section 50.2	open_logic
Z1QDEQZFSG	proof	proof, section 79.6	open_logic
Z2ATWFY713	statement	prop, section 50.6	open_logic
Z2KDJ7K8GF	proof	proof, section 50.13	open_logic
Z2NYT8E1T7	proof	proof, section 79.5	open_logic
Z3FHZTVJRW	statement	prop, section 3.20	open_logic
Z49NRZ3VY8	proof	proof, section 71.8	open_logic
Substitution	definition	defn, section 38.15	open_logic
Z4ET8K6PQK	statement	prop, section 44.8	open_logic
Z4T36G4EQ4	definition	defn, section 50.11	open_logic
Z54TFQH62R	statement	prop, section 8.8	open_logic
Enumeration, formally	definition	defn, section 83.5	open_logic
Z6V3N703CM	proof	proof, section 28.6	open_logic
Z79EK2HHRC	statement	thm, section 50.13	open_logic
Z7K2XZDJCK	exercise	prob, section 3.20	open_logic
Z7R677WK7M	statement	cor, section 72.5	open_logic
Z7RQPKS0V8	proof	proof, section 38.14	open_logic
Z8RBP0W1R5	exercise	prob, section 83.5	open_logic
Z8VJP5A93V	proof	proof, section 51.10	open_logic
Second-order \usetoken{s}{formula}	definition	defn, section 68.1	open_logic
ZB2B2R1DZX	proof	proof, section 22.2	open_logic
ZB5XAYK7ZG	statement	prop, section 50.8	open_logic
ZBFRW3C622	definition	defn, section 78.1	open_logic
ZBZQR1AQSG	proof	proof, section 29.2	open_logic
ZC76XSXK8F	proof	proof, section 83.8	open_logic
ZCNG3FNSQJ	definition	defn, section 3.30	open_logic
ZCTR9RVGT2	statement	prop, section 44.11	open_logic
ZD17ZZEAMY	proof	proof, section 61.9	open_logic
Robinson's Joint Consistency Theorem	statement	thm, section 57.1	open_logic
ZEBK1MTP25	exercise	prob, section 86.1	open_logic
ZF6BC87GW4	statement	cor, section 55.4	open_logic
ZGHFRQYJ32	exercise	prob, section 67.5	open_logic
ZGR9T95A3Z	exercise	prob, section 83.11	open_logic
ZH63F44186	statement	prop, section 50.8	open_logic
ZH6WGSH4MY	proof	proof, section 56.1	open_logic
ZJ00DKSYKA	proof	proof, section 8.10	open_logic
ZJ14K50Z8E	proof	proof, section 19.15	open_logic
ZJ5CABNR4F	exercise	prob, section 19.2	open_logic
ZJXY9F7DV3	exercise	prob, section 29.3	open_logic
Axioms	definition	defn, section 31.1	open_logic
ZM8H7VC9CA	example	ex, section 5.4	open_logic
ZM9J83SKP3	proof	proof, section 46.5	open_logic
ZMCZPRK25Y	definition	defn, section 83.2	open_logic
ZMY201767B	definition	defn, section 51.10	open_logic
ZN58HMJBR2	proof	proof, section 27.6	open_logic
ZNCABJ0HZJ	exercise	prob, section 42.5	open_logic
ZNV0WZ7HJS	proof	proof, section 8.6	open_logic
ZP3AJ2GGE7	definition	defn, section 28.7	open_logic
ZQ6RA0J8F7	exercise	prob, section 11.1	open_logic
ZQX6T61Y62	example	ex, section 13.5	open_logic
ZRGRHP35GB	exercise	prob, section 19.6	open_logic
ZSDH9M6PS2	definition	defn, section 11.4	open_logic
ZSHSXWKJD2	proof	proof, section 3.30	open_logic
ZTA5546W3J	proof	proof, section 50.13	open_logic
ZV1DEVBWCP	definition	defn, section 70.2	open_logic
ZV3N3YZ64T	proof	proof, section 60.4	open_logic
ZV4R8D1JVY	example	ex, section 27.6	open_logic
ZVEWZCF9C4	statement	prop, section 58.3	open_logic
ZVGXS2KJB4	statement	thm, section 38.15	open_logic
ZW9CXJ0DRW	proof	proof, section 46.8	open_logic
Arithmetical induction	statement	thm, section 79.7	open_logic
ZWJZ0S4PXF	proof	proof, section 79.1	open_logic
ZWP9N92HVF	exercise	prob, section 80.4	open_logic
ZWR7PKYMC4	proof	proof, section 62.2	open_logic
Initial configuration	definition	defn, section 85.4	open_logic
ZXA0XJ12F1	proof	proof, section 69.4	open_logic
ZXBC7008J7	proof	proof, section 72.1	open_logic
ZXP4KW1E3T	statement	lem, section 47.2	open_logic
ZXPZESQQ3Q	proof	proof, section 51.3	open_logic
ZY8H7RRG3N	statement	prop, section 17.8	open_logic
ZYB428SC7G	definition	defn, section 70.5	open_logic
ZYNDQX1MJ4	example	ex, section 62.3	open_logic
Burali-Forti Paradox	statement	thm, section 72.2	open_logic
ZZG39XNK2D	definition	defn, section 33.2	open_logic
Local Determination	statement	thm, section 63.1	open_logic
ZZV5QC8HSQ	statement	prop, section 37.8	open_logic

Catalogue records

open_logic: open_logic (work)