The Open Logic Project PKGMM3P5QY

URI	`m2://res/PKGMM3P5QY`
Kind	textbook
Creators	The Open Logic Project
Scope	deferred (no test decides the record, and the classifier has no model)

Expressions

e1: edition

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

Catalogue records

open_logic: open_logic (work)