http://builds.openlogicproject.org/

Open Logic Project Builds

This site contains PDFs built from the source LaTeX files of the most
recent version of the Open Logic Text.

Complete PDFs

We have PDFs of the complete text in the Open Logic master branch,
arranged in a somewhat sensible manner, including editorial comments.
It's not intended as a textbook, but it shows what's there.

  * Open Logic Text, Complete Clean Version: one big PDF of all the
    material, without extra markup.
  * Open Logic Text, Complete Debug Version: one big PDF with
    additional markup to identify source files and OLT-specific
    commands.

Individual Textbooks

There are already a few textbooks that show how one might "remix" the
material in the Open Logic Project to produce nice textbooks. These
vary in the material that's included, the design, and the
configuration options used. They may also include additional material
specific to those courses.

Sets, Logic, Computation

[slc]A textbook on metalogic, developed for Calgary's Logic II
course: includes the material on set theory, first-order logic
(including both sequent calculus and natural deduction), and Turing
machines (including undecidability). Appendices cover proofs and
induction and biographies of some logicians. This text also includes
chapter summaries and a glossary. Problems are collected at the end
of chapters.

  * slc-screen.pdf for screen reading (color, smaller margins,
    low-res images)
  * slc-print.pdf for print-on-demand (without cover)
  * Source code for generating this textbook is on GitHub in a
    separate repository.

Incompleteness and Computability

[ic]A textbook on Godel's incompleteness theorems and computability
theory, developed for Calgary's Logic III course: includes the
material on recursive functions, Godel's incompleteness theorem,
models of arithmetic, second-order logic, and the lambda calculus.
Appendices cover basics of first-order logic with natural deduction,
and biographies of some logicians. This text also includes chapter
summaries.

  * ic-screen.pdf for screen reading (color, smaller margins, low-res
    images)
  * ic-print.pdf for print-on-demand (without cover)
  * Source code for generating this textbook is on GitHub in a
    separate repository.

Boxes and Diamonds

[bd]A textbook for modal and other intensional logics based on the
Open Logic Project; includes the material on normal modal logic,
intutionistic logic, and counterfactuals, with appendices on basic
set theory and classical propositional logic.

  * bd-screen.pdf for screen reading (color, smaller margins, low-res
    images)
  * Source code for generating this textbook is on GitHub in a
    separate repository.

Set Theory: An Open Introduction

[settheory]A brief introduction to the philosophy of set theory;
covers why set theory came about; how to reduce large swathes of
mathematics to set theory + arithmetic; how to embed arithmetic in
set theory; what the cumulative iterative conception of set amounts
to; how one might try to justify the axioms of ZFC. Most of the
material making up the text comes from Tim Button's Open Set Theory.

  * settheory-screen.pdf for screen reading (color, smaller margins,
    low-res images)
  * Source code for generating this textbook is on GitHub in a
    separate repository.

Intermediate Logic

[il]A textbook for McGill's Intermediate Logic (Phil 310) course:
includes the material on naive set theory, first order logic through
the Completeness Theorem, recursive functions, Godel's incompleteness
theorem, and models of arithmetic. Appendices cover proofs and
induction and biographies of some logicians. This text also includes
chapter summaries.

  * il-screen.pdf for screen reading (color, smaller margins, low-res
    images)
  * Source code for generating this textbook is on GitHub in a
    separate repository.

What If?

[wi]A textbook used for Calgary's Philosophy of Logic (Phil 473) and
Victoria's Non-Classical Logics (Phil 371) courses. It includes the
OLP material on propositional classical, many-valued, modal
(including epistemic, temporal, and conditional logics), and
intuitionistic logics. Appendices cover sets and relations, as well
as proofs and induction. This is currently an incomplete draft.
Material on epistemic and temporal logic is yet to be merged into the
main OLP repository.

  * wi-screen.pdf for screen reading (color, smaller margins, low-res
    images)
  * Source code for generating this textbook is on GitHub in a
    separate repository.

Sample Texts

The OLP main repository also includes two sample textbooks that serve
just to illustrate how one might produce texts using different
formatting conventions.

  * open-logic-enderton, a sample textbook that follows the
    conventions of Enderton's popular A Mathematical Introduction to
    Logic.
  * open-logic-sample, a selection including set theory, first-order
    logic, Turing machines, and incompleteness, using yet other
    conventions.

Active Branches

At any point, there may be active branches of the Open Logic Project
in GitHub. This branches may contain additional material, or
revisions of the material in the master branch which are being worked
on or reviewed for inclusion. We provide PDFs of the complete text as
it looks in these branches.

  * slc-f21-bis: debug | complete

Parts, Chapters, Sections

 1. sets-functions-relations-complete
     1. sets
         1. basics
         2. subsets
         3. important-sets
         4. unions-and-intersections
         5. pairs-and-products
         6. russells-paradox
     2. relations-complete
         1. relations-as-sets
         2. reflections
         3. special-properties
         4. equivalence-relations
         5. orders
         6. graphs
         7. operations
     3. functions
         1. function-basics
         2. function-kinds
         3. functions-relations
         4. inverses
         5. composition
         6. isomorphic-functions
         7. partial-functions
     4. size-of-sets-complete
         1. introduction
         2. enumerability
         3. zig-zag
         4. pairing
         5. pairing-alt
         6. non-enumerability
         7. reduction
         8. equinumerous-sets
         9. comparing-size
        10. schroder-bernstein
        11. enumerability-alt
        12. non-enumerability-alt
        13. reduction-alt
     5. arithmetization
         1. integers
         2. rationals
         3. reals
         4. cuts
         5. reflections
         6. checking-details
         7. cauchy
     6. infinite
         1. hilberts-hotel
         2. dedekind-algebra
         3. dedekind-induction
         4. dedekinds-proof
         5. card-sb
 2. propositional-logic
     1. syntax-and-semantics
         1. introduction
         2. formulas
         3. preliminaries
         4. valuations-sat
         5. semantic-notions
 3. first-order-logic
     1. introduction
         1. first-order-logic
         2. syntax
         3. formulas
         4. satisfaction
         5. sentences
         6. semantic-notions
         7. substitution
         8. models-theories
         9. soundness-completeness
     2. syntax
         1. intro-syntax
         2. first-order-languages
         3. terms-formulas
         4. unique-readability
         5. main-operator
         6. subformulas
         7. free-vars-sentences
         8. substitution
     3. semantics
         1. intro-semantics
         2. structures
         3. covered-structures
         4. satisfaction
         5. assignments
         6. extensionality
         7. semantic-notions
     4. models-theories
         1. introduction
         2. expressing-props-of-structures
         3. theories
         4. expressing-relations
         5. set-theory
         6. size-of-structures
     5. proof-systems
         1. introduction
         2. sequent-calculus
         3. natural-deduction
         4. tableaux
         5. axiomatic-deduction
     6. sequent-calculus
         1. rules-and-proofs
         2. propositional-rules
         3. quantifier-rules
         4. structural-rules
         5. derivations
         6. proving-things
         7. proving-things-quant
         8. proof-theoretic-notions
         9. provability-consistency
        10. provability-propositional
        11. provability-quantifiers
        12. soundness
        13. identity
        14. soundness-identity
     7. natural-deduction
         1. rules-and-proofs
         2. propositional-rules
         3. quantifier-rules
         4. derivations
         5. proving-things
         6. proving-things-quant
         7. proof-theoretic-notions
         8. provability-consistency
         9. provability-propositional
        10. provability-quantifiers
        11. soundness
        12. identity
        13. soundness-identity
     8. tableaux
         1. rules-and-proofs
         2. propositional-rules
         3. quantifier-rules
         4. derivations
         5. proving-things
         6. proving-things-quant
         7. proof-theoretic-notions
         8. provability-consistency
         9. provability-propositional
        10. provability-quantifiers
        11. soundness
        12. identity
        13. soundness-identity
     9. axiomatic-deduction
         1. rules-and-proofs
         2. axioms-rules-propositional
         3. axioms-rules-quantifiers
         4. proving-things
         5. proving-things-quant
         6. proof-theoretic-notions
         7. deduction-theorem
         8. deduction-theorem-quantifiers
         9. provability-consistency
        10. provability-propositional
        11. provability-quantifiers
        12. soundness
        13. identity
    10. completeness
         1. introduction
         2. outline
         3. complete-consistent-sets
         4. henkin-expansions
         5. lindenbaums-lemma
         6. construction-of-model
         7. identity
         8. completeness-thm
         9. compactness
        10. compactness-direct
        11. downward-ls
    11. beyond
         1. introduction
         2. many-sorted-logic
         3. second-order-logic
         4. higher-order-logic
         5. intuitionistic-logic
         6. modal-logics
         7. other-logics
 4. model-theory
     1. basics
         1. reducts-and-expansions
         2. substructures
         3. overspill
         4. isomorphism
         5. theory-of-m
         6. partial-iso
         7. dlo
         8. nonstandard-arithmetic
     2. models-of-arithmetic
         1. introduction
         2. standard-models
         3. non-standard-models
         4. models-of-q
         5. models-of-pa
         6. computable-models
     3. interpolation
         1. introduction
         2. separation
         3. interpolation-proof
         4. definability
     4. lindstrom
         1. introduction
         2. abstract-logics
         3. ls-property
         4. lindstrom-proof
 5. computability
     1. recursive-functions
         1. introduction
         2. primitive-recursion
         3. composition
         4. pr-functions
         5. notation-pr-functions
         6. pr-functions-computable
         7. examples
         8. pr-relations
         9. bounded-minimization
        10. primes
        11. sequences
        12. trees
        13. other-recursions
        14. non-pr-functions
        15. partial-functions
        16. normal-form
        17. halting-problem
        18. general-recursive-functions
     2. computability-theory
         1. introduction
         2. coding-computations
         3. normal-form
         4. s-m-n
         5. universal-part-function
         6. no-universal-function
         7. halting-problem
         8. russells-paradox
         9. computable-sets
        10. ce-sets
        11. equiv-ce-defs
        12. ce-closed-cup-cap
        13. complement-ce
        14. reducibility
        15. prop-reduce
        16. complete-ce-sets
        17. k-1
        18. total
        19. rice-theorem
        20. fixed-point-thm
        21. application-fixed-point
        22. def-functions-self-reference
        23. minimization-lambda
 6. turing-machines
     1. machines-computations
         1. introduction
         2. representing-tms
         3. turing-machines
         4. configuration
         5. unary-numbers
         6. halting-states
         7. disciplined-machines
         8. combining-machines
         9. variants
        10. church-turing-thesis
     2. undecidability
         1. introduction
         2. enumerating-tms
         3. universal-tm
         4. halting-problem
         5. decision-problem
         6. representing-tms
         7. verification
         8. unsolvability-decision-problem
         9. trakhtenbrot
 7. incompleteness
     1. introduction
         1. historical-background
         2. definitions
         3. overview
         4. undecidability
     2. arithmetization-syntax
         1. introduction
         2. coding-symbols
         3. coding-terms
         4. coding-formulas
         5. substitution
         6. proofs-in-lk
         7. proofs-in-nd
         8. proofs-in-ax}{}
     3. representability-in-q
         1. introduction
         2. representable-comp
         3. beta-function
         4. prim-rec
         5. basic-representable
         6. composition-representable
         7. minimization-representable
         8. comp-representable
         9. representing-relations
        10. undecidability
     4. theories-computability
         1. introduction
         2. q-is-ce
         3. oconsis-ext-of-q-undec
         4. extensions-of-q-not-decidable
         5. computably-axiomatizable
         6. complete-decidable
         7. first-incompleteness
         8. inseparability
         9. consis-with-q
        10. interpretability
     5. incompleteness-provability
         1. introduction
         2. fixed-point-lemma
         3. first-incompleteness-thm
         4. rosser-thm
         5. godels-paper
         6. provability-conditions
         7. second-incompleteness-thm
         8. lob-thm
         9. tarski-thm
 8. second-order-logic
     1. syntax-and-semantics
         1. introduction
         2. terms-formulas
         3. satisfaction
         4. semantic-notions
         5. expressive-power
         6. inf-count
     2. metatheory
         1. introduction
         2. second-order-arithmetic
         3. undecidability-and-axiomatizability
         4. compactness
         5. loewenheim-skolem
     3. sol-and-set-theory
         1. introduction
         2. comparing-sets
         3. cardinalities
         4. power-of-continuum
 9. lambda-calculus
     1. introduction
         1. overview
         2. syntax
         3. reduction
         4. church-rosser
         5. currying
         6. lambda-definability
         7. lambda-computable
         8. computable-lambda
         9. basic-pr-lambda
        10. composition
        11. primitive-recursion
        12. fixed-point-combinator
        13. minimization
     2. syntax
         1. terms
         2. unique-readability
         3. abbreviated-syntax
         4. free-variables
         5. substitution
         6. alpha
         7. de-bruijn
         8. term-revisited
         9. beta
        10. eta
     3. church-rosser
         1. definitions-and-properties
         2. parallel-beta-reduction
         3. beta-reduction
         4. parallel-beta-eta-reduction
         5. beta-eta-reduction
     4. lambda-definability
         1. introduction
         2. arithmetical-functions
         3. pairs
         4. truth-values
         5. lists
         6. primitive-recursive-functions
         7. fixpoints
         8. minimization
         9. partial-recursive-functions
        10. lambda-definable-recursive
10. many-valued-logic
     1. syntax-and-semantics
         1. introduction
         2. connectives
         3. formulas
         4. matrices
         5. valuations-sat
         6. semantic-notions
         7. sublogics
     2. three-valued-logics
         1. introduction
         2. lukasiewicz
         3. kleene
         4. goedel
         5. multiple-designation
     3. infinite-valued-logics
         1. introduction
         2. lukasiewicz
         3. goedel
     4. sequent-calculus
         1. introduction
         2. rules-and-proofs
         3. structural-rules
         4. propositional-rules
11. normal-modal-logic
     1. syntax-and-semantics
         1. introduction
         2. language-modal-logic
         3. substitution
         4. relational-models
         5. truth-at-w
         6. truth-in-model
         7. modal-validity
         8. tautological-instances
         9. schemas
        10. entailment
     2. frame-definability
         1. introduction
         2. properties-accessibility
         3. frames
         4. definability
         5. first-order-definability
         6. equivalence-S5
         7. second-order-definability
     3. axioms-systems
         1. introduction
         2. normal-logics
         3. logics-proofs
         4. proofs-in-K
         5. derived-rules
         6. more-proofs-in-K
         7. duals
         8. proofs-modal-systems
         9. soundness
        10. systems-distinct
        11. provability-from-set
        12. provability-properties
        13. consistency
     4. completeness
         1. introduction
         2. complete-consistent-sets
         3. lindenbaums-lemma
         4. modalities-ccs
         5. canonical-models
         6. truth-lemma
         7. completeness-K
         8. frame-completeness
     5. filtrations
         1. introduction
         2. preliminaries
         3. filtrations-def
         4. examples-of-filtrations
         5. finite
         6. S5-fmp
         7. S5-decidable
         8. more-filtrations
         9. euclidean-filtrations
     6. tableaux
         1. introduction
         2. rules-for-K
         3. proofs-in-K
         4. soundness
         5. more-rules
         6. more-soundness
         7. simple-S5
         8. completeness
         9. countermodels
12. intuitionistic-logic
     1. introduction
         1. constructive-reasoning
         2. syntax
         3. bhk-interpretation
         4. natural-deduction
         5. axiomatic-derivations
     2. semantics
         1. introduction
         2. relational-models
         3. semantic-notions
         4. topological-semantics
     3. soundness-completeness
         1. soundness-axd
         2. soundness-nd
         3. lindenbaum
         4. canonical-model
         5. truth-lemma
         6. completeness-thm
         7. decidability
     4. propositions-as-types
         1. introduction
         2. sequent-natural-deduction
         3. proof-terms
         4. proofs-to-terms
         5. terms-to-proofs
         6. reduction
         7. normalization
13. counterfactuals
     1. introduction
         1. material-conditional
         2. paradoxes-material
         3. strict-conditional
         4. counterfactuals
     2. minimal-change-semantics
         1. introduction
         2. sphere-models
         3. true-false
         4. antecedent-strengthening
         5. transitivity
         6. contraposition
14. set-theory
     1. story
         1. extensionality
         2. russells-paradox-again
         3. predicativity
         4. cumulative-approach
         5. urelements
         6. grundgesetze
     2. z
         1. story
         2. separation
         3. union
         4. pairs
         5. powerset
         6. infinity-again
         7. milestone
         8. nat
         9. arbintersections
     3. ordinals
         1. introduction
         2. idea
         3. wo
         4. iso
         5. vn
         6. basic
         7. replacement
         8. milestone
         9. ordtype
        10. opps
     4. spine
         1. idea
         2. recursion
         3. stagesbasics
         4. foundation
         5. zf
         6. rank
     5. replacement
         1. introduction
         2. strength
         3. extrinsic
         4. limofsize
         5. absinf
         6. ref
         7. refproofs
         8. finiteaxiomatizability
     6. ord-arithmetic
         1. introduction
         2. addition
         3. using-addition
         4. multiplication
         5. exponentiation
     7. cardinals
         1. cp
         2. cardsasords
         3. milestone
         4. classing
         5. hp
     8. card-arithmetic
         1. opps
         2. simp
         3. expotough
         4. ch
         5. fix
     9. choice
         1. introduction
         2. tarskiscott
         3. hartogs
         4. wellorderingproblem
         5. countablechoice
         6. justifications
         7. banach
         8. vitali
15. methods
     1. proofs
         1. introduction
         2. starting-proofs
         3. using-definitions
         4. inference-patterns
         5. example-1
         6. example-2
         7. proof-by-contradiction
         8. reading-proofs
         9. cant-do-it
        10. resources
     2. induction
         1. introduction
         2. induction-on-N
         3. strong-induction
         4. inductive-definitions
         5. structural-induction
         6. relations
16. history
     1. biographies
         1. georg-cantor
         2. alonzo-church
         3. gerhard-gentzen
         4. kurt-goedel
         5. emmy-noether
         6. rozsa-peter
         7. julia-robinson
         8. bertrand-russell
         9. alfred-tarski
        10. alan-turing
        11. ernst-zermelo
     2. set-theory
         1. infinitesimals
         2. limits
         3. pathologies
         4. mythology
         5. cantor-plane
         6. hilbert-curve
17. reference
     1. greek-alphabet
     2. fraktur-alphabet

Generated from Git revision 0552395 (2022-04-04)