;; (find-sh "cd ~/books/ && find * | sort") ;; (find-sh "cd ~/books/__logic/ && find * | sort") ;; «.abramsky» (to "abramsky") ;; «.abramsky-lazy» (to "abramsky-lazy") ;; «.aczel» (to "aczel") ;; «.allen» (to "allen") ;; «.allwein-barwise» (to "allwein-barwise") ;; «.altenkirch» (to "altenkirch") ;; «.altenkirch-dtwos» (to "altenkirch-dtwos") ;; «.andrews» (to "andrews") ;; «.aschieri-zorzi» (to "aschieri-zorzi") ;; «.atten» (to "atten") ;; «.baader-nipkow» (to "baader-nipkow") ;; «.barendregt» (to "barendregt") ;; «.barthe» (to "barthe") ;; «.barwise» (to "barwise") ;; «.barwise-etchemendy» (to "barwise-etchemendy") ;; «.barwise-moss» (to "barwise-moss") ;; «.beeson-narboux-wiedijk» (to "beeson-narboux-wiedijk") ;; «.bell-machover» (to "bell-machover") ;; «.benthem» (to "benthem") ;; «.bernays» (to "bernays") ;; «.beziau» (to "beziau") ;; «.bierman-depaiva» (to "bierman-depaiva") ;; «.birkedal» (to "birkedal") ;; «.blok-pigozzi» (to "blok-pigozzi") ;; «.brown» (to "brown") ;; «.debruijn» (to "debruijn") ;; «.debruijn-telesc» (to "debruijn-telesc") ;; «.bueno» (to "bueno") ;; «.bunder-seldin» (to "bunder-seldin") ;; «.carnap» (to "carnap") ;; «.carnielli» (to "carnielli") ;; «.carnielli-coniglio» (to "carnielli-coniglio") ;; «.chagrov» (to "chagrov") ;; «.changkeisler» (to "changkeisler") ;; «.chew» (to "chew") ;; «.chuaqui» (to "chuaqui") ;; «.ciabattoni-ferrari» (to "ciabattoni-ferrari") ;; «.coniglio» (to "coniglio") ;; «.conway» (to "conway") ;; «.copi» (to "copi") ;; «.coquand» (to "coquand") ;; «.coquand-huet» (to "coquand-huet") ;; «.corcoran» (to "corcoran") ;; «.corcoran-alaimi» (to "corcoran-alaimi") ;; «.crossley-dummett» (to "crossley-dummett") ;; «.curry» (to "curry") ;; «.dagostino» (to "dagostino") ;; «.damas» (to "damas") ;; «.davis» (to "davis") ;; «.degroote-hindley» (to "degroote-hindley") ;; «.devlin» (to "devlin") ;; «.dore» (to "dore") ;; «.dummett» (to "dummett") ;; «.ebbinghaus» (to "ebbinghaus") ;; «.enderton» (to "enderton") ;; «.farmer» (to "farmer") ;; «.farmer-chiron» (to "farmer-chiron") ;; «.feferman» (to "feferman") ;; «.fenstadt» (to "fenstadt") ;; «.ferreira» (to "ferreira") ;; «.fitting» (to "fitting") ;; «.flower-masthoff-stapleton» (to "flower-masthoff-stapleton") ;; «.frade» (to "frade") ;; «.fraenkel» (to "fraenkel") ;; «.fraser» (to "fraser") ;; «.gabbay» (to "gabbay") ;; «.gentzen» (to "gentzen") ;; «.geuvers» (to "geuvers") ;; «.giardino» (to "giardino") ;; «.girard» (to "girard") ;; «.girard-blind-spot» (to "girard-blind-spot") ;; «.girard-tcs87» (to "girard-tcs87") ;; «.girard-tet» (to "girard-tet") ;; «.godel» (to "godel") ;; «.goranko» (to "goranko") ;; «.grande» (to "grande") ;; «.grande-silva» (to "grande-silva") ;; «.krantz-parks» (to "krantz-parks") ;; «.gries-schneider» (to "gries-schneider") ;; «.gun» (to "gun") ;; «.handbook-of-logic-in-CS» (to "handbook-of-logic-in-CS") ;; «.henkin» (to "henkin") ;; «.herbelin» (to "herbelin") ;; «.hermogenesoliveira» (to "hermogenesoliveira") ;; «.hesseling» (to "hesseling") ;; «.heyting» (to "heyting") ;; «.hindley» (to "hindley") ;; «.hindley-seldin2» (to "hindley-seldin2") ;; «.hintikka» (to "hintikka") ;; «.hofstadter» (to "hofstadter") ;; «.howard» (to "howard") ;; «.hott» (to "hott") ;; «.humberstone» (to "humberstone") ;; «.hurd» (to "hurd") ;; «.hurd-loeb» (to "hurd-loeb") ;; «.hurkens» (to "hurkens") ;; «.jamnik» (to "jamnik") ;; «.kamareddine» (to "kamareddine") ;; «.kelley» (to "kelley") ;; «.kleene» (to "kleene") ;; «.knuth» (to "knuth") ;; «.kohlenbach» (to "kohlenbach") ;; «.kripke» (to "kripke") ;; «.krivine» (to "krivine") ;; «.kubota» (to "kubota") ;; «.kunen» (to "kunen") ;; «.lacompling2018» (to "lacompling2018") ;; «.landau» (to "landau") ;; «.leary» (to "leary") ;; «.lecomte» (to "lecomte") ;; «.leeds1990» (to "leeds1990") ;; «.leroy» (to "leroy") ;; «.lifschitz» (to "lifschitz") ;; «.lukasiewicz» (to "lukasiewicz") ;; «.luo» (to "luo") ;; «.luo-callaghan» (to "luo-callaghan") ;; «.luo-proofirr» (to "luo-proofirr") ;; «.luxemburg-robinson» (to "luxemburg-robinson") ;; «.machover» (to "machover") ;; «.machover-hirschfeld» (to "machover-hirschfeld") ;; «.maddy» (to "maddy") ;; «.marcos» (to "marcos") ;; «.martin-lof» (to "martin-lof") ;; «.martin-lof-cmcp» (to "martin-lof-cmcp") ;; «.martin-lof-as» (to "martin-lof-as") ;; «.martin-lof-mean» (to "martin-lof-mean") ;; «.martin-lof-atot» (to "martin-lof-atot") ;; «.martin-lof-ittpp» (to "martin-lof-ittpp") ;; «.martin-lof-transcriptions» (to "martin-lof-transcriptions") ;; «.meleiro» (to "meleiro") ;; «.mendelson» (to "mendelson") ;; «.mints» (to "mints") ;; «.monin-ene-perin» (to "monin-ene-perin") ;; «.moraes-queiroz» (to "moraes-queiroz") ;; «.mortari» (to "mortari") ;; «.mortensen» (to "mortensen") ;; «.mummaphd» (to "mummaphd") ;; «.nederpelt» (to "nederpelt") ;; «.nederpelt-geuvers» (to "nederpelt-geuvers") ;; «.negarestani» (to "negarestani") ;; «.negri-vonplato» (to "negri-vonplato") ;; «.nelson» (to "nelson") ;; «.nolt-rohatyn» (to "nolt-rohatyn") ;; «.nordstrom» (to "nordstrom") ;; «.nye» (to "nye") ;; «.oliva» (to "oliva") ;; «.open-logic» (to "open-logic") ;; «.paleo-delahaye» (to "paleo-delahaye") ;; «.papineau» (to "papineau") ;; «.patterson» (to "patterson") ;; «.paulin-mohring» (to "paulin-mohring") ;; «.pelletier» (to "pelletier") ;; «.pohlers» (to "pohlers") ;; «.pradic-brown» (to "pradic-brown") ;; «.prawitz» (to "prawitz") ;; «.priest» (to "priest") ;; «.priest-incl» (to "priest-incl") ;; «.reid» (to "reid") ;; «.restall» (to "restall") ;; «.reynolds» (to "reynolds") ;; «.robinson» (to "robinson") ;; «.rose-shepherdson» (to "rose-shepherdson") ;; «.russell» (to "russell") ;; «.sambin-smith» (to "sambin-smith") ;; «.saracino-weispfenning» (to "saracino-weispfenning") ;; «.scheele» (to "scheele") ;; «.second-order» (to "second-order") ;; «.shieh» (to "shieh") ;; «.shin» (to "shin") ;; «.smith» (to "smith") ;; «.smith-ifl» (to "smith-ifl") ;; «.smith-igt» (to "smith-igt") ;; «.smullyan» (to "smullyan") ;; «.smullyan» (to "smullyan") ;; «.spencer-brown» (to "spencer-brown") ;; «.steinhart» (to "steinhart") ;; «.stenlund» (to "stenlund") ;; «.stroyan» (to "stroyan") ;; «.stroyan-luxemburg» (to "stroyan-luxemburg") ;; «.szabo-arpad» (to "szabo-arpad") ;; «.tarski» (to "tarski") ;; «.tarskiaot» (to "tarskiaot") ;; «.tarskisclh» (to "tarskisclh") ;; «.trafford» (to "trafford") ;; «.troelstra» (to "troelstra") ;; «.umezawa» (to "umezawa") ;; «.vaananen» (to "vaananen") ;; «.van_dalen» (to "van_dalen") ;; «.vandenberg-neves» (to "vandenberg-neves") ;; «.vandoulakis» (to "vandoulakis") ;; «.vonplato» (to "vonplato") ;; «.wickerson-dodds-parkinson» (to "wickerson-dodds-parkinson") ;; «.wiedijk» (to "wiedijk") ;; «.wiedijk-dbf» (to "wiedijk-dbf") ;; «.wilander» (to "wilander") ;; «.velleman» (to "velleman") ;; «.victor-nascimento» (to "victor-nascimento") ;; «.automath» (to "automath") ;; «.ctt» (to "ctt") ;; «.games» (to "games") ;; «.iapt-buffalo68» (to "iapt-buffalo68") ;; «.logic-and-alg-spec» (to "logic-and-alg-spec") ;; «.nsa» (to "nsa") ;; «.tableaux» (to "tableaux") ;; «.tapsoft93» (to "tapsoft93") ;; «.term-rewriting» (to "term-rewriting") ;; «.typetheory» (to "typetheory") ;; «abramsky» (to ".abramsky") ;; http://gigapedia.com/items/124504/handbook-of-logic-in-computer-science-5 (code-djvu "hlics5" "~/books/__logic/abramsky_gabbay_maibaum__handbook_of_logic_in_computer_science__vol_5.djvu") (code-djvutotext "hlics5" "~/books/__logic/abramsky_gabbay_maibaum__handbook_of_logic_in_computer_science__vol_5.djvu") ;; (find-hlics5page 9 "Contents") ;; (find-hlics5page (+ 18 1) "Nordstrom") ;; (find-hlics5page (+ 18 39) "Categorical Logic") ;; (find-hlics5page (+ 18 78) "Hyperdoctrines") ;; (find-hlics5text "") ;; «abramsky-lazy» (to ".abramsky-lazy") ;; The Lazy Lambda Calculus (2006) ;; https://www.cs.ox.ac.uk/files/293/lazy.pdf (code-pdf-page "abramskylazy" "$S/https/www.cs.ox.ac.uk/files/293/lazy.pdf") (code-pdf-text "abramskylazy" "$S/https/www.cs.ox.ac.uk/files/293/lazy.pdf") ;; (find-abramskylazypage) ;; (find-abramskylazytext) ;; «aczel» (to ".aczel") ;; http://www.cs.man.ac.uk/~petera/russ-praw.ps.gz ;; http://www.cs.man.ac.uk/~petera/russ-praw.pdf ;; «allen» (to ".allen") ;; (find-books "__logic/__logic.el" "allen") ;; Stuart Allen: "A Non-Type-Theoretic Definition of Martin-Löf's Types" (1987) ;; http://www.cs.cornell.edu/Info/Projects/NuPrl/documents/Allen/lics87.html ;; http://www.cs.cornell.edu/Info/Projects/NuPrl/documents/Allen/TR87-832-RESET.ps (code-pdf-page "allenntt" "$S/http/www.cs.cornell.edu/Info/Projects/NuPrl/documents/Allen/TR87-832-RESET.pdf") (code-pdf-text "allenntt" "$S/http/www.cs.cornell.edu/Info/Projects/NuPrl/documents/Allen/TR87-832-RESET.pdf") ;; (find-allennttpage) ;; (find-allenntttext) ;; «allwein-barwise» (to ".allwein-barwise") ;; http://gigapedia.com/items/120086/logical-reasoning-with-diagrams--studies-in-logic-and-computation- (code-xpdf "logreaswithdiags" "~/books/__logic/allwein_barwise__logical_reasoning_with_diagrams.pdf") ;; (find-logreaswithdiagspage 13 "Contents") ;; (find-logreaswithdiagspage (+ 16 49) "Diagrams and the Concept of Logical Systems") ;; (find-logreaswithdiagspage (+ 16 81) "Situation-theoretic Account of Valid Reasoning with Venn Diagrams") ;; (find-logreaswithdiagspage (+ 16 267) "Index") ;; «altenkirch» (to ".altenkirch") ;; (find-books "__logic/__logic.el" "altenkirch") ;; http://www.cs.nott.ac.uk/~psztxa/ ;; http://www.cs.nott.ac.uk/~psztxa/publ/ ;; http://www.cs.nott.ac.uk/~psztxa/publ/fomus19.pdf ;; Thorsten Altenkirch: "Naive Type Theory" (code-pdf-page "altenkirchntt" "$S/http/www.cs.nott.ac.uk/~psztxa/publ/fomus19.pdf") (code-pdf-text "altenkirchntt" "$S/http/www.cs.nott.ac.uk/~psztxa/publ/fomus19.pdf") ;; (find-altenkirchnttpage) ;; (find-altenkirchntttext) ;; (find-altenkirchnttpage 1 "1 Introduction") ;; (find-altenkirchnttpage 2 "2 Type Theory vs Set Theory") ;; (find-altenkirchnttpage 3 "choice of representation") ;; (find-altenkirchntttext 3 "choice of representation") ;; (find-altenkirchnttpage 3 "type of its evidence") ;; (find-altenkirchntttext 3 "type of its evidence") ;; (find-altenkirchnttpage 4 "3 Non-dependent types") ;; (find-altenkirchnttpage 4 "3.1 Universes") ;; (find-altenkirchnttpage 4 "3.2 Functions") ;; (find-altenkirchnttpage 5 "3.3 Products and sums") ;; (find-altenkirchnttpage 7 "4 Dependent types") ;; (find-altenkirchnttpage 8 "4.1 -types and -types") ;; (find-altenkirchnttpage 10 "4.2 Induction and recursion") ;; (find-altenkirchnttpage 12 "4.3 The equality type") ;; (find-altenkirchnttpage 14 "5 Homotopy Type Theory") ;; (find-altenkirchnttpage 14 "5.1 Proof relevant equality") ;; (find-altenkirchnttpage 15 "5.2 What is a proposition?") ;; (find-altenkirchnttpage 17 "5.3 Dimensions of types") ;; (find-altenkirchnttpage 19 "5.4 Extensionality and univalence") ;; (find-altenkirchnttpage 22 "5.5 Higher Inductive Types") ;; (find-altenkirchnttpage 26 "5.6 Example: Definition of the Integers") ;; «altenkirch-dtwos» (to ".altenkirch-dtwos") ;; (find-books "__logic/__logic.el" "altenkirch-dtwos") ;; Altenkirch/Danielsson/Loh/Oury: "PiSigma: Dependent Types without the Sugar" ;; https://www.andres-loeh.de/PiSigma/PiSigma.pdf ;; (find-fline "$S/https/www.andres-loeh.de/PiSigma/") (code-pdf-page "deptypeswosugar" "$S/https/www.andres-loeh.de/PiSigma/PiSigma.pdf") (code-pdf-text "deptypeswosugar" "$S/https/www.andres-loeh.de/PiSigma/PiSigma.pdf") ;; (find-deptypeswosugarpage) ;; (find-deptypeswosugartext) ;; «andrews» (to ".andrews") ;; (find-books "__logic/__logic.el" "andrews") (code-pdf "andrewstttp" "~/books/__logic/andrews__an_introduction_to_mathematical_logic_and_type_theory_to_truth_through_proof.pdf") (code-pdftotext "andrewstttp" "~/books/__logic/andrews__an_introduction_to_mathematical_logic_and_type_theory_to_truth_through_proof.pdf" 13) ;; (find-andrewstttppage) ;; (find-andrewstttppage 6 "Contents") ;; (find-andrewstttptext 6 "Contents") ;; (find-andrewstttppage (+ 13 383) "Index") ;; (find-andrewstttptext (+ 13 383) "Index") ;; (find-andrewstttptext "") ;; «aschieri-zorzi» (to ".aschieri-zorzi") ;; Federico Aschieri/Margherita Zorzi: "On Natural Deduction in ;; Classical First-Order Logic: Curry-Howard Correspondence, Strong ;; Normalization and Herbrand's Theorem" ;; https://www.sciencedirect.com/science/article/pii/S0304397516001596 ;; https://dmg.tuwien.ac.at/aschieri/EMherbrandFinal.pdf (code-pdf-page "aschieri-zorzi" "$S/https/dmg.tuwien.ac.at/aschieri/EMherbrandFinal.pdf") (code-pdf-text "aschieri-zorzi" "$S/https/dmg.tuwien.ac.at/aschieri/EMherbrandFinal.pdf") ;; (find-aschieri-zorzipage) ;; (find-aschieri-zorzitext) ;; «atten» (to ".atten") ;; (find-books "__logic/__logic.el" "atten") (code-pdf-page "atten100" "~/books/__logic/atten_et_al_eds__one_hundred_years_of_intuitionism.pdf") (code-pdf-text "atten100" "~/books/__logic/atten_et_al_eds__one_hundred_years_of_intuitionism.pdf" 12) ;; (find-atten100page) ;; (find-atten100page 7 "Contents") ;; (find-atten100text 7 "Contents") ;; (find-atten100page (+ 12 1) "Part I: Brouwer and Brouwerian intuitionism") ;; (find-atten100page (+ 12 3) "Another look at Brouwer's dissertation") ;; (find-atten100page (+ 12 21) "Brouwerian infinity") ;; (find-atten100page (+ 12 37) "The new intuitionism") ;; (find-atten100page (+ 12 50) "Truth and experience of truth") ;; (find-atten100page (+ 12 60) "The proper explanation of intuitionistic logic: on Brouwer's demonstration of the Bar Theorem") ;; (find-atten100page (+ 12 78) "The intersection of intuitionism (Brouwer) and phenomenology (Husserl)") ;; (find-atten100page (+ 12 96) "Brouwer on `hypotheses' and the middle Wittgenstein") ;; (find-atten100page (+ 12 115) "Brouwer's notion of intuition and theory of knowledge by presence.") ;; (find-atten100page (+ 12 131) "Buddhist models of the mind and the common core thesis on mysticism") ;; (find-atten100page (+ 11 147) "Part II: Kindred spirits") ;; (find-atten100page (+ 10 149) "Remarks on the supposed French `semi-' or `pre-intuitionism'.") ;; (find-atten100page (+ 10 163) "Poincaré: intuitionism, intuition, and convention") ;; (find-atten100page (+ 10 178) "Some of Julius König's mathematical dreams in his New Foundations of Logic, Arithmetic, and Set Theory") ;; (find-atten100page (+ 10 198) "Gödel, constructivity, impredicativity, and feasibility.") ;; (find-atten100page (+ 10 214) "Lorenzen's operative justification of intuitionistic logic") ;; (find-atten100page (+ 10 241) "Part III: Mathematical perspectives") ;; (find-atten100page (+ 9 243) "The Hilbert-Brouwer controversy resolved?") ;; (find-atten100page (+ 9 257) "Proof theory and Martin-Löf Type Theory") ;; (find-atten100page (+ 9 280) "Some remarks on linear logic") ;; (find-atten100page (+ 9 301) "Two applications of dynamic constructivism: Brouwer's continuity principle and choice sequences in formal topology") ;; (find-atten100page (+ 9 316) "A reverse look at Brouwer's Fan Theorem") ;; (find-atten100page (+ 9 326) "Some applications of Brouwer's Thesis on Bars") ;; (find-atten100page (+ 9 341) "Concluding remarks at the Cerisy conference") ;; (find-atten100page (+ 9 343) "A bibliography of L.E.J. Brouwer") ;; (find-atten100page (+ 9 391) "References") ;; (find-atten100page (+ 9 417) "Index of citations") ;; (find-atten100page (+ 12 3) "Another look at Brouwer's dissertation") ;; (find-atten100page (+ 1 189) "Index") ;; (find-atten100text "") ;; «baader-nipkow» (to ".baader-nipkow") ;; «term-rewriting» (to ".term-rewriting") ;; http://gigapedia.com/items/329059/term-rewriting-and-all-that (code-djvu "termrewrit" "~/books/__logic/baader_nipkow__term_rewriting_and_all_that.djvu") (code-djvutotext "termrewrit" "~/books/__logic/baader_nipkow__term_rewriting_and_all_that.djvu" 11) ;; (find-termrewritpage 5 "Contents") ;; (find-termrewritpage (+ 11 1) "Chapter 1") ;; (find-termrewritpage (+ 11 278) "A Bluffer's Guide to ML") ;; (find-termrewritpage (+ 11 297) "Index") ;; «barendregt» (to ".barendregt") ;; (find-books "__logic/__logic.el" "barendregt") ;; https://dl.acm.org/doi/10.5555/162552.162561 ;; https://ttic.uchicago.edu/~dreyer/course/papers/barendregt.pdf (code-pdf-page "bdrgt" "$S/https/ttic.uchicago.edu/~dreyer/course/papers/barendregt.pdf") (code-pdf-text "bdrgt" "$S/https/ttic.uchicago.edu/~dreyer/course/papers/barendregt.pdf") ;; (find-bdrgtpage) ;; (find-bdrgtpage 2 "Contents") ;; (find-bdrgtpage (+ 1 77) "Cube") ;; (find-bdrgtpage (+ 1 86) "Abstraction rule") ;; (find-bdrgttext) ;; «barthe» (to ".barthe") ;; (find-books "__logic/__logic.el" "barthe") ;; https://link.springer.com/chapter/10.1007/BFb0014042 (code-pdf-page "barthe" "~/books/__logic/barthe__extensions_of_pure_type_systems.pdf") (code-pdf-text "barthe" "~/books/__logic/barthe__extensions_of_pure_type_systems.pdf" -15) ;; (find-barthepage) ;; (find-barthetext) ;; (find-barthepage (+ -15 31) "Appendix: pure type systems with strong sums") ;; (find-barthetext (+ -15 31) "Appendix: pure type systems with strong sums") ;; «barwise» (to ".barwise") ;; http://gigapedia.com/items/35813/handbook-of-mathematical-logic--studies-in-logic-and-the-foundations-of-mathematics- (code-djvu "barwisehandbook" "~/books/__logic/barwise__handbook_of_mathematical_logic.djvu") (code-djvutotext "barwisehandbook" "~/books/__logic/barwise__handbook_of_mathematical_logic.djvu") ;; (find-barwisehandbookpage 10 "Contents") ;; (find-barwisehandbookpage (+ 12 283) "Kock, Reyes" "Doctrines in Categorical Logic") ;; (find-barwisehandbookpage (+ 12 284) "only differ in what operations are considered primitve and which derived") ;; (find-barwisehandbookpage (+ 12 289) "functor ``circle''") ;; (find-barwisehandbookpage (+ 12 305) "recursive") ;; (find-barwisehandbookpage (+ 12 453) "classes") ;; (find-barwisehandbookpage (+ 12 453) "Devlin" "Constructibility") ;; (find-barwisehandbookpage (+ 12 739) "Aczel" "An introduction to inductive definitions") ;; (find-barwisehandbooktext "") ;; «barwise-etchemendy» (to ".barwise-etchemendy") ;; (find-books "__logic/__logic.el" "barwise-etchemendy") ;; (find-es "tex" "lplfitch") (code-xpdf "barwiseetchemendy" "~/books/__logic/barwise_etchemendy__language_proof_and_logic.pdf") (code-pdftotext "barwiseetchemendy" "~/books/__logic/barwise_etchemendy__language_proof_and_logic.pdf" 10) ;; Old ;; (find-barwiseetchemendypage (+ 10 22) "Cube(a)") ;; (find-barwiseetchemendytext (+ 10 22) "Cube(a)") ;; (find-barwiseetchemendypage (+ 10 150) "or-elim") ;; (find-barwiseetchemendypage (+ 10 206) "->-intro") ;; (find-barwiseetchemendypage (+ 10 342) "Fa-elim") ;; (find-barwiseetchemendypage (+ 10 343) "Fa-intro") ;; (find-barwiseetchemendypage (+ 10 347) "Ex-intro") ;; (find-barwiseetchemendypage (+ 10 348) "Ex-elim") ;; (find-barwiseetchemendypage (+ 14 559) "First-order rules") ;; (find-barwiseetchemendypage (+ 14 562) "Glossary") ;; (find-barwiseetchemendypage (+ 14 573) "Summary of rules") ;; (find-barwiseetchemendypage (+ 14 579) "Glossary") ;; (find-barwiseetchemendypage (+ 14 579) "General Index") ;; (find-barwiseetchemendytext "") ;; trim = function (str) return (str:match "^ *(.-) *$") end ;; redsp = function (str) return (str:gsub(" +", " ")) end ;; PP(trim(" ab cd ef ")) ;; PP(redsp("ab cd e f")) ;; titi = function (str) return str:match("^(.-) *([0-9]+)$") end ;; tif = function (tit, p) ;; if tit then ;; printf(";; (find-barwiseetchemendypage (+ 10 %3s) \"%s\")\n", p, tit) ;; end end ;; f = function (str) tif(titi(redsp(trim(str)))) end ;; fs = function (bigstr) for _,li in ipairs(splitlines(bigstr)) do f(li) end end ;; (find-barwiseetchemendypage) ;; (find-barwiseetchemendytext) ;; (find-barwiseetchemendypage 9 "Contents") ;; (find-barwiseetchemendypage (+ 14 1) "Introduction") ;; (find-barwiseetchemendypage (+ 14 1) "The special role of logic in rational inquiry") ;; (find-barwiseetchemendypage (+ 14 2) "Why learn an artificial language?") ;; (find-barwiseetchemendypage (+ 14 4) "Consequence and proof") ;; (find-barwiseetchemendypage (+ 14 5) "Instructions about homework exercises (essential!)") ;; (find-barwiseetchemendypage (+ 14 10) "To the instructor") ;; (find-barwiseetchemendypage (+ 14 15) "Web address") ;; (find-barwiseetchemendypage (+ 14 17) "I Propositional Logic") ;; (find-barwiseetchemendypage (+ 14 19) "1 Atomic Sentences") ;; (find-barwiseetchemendypage (+ 14 19) "1.1 Individual constants") ;; (find-barwiseetchemendypage (+ 14 20) "1.2 Predicate symbols") ;; (find-barwiseetchemendypage (+ 14 23) "1.3 Atomic sentences") ;; (find-barwiseetchemendypage (+ 14 26) "Cube(a)") ;; (find-barwiseetchemendypage (+ 14 28) "1.4 General first-order languages") ;; (find-barwiseetchemendypage (+ 14 31) "1.5 Function symbols (optional)") ;; (find-barwiseetchemendypage (+ 14 37) "1.6 The first-order language of set theory (optional)") ;; (find-barwiseetchemendypage (+ 14 38) "1.7 The first-order language of arithmetic (optional)") ;; (find-barwiseetchemendypage (+ 14 40) "1.8 Alternative notation (optional)") ;; (find-barwiseetchemendypage (+ 14 41) "2 The Logic of Atomic Sentences") ;; (find-barwiseetchemendypage (+ 14 41) "2.1 Valid and sound arguments") ;; (find-barwiseetchemendypage (+ 14 46) "2.2 Methods of proof") ;; (find-barwiseetchemendypage (+ 14 54) "2.3 Formal proofs") ;; (find-barwiseetchemendypage (+ 14 58) "2.4 Constructing proofs in Fitch") ;; (find-barwiseetchemendypage (+ 14 63) "2.5 Demonstrating nonconsequence") ;; (find-barwiseetchemendypage (+ 14 66) "2.6 Alternative notation (optional)") ;; (find-barwiseetchemendypage (+ 14 67) "3 The Boolean Connectives") ;; (find-barwiseetchemendypage (+ 14 68) "3.1 Negation symbol: nt") ;; (find-barwiseetchemendypage (+ 14 71) "3.2 Conjunction symbol: and") ;; (find-barwiseetchemendypage (+ 14 74) "3.3 Disjunction symbol: or") ;; (find-barwiseetchemendypage (+ 14 77) "3.4 Remarks about the game") ;; (find-barwiseetchemendypage (+ 14 79) "3.5 Ambiguity and parentheses") ;; (find-barwiseetchemendypage (+ 14 82) "3.6 Equivalent ways of saying things") ;; (find-barwiseetchemendypage (+ 14 84) "3.7 Translation") ;; (find-barwiseetchemendypage (+ 14 89) "3.8 Alternative notation (optional)") ;; (find-barwiseetchemendypage (+ 14 93) "4 The Logic of Boolean Connectives") ;; (find-barwiseetchemendypage (+ 14 94) "4.1 Tautologies and logical truth") ;; (find-barwiseetchemendypage (+ 14 106) "4.2 Logical and tautological equivalence") ;; (find-barwiseetchemendypage (+ 14 110) "4.3 Logical and tautological consequence") ;; (find-barwiseetchemendypage (+ 14 114) "4.4 Tautological consequence in Fitch") ;; (find-barwiseetchemendypage (+ 14 117) "4.5 Pushing negation around (optional)") ;; (find-barwiseetchemendypage (+ 14 121) "4.6 Conjunctive and disjunctive normal forms (optional)") ;; (find-barwiseetchemendypage (+ 14 127) "5 Methods of Proof for Boolean Logic") ;; (find-barwiseetchemendypage (+ 14 128) "5.1 Valid inference steps") ;; (find-barwiseetchemendypage (+ 14 131) "5.2 Proof by cases") ;; (find-barwiseetchemendypage (+ 14 136) "5.3 Indirect proof: proof by contradiction") ;; (find-barwiseetchemendypage (+ 14 140) "5.4 Arguments with inconsistent premises (optional)") ;; (find-barwiseetchemendypage (+ 14 142) "6 Formal Proofs and Boolean Logic") ;; (find-barwiseetchemendypage (+ 14 143) "6.1 Conjunction rules") ;; (find-barwiseetchemendypage (+ 14 148) "6.2 Disjunction rules") ;; (find-barwiseetchemendypage (+ 14 154) "6.3 Negation rules") ;; (find-barwiseetchemendypage (+ 14 163) "6.4 The proper use of subproofs") ;; (find-barwiseetchemendypage (+ 14 167) "6.5 Strategy and tactics") ;; (find-barwiseetchemendypage (+ 14 173) "6.6 Proofs without premises (optional)") ;; (find-barwiseetchemendypage (+ 14 176) "7 Conditionals") ;; (find-barwiseetchemendypage (+ 14 178) "7.1 Material conditional symbol: ->") ;; (find-barwiseetchemendypage (+ 14 181) "7.2 Biconditional symbol: <->") ;; (find-barwiseetchemendypage (+ 14 187) "7.3 Conversational implicature") ;; (find-barwiseetchemendypage (+ 14 190) "7.4 Truth-functional completeness (optional)") ;; (find-barwiseetchemendypage (+ 14 196) "7.5 Alternative notation (optional)") ;; (find-barwiseetchemendypage (+ 14 198) "8 The Logic of Conditionals") ;; (find-barwiseetchemendypage (+ 14 198) "8.1 Informal methods of proof") ;; (find-barwiseetchemendypage (+ 14 206) "8.2 Formal rules of proof for -> and <->") ;; (find-barwiseetchemendypage (+ 14 214) "8.3 Soundness and completeness (optional)") ;; (find-barwiseetchemendypage (+ 14 222) "8.4 Valid arguments: some review exercises") ;; (find-barwiseetchemendypage (+ 14 225) "II Quantifiers") ;; (find-barwiseetchemendypage (+ 14 227) "9 Introduction to Quantification") ;; (find-barwiseetchemendypage (+ 14 228) "9.1 Variables and atomic wffs") ;; (find-barwiseetchemendypage (+ 14 230) "9.2 The quantifier symbols: Fa, Ex") ;; (find-barwiseetchemendypage (+ 14 231) "9.3 Wffs and sentences") ;; (find-barwiseetchemendypage (+ 14 234) "9.4 Semantics for the quantifiers") ;; (find-barwiseetchemendypage (+ 14 239) "9.5 The four Aristotelian forms") ;; (find-barwiseetchemendypage (+ 14 243) "9.6 Translating complex noun phrases") ;; (find-barwiseetchemendypage (+ 14 251) "9.7 Quantifiers and function symbols (optional)") ;; (find-barwiseetchemendypage (+ 14 255) "9.8 Alternative notation (optional)") ;; (find-barwiseetchemendypage (+ 14 257) "10 The Logic of Quantifiers") ;; (find-barwiseetchemendypage (+ 14 257) "10.1 Tautologies and quantification") ;; (find-barwiseetchemendypage (+ 14 266) "10.2 First-order validity and consequence") ;; (find-barwiseetchemendypage (+ 14 275) "10.3 First-order equivalence and DeMorgan s laws") ;; (find-barwiseetchemendypage (+ 14 280) "10.4 Other quantifier equivalences (optional)") ;; (find-barwiseetchemendypage (+ 14 283) "10.5 The axiomatic method (optional)") ;; (find-barwiseetchemendypage (+ 14 289) "11 Multiple Quantifiers") ;; (find-barwiseetchemendypage (+ 14 289) "11.1 Multiple uses of a single quantifier") ;; (find-barwiseetchemendypage (+ 14 285) "2. (Null quantification)") ;; (find-barwiseetchemendytext (+ 14 285) "2. (Null quantification)") ;; (find-barwiseetchemendypage (+ 14 293) "11.2 Mixed quantifiers") ;; (find-barwiseetchemendypage (+ 14 298) "11.3 The step-by-step method of translation") ;; (find-barwiseetchemendypage (+ 14 300) "11.4 Paraphrasing English") ;; (find-barwiseetchemendypage (+ 14 304) "11.5 Ambiguity and context sensitivity") ;; (find-barwiseetchemendypage (+ 14 308) "11.6 Translations using function symbols (optional)") ;; (find-barwiseetchemendypage (+ 14 311) "11.7 Prenex form (optional)") ;; (find-barwiseetchemendypage (+ 14 315) "11.8 Some extra translation problems") ;; (find-barwiseetchemendypage (+ 14 319) "12 Methods of Proof for Quantifiers") ;; (find-barwiseetchemendypage (+ 14 319) "12.1 Valid quantifier steps") ;; (find-barwiseetchemendypage (+ 14 322) "12.2 The method of existential instantiation") ;; (find-barwiseetchemendypage (+ 14 323) "12.3 The method of general conditional proof") ;; (find-barwiseetchemendypage (+ 14 329) "12.4 Proofs involving mixed quantifiers") ;; (find-barwiseetchemendypage (+ 14 338) "12.5 Axiomatizing shape (optional)") ;; (find-barwiseetchemendypage (+ 14 342) "13 Formal Proofs and Quantifiers") ;; (find-barwiseetchemendypage (+ 14 342) "13.1 Universal quantifier rules") ;; (find-barwiseetchemendypage (+ 14 347) "13.2 Existential quantifier rules") ;; (find-barwiseetchemendypage (+ 14 352) "13.3 Strategy and tactics") ;; (find-barwiseetchemendypage (+ 14 361) "13.4 Soundness and completeness (optional)") ;; (find-barwiseetchemendypage (+ 14 361) "13.5 Some review exercises (optional)") ;; (find-barwiseetchemendypage (+ 14 364) "14 More about Quantification (optional)") ;; (find-barwiseetchemendypage (+ 14 366) "14.1 Numerical quantification") ;; (find-barwiseetchemendypage (+ 14 374) "14.2 Proving numerical claims") ;; (find-barwiseetchemendypage (+ 14 379) "14.3 The, both, and neither") ;; (find-barwiseetchemendypage (+ 14 383) "14.4 Adding other determiners to fol") ;; (find-barwiseetchemendypage (+ 14 389) "14.5 The logic of generalized quantification") ;; (find-barwiseetchemendypage (+ 14 397) "14.6 Other expressive limitations of first-order logic") ;; (find-barwiseetchemendypage (+ 14 403) "III Applications and Metatheory") ;; (find-barwiseetchemendypage (+ 14 405) "15 First-order Set Theory") ;; (find-barwiseetchemendypage (+ 14 406) "15.1 Naive set theory") ;; (find-barwiseetchemendypage (+ 14 412) "15.2 Singletons, the empty set, subsets") ;; (find-barwiseetchemendypage (+ 14 415) "15.3 Intersection and union") ;; (find-barwiseetchemendypage (+ 14 419) "15.4 Sets of sets") ;; (find-barwiseetchemendypage (+ 14 422) "15.5 Modeling relations in set theory") ;; (find-barwiseetchemendypage (+ 14 427) "15.6 Functions") ;; (find-barwiseetchemendypage (+ 14 429) "15.7 The powerset of a set (optional)") ;; (find-barwiseetchemendypage (+ 14 432) "15.8 Russell s Paradox (optional)") ;; (find-barwiseetchemendypage (+ 14 433) "15.9 Zermelo Frankel set theory zfc (optional)") ;; (find-barwiseetchemendypage (+ 14 442) "16 Mathematical Induction") ;; (find-barwiseetchemendypage (+ 14 443) "16.1 Inductive definitions and inductive proofs") ;; (find-barwiseetchemendypage (+ 14 451) "16.2 Inductive definitions in set theory") ;; (find-barwiseetchemendypage (+ 14 453) "16.3 Induction on the natural numbers") ;; (find-barwiseetchemendypage (+ 14 456) "16.4 Axiomatizing the natural numbers (optional)") ;; (find-barwiseetchemendypage (+ 14 458) "16.5 Proving programs correct (optional)") ;; (find-barwiseetchemendypage (+ 14 468) "17 Advanced Topics in Propositional Logic") ;; (find-barwiseetchemendypage (+ 14 468) "17.1 Truth assignments and truth tables") ;; (find-barwiseetchemendypage (+ 14 470) "17.2 Completeness for propositional logic") ;; (find-barwiseetchemendypage (+ 14 479) "17.3 Horn sentences (optional)") ;; (find-barwiseetchemendypage (+ 14 488) "17.4 Resolution (optional)") ;; (find-barwiseetchemendypage (+ 14 495) "18 Advanced Topics in FOL") ;; (find-barwiseetchemendypage (+ 14 495) "18.1 First-order structures") ;; (find-barwiseetchemendypage (+ 14 500) "18.2 Truth and satisfaction, revisited") ;; (find-barwiseetchemendypage (+ 14 509) "18.3 Soundness for fol") ;; (find-barwiseetchemendypage (+ 14 512) "18.4 The completeness of the shape axioms (optional)") ;; (find-barwiseetchemendypage (+ 14 514) "18.5 Skolemization (optional)") ;; (find-barwiseetchemendypage (+ 14 516) "18.6 Unification of terms (optional)") ;; (find-barwiseetchemendypage (+ 14 519) "18.7 Resolution, revisited (optional)") ;; (find-barwiseetchemendypage (+ 14 526) "19 Completeness and Incompleteness") ;; (find-barwiseetchemendypage (+ 14 527) "19.1 The Completeness Theorem for fol") ;; (find-barwiseetchemendypage (+ 14 529) "19.2 Adding witnessing constants") ;; (find-barwiseetchemendypage (+ 14 531) "19.3 The Henkin theory") ;; (find-barwiseetchemendypage (+ 14 534) "19.4 The Elimination Theorem") ;; (find-barwiseetchemendypage (+ 14 540) "19.5 The Henkin Construction") ;; (find-barwiseetchemendypage (+ 14 546) "19.6 The Lowenheim-Skolem Theorem") ;; (find-barwiseetchemendypage (+ 14 548) "19.7 The Compactness Theorem") ;; (find-barwiseetchemendypage (+ 14 552) "19.8 The Godel Incompleteness Theorem") ;; (find-barwiseetchemendypage (+ 14 557) "Summary of Formal Proof Rules") ;; (find-barwiseetchemendypage (+ 14 557) "Propositional rules") ;; (find-barwiseetchemendypage (+ 14 559) "First-order rules") ;; (find-barwiseetchemendypage (+ 14 561) "Inference Procedures (Con Rules)") ;; (find-barwiseetchemendypage (+ 14 562) "Glossary") ;; (find-barwiseetchemendypage (+ 14 573) "General Index") ;; (find-barwiseetchemendypage (+ 14 585) "Exercise Files Index") ;; (find-barwiseetchemendypage (+ 14 113) "Tautological consequence") ;; «barwise-moss» (to ".barwise-moss") ;; http://gigapedia.org/items/47442/vicious-circles--center-for-the-study-of-language-and-information---lecture-notes- (code-djvu "viccircles" "~/books/__logic/barwise_moss__vicious_circles.djvu") ;; (find-viccirclespage 7 "Contents") ;; (find-viccirclespage (+ 10 385) "Index") ;; «beeson-narboux-wiedijk» (to ".beeson-narboux-wiedijk") ;; (find-books "__logic/__logic.el" "beeson-narboux-wiedijk") (code-pdf-page "prfchkeuc" "~/books/__logic/beeson_narboux_wiedijk__proof-checking_euclid.pdf") (code-pdf-text "prfchkeuc" "~/books/__logic/beeson_narboux_wiedijk__proof-checking_euclid.pdf" 1) ;; (find-prfchkeucpage) ;; (find-prfchkeucpage 1 "Contents") ;; (find-prfchkeucpage (+ 1 189) "Index") ;; (find-prfchkeuctext "") ;; «bell-machover» (to ".bell-machover") (code-djvu "bellmachover" "~/books/__logic/bell_machover__a_course_in_mathematical_logic.djvu") (code-djvutotext "bellmachover" "~/books/__logic/bell_machover__a_course_in_mathematical_logic.djvu") ;; (find-bellmachoverpage 8 "Contents") ;; (find-bellmachoverpage (+ 18 585) "Index") ;; (find-bellmachovertext "") ;; «benthem» (to ".benthem") ;; (find-books "__logic/__logic.el" "benthem") (code-pdf-page "theageofaltlogs" "~/books/__logic/benthem_heinzmann__the_age_of_alternative_logics.pdf") (code-pdf-text "theageofaltlogs" "~/books/__logic/benthem_heinzmann__the_age_of_alternative_logics.pdf" 1) ;; (find-theageofaltlogspage) ;; (find-theageofaltlogspage 1 "Contents") ;; (find-theageofaltlogspage (+ -1 167) "in which structures swim") ;; (find-theageofaltlogstext (+ -1 167) "in which structures swim") ;; (find-theageofaltlogspage (+ 1 189) "Index") ;; (find-theageofaltlogstext "") ;; «bernays» (to ".bernays") (code-djvu "scowbernays" "~/books/__logic/mueller__sets_and_classes_on_the_work_of_paul_bernays.djvu") ;; (find-scowbernayspage 1 "Contents") ;; (find-scowbernayspage (+ 19 1) "1") ;; (find-scowbernayspage (+ 14 353) "Index") ;; «beziau» (to ".beziau") ;; http://gigapedia.com/items/51559/logica-universalis--towards-a-general-theory-of-logic ;; http://gigapedia.com/items/70500/logica-universalis--towards-a-general-theory-of-logic-2nd-ed (code-xpdf "logicauniversalis" "~/books/__logic/beziau__logica_universalis_towards_a_general_theory_of_logic.pdf") ;; (find-logicauniversalispage 5 "Contents") ;; (find-logicauniversalispage (+ -1 169) "The humbug of many logical values") ;; «bierman-depaiva» (to ".bierman-depaiva") ;; (find-books "__logic/__logic.el" "bierman-depaiva") (code-pdf-page "biermandepaiva" "~/books/__logic/bierman_depaiva__on_an_intuitionistic_modal_logic.pdf") (code-pdf-text "biermandepaiva" "~/books/__logic/bierman_depaiva__on_an_intuitionistic_modal_logic.pdf" 1) ;; (find-biermandepaivapage) ;; (find-biermandepaivapage 1 "Contents") ;; (find-biermandepaivapage (+ 1 189) "Index") ;; (find-biermandepaivatext "") ;; «birkedal» (to ".birkedal") ;; https://arxiv.org/abs/2010.13926 ;; https://arxiv.org/pdf/2010.13926.pdf ;; Qian/Kavvos/Birkedal: "Client-Server Sessions in Linear Logic" (code-pdf-page "clislll" "$S/https/arxiv.org/pdf/2010.13926.pdf") (code-pdf-text "clislll" "$S/https/arxiv.org/pdf/2010.13926.pdf") ;; (find-clislllpage) ;; (find-clisllltext) ;; «blok-pigozzi» (to ".blok-pigozzi") ;; (find-books "__logic/__logic.el" "blok-pigozzi") (code-pdf "blokpig" "~/books/__logic/blok_pigozzi__algebraizable_logics.pdf") (code-pdftotext "blokpig" "~/books/__logic/blok_pigozzi__algebraizable_logics.pdf" 1) ;; (find-blokpigpage) ;; (find-blokpigpage 1 "Contents") ;; (find-blokpigpage (+ 1 189) "Index") ;; (find-blokpigtext "") ;; «brown» (to ".brown") ;; (find-books "__logic/__logic.el" "brown") ;; (find-books "__logic/__logic.el" "brown" "proofsandpictures") ;; James Robert Brown: "Proofs and Pictures" ;; http://jwood.faculty.unlv.edu/unlv/Articles/Brown.pdf ;; (find-fline "$S/http/jwood.faculty.unlv.edu/unlv/Articles/") (code-xpdf "proofsandpictures" "$S/http/jwood.faculty.unlv.edu/unlv/Articles/Brown.pdf") (code-pdf-text "proofsandpictures" "$S/http/jwood.faculty.unlv.edu/unlv/Articles/Brown.pdf" -160) ;; (find-proofsandpicturespage) ;; (find-proofsandpicturestext) ;; (find-proofsandpicturespage (+ -160 161) "1 Bolzano's") ;; (find-proofsandpicturestext (+ -160 161) "1 Bolzano's") ;; (find-proofsandpicturespage (+ -160 174) "7 A Kantian objection") ;; (find-proofsandpicturestext (+ -160 174) "7 A Kantian objection") ;; «debruijn» (to ".debruijn") ;; (find-books "__logic/__logic.el" "debruijn") ;; ;; «debruijn-telesc» (to ".debruijn-telesc") ;; (find-books "__logic/__logic.el" "debruijn-telesc") ;; https://doi.org/10.1016/0890-5401(91)90066-B ;; https://dl.acm.org/doi/abs/10.1016/0890-5401%2891%2990066-b (code-pdf-page "debruijntmintlc" "~/books/__logic/de_bruijn__telescopic_mappings_in_typed_lambda_calculus.pdf") (code-pdf-text "debruijntmintlc" "~/books/__logic/de_bruijn__telescopic_mappings_in_typed_lambda_calculus.pdf" 1) ;; (find-debruijntmintlcpage) ;; (find-debruijntmintlcpage 1 "Contents") ;; (find-debruijntmintlcpage (+ 1 189) "Index") ;; (find-debruijntmintlctext "") ;; «bueno» (to ".bueno") ;; (find-books "__logic/__logic.el" "bueno") ;; https://link.springer.com/article/10.1007/s10516-010-9101-4 (code-pdf-page "bueno2ndorder" "~/books/__logic/bueno__a_defense_of_second-order_logic.pdf") (code-pdf-text "bueno2ndorder" "~/books/__logic/bueno__a_defense_of_second-order_logic.pdf" 1) ;; (find-bueno2ndorderpage) ;; (find-bueno2ndorderpage 1 "Contents") ;; (find-bueno2ndorderpage (+ 1 189) "Index") ;; (find-bueno2ndordertext "") ;; «bunder-seldin» (to ".bunder-seldin") ;; (find-books "__logic/__logic.el" "bunder-seldin") ;; http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.88.9497 ;; Bunder/Seldin: Variants of the Basic Calculus of Constructions (code-pdf-page "bunderseldin" "~/books/__logic/bunder_seldin__variants_of_the_basic_calculus_of_constructions.pdf") (code-pdf-text "bunderseldin" "~/books/__logic/bunder_seldin__variants_of_the_basic_calculus_of_constructions.pdf" 1) ;; (find-bunderseldinpage) ;; (find-bunderseldinpage 1 "Contents") ;; (find-bunderseldinpage (+ 1 189) "Index") ;; (find-bunderseldintext "") ;; «carnap» (to ".carnap") (code-djvu "carnapprob" "~/books/__logic/carnap__logical_foundations_of_probability.djvu") (code-djvutotext "carnapprob" "~/books/__logic/carnap__logical_foundations_of_probability.djvu" 25) ;; (find-carnapprobpage) ;; (find-carnapprobpage 21 "Contents") ;; (find-carnapprobpage (+ 17 605) "Index") ;; (find-carnapprobtext "") ;; «carnielli» (to ".carnielli") ;; «carnielli-coniglio» (to ".carnielli-coniglio") ;; (find-books "__logic/__logic.el" "carnielli-coniglio") ;; (find-books "__logic/__logic.el" "carnielli") (code-pdf "cacoparalococo" "~/books/__logic/carnielli_coniglio__paraconsistent_logic_consistency_contradiction_and_negation.pdf") (code-pdftotext "cacoparalococo" "~/books/__logic/carnielli_coniglio__paraconsistent_logic_consistency_contradiction_and_negation.pdf" 23) ;; (find-cacoparalococopage) ;; (find-cacoparalococopage 20 "Contents") ;; (find-cacoparalococopage (+ 19 391) "Index") ;; (find-cacoparalococotext "") (code-pdf-page "cacoasl" "~/books/__logic/carnielli_coniglio_et_al__analysis_and_synthesis_of_logics_how_to_cut_and_paste_reasoning_systems.pdf") (code-pdf-text "cacoasl" "~/books/__logic/carnielli_coniglio_et_al__analysis_and_synthesis_of_logics_how_to_cut_and_paste_reasoning_systems.pdf" 16) ;; (find-cacoaslpage) ;; (find-cacoaslpage 6 "Contents") ;; (find-cacoaslpage (+ 12 579) "Subject Index") ;; (find-cacoasltext "") ;; "Paraconsistent set theory by predicating on consistency" ;; http://www.cle.unicamp.br/prof/coniglio/Carnielli-Coniglio-ParST.pdf (code-pdf-page "cacoparst" "$S/http/www.cle.unicamp.br/prof/coniglio/Carnielli-Coniglio-ParST.pdf") (code-pdf-text "cacoparst" "$S/http/www.cle.unicamp.br/prof/coniglio/Carnielli-Coniglio-ParST.pdf") ;; (find-cacoparstpage) ;; (find-cacoparsttext) ;; «chagrov» (to ".chagrov") ;; (find-books "__logic/__logic.el" "chagrov") ;; (find-LATEX "catsem-u.bib" "bib-ChagrovZakharyaschev") (code-pdf-page "chagrovzml" "~/books/__logic/chagrov_zakharyaschev__modal_logic.pdf") (code-pdf-text "chagrovzml" "~/books/__logic/chagrov_zakharyaschev__modal_logic.pdf" 15) ;; (find-chagrovzmlpage) ;; (find-chagrovzmlpage 11 "Contents") ;; (find-chagrovzmlpage (+ 15 109) "4.1. Superintuitionistic logics") ;; (find-chagrovzmlpage (+ 15 112) "BW_n") ;; (find-chagrovzmlpage (+ 6 597) "Index") ;; (find-chagrovzmltext "") ;; «changkeisler» (to ".changkeisler") ;; http://gigapedia.com/items/155775/model-theory--studies-in-logic-and-the-foundations-of-mathematics- (code-djvu "changkeisler" "~/books/__logic/chang_keisler__model_theory.djvu") ;; (find-changkeislerpage 1 "Contents") ;; (find-changkeislerpage (+ 1 1) "Index") ;; «chew» (to ".chew") ;; Xuanyi Chew: "Closure Calculus is Better than the Pure lambda-Calculus" ;; https://blog.chewxy.com/ ;; https://blog.chewxy.com/wp-content/uploads/personal/dissertation31482.pdf ;; (find-fline "$S/https/blog.chewxy.com/wp-content/uploads/personal/") (code-pdf-page "chew" "$S/https/blog.chewxy.com/wp-content/uploads/personal/dissertation31482.pdf") (code-pdf-text "chew" "$S/https/blog.chewxy.com/wp-content/uploads/personal/dissertation31482.pdf" 1) ;; (find-chewpage) ;; (find-chewtext) ;; (find-chewpage 2 "Contents") ;; (find-chewtext 2 "Contents") ;; (find-chewpage (+ 1 5) "Introduction") ;; (find-chewtext (+ 1 5) "Introduction") ;; «chuaqui» (to ".chuaqui") (code-djvu "chuaqui" "~/books/__logic/chuaqui__axiomatic_set_theory.djvu") ;; (find-chuaquipage 1 "Contents") ;; (find-chuaquipage (+ 1 1) "Index") ;; «ciabattoni-ferrari» (to ".ciabattoni-ferrari") ;; (find-books "__logic/__logic.el" "ciabattoni-ferrari") ;; Hypersequent Calculi for some Intermediate Logics with Bounded Kripke Models ;; https://academic.oup.com/logcom/article-abstract/11/2/283/936181 ;; https://doi.org/10.1093/logcom/11.2.283 ;; https://www.logic.at/staff/agata/publications.html ;; https://www.logic.at/staff/agata/jlc2000.pdf ;; (find-fline "$S/https/www.logic.at/staff/agata/") (code-pdf-page "boundedkripkemodels" "$S/https/www.logic.at/staff/agata/jlc2000.pdf") (code-pdf-text "boundedkripkemodels" "$S/https/www.logic.at/staff/agata/jlc2000.pdf") ;; (find-boundedkripkemodelspage) ;; (find-boundedkripkemodelstext) ;; (find-boundedkripkemodelspage 5 "3 Logics of Bounded Width Kripke Models") ;; (find-boundedkripkemodelstext 5 "3 Logics of Bounded Width Kripke Models") ;; «coniglio» (to ".coniglio") ;; Coniglio: "Recovering a logic from its fragments by meta-fibring" ;; http://www.cle.unicamp.br/prof/coniglio/CombSEQ-final.pdf ;; «conway» (to ".conway") ;; http://gigapedia.com/items/67259/on-numbers-and-games--l-m-s--monographs---no--6- ;; http://gigapedia.com/items/20515/the-book-of-numbers (code-djvu "onag" "~/books/__logic/conway__on_numbers_and_games.djvu") (code-djvu "bookofnumbers" "~/books/__logic/conway_guy__the_book_of_numbers.djvu") ;; (find-onagpage 9 "Contents") ;; (find-onagpage (+ 5 231) "Index") ;; (find-bookofnumberspage 6 "Contents") ;; (find-bookofnumberspage 301 "Index") ;; «copi» (to ".copi") ;; (find-books "__logic/__logic.el" "copi") (code-djvu "copipt" "~/books/__logic/copi__introducao_a_logica.djvu") (code-djvutotext "copipt" "~/books/__logic/copi__introducao_a_logica.djvu" 1) ;; (find-copiptpage) ;; (find-copiptpage 1 "Contents") ;; (find-copiptpage (+ 3 477) "Index") ;; (find-copipttext "") (code-pdf "copien" "~/books/__logic/copi__introduction_to_logic.pdf") (code-pdftotext "copien" "~/books/__logic/copi__introduction_to_logic.pdf" 1) ;; (find-copienpage) ;; (find-copienpage 1 "Contents") ;; (find-copienpage (+ 1 189) "Index") ;; (find-copientext "") ;; «coquand» (to ".coquand") ;; (find-books "__logic/__logic.el" "coquand") ;; "A New Paradox in Type Theory" (1994) ;; http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.53.4920 (code-pdf-page "coquandnptt" "~/books/__logic/coquand__a_new_paradox_in_type_theory.pdf") (code-pdf-text "coquandnptt" "~/books/__logic/coquand__a_new_paradox_in_type_theory.pdf" 1) ;; (find-coquandnpttpage) ;; (find-coquandnpttpage 1 "Contents") ;; (find-coquandnpttpage (+ 1 189) "Index") ;; (find-coquandnptttext "") ;; «coquand-huet» (to ".coquand-huet") ;; (find-books "__logic/__logic.el" "coquand-huet") ;; Coquand/Huet: "The Calculus of Constructions" ;; Information and Computation 76, 95-120 (1988) ;; https://core.ac.uk/download/pdf/82038778.pdf ;; (find-fline "$S/https/core.ac.uk/download/pdf/") (code-pdf-page "coquandhuet" "$S/https/core.ac.uk/download/pdf/82038778.pdf") (code-pdf-text "coquandhuet" "$S/https/core.ac.uk/download/pdf/82038778.pdf" -94) ;; (find-coquandhuetpage) ;; (find-coquandhuettext) ;; (find-coquandhuetpage (+ -94 95) "1. THE ABSTRACT" "SYNTAX OF TERMS") ;; (find-coquandhuettext (+ -94 95) "1. THE ABSTRACT" "SYNTAX OF TERMS") ;; (find-coquandhuetpage (+ -94 98) "2. A FIRST ATTEMPT" "AT A CONSTRUCTION" "CALCULUS") ;; (find-coquandhuettext (+ -94 98) "2. A FIRST ATTEMPT" "AT A CONSTRUCTION" "CALCULUS") ;; (find-coquandhuetpage (+ -94 101) "3. THE CALCULUS WITH CONVERSION RULES") ;; (find-coquandhuettext (+ -94 101) "3. THE CALCULUS WITH CONVERSION RULES") ;; (find-coquandhuetpage (+ -94 105) "4." "STRIPPING") ;; (find-coquandhuettext (+ -94 105) "4." "STRIPPING") ;; (find-coquandhuetpage (+ -94 107) "5. AN INTERPRETATION" "OF CONSTRUCTIONS") ;; (find-coquandhuettext (+ -94 107) "5. AN INTERPRETATION" "OF CONSTRUCTIONS") ;; (find-coquandhuetpage (+ -94 111) "6. VARIATIONS" "ON THE BASIC CALCULUS") ;; (find-coquandhuettext (+ -94 111) "6. VARIATIONS" "ON THE BASIC CALCULUS") ;; (find-coquandhuetpage (+ -94 113) "7. TOWARDS" "A REASONABLE" "USER INTERFACE") ;; (find-coquandhuettext (+ -94 113) "7. TOWARDS" "A REASONABLE" "USER INTERFACE") ;; (find-coquandhuetpage (+ -94 113) "7.1. Introducing Constants") ;; (find-coquandhuettext (+ -94 113) "7.1. Introducing Constants") ;; (find-coquandhuetpage (+ -94 113) "7.2. Synthesis of Implicit Arguments") ;; (find-coquandhuettext (+ -94 113) "7.2. Synthesis of Implicit Arguments") ;; (find-coquandhuetpage (+ -94 116) "8. POSSIBLE EXTENSTIONS") ;; (find-coquandhuettext (+ -94 116) "8. POSSIBLE EXTENSTIONS") ;; «corcoran» (to ".corcoran") ;; (find-books "__logic/__logic.el" "corcoran") ;; John Corcoran: "Aristotle's Prototype Rule-Based Underlying Logic" (LU, 2018) ;; https://doi.org/10.1007/s11787-018-0189-4 (code-pdf-page "corcoran2018" "~/books/__logic/corcoran2018.pdf") (code-pdf-text "corcoran2018" "~/books/__logic/corcoran2018.pdf" 1) ;; (find-corcoran2018page) ;; (find-corcoran2018page 1 "Contents") ;; (find-corcoran2018page (+ 1 189) "Index") ;; (find-corcoran2018text "") ;; «corcoran-alaimi» (to ".corcoran-alaimi") ;; John Corcoran (ed.): "Ancient Logic and Its Modern Interpretations" (1974) ;; https://philarchive.org/rec/CORALA ;; https://philarchive.org/archive/CORALA ;; (find-fline "$S/https/philarchive.org/archive/") (code-pdf-page "alaimi" "$S/https/philarchive.org/archive/CORALA") (code-pdf-text "alaimi" "$S/https/philarchive.org/archive/CORALA" 8) ;; (find-alaimipage) ;; (find-alaimitext) ;; (find-alaimipage (+ 8 3) "Norman Kretzmann / Aristotle on Spoken Sound Signi1icant by Convention") ;; (find-alaimipage (+ 7 23) "Ronald Zirin / Inarticulate Noises") ;; (find-alaimipage (+ 6 27) "Newton Garver / Notes for a Linguistic Reading of the Categories") ;; (find-alaimipage (+ 5 35) "Ian Mueller / Greek Mathematics and Greek Logic") ;; (find-alaimipage (+ 5 71) "John Mulhern / Modem Notations and Ancient Logic") ;; (find-alaimipage (+ 4 85) "John Corcoran / Aristotle's Natural Deduction System") ;; (find-alaimipage (+ 3 133) "Mary Mulhern / Corcoran on Aristotle's Logical Theory") ;; (find-alaimipage (+ 2 151) "Josiah Gould / Deduction in Stoic Logic") ;; (find-alaimipage (+ 2 169) "John Corcoran / Remarks on Stoic Deduction") ;; (find-alaimipage (+ 0 185) "John Corcoran / Future Research on Ancient Theories or Communication and Reasoning") ;; (find-alaimipage (+ -1 189) "A Panel Discussion on Future Research in Ancient Logical Theory") ;; (find-alaimipage (+ -1 209) "INDEX OF NAMES") ;; John Corcoran: "Aristotle's Natural Deduction System" (1974) ;; https://philarchive.org/rec/CORAND ;; https://philarchive.org/archive/CORAND (code-pdf-page "corcoranands" "$S/https/philarchive.org/archive/CORAND") (code-pdf-text "corcoranands" "$S/https/philarchive.org/archive/CORAND") ;; (find-corcoranandspage) ;; (find-corcoranandstext) ;; «crossley-dummett» (to ".crossley-dummett") ;; (find-books "__logic/__logic.el" "crossley-dummett") (code-pdf-page "formalsrfp" "~/books/__logic/crossley_dummett__formal_systems_and_recursive_functions_proceedings_of_the_eighth_logic_colloquium_oxford_july_1963.pdf") (code-pdf-text "formalsrfp" "~/books/__logic/crossley_dummett__formal_systems_and_recursive_functions_proceedings_of_the_eighth_logic_colloquium_oxford_july_1963.pdf" 3) ;; (find-formalsrfppage) ;; (find-formalsrfppage 1 "Contents") ;; (find-formalsrfppage (+ 3 92) "SEMANTICAL ANALYSIS OF INTUITIONISTIC LOGIC I") ;; (find-formalsrfptext (+ 3 92) "SEMANTICAL ANALYSIS OF INTUITIONISTIC LOGIC I") ;; (find-formalsrfppage (+ 3 92) "KRIPKE") ;; (find-formalsrfptext (+ 3 92) "KRIPKE") ;; (find-formalsrfppage (+ 1 304) "Wang") ;; (find-formalsrfptext "") ;; «curry» (to ".curry") ;; http://gigapedia.com/items/126830/foundations-of-mathematical-logic ;; http://gigapedia.com/items/259486/combinatory-logic--volumes-i-and-ii--studies-in-logic-and-the-foundations-of-mathematics- (code-djvu "curryfound" "~/books/__logic/curry__foundations_of_mathematical_logic.djvu") ;; (find-curryfoundpage 7 "Contents") ;; (find-curryfoundpage (+ 9 391) "Index") (code-djvu "curryfeys1" "~/books/__logic/curry_feys__combinatory_logic_vol_1.djvu") ;; (find-curryfeys1page 1 "Contents") ;; (find-curryfeys1page (+ 7 397) "Index") ;; «dagostino» (to ".dagostino") ;; (find-books "__logic/__logic.el" "dagostino") ;; https://www.researchgate.net/publication/221350906_Classical_Natural_Deduction (code-pdf-page "dagostinocnd" "~/books/__logic/dagostino__classical_natural_deduction.pdf") (code-pdf-text "dagostinocnd" "~/books/__logic/dagostino__classical_natural_deduction.pdf" -427) ;; (find-dagostinocndpage) ;; (find-dagostinocndtext) ;; (find-dagostinocndpage (+ -427 429) "1 Introduction") ;; (find-dagostinocndtext (+ -427 429) "1 Introduction") ;; (find-dagostinocndpage (+ -427 438) "non-intuitionistic de Morgan law") ;; (find-dagostinocndtext (+ -427 438) "non-intuitionistic de Morgan law") ;; (find-dagostinocndpage (+ -427 439) "A tableau proof of the non-intuitionistic de Morgan Law") ;; (find-dagostinocndtext (+ -427 439) "A tableau proof of the non-intuitionistic de Morgan Law") ;; (find-dagostinocndtext "") ;; «damas» (to ".damas") ;; (find-books "__logic/__logic.el" "damas") ;; Luis Damas: "Type Assignment in Programming Languages" (PhD Thesis, 1984) ;; http://prl.ccs.neu.edu/img/d-thesis-1984.pdf ;; (find-fline "$S/http/prl.ccs.neu.edu/img/") (code-pdf-page "damasphd" "$S/http/prl.ccs.neu.edu/img/d-thesis-1984.pdf") (code-pdf-text "damasphd" "$S/http/prl.ccs.neu.edu/img/d-thesis-1984.pdf" 6) ;; (find-damasphdpage) ;; (find-damasphdtext) ;; (find-damasphdpage 5 "Table of Contents") ;; (find-damasphdtext 5 "Table of Contents") ;; (find-damasphdpage (+ 6 1) "Introduction") ;; (find-damasphdpage (+ 7 14) "1. A type inference system for an applicative language") ;; (find-damasphdpage (+ 7 14) "1.1. Introduction") ;; (find-damasphdpage (+ 7 16) "1.2. Expressions") ;; (find-damasphdpage (+ 7 18) "1.3. Types") ;; (find-damasphdpage (+ 7 20) "1.4. Semantics") ;; (find-damasphdpage (+ 7 26) "1.5. Type inference") ;; (find-damasphdpage (+ 7 35) "1.6. A type assignment algorithm") ;; (find-damasphdpage (+ 7 42) "1.7. Principal types and completeness of T") ;; (find-damasphdpage (+ 7 48) "1.8. Type schemes, assumption schemes and type inference") ;; (find-damasphdpage (+ 7 59) "1.9. Type assignment and overloading") ;; (find-damasphdpage (+ 8 65) "2. A type scheme inference system") ;; (find-damasphdpage (+ 8 65) "2.1. Introduction") ;; (find-damasphdpage (+ 8 66) "2.2. Preliminaries") ;; (find-damasphdpage (+ 8 68) "2.3. Type inference") ;; (find-damasphdpage (+ 8 72) "2.4. The type assignment algorithm W") ;; (find-damasphdpage (+ 8 74) "2.5. The completeness of W and principal type schemes") ;; (find-damasphdpage (+ 8 84) "2.6. Comparison with the inference system of chapter I") ;; (find-damasphdpage (+ 9 88) "3. References to a store and type inference") ;; (find-damasphdpage (+ 9 88) "3.1. Introduction") ;; (find-damasphdpage (+ 9 92) "3.2. The language and its semantics") ;; (find-damasphdpage (+ 9 94) "3.3. Types, type schemes and their semantics") ;; (find-damasphdpage (+ 9 107) "3.4. Type inference") ;; (find-damasphdpage (+ 9 115) "3.5. A type assignment algorithm") ;; (find-damasphdpage (+ 9 118) "3.6. Weak polymorphism and programming examples") ;; (find-damasphdpage (+ 10 124) "4. Conclusions and directions for further research") ;; (find-damasphdpage (+ 10 127) "References") ;; «davis» (to ".davis") ;; http://gigapedia.com/items/135960/engines-of-logic--or-the-universal-computer---mathematicians-and-the-origin-of-the-computer (code-djvu "enginesoflogic" "~/books/__logic/davis__engines_of_logic.djvu") ;; (find-enginesoflogicpage 6 "Contents") ;; (find-enginesoflogicpage (+ 11 249) "Index") ;; «degroote-hindley» (to ".degroote-hindley") ;; http://gigapedia.com/items/114823/typed-lambda-calculi-and-applications--third-international-conference-on-typed-lambda-calculi-and-applications--tlca---039-97--nancy--france--april-2-4--1997-------lecture-notes-in-computer-science- (code-xpdf "tlca97" "~/books/__logic/de_groote_hindley__tlca_97.pdf") ;; (find-tlca97page 6 "Contents") ;; (find-tlca97page (+ 7 82) "Torben Brauner" "A simple adequate categorical model for PCF") ;; (find-tlca97page (+ 7 164) "Neil Ghani" "Eta-expansions in Dependent Type Theory") ;; (find-tlca97page (+ 7 181) "Martini/Masini") ;; (find-tlca97page (+ 7 354) "Takeuti, Izumi" "An Axiomatic System of Parametricity") ;; (find-tlca97page (+ 7 373) "Urzyczyn") ;; «devlin» (to ".devlin") ;; http://gigapedia.com/items/119048/the-joy-of-sets--fundamentals-of-contemporary-set-theory--undergraduate-texts-in-mathematics---second-edition (code-djvu "devlin" "~/books/__logic/devlin__the_joy_of_sets.djvu") ;; (find-devlinpage 10 "Contents") ;; (find-devlinpage (+ 11 189) "Index") ;; «dore» (to ".dore") ;; (find-books "__logic/__logic.el" "dore") ;; Maximilian Doré: "Constructivity in Homotopy Type Theory" ;; https://www.cs.ox.ac.uk/people/maximilian.dore/master.pdf (code-pdf-page "dore" "$S/https/www.cs.ox.ac.uk/people/maximilian.dore/master.pdf") (code-pdf-text "dore" "$S/https/www.cs.ox.ac.uk/people/maximilian.dore/master.pdf") ;; (find-dorepage) ;; (find-doretext) ;; (find-dorepage (+ 3 2) "constructivity in the \"algorithmic\" sense") ;; (find-doretext (+ 3 2) "constructivity in the \"algorithmic\" sense") ;; (find-dorepage (+ 3 2) "\"intuitionistic\" sense") ;; (find-doretext (+ 3 2) "\"intuitionistic\" sense") ;; «dummett» (to ".dummett") ;; (find-books "__logic/__logic.el" "dummett") ;; (find-LATEX "catsem-u.bib" "bib-Dummett") (code-pdf-page "dummettei" "~/books/__logic/dummett__elements_of_intuitionism_2nd_ed.pdf") (code-pdf-text "dummettei" "~/books/__logic/dummett__elements_of_intuitionism_2nd_ed.pdf" 14) ;; (find-dummetteipage) ;; (find-dummetteipage 13 "Contents") ;; (find-dummetteipage (+ 14 1) "Introductory remarks") ;; (find-dummetteipage (+ 14 6) "1. Preliminaries") ;; (find-dummetteipage (+ 14 8) "1.2. The meaning of the logical constants") ;; (find-dummetteipage (+ 14 14) "Domains of quantification") ;; (find-dummetteipage (+ 14 21) "1.4." "Rieger-Nishimura") ;; (find-dummetteipage (+ 14 88) "4. The formalization of intuitionistic logic") ;; (find-dummetteipage (+ 14 88) "4.1. Natural Deduction") ;; (find-dummetteipage (+ 14 89) "logical rules") ;; (find-dummetteipage (+ 14 96) "4.2. The sequent calculus") ;; (find-dummetteipage (+ 14 328) "Index") ;; (find-dummetteitext "") ;; «ebbinghaus» (to ".ebbinghaus") ;; (find-books "__logic/__logic.el" "ebbinghaus") (code-pdf-page "ebbinghaus" "~/books/__logic/ebbinghaus__mathematical_logic.pdf") (code-pdf-text "ebbinghaus" "~/books/__logic/ebbinghaus__mathematical_logic.pdf" 9) (find-pdf-page "~/books/__logic/ebbinghaus__mathematical_logic_lista02.pdf" 1) ;; (find-ebbinghauspage) ;; (find-ebbinghauspage 7 "Contents") ;; (find-ebbinghauspage (+ 9 3) "1. Introduction") ;; (find-ebbinghauspage (+ 7 27) "3. Semantics of first-order languages") ;; (find-ebbinghauspage (+ -1 283) "Index") ;; (find-ebbinghaustext "") ;; «enderton» (to ".enderton") ;; http://www.math.ucla.edu/~hbe/amil/ ;; http://gigapedia.com/items/35707/a-mathematical-introduction-to-logic--2nd-edition ;; http://gigapedia.com/items/10671/elements-of-set-theory (code-djvu "enderton" "~/books/__logic/enderton__a_mathematical_introduction_to_logic.djvu") (code-djvu "endertonst" "~/books/__logic/enderton__elements_of_set_theory.djvu") ;; (find-endertonpage 4 "Contents") ;; (find-endertonpage (+ 9 311) "Index") ;; (find-endertonstpage 4 "Contents") ;; (find-endertonstpage (+ 10 273) "Index") ;; «farmer» (to ".farmer") ;; (find-books "__logic/__logic.el" "farmer") ;; (find-angg ".emacs.papers" "farmer") ;; «farmer-chiron» (to ".farmer-chiron") ;; (find-books "__logic/__logic.el" "farmer-chiron") ;; Chiron: A Set Theory with Types, Undefinedness, Quotation, and Evaluation ;; https://arxiv.org/abs/1305.6206 ;; https://arxiv.org/pdf/1305.6206.pdf (code-pdf-page "farmerchiron" "$S/https/arxiv.org/pdf/1305.6206.pdf") (code-pdf-text "farmerchiron" "$S/https/arxiv.org/pdf/1305.6206.pdf") ;; (find-farmerchironpage) ;; (find-farmerchirontext) ;; «feferman» (to ".feferman") ;; (find-books "__logic/__logic.el" "feferman") ;; https://link.springer.com/article/10.1007/s11229-011-9985-6 (code-pdf-page "andsoon" "~/books/__logic/feferman__and_so_on_reasoning_with_infinite_diagrams.pdf") (code-pdf-text "andsoon" "~/books/__logic/feferman__and_so_on_reasoning_with_infinite_diagrams.pdf" -370) ;; (find-andsoonpage) ;; (find-andsoontext "") ;; (find-andsoonpage (+ -370 381) "Jamnik") ;; (find-andsoontext (+ -370 381) "Jamnik") ;; «fenstadt» (to ".fenstadt") ;; http://gigapedia.com/items/124942/introduction-to-metamathematics--bibliotheca-mathematica---bibliotheca-mathematica- ;; http://gigapedia.com/items/259363/proceedings-of-the-second-scandinavian-logic-symposium--studies-in-logic-and-the-foundations-of-mathematics- (code-xpdf "2ndscandlogsymp" "~/books/__logic/fenstad_ed__proceedings_of_the_second_scandinavian_logic_symposium.pdf") ;; (find-2ndscandlogsymppage (+ 4 1) "On the decision problems...") ;; (find-2ndscandlogsymppage (+ 1 1) "Index") ;; (find-2ndscandlogsymppage (+ 3 63) "Girard") ;; (find-2ndscandlogsymppage (+ 3 179) "Martin-Löf") ;; (find-2ndscandlogsymppage (+ 2 217) "Martin-Löf") ;; (find-2ndscandlogsymppage (+ 1 235) "Prawitz") ;; (find-2ndscandlogsymppage (+ 0 309) "Quine") ;; (find-2ndscandlogsymppage (+ -2 369) "Troelstra") ;; «ferreira» (to ".ferreira") ;; (find-books "__logic/__logic.el" "ferreira") ;; https://mail.google.com/mail/u/0/#inbox/FMfcgzGwJckHGQWmzRFJhgVVLXRTQChS ;; https://langsci-press.org/catalog/book/200 Curso de semântica formal - Marcelo Ferreira (code-pdf-page "semfor" "~/books/__logic/ferreira__curso_de_semantica_formal.pdf") (code-pdf-text "semfor" "~/books/__logic/ferreira__curso_de_semantica_formal.pdf" 14) ;; (find-semforpage) ;; (find-semforpage 5 "Sumário") ;; (find-semforpage (+ 1 189) "Index") ;; (find-semfortext "") ;; (find-semforpage (+ 14 1) "1 Significado e condições de verdade") ;; (find-semforpage (+ 14 1) "1.1 Significado, verdade e mundo") ;; (find-semforpage (+ 14 3) "1.2 Relações semânticas entre sentenças") ;; (find-semforpage (+ 14 5) "1.3 Composicionalidade") ;; (find-semforpage (+ 14 9) "1.4 Linguagem objeto e metalinguagem") ;; (find-semforpage (+ 14 10) "1.5 Extensões") ;; (find-semforpage (+ 14 18) "1.6 Além de extensões e condições de verdade") ;; (find-semforpage (+ 14 22) "Sugestões de leitura") ;; (find-semforpage (+ 14 23) "Exercícios") ;; (find-semforpage (+ 14 27) "2 Predicação") ;; (find-semforpage (+ 14 27) "2.1 Funções e a notação lambda") ;; (find-semforpage (+ 14 27) "2.1.1 Funções") ;; (find-semforpage (+ 14 29) "2.1.2 Conjuntos e funções características") ;; (find-semforpage (+ 14 31) "2.1.3 Funções, conjuntos e predicados") ;; (find-semforpage (+ 14 31) "2.2 Verbos intransitivos e aplicação funcional") ;; (find-semforpage (+ 14 34) "2.3 Verbos transitivos") ;; (find-semforpage (+ 14 37) "2.4 Tipos e domínios semânticos") ;; (find-semforpage (+ 14 39) "2.5 Verbos bitransitivos") ;; (find-semforpage (+ 14 41) "2.6 Predicados não verbais") ;; (find-semforpage (+ 14 45) "2.7 Relações, funções e currying") ;; (find-semforpage (+ 14 47) "Apêndice: mais sobre conversões lambda e alfa") ;; (find-semforpage (+ 14 51) "Sugestões de leitura") ;; (find-semforpage (+ 14 51) "Exercícios") ;; (find-semforpage (+ 14 55) "3 Coordenação e negação") ;; (find-semforpage (+ 14 55) "3.1 Coordenação") ;; (find-semforpage (+ 14 59) "3.2 A flexibilidade da coordenação") ;; (find-semforpage (+ 14 66) "3.3 Negação") ;; (find-semforpage (+ 14 71) "Sugestões de leitura") ;; (find-semforpage (+ 14 71) "Exercícios") ;; (find-semforpage (+ 14 75) "4 Referência") ;; (find-semforpage (+ 14 75) "4.1 Descrições definidas") ;; (find-semforpage (+ 14 77) "4.1.1 Unicidade") ;; (find-semforpage (+ 14 80) "4.2 Nomes próprios") ;; (find-semforpage (+ 14 83) "4.2.1 Nomes próprios como predicados") ;; (find-semforpage (+ 14 86) "4.3 Pronomes") ;; (find-semforpage (+ 14 93) "Sugestões de leitura") ;; (find-semforpage (+ 14 93) "Exercícios") ;; (find-semforpage (+ 14 97) "5 Modificação nominal") ;; (find-semforpage (+ 14 97) "5.1 Modificadores nominais") ;; (find-semforpage (+ 14 98) "5.2 Sintagmas adjetivais") ;; (find-semforpage (+ 14 101) "5.3 Mudança de tipos") ;; (find-semforpage (+ 14 103) "5.4 Conjunção funcional") ;; (find-semforpage (+ 14 105) "5.5 Modificação e classes de comparação") ;; (find-semforpage (+ 14 107) "5.6 Orações relativas") ;; (find-semforpage (+ 14 113) "5.6.1 Vestígios e movimento sintático") ;; (find-semforpage (+ 14 116) "Sugestões de leitura") ;; (find-semforpage (+ 14 117) "Exercícios") ;; (find-semforpage (+ 14 119) "6 Quantificação nominal") ;; (find-semforpage (+ 14 119) "6.1 Expressões quantificadoras e indivíduos") ;; (find-semforpage (+ 14 122) "6.2 Quantificadores generalizados") ;; (find-semforpage (+ 14 124) "6.3 Determinantes quantificadores") ;; (find-semforpage (+ 14 128) "6.4 De volta aos nomes próprios e às descrições definidas") ;; (find-semforpage (+ 14 130) "6.5 Outros DPs quantificadores") ;; (find-semforpage (+ 14 133) "6.6 Coordenação de DPs") ;; (find-semforpage (+ 14 137) "6.7 Conservatividade: um universal semântico") ;; (find-semforpage (+ 14 143) "6.8 Quantificação e escopo") ;; (find-semforpage (+ 14 143) "6.8.1 DPs quantificadores em posição de objeto") ;; (find-semforpage (+ 14 144) "6.8.2 Interação de escopo entre DPs") ;; (find-semforpage (+ 14 145) "6.8.3 Negação e escopo") ;; (find-semforpage (+ 14 146) "6.9 Quantificação e movimento") ;; (find-semforpage (+ 14 149) "6.9.1 Movimento e escopo") ;; (find-semforpage (+ 14 153) "6.9.2 Negação e alçamento de quantificadores") ;; (find-semforpage (+ 14 158) "6.10 Quantificação e mudança de tipos") ;; (find-semforpage (+ 14 160) "6.10.1 Mudança de tipos e escopo") ;; (find-semforpage (+ 14 163) "6.10.2 Mudança de tipos, negação e escopo") ;; (find-semforpage (+ 14 165) "Sugestões de leitura") ;; (find-semforpage (+ 14 166) "Exercícios") ;; (find-semforpage (+ 14 169) "7 De volta aos pronomes") ;; (find-semforpage (+ 14 169) "7.1 Pronomes livres e ligados") ;; (find-semforpage (+ 14 170) "7.2 Correferência vs. ligação") ;; (find-semforpage (+ 14 173) "7.3 Ligação sem índices nem atribuições") ;; (find-semforpage (+ 14 178) "7.3.1 Limitando composição e ligação funcional") ;; (find-semforpage (+ 14 180) "7.3.2 Pronomes livres novamente") ;; (find-semforpage (+ 14 181) "Sugestões de leitura") ;; (find-semforpage (+ 14 182) "Exercícios") ;; (find-semforpage (+ 14 183) "Referências Bibliográficas") ;; «fitting» (to ".fitting") ;; http://gigapedia.com/items/255507/intuitionistic-logic--model-theory-and-forcing--studies-in-logic-and-the-foundations-of-mathematics- (code-xpdf "fittingforcing" "~/books/__logic/fitting__intuitionistic_logic_model_theory_and_forcing.pdf") ;; (find-fittingforcingpage 8 "Chapter 1") ;; (find-fittingforcingpage (+ -14 190) "Index") ;; «flower-masthoff-stapleton» (to ".flower-masthoff-stapleton") ;; (find-books "__logic/__logic.el" "flower-masthoff-stapleton") (code-pdf-page "genrps" "~/books/__logic/flower_masthoff_stapleton__generating_readable_proofs_a_heuristic_approach_to_theorem_proving_with_spider_diagrams.pdf") (code-pdf-text "genrps" "~/books/__logic/flower_masthoff_stapleton__generating_readable_proofs_a_heuristic_approach_to_theorem_proving_with_spider_diagrams.pdf" 1) ;; (find-genrpspage) ;; (find-genrpstext "") ;; (find-genrpspage (+ -165 180) "Jamnik") ;; (find-genrpstext (+ -165 180) "Jamnik") ;; «frade» (to ".frade") ;; (find-books "__logic/__logic.el" "frade") ;; Maria Joao Frade: "Calculus of Inductive Constructions" ;; http://www4.di.uminho.pt/~mjf/ ;; http://www4.di.uminho.pt/~mjf/pub/SFV-CIC-2up.pdf (code-pdf-page "frade" "$S/http/www4.di.uminho.pt/~mjf/pub/SFV-CIC-2up.pdf") (code-pdf-text "frade" "$S/http/www4.di.uminho.pt/~mjf/pub/SFV-CIC-2up.pdf") ;; (find-fradepage) ;; (find-fradetext) ;; «fraenkel» (to ".fraenkel") ;; http://gigapedia.com/items/255513/abstract-set-theory--studies-in-logic-and-the-foundations-of-mathematics- (code-xpdf "fraenkelast" "~/books/__logic/fraenkel__abstract_set_theory.pdf") ;; (find-fraenkelastpage 1 "Contents") ;; (find-fraenkelastpage (+ 1 1) "Index") ;; «fraser» (to ".fraser") ;; (find-books "__logic/__logic.el" "fraser") (code-pdf-page "frasergbaf" "~/books/__logic/fraser__go_back_to_an-fang.pdf") (code-pdf-text "frasergbaf" "~/books/__logic/fraser__go_back_to_an-fang.pdf" 1) ;; (find-frasergbafpage) ;; (find-frasergbafpage 24 "0.4 An-Fang: introduction to ludics") ;; (find-frasergbaftext 24 "0.4 An-Fang: introduction to ludics") ;; (find-frasergbafpage 1 "Contents") ;; (find-frasergbafpage (+ 1 189) "Index") ;; (find-frasergbaftext "") ;; «gabbay» (to ".gabbay") ;; http://gigapedia.com/items/120096/labelled-deductive-systems--volume-1--oxford-logic-guides- (code-djvu "gabbaylds1" "~/books/__logic/gabbay__labelled_deductive_systems_vol_1.djvu") (code-djvutotext "gabbaylds1" "~/books/__logic/gabbay__labelled_deductive_systems_vol_1.djvu") ;; (find-gabbaylds1page 11 "Contents") ;; (find-gabbaylds1page (+ 14 1) "1. What is a logical system?") ;; (find-gabbaylds1page (+ 14 10) "Surgical cut") ;; (find-gabbaylds1page (+ 14 141) "3. Introducing Algebraic Labelled Deductive Systems") ;; (find-gabbaylds1page (+ 14 159) "Diagram rule") ;; (find-gabbaylds1page (+ 14 160) "Quantifier elimination and introduction rules") ;; (find-gabbaylds1page (+ 14 161) "proof from a database") ;; (find-gabbaylds1page (+ 14 176) "3.3. Introduction rules: a discussion") ;; (find-gabbaylds1page (+ 14 198) "3.5. The metabox system") ;; (find-gabbaylds1page (+ 14 251) "defeasible") ;; (find-gabbaylds1page (+ 14 321) "Micro-PROLOG") ;; (find-gabbaylds1page (+ 14 323) "6.5. Metalevel features via connectives") ;; (find-gabbaylds1page (+ 14 375) "8. Extending the Curry-Howard Interpretation to LDS Systems") ;; (find-gabbaylds1page (+ 14 493) "Index") ;; (find-gabbaylds1text "") ;; (find-books "__logic/__logic.el" "gabbay") (code-pdf "siihil" "~/books/__logic/gabbay__semantical_investigations_in_heytings_intuitionistic_logic.pdf") (code-pdftotext "siihil" "~/books/__logic/gabbay__semantical_investigations_in_heytings_intuitionistic_logic.pdf" 10) ;; (find-siihilpage) ;; (find-siihilpage 7 "Contents") ;; (find-siihilpage (+ 10 1) "Introduction") ;; (find-siihilpage (+ 10 285) "Index") ;; (find-siihiltext "") ;; «gentzen» (to ".gentzen") ;; (find-books "__logic/__logic.el" "gentzen") ;; (find-LATEX "catsem-u.bib" "bib-Gentzen") (code-pdf-page "gentzenpapers" "~/books/__logic/gentzen__the_collected_papers.pdf") (code-pdf-text "gentzenpapers" "~/books/__logic/gentzen__the_collected_papers.pdf" 7) ;; (find-gentzenpaperspage 5 "Contents") ;; (find-gentzenpaperspage (+ 7 68) "Investigations into logical deduction") ;; (find-gentzenpaperspage (+ 7 74) "11. THE CALCULUS OF NATURAL DEDUCTION") ;; (find-gentzenpaperstext (+ 7 74) "11. THE CALCULUS OF NATURAL DEDUCTION") ;; (find-gentzenpaperspage (+ 7 77) "The inference figure schemata:") ;; (find-gentzenpaperstext (+ 7 77) "The inference figure schemata:") ;; (find-gentzenpaperspage (+ 7 78) "Informal sense of NJ-inference figures") ;; (find-gentzenpaperstext (+ 7 78) "Informal sense of NJ-inference figures") ;; (find-gentzenpaperspage (+ 7 79) "The three examples of" "5 1" "as NJ-derivations") ;; (find-gentzenpaperstext (+ 7 79) "The three examples of" "5 1" "as NJ-derivations") ;; (find-gentzenpaperspage (+ 7 324) "Index of subjects") ;; (find-gentzenpaperstext (+ 7 74) "") ;; «geuvers» (to ".geuvers") ;; (find-books "__logic/__logic.el" "geuvers") (code-pdf "geuversndgraphs" "~/books/__logic/geuvers_loeb__natural_deduction_via_graphs.pdf") (code-pdftotext "geuversndgraphs" "~/books/__logic/geuvers_loeb__natural_deduction_via_graphs.pdf" 1) ;; (find-geuversndgraphspage) ;; (find-geuversndgraphspage 1 "Contents") ;; (find-geuversndgraphspage (+ 1 189) "Index") ;; (find-geuversndgraphstext "") ;; «giardino» (to ".giardino") ;; (find-books "__logic/__logic.el" "giardino") (code-pdf-page "giardinodrim" "~/books/__logic/giardino__diagrammatic_reasoning_in_mathematics.pdf") (code-pdf-text "giardinodrim" "~/books/__logic/giardino__diagrammatic_reasoning_in_mathematics.pdf" -498) ;; (find-giardinodrimpage) ;; (find-giardinodrimtext "") ;; (find-giardinodrimpage (+ -498 517) "Jamnik") ;; (find-giardinodrimtext (+ -498 517) "Jamnik") ;; «girard» (to ".girard") ;; (find-books "__logic/__logic.el" "girard") ;; (find-LATEX "catsem-u.bib" "bib-GLT") ;; http://www.paultaylor.eu/stable/Proofs+Types.html ;; http://www.paultaylor.eu/stable/prot.pdf (code-pdf-page "proofsandtypes" "~/books/__logic/girard__proofs_and_types.pdf") (code-pdf-text "proofsandtypes" "~/books/__logic/girard__proofs_and_types.pdf" 8) ;; (find-proofsandtypespage) ;; (find-proofsandtypespage 4 "Contents") ;; (find-proofsandtypespage (+ 8 1) "1 Sense, Denotation and Semantics") ;; (find-proofsandtypespage (+ 8 1) "1.1 Sense and denotation in logic") ;; (find-proofsandtypespage (+ 8 3) "1.1.1 The algebraic tradition") ;; (find-proofsandtypespage (+ 8 3) "1.1.2 The syntactic tradition") ;; (find-proofsandtypespage (+ 8 4) "1.2 The two semantic traditions") ;; (find-proofsandtypespage (+ 8 4) "1.2.1 Tarski") ;; (find-proofsandtypespage (+ 8 5) "1.2.2 Heyting") ;; (find-proofsandtypespage (+ 8 8) "2 Natural Deduction") ;; (find-proofsandtypespage (+ 8 9) "2.1 The calculus") ;; (find-proofsandtypespage (+ 8 10) "2.1.1 The rules") ;; (find-proofsandtypespage (+ 8 10) "2.2 Computational significance") ;; (find-proofsandtypespage (+ 8 11) "2.2.1 Interpretation of the rules") ;; (find-proofsandtypespage (+ 8 13) "2.2.2 Identification of deductions") ;; (find-proofsandtypespage (+ 8 14) "3 The Curry-Howard Isomorphism") ;; (find-proofsandtypespage (+ 8 15) "3.1 Lambda Calculus") ;; (find-proofsandtypespage (+ 8 15) "3.1.1 Types") ;; (find-proofsandtypespage (+ 8 15) "3.1.2 Terms") ;; (find-proofsandtypespage (+ 8 16) "3.2 Denotational significance") ;; (find-proofsandtypespage (+ 8 17) "3.3 Operational significance") ;; (find-proofsandtypespage (+ 8 18) "3.4 Conversion") ;; (find-proofsandtypespage (+ 8 19) "3.5 Description of the isomorphism") ;; (find-proofsandtypespage (+ 8 20) "3.6 Relevance of the isomorphism") ;; (find-proofsandtypespage (+ 8 22) "4 The Normalisation Theorem") ;; (find-proofsandtypespage (+ 8 22) "4.1 The Church-Rosser property") ;; (find-proofsandtypespage (+ 8 24) "4.2 The weak normalisation theorem") ;; (find-proofsandtypespage (+ 8 24) "4.3 Proof of the weak normalisation theorem") ;; (find-proofsandtypespage (+ 8 25) "4.3.1 Degree and substitution") ;; (find-proofsandtypespage (+ 8 25) "4.3.2 Degree and conversion") ;; (find-proofsandtypespage (+ 8 26) "4.3.3 Conversion of maximal degree") ;; (find-proofsandtypespage (+ 8 26) "4.3.4 Proof of the theorem") ;; (find-proofsandtypespage (+ 8 26) "4.4 The strong normalisation theorem") ;; (find-proofsandtypespage (+ 8 28) "5 Sequent Calculus") ;; (find-proofsandtypespage (+ 8 29) "5.1 The calculus") ;; (find-proofsandtypespage (+ 8 29) "5.1.1 Sequents") ;; (find-proofsandtypespage (+ 8 29) "5.1.2 Structural rules") ;; (find-proofsandtypespage (+ 8 30) "5.1.3 The intuitionistic case") ;; (find-proofsandtypespage (+ 8 30) "5.1.4 The "identity" group") ;; (find-proofsandtypespage (+ 8 31) "5.1.5 Logical rules") ;; (find-proofsandtypespage (+ 8 32) "5.2 Some properties of the system without cut") ;; (find-proofsandtypespage (+ 8 33) "5.2.1 The last rule") ;; (find-proofsandtypespage (+ 8 33) "5.2.2 Subformula property") ;; (find-proofsandtypespage (+ 8 34) "5.2.3 Asymmetrical interpretation") ;; (find-proofsandtypespage (+ 8 35) "5.3 Sequent Calculus and Natural Deduction") ;; (find-proofsandtypespage (+ 8 38) "5.4 Properties of the translation") ;; (find-proofsandtypespage (+ 8 41) "6 Strong Normalisation Theorem") ;; (find-proofsandtypespage (+ 8 41) "6.1 Reducibility") ;; (find-proofsandtypespage (+ 8 42) "6.2 Properties of reducibility") ;; (find-proofsandtypespage (+ 8 42) "6.2.1 Atomic types") ;; (find-proofsandtypespage (+ 8 43) "6.2.2 Product type") ;; (find-proofsandtypespage (+ 8 43) "6.2.3 Arrow type") ;; (find-proofsandtypespage (+ 8 44) "6.3 Reducibility theorem") ;; (find-proofsandtypespage (+ 8 44) "6.3.1 Pairing") ;; (find-proofsandtypespage (+ 8 44) "6.3.2 Abstraction") ;; (find-proofsandtypespage (+ 8 45) "6.3.3 The theorem") ;; (find-proofsandtypespage (+ 8 46) "7 Godel's system T") ;; (find-proofsandtypespage (+ 8 47) "7.1 The calculus") ;; (find-proofsandtypespage (+ 8 47) "7.1.1 Types") ;; (find-proofsandtypespage (+ 8 47) "7.1.2 Terms") ;; (find-proofsandtypespage (+ 8 47) "7.1.3 Intended meaning") ;; (find-proofsandtypespage (+ 8 47) "7.1.4 Conversions") ;; (find-proofsandtypespage (+ 8 48) "7.2 Normalisation theorem") ;; (find-proofsandtypespage (+ 8 49) "7.3 Expressive power: examples") ;; (find-proofsandtypespage (+ 8 49) "7.3.1 Booleans") ;; (find-proofsandtypespage (+ 8 49) "7.3.2 Integers") ;; (find-proofsandtypespage (+ 8 51) "7.4 Expressive power: results") ;; (find-proofsandtypespage (+ 8 51) "7.4.1 Canonical forms") ;; (find-proofsandtypespage (+ 8 51) "7.4.2 Representable functions") ;; (find-proofsandtypespage (+ 8 53) "8 Coherence Spaces") ;; (find-proofsandtypespage (+ 8 53) "8.1 General ideas") ;; (find-proofsandtypespage (+ 8 55) "8.2 Coherence Spaces") ;; (find-proofsandtypespage (+ 8 55) "8.2.1 The web of a coherence space") ;; (find-proofsandtypespage (+ 8 56) "8.2.2 Interpretation") ;; (find-proofsandtypespage (+ 8 57) "8.3 Stable functions") ;; (find-proofsandtypespage (+ 8 59) "8.3.1 Stable functions on a flat space") ;; (find-proofsandtypespage (+ 8 59) "8.3.2 Parallel Or") ;; (find-proofsandtypespage (+ 8 60) "8.4 Direct product of two coherence spaces") ;; (find-proofsandtypespage (+ 8 61) "8.5 The Function-Space") ;; (find-proofsandtypespage (+ 8 61) "8.5.1 The trace of a stable function") ;; (find-proofsandtypespage (+ 8 63) "8.5.2 Representation of the function space") ;; (find-proofsandtypespage (+ 8 64) "8.5.3 The Berry order") ;; (find-proofsandtypespage (+ 8 65) "8.5.4 Partial functions") ;; (find-proofsandtypespage (+ 8 66) "9 Denotational Semantics of T") ;; (find-proofsandtypespage (+ 8 66) "9.1 Simple typed calculus") ;; (find-proofsandtypespage (+ 8 66) "9.1.1 Types") ;; (find-proofsandtypespage (+ 8 67) "9.1.2 Terms") ;; (find-proofsandtypespage (+ 8 68) "9.2 Properties of the interpretation") ;; (find-proofsandtypespage (+ 8 69) "9.3 Godel's system") ;; (find-proofsandtypespage (+ 8 69) "9.3.1 Booleans") ;; (find-proofsandtypespage (+ 8 69) "9.3.2 Integers") ;; (find-proofsandtypespage (+ 8 71) "9.3.3 Infinity and fixed point") ;; (find-proofsandtypespage (+ 8 72) "10 Sums in Natural Deduction") ;; (find-proofsandtypespage (+ 8 72) "10.1 Defects of the system") ;; (find-proofsandtypespage (+ 8 73) "10.2 Standard conversions") ;; (find-proofsandtypespage (+ 8 74) "10.3 The need for extra conversions") ;; (find-proofsandtypespage (+ 8 75) "10.3.1 Subformula Property") ;; (find-proofsandtypespage (+ 8 76) "10.3.2 Extension to the full fragment") ;; (find-proofsandtypespage (+ 8 76) "10.4 Commuting conversions") ;; (find-proofsandtypespage (+ 8 78) "10.5 Properties of conversion") ;; (find-proofsandtypespage (+ 8 79) "10.6 The associated functional calculus") ;; (find-proofsandtypespage (+ 8 79) "10.6.1 Empty type (corresponding to )") ;; (find-proofsandtypespage (+ 8 80) "10.6.2 Sum type (corresponding to )") ;; (find-proofsandtypespage (+ 8 80) "10.6.3 Additional conversions") ;; (find-proofsandtypespage (+ 8 81) "11 System F") ;; (find-proofsandtypespage (+ 8 81) "11.1 The calculus") ;; (find-proofsandtypespage (+ 8 82) "11.2 Comments") ;; (find-proofsandtypespage (+ 8 83) "11.3 Representation of simple types") ;; (find-proofsandtypespage (+ 8 83) "11.3.1 Booleans") ;; (find-proofsandtypespage (+ 8 83) "11.3.2 Product of types") ;; (find-proofsandtypespage (+ 8 84) "11.3.3 Empty type") ;; (find-proofsandtypespage (+ 8 84) "11.3.4 Sum type") ;; (find-proofsandtypespage (+ 8 85) "11.3.5 Existential type") ;; (find-proofsandtypespage (+ 8 85) "11.4 Representation of a free structure") ;; (find-proofsandtypespage (+ 8 86) "11.4.1 Free structure") ;; (find-proofsandtypespage (+ 8 87) "11.4.2 Representation of the constructors") ;; (find-proofsandtypespage (+ 8 87) "11.4.3 Induction") ;; (find-proofsandtypespage (+ 8 88) "11.5 Representation of inductive types") ;; (find-proofsandtypespage (+ 8 88) "11.5.1 Integers") ;; (find-proofsandtypespage (+ 8 90) "11.5.2 Lists") ;; (find-proofsandtypespage (+ 8 92) "11.5.3 Binary trees") ;; (find-proofsandtypespage (+ 8 92) "11.5.4 Trees of branching type U") ;; (find-proofsandtypespage (+ 8 93) "11.6 The Curry-Howard Isomorphism") ;; (find-proofsandtypespage (+ 8 94) "12 Coherence Semantics of the Sum") ;; (find-proofsandtypespage (+ 8 95) "12.1 Direct sum") ;; (find-proofsandtypespage (+ 8 95) "12.2 Lifted sum") ;; (find-proofsandtypespage (+ 8 97) "12.2.1 dI-domains") ;; (find-proofsandtypespage (+ 8 98) "12.3 Linearity") ;; (find-proofsandtypespage (+ 8 98) "12.3.1 Characterisation in terms of preservation") ;; (find-proofsandtypespage (+ 8 99) "12.3.2 Linear implication") ;; (find-proofsandtypespage (+ 8 100) "12.4 Linearisation") ;; (find-proofsandtypespage (+ 8 102) "12.5 Linearised sum") ;; (find-proofsandtypespage (+ 8 103) "12.6 Tensor product and units") ;; (find-proofsandtypespage (+ 8 104) "13 Cut Elimination (Hauptsatz)") ;; (find-proofsandtypespage (+ 8 104) "13.1 The key cases") ;; (find-proofsandtypespage (+ 8 108) "13.2 The principal lemma") ;; (find-proofsandtypespage (+ 8 110) "13.3 The Hauptsatz") ;; (find-proofsandtypespage (+ 8 111) "13.4 Resolution") ;; (find-proofsandtypespage (+ 8 113) "14 Strong Normalisation for F") ;; (find-proofsandtypespage (+ 8 114) "14.1 Idea of the proof") ;; (find-proofsandtypespage (+ 8 114) "14.1.1 Reducibility candidates") ;; (find-proofsandtypespage (+ 8 114) "14.1.2 Remarks") ;; (find-proofsandtypespage (+ 8 115) "14.1.3 Definitions") ;; (find-proofsandtypespage (+ 8 116) "14.2 Reducibility with parameters") ;; (find-proofsandtypespage (+ 8 117) "14.2.1 Substitution") ;; (find-proofsandtypespage (+ 8 117) "14.2.2 Universal abstraction") ;; (find-proofsandtypespage (+ 8 117) "14.2.3 Universal application") ;; (find-proofsandtypespage (+ 8 118) "14.3 Reducibility theorem") ;; (find-proofsandtypespage (+ 8 119) "15 Representation Theorem") ;; (find-proofsandtypespage (+ 8 120) "15.1 Representable functions") ;; (find-proofsandtypespage (+ 8 120) "15.1.1 Numerals") ;; (find-proofsandtypespage (+ 8 121) "15.1.2 Total recursive functions") ;; (find-proofsandtypespage (+ 8 122) "15.1.3 Provably total functions") ;; (find-proofsandtypespage (+ 8 123) "15.2 Proofs into programs") ;; (find-proofsandtypespage (+ 8 124) "15.2.1 Formulation of HA2") ;; (find-proofsandtypespage (+ 8 125) "15.2.2 Translation of HA2 into F") ;; (find-proofsandtypespage (+ 8 126) "15.2.3 Representation of provably total functions") ;; (find-proofsandtypespage (+ 8 128) "15.2.4 Proof without undefined objects") ;; (find-proofsandtypespage (+ 8 131) "A Semantics of System F") ;; (find-proofsandtypespage (+ 8 131) "A.1 Terms of universal type") ;; (find-proofsandtypespage (+ 8 131) "A.1.1 Finite approximation") ;; (find-proofsandtypespage (+ 8 132) "A.1.2 Saturated domains") ;; (find-proofsandtypespage (+ 8 133) "A.1.3 Uniformity") ;; (find-proofsandtypespage (+ 8 134) "A.2 Rigid Embeddings") ;; (find-proofsandtypespage (+ 8 135) "A.2.1 Functoriality of arrow") ;; (find-proofsandtypespage (+ 8 136) "A.3 Interpretation of Types") ;; (find-proofsandtypespage (+ 8 137) "A.3.1 Tokens for universal types") ;; (find-proofsandtypespage (+ 8 138) "A.3.2 Linear notation for tokens") ;; (find-proofsandtypespage (+ 8 139) "A.3.3 The three simplest types") ;; (find-proofsandtypespage (+ 8 140) "A.4 Interpretation of terms") ;; (find-proofsandtypespage (+ 8 140) "A.4.1 Variable coherence spaces") ;; (find-proofsandtypespage (+ 8 141) "A.4.2 Coherence of tokens") ;; (find-proofsandtypespage (+ 8 143) "A.4.3 Interpretation of F") ;; (find-proofsandtypespage (+ 8 144) "A.5 Examples") ;; (find-proofsandtypespage (+ 8 144) "A.5.1 Of course") ;; (find-proofsandtypespage (+ 8 146) "A.5.2 Natural Numbers") ;; (find-proofsandtypespage (+ 8 147) "A.5.3 Linear numerals") ;; (find-proofsandtypespage (+ 8 148) "A.6 Total domains") ;; (find-proofsandtypespage (+ 8 149) "B What is Linear Logic?") ;; (find-proofsandtypespage (+ 8 149) "B.1 Classical logic is not constructive") ;; (find-proofsandtypespage (+ 8 151) "B.2 Linear Sequent Calculus") ;; (find-proofsandtypespage (+ 8 154) "B.3 Proof nets") ;; (find-proofsandtypespage (+ 8 157) "B.4 Cut elimination") ;; (find-proofsandtypespage (+ 8 160) "B.5 Proof nets and natural deduction") ;; (find-proofsandtypespage (+ 8 161) "Bibliography") ;; (find-proofsandtypespage (+ 8 165) "Index and index of notation") ;; (find-proofsandtypestext "") ;; ;; file:///home/edrx/snarf/http/www.paultaylor.eu/stable/prot.pdf ;; «girard-blind-spot» (to ".girard-blind-spot") ;; (find-books "__logic/__logic.el" "girard-blind-spot") ;; https://www.ems-ph.org/books/book.php?proj_nr=136&srch=browse_authors%7CGirard%2C+Jean-Yves ;; https://www.maa.org/press/maa-reviews/the-blind-spot-lectures-on-logic ;; https://news.ycombinator.com/item?id=14249733 ;; https://www.ems-ph.org/books/toc/136/Review%20in%20MR%202896656.pdf (code-pdf-page "blindspot" "~/books/__logic/girard__the_blind_spot.pdf") (code-pdf-text "blindspot" "~/books/__logic/girard__the_blind_spot.pdf" 1) ;; (find-blindspotpage) ;; (find-blindspotpage 6 "Contents") ;; (find-blindspotpage (+ 1 189) "Index") ;; (find-blindspottext "") ;; «girard-tcs87» (to ".girard-tcs87") ;; (find-books "__logic/__logic.el" "girard-tcs87") ;; https://www.sciencedirect.com/journal/theoretical-computer-science/vol/50/issue/1 (code-pdf-page "girardtcs87" "~/books/__logic/girard__linear_logic_tcs_1987.pdf") (code-pdf-text "girardtcs87" "~/books/__logic/girard__linear_logic_tcs_1987.pdf" 1) ;; (find-girardtcs87page) ;; (find-girardtcs87page 1 "Contents") ;; (find-girardtcs87text 1 "Contents") ;; (find-girardtcs87page 2 "I. Introduction and abstract") ;; (find-girardtcs87page 4 "II. Linear logic explained to a proof-theorist.") ;; (find-girardtcs87page 4 "11.1. The maintenance of space in sequent calculus") ;; (find-girardtcs87page 4 "11.2. Linear logic as a sequent calculus") ;; (find-girardtcs87page 5 "11.3. Strength of linear logic") ;; (find-girardtcs87page 6 "11.4. Subtlety of linear logic") ;; (find-girardtcs87page 6 "11.5. me semantics of linear logic: phased") ;; (find-girardtcs87page 7 "III. Linear logic explained to a (theoretical) computer scientist") ;; (find-girardtcs87page 8 "111.1. The semantics of linear logic: coherent spaces") ;; (find-girardtcs87page 8 "111.2. Proof-nets: a Glassical natural deduction") ;; (find-girardtcs87page 11 "III.3. Normalization for proof-nets") ;; (find-girardtcs87page 12 "111.4. Relevance for computer science.") ;; (find-girardtcs87page 12 "111.4.1. Questions and answers") ;; (find-girardtcs87page 12 "111.4.2. Towards parallelism") ;; (find-girardtcs87page 13 "111.4.3. Communication and trips") ;; (find-girardtcs87page 14 "111.4.4. Work in progress") ;; (find-girardtcs87page 14 "IV. Pons asinorum: from usual implication to linear implication") ;; (find-girardtcs87page 15 "IV.l. Interpretation of functional languages.") ;; (find-girardtcs87page 15 "IV.2. Thedisturbance") ;; (find-girardtcs87page 16 "IV.3. The decomposition") ;; (find-girardtcs87page 17 "IV.4. Further questions") ;; (find-girardtcs87page 17 "1. The phase semantics") ;; (find-girardtcs87page 28 "2. Proof-nets") ;; (find-girardtcs87page 30 "2.1. The concept of trip") ;; (find-girardtcs87page 40 "2.2. Thecutrule") ;; (find-girardtcs87page 41 "2.3. Cut elimination") ;; (find-girardtcs87page 44 "2.4. Thesystem PNl") ;; (find-girardtcs87page 46 "2.5. The system PN2") ;; (find-girardtcs87page 47 "2.6. Discussion.") ;; (find-girardtcs87page 48 "3. Conetent semantics") ;; (find-girardtcs87page 60 "4. Normalization in PN2") ;; (find-girardtcs87page 61 "4.1. Axiomcontraction") ;; (find-girardtcs87page 62 "4.2. Symmetric contractions") ;; (find-girardtcs87page 65 "4.3. Commutative contractions") ;; (find-girardtcs87page 78 "5. Some useful transiations") ;; (find-girardtcs87page 78 "5.1. The translation of intuitionisiic logic") ;; (find-girardtcs87page 82 "5.2. The translation of the system F") ;; (find-girardtcs87page 82 "5.2.1. Types") ;; (find-girardtcs87page 82 "5.2.2. Translation of terms.") ;; (find-girardtcs87page 84 "5.2.3. Semantic soundness of the translation") ;; (find-girardtcs87page 85 "5.2.4. Syntactic soundness of the translation") ;; (find-girardtcs87page 85 "5.3. The translation of current data in PN2") ;; (find-girardtcs87page 86 "5.3.1. Booleans") ;; (find-girardtcs87page 86 "5.3.2. Integers") ;; (find-girardtcs87page 90 "5.33. Lists, trees") ;; (find-girardtcs87page 90 "5.4. Interpretation of classical logic") ;; (find-girardtcs87page 91 "5.5. Translation of cut-free classical logic.") ;; (find-girardtcs87page 92 "5.6. The Approximation Theorem") ;; (find-girardtcs87page 93 "6. Work in progress: slices") ;; (find-girardtcs87page 97 "V. Two years of linear logic: selection from the garbage collector") ;; (find-girardtcs87page 97 "V.l. The first glimpses") ;; (find-girardtcs87page 98 "V.2. The quantitative attempt") ;; (find-girardtcs87page 98 "V.3. The intuitionistic attempt") ;; (find-girardtcs87page 99 "V.4. Recent developments") ;; (find-girardtcs87page 100 "V.5. The exponentials") ;; (find-girardtcs87page 101 "Acknowledgment") ;; (find-girardtcs87page 102 "References") ;; (find-girardtcs87text "") ;; «girard-tet» (to ".girard-tet") ;; Jean-Yves Girard: titres et travaux ;; https://girard.perso.math.cnrs.fr/titres.pdf (code-pdf-page "girardtet" "$S/https/girard.perso.math.cnrs.fr/titres.pdf") (code-pdf-text "girardtet" "$S/https/girard.perso.math.cnrs.fr/titres.pdf") ;; (find-girardtetpage) ;; (find-girardtettext) ;; (find-girardtetpage 31 "Bibliographie sélective") ;; (find-girardtettext 31 "Bibliographie sélective") ;; https://www.sciencedirect.com/journal/theoretical-computer-science/vol/50/issue/1 ;; https://girard.perso.math.cnrs.fr/Logique.html ;; https://girard.perso.math.cnrs.fr/Accueil.html ;; https://girard.perso.math.cnrs.fr/Ringard.html ;; https://girard.perso.math.cnrs.fr/Archives.html ;; https://girard.perso.math.cnrs.fr/titres.pdf ;; On Girard's latest works: ;; https://nguyentito.eu/ ;; https://nguyentito.eu/ Nguyen Le Than Dung ;; https://nguyentito.eu/2018-11-scalp.pdf ;; https://engboris.github.io/ ;; https://engboris.github.io/documents/report_m2.pdf ;; https://engboris.github.io/library/ ;; https://www.engboris.fr/ts/ girard - transcendental syntax ;; https://www.seiller.org/documents/articles/Stellar.pdf ;; «godel» (to ".godel") ;; (find-books "__logic/__logic.el" "godel") ;; (find-LATEX "catsem.bib" "bib-Goedel") (code-pdf "godel1" "~/books/__logic/godel___collected_works_1.pdf") (code-pdftotext "godel1" "~/books/__logic/godel___collected_works_1.pdf" 27) (code-pdf "godel2" "~/books/__logic/godel___collected_works_2.pdf") (code-pdftotext "godel2" "~/books/__logic/godel___collected_works_2.pdf" 19) ;; (find-godel1page) ;; (find-godel1page 18 "Contents") ;; (find-godel1page (+ 27 16) "Works in the first two volumes") ;; (find-godel1page (+ 27 223) "On the intuitionistic propositional calculus") ;; (find-godel1page (+ 27 296) "Introductory note to 1933f") ;; (find-godel1page (+ 27 301) "An interpretation of the intuitionistic propositional calculus (1933f)") ;; (find-godel1page (+ 27 461) "Index") ;; (find-godel1text "") ;; (find-godel2page) ;; (find-godel2page 14 "Contents") ;; (find-godel2page (+ 19 1) "Index") ;; (find-godel2page (+ 19 393) "Index") ;; (find-godel2text "") ;; «goranko» (to ".goranko") ;; (find-books "__logic/__logic.el" "goranko") ;; http://www2.imm.dtu.dk/courses/02286/Slides/FirstOrderLogicSyntaxFreeBoundVarsQuantScopeCaptureSubstRenamingTrans.pdf (code-pdf-page "gorankosubs" "$S/http/www2.imm.dtu.dk/courses/02286/Slides/FirstOrderLogicSyntaxFreeBoundVarsQuantScopeCaptureSubstRenamingTrans.pdf") (code-pdf-text "gorankosubs" "$S/http/www2.imm.dtu.dk/courses/02286/Slides/FirstOrderLogicSyntaxFreeBoundVarsQuantScopeCaptureSubstRenamingTrans.pdf") ;; (find-gorankosubspage) ;; (find-gorankosubstext) ;; «grande» (to ".grande") ;; (find-books "__logic/__logic.el" "grande") (code-pdf-page "grandesymm" "~/books/__logic/grande__on_symbolization_in_mathematics.pdf") (code-pdf-text "grandesymm" "~/books/__logic/grande__on_symbolization_in_mathematics.pdf" 1) ;; (find-grandesymmpage) ;; (find-grandesymmpage 1 "Contents") ;; (find-grandesymmpage (+ 1 189) "Index") ;; (find-grandesymmtext "") ;; «grande-silva» (to ".grande-silva") ;; (find-books "__logic/__logic.el" "grande-silva") ;; https://www.editorafi.org/251simbolo (code-pdf-page "simbolo" "~/books/__logic/grande_silva__o_simbolo_e_a_realidade.pdf") (code-pdf-text "simbolo" "~/books/__logic/grande_silva__o_simbolo_e_a_realidade.pdf" 1) ;; (find-simbolopage) ;; (find-simbolopage 9 "Contents") ;; (find-simbolopage (+ 1 189) "Index") ;; (find-simbolotext "") ;; (find-simbolopage 11 "Prefácio") ;; (find-simbolopage 13 "1 Introdução") ;; (find-simbolopage 13 "1.1 O fascínio pelos números") ;; (find-simbolopage 16 "1.2 Objetivos, linguagem e reflexão filosófica") ;; (find-simbolopage 22 "2 Tipos de notação") ;; (find-simbolopage 29 "3 Funções básicas da notação matemática") ;; (find-simbolopage 29 "3.1 Preâmbulo filosófico") ;; (find-simbolopage 31 "3.2 Aspectos fundamentais da notação") ;; (find-simbolopage 33 "de modo implícito") ;; (find-simbolotext 33 "de modo implícito") ;; (find-simbolopage 67 "4 O símbolo e a realidade - análise filosófica") ;; (find-simbolopage 67 "4.1 Realidade fenomênica") ;; (find-simbolopage 73 "4.2 O Estruturalismo e o realismo de Born") ;; (find-simbolopage 77 "5 Conclusões") ;; (find-simbolopage 79 "6 Apêndice: raciocínio diagramático em mecânica quântica") ;; (find-simbolopage 79 "6.1 Introdução histórica") ;; (find-simbolopage 82 "6.2 O que é um diagrama de Feynman?") ;; (find-simbolopage 82 "6.2.1 Raciocínios diagramáticos") ;; (find-simbolopage 85 "6.2.2 Diagramas de Feynman") ;; (find-simbolopage 88 "6.3 O que exatamente um diagrama de Feynman representa?") ;; (find-simbolopage 88 "6.3.1 A matemática e a realidade empírica") ;; (find-simbolopage 90 "6.3.2 Diagramática geral - uma abordagem informal") ;; (find-simbolopage 92 "6.3.3 Exemplo prático") ;; (find-simbolopage 94 "6.4 Observações") ;; (find-simbolopage 95 "6.5 Conclusões") ;; (find-simbolopage 96 "7 Apêndice: o pensamento simbólico em Granger") ;; (find-simbolopage 96 "7.1 Introdução") ;; (find-simbolopage 101 "7.2 Forma e conteúdo na física") ;; (find-simbolopage 105 "7.3 Paradigma e tema") ;; (find-simbolopage 108 "7.4.1 Grau zero da relação forma-conteúdo e o cálculo proposicional") ;; (find-simbolopage 110 "7.4.2 Objeto matemático") ;; (find-simbolopage 114 "7.5 Conclusões") ;; (find-simbolopage 116 "8 Apêndice: Sobre a história da matemática e o uso...") ;; (find-simbolopage 132 "Conclusões") ;; (find-simbolopage 133 "Referências") ;; (find-simbolotext 133 "Referências") ;; «krantz-parks» (to ".krantz-parks") ;; (find-books "__logic/__logic.el" "krantz-parks") (code-pdf-page "implift" "~/books/__logic/krantz_parks__the_implicit_function_theorem_history_theory_and_applications.pdf") (code-pdf-text "implift" "~/books/__logic/krantz_parks__the_implicit_function_theorem_history_theory_and_applications.pdf" 10) ;; (find-impliftpage) ;; (find-impliftpage 6 "Contents") ;; (find-impliftpage (+ 10 1) "Index") ;; (find-implifttext "") ;; «gries-schneider» (to ".gries-schneider") (code-xpdf "griesschneider" "~/books/__logic/gries_schneider__a_logical_approach_to_discrete_math.pdf") (code-pdftotext "griesschneider" "~/books/__logic/gries_schneider__a_logical_approach_to_discrete_math.pdf") ;; (find-griesschneiderpage 1 "Contents") ;; (find-griesschneiderpage (+ 1 1) "Index") ;; (find-griesschneidertext "") ;; «gun» (to ".gun") ;; (find-books "__logic/__logic.el" "gun") ;; https://fu-berlin.academia.edu/OzgeEkin ;; https://hesperusisbosphorus.wordpress.com/2016/09/18/two-talks-at-bogazici-by-ozge-ekin-gun-on-the-philosophy-of-maths-and-kant-2223092016/ ;; https://hesperusisbosphorus.files.wordpress.com/2016/09/ozge-kant-talk.pdf ;; ;; Ozge Ekin Gun: "New Approaches to Visual Reasoning in Mathematics ;; and Kantian Characterization of Mathematics" (PhD thesis, 2015) ;; https://refubium.fu-berlin.de/bitstream/handle/fub188/4990/PhD.pdf (code-pdf-page "gunphd" "$S/https/refubium.fu-berlin.de/bitstream/handle/fub188/4990/PhD.pdf") (code-pdf-text "gunphd" "$S/https/refubium.fu-berlin.de/bitstream/handle/fub188/4990/PhD.pdf") ;; (find-gunphdpage) ;; (find-gunphdtext) ;; (find-gunphdpage 3 "TABLE OF CONTENTS") ;; (find-gunphdtext 3 "TABLE OF CONTENTS") ;; (find-gunphdpage (+ 5 6) "I. Introduction") ;; (find-gunphdpage (+ 5 6) "1.1 Intuition, Diagram, Visual Reasoning in Mathematics") ;; (find-gunphdpage (+ 5 11) "1.2 The History and the Critique of Logicism") ;; (find-gunphdpage (+ 5 16) "1.3 Why is the Change in Perception of How One Practices Mathematics Necessary?") ;; (find-gunphdpage (+ 5 24) "1.4 Contemporary State of Visualization in Mathematics") ;; (find-gunphdpage (+ 5 30) "II. The Medium for Visual Reasoning:") ;; (find-gunphdpage (+ 5 32) "2.1 What is space?") ;; (find-gunphdpage (+ 5 38) "2.2 Kant's Notion of Space") ;; (find-gunphdpage (+ 5 40) "2.2.1 Kant's Historical Background") ;; (find-gunphdpage (+ 5 41) "2.2.2 Space as Pure Intuition: The Metaphysical Exposition") ;; (find-gunphdpage (+ 5 44) "2.2.3 Space as Form of Sensibility: The Transcendental Exposition") ;; (find-gunphdpage (+ 5 46) "2.2.4 Representations (Vorstellungen)") ;; (find-gunphdpage (+ 5 48) "2.2.5 Method for Representing: Schema") ;; (find-gunphdpage (+ 5 59) "2.2.6 The General Representation: Concept") ;; (find-gunphdpage (+ 5 60) "2.2.7 The Singular Representation: Intuition") ;; (find-gunphdpage (+ 5 65) "2.3 Kant's Characterization of Space and Visual Reasoning in Mathematics") ;; (find-gunphdpage (+ 5 70) "III. Methods for Visual Reasoning: Synthetic a priori, Construction and Abstraction") ;; (find-gunphdpage (+ 5 71) "3.1 The Definitions of Visualization and Methods Associated with these Definitions") ;; (find-gunphdpage (+ 5 77) "3.2 "Construction" and "Synthetic a priori " method") ;; (find-gunphdpage (+ 5 82) "3.2.1 The Method of Visual Reasoning in Mathematics") ;; (find-gunphdpage (+ 5 85) "3.2.2 Analytic and Synthetic") ;; (find-gunphdpage (+ 5 87) "3.2.3 Analytic and Synthetic in the Kantian Transcendental Philosophy") ;; (find-gunphdpage (+ 5 93) "3.2.4 Analytic and Synthetic as Judgments") ;; (find-gunphdpage (+ 5 98) "IV. Interpretations on Kant's notion of Space and Synthetic a priori Method") ;; (find-gunphdpage (+ 5 101) "4.1 Spaces's Original Representation is not a Concept") ;; (find-gunphdpage (+ 5 107) "4.2 Space's Original Representation is Pure Intuition") ;; (find-gunphdpage (+ 5 113) "4.3 Where does Synthetic and a priori Character of Mathematics Appear in Kant's Doctrine? Different Interpretations.") ;; (find-gunphdpage (+ 5 120) "4.3.1 Hintikka's Reconstruction of Kant's Mathematical Intuition") ;; (find-gunphdpage (+ 5 126) "4.4 Kant's Characterization of Mathematics and Modern Logic") ;; (find-gunphdpage (+ 5 129) "V. Visual Reasoning") ;; (find-gunphdpage (+ 5 131) "5.1 Diagrams as Formal Representation Systems") ;; (find-gunphdpage (+ 5 132) "5.1.1 Valid Reasoning with Diagrams") ;; (find-gunphdpage (+ 5 135) "5.1.2 Venn Diagrams as an Information Manipulating Formal Representation System") ;; (find-gunphdpage (+ 5 146) "5.2 Diagrams as Valid Reasoning Tools") ;; (find-gunphdpage (+ 5 146) "5.2.1 Diagrams in Proofs") ;; (find-gunphdpage (+ 5 164) "5.3 Visual Reasoning with Diagrams") ;; (find-gunphdpage (+ 5 166) "5.3.1 Perception and Recognition") ;; (find-gunphdpage (+ 5 173) "5.3.2 Diagrams and Mathematical Knowledge") ;; (find-gunphdpage (+ 5 182) "5.4 Valid Use of Diagrams in Mathematics") ;; (find-gunphdpage (+ 5 189) "VI. Conclusion") ;; ;; Ozge Ekin Gun: "Necessity of Visual Representations in Mathematics" (2016) (code-pdf-page "gunnovrim" "~/books/__logic/gun__necessity_of_visual_representations_in_mathematics.pdf") (code-pdf-text "gunnovrim" "~/books/__logic/gun__necessity_of_visual_representations_in_mathematics.pdf" 1) ;; (find-gunnovrimpage) ;; (find-gunnovrimpage 1 "Contents") ;; (find-gunnovrimpage (+ 1 189) "Index") ;; (find-gunnovrimtext "") ;; Gun: "Computer Imagery and the Rigor It Provides for the Mathematical Visual Reasoning" (2017) (code-pdf-page "guncomputerim" "~/books/__logic/gun__computer_imagery_and_the_rigor_it_provides_for_the_mathematical_visual_reasoning.pdf") (code-pdf-text "guncomputerim" "~/books/__logic/gun__computer_imagery_and_the_rigor_it_provides_for_the_mathematical_visual_reasoning.pdf" 1) ;; (find-guncomputerimpage) ;; (find-guncomputerimpage 1 "Contents") ;; (find-guncomputerimpage (+ 1 189) "Index") ;; (find-guncomputerimtext "") ;; Gun: "Kantian Intuition of Mathematical Objects and Diagrams" (2011) (code-pdf-page "gundiagkant" "~/books/__logic/gun__diagrams_and_kantian_intuitions.pdf") (code-pdf-text "gundiagkant" "~/books/__logic/gun__diagrams_and_kantian_intuitions.pdf" 1) ;; (find-gundiagkantpage) ;; (find-gundiagkantpage 1 "Contents") ;; (find-gundiagkantpage (+ 1 189) "Index") ;; (find-gundiagkanttext "") ;; «handbook-of-logic-in-CS» (to ".handbook-of-logic-in-CS") ;; (find-books "__logic/__logic.el" "handbook-of-logic-in-CS") (code-pdf-page "handbookoflogicincs1" "~/books/__logic/handbook_of_logic_in_computer_science_vol_1_background_mathematical_structures.pdf") (code-pdf-text "handbookoflogicincs1" "~/books/__logic/handbook_of_logic_in_computer_science_vol_1_background_mathematical_structures.pdf" 1) ;; (find-handbookoflogicincs1page) ;; (find-handbookoflogicincs1page 5 "Contents") ;; (find-handbookoflogicincs1page (+ 1 189) "Index") ;; (find-handbookoflogicincs1text "") ;; ;; (find-books "__logic/__logic.el" "handbook-of-logic-in-CS") (code-pdf-page "handbookoflogicincs2" "~/books/__logic/handbook_of_logic_in_computer_science_vol_2_background_computational_structures.pdf") (code-pdf-text "handbookoflogicincs2" "~/books/__logic/handbook_of_logic_in_computer_science_vol_2_background_computational_structures.pdf" 1) ;; (find-handbookoflogicincs2page) ;; (find-handbookoflogicincs2page 8 "Contents") ;; (find-handbookoflogicincs2page (+ 1 189) "Index") ;; (find-handbookoflogicincs2text "") ;; ;; (find-books "__logic/__logic.el" "handbook-of-logic-in-CS") (code-pdf-page "handbookoflogicincs3" "~/books/__logic/handbook_of_logic_in_computer_science_vol_3_semantic_structures.pdf") (code-pdf-text "handbookoflogicincs3" "~/books/__logic/handbook_of_logic_in_computer_science_vol_3_semantic_structures.pdf" 1) ;; (find-handbookoflogicincs3page) ;; (find-handbookoflogicincs3page 10 "Contents") ;; (find-handbookoflogicincs3page (+ 1 189) "Index") ;; (find-handbookoflogicincs3text "") ;; «henkin» (to ".henkin") ;; Leon Henkin: The logic of equality (1977) ;; https://www.jstor.org/stable/2321009 ;; (find-books "__logic/__logic.el" "henkin") (code-pdf "henkinleq" "~/books/__logic/henkin1977.pdf") (code-pdftotext "henkinleq" "~/books/__logic/henkin1977.pdf" -595) ;; (find-henkinleqpage) ;; (find-henkinleqpage 1 "Contents") ;; (find-henkinleqpage (+ 1 189) "Index") ;; (find-henkinleqpage (+ -595 597)) ;; (find-henkinleqtext (+ -595 597)) ;; (find-henkinleqtext "") ;; «herbelin» (to ".herbelin") ;; http://pauillac.inria.fr/~herbelin/ ;; https://www.cs.uoregon.edu/research/summerschool/summer11/lectures/oplss-herbelin1.pdf (code-pdf-page "herbelin" "$S/https/www.cs.uoregon.edu/research/summerschool/summer11/lectures/oplss-herbelin1.pdf") (code-pdf-text "herbelin" "$S/https/www.cs.uoregon.edu/research/summerschool/summer11/lectures/oplss-herbelin1.pdf") ;; (find-herbelinpage) ;; (find-herbelintext) ;; «hermogenesoliveira» (to ".hermogenesoliveira") ;; (find-books "__logic/__logic.el" "hermogenesoliveira") (code-pdf-page "hermogenesolivphd" "~/books/__logic/hermogenes_oliveira__dissertation.pdf") (code-pdf-text "hermogenesolivphd" "~/books/__logic/hermogenes_oliveira__dissertation.pdf" 10) ;; (find-hermogenesolivphdpage) ;; (find-hermogenesolivphdpage 9 "Contents") ;; (find-hermogenesolivphdtext 9 "Contents") ;; (find-hermogenesolivphdpage (+ 1 189) "Index") ;; (find-hermogenesolivphdtext "") ;; (find-hermogenesolivphdpage (+ 10 11) "1.2.3 The BHK interpretation") ;; (find-hermogenesolivphdtext (+ 10 11) "1.2.3 The BHK interpretation") ;; (find-hermogenesolivphdpage (+ 10 43) "5.1 BHK vs Gentzen") ;; (find-hermogenesolivphdtext (+ 10 43) "5.1 BHK vs Gentzen") ;; «hesseling» (to ".hesseling") ;; (find-books "__logic/__logic.el" "hesseling") ;; (find-LATEX "catsem-u.bib" "bib-Hesseling") (code-pdf-page "gnomesinthefog" "~/books/__logic/hesseling__gnomes_in_the_fog_the_reception_of_brouwer_s_intuitionism_in_the_1920s.pdf") (code-pdf-text "gnomesinthefog" "~/books/__logic/hesseling__gnomes_in_the_fog_the_reception_of_brouwer_s_intuitionism_in_the_1920s.pdf" 21) ;; (find-gnomesinthefogpage) ;; (find-gnomesinthefogpage 7 "Contents") ;; (find-gnomesinthefogpage (+ 21 1) "1 Kronecker, the semi-intuitionists, Poincare") ;; (find-gnomesinthefogpage (+ 21 1) "1.1 Introduction") ;; (find-gnomesinthefogpage (+ 21 2) "1.1.1 Mathematical prerequisites") ;; (find-gnomesinthefogpage (+ 21 4) "1. 2 Kronecker..........") ;; (find-gnomesinthefogpage (+ 21 5) "1.2.1 Kronecker's conflicts") ;; (find-gnomesinthefogpage (+ 21 6) "1.2.2 Kronecker's views") ;; (find-gnomesinthefogpage (+ 21 8) "1.3 The French semi-intuitionists") ;; (find-gnomesinthefogpage (+ 21 9) "1.3.1 The French semi-intuitionists' main conflict") ;; (find-gnomesinthefogpage (+ 21 12) "1.3.2 The French semi-intuitionists' views") ;; (find-gnomesinthefogpage (+ 21 18) "1.4 Poincare..........") ;; (find-gnomesinthefogpage (+ 21 18) "1.4.1 Poincare's conflicts") ;; (find-gnomesinthefogpage (+ 21 20) "1.4.2 Poincare's views") ;; (find-gnomesinthefogpage (+ 21 23) "1.5 Conclusion") ;; (find-gnomesinthefogpage (+ 21 25) "2 The genesis of Brouwer's intuitionism") ;; (find-gnomesinthefogpage (+ 21 25) "2.1 Introduction") ;; (find-gnomesinthefogpage (+ 21 26) "2.2 The early years") ;; (find-gnomesinthefogpage (+ 21 26) "2.2.1 Brouwer's youth") ;; (find-gnomesinthefogpage (+ 21 26) "2.2.2 Brouwer's profession of faith") ;; (find-gnomesinthefogpage (+ 21 28) "2.2.3 Mannoury......") ;; (find-gnomesinthefogpage (+ 21 30) "2.2.4 Brouwer's mysticism") ;; (find-gnomesinthefogpage (+ 21 34) "2.3 The first act of intuitionism") ;; (find-gnomesinthefogpage (+ 21 35) "2.3.1 Brouwer's dissertation") ;; (find-gnomesinthefogpage (+ 21 46) "2.3.2 The unreliability of the logical principles.") ;; (find-gnomesinthefogpage (+ 21 48) "2.4 Topology") ;; (find-gnomesinthefogpage (+ 21 52) "2.5 Intuitionism and formalism") ;; (find-gnomesinthefogpage (+ 21 58) "2.6 The second act of intuitionism") ;; (find-gnomesinthefogpage (+ 21 60) "2.6.1 Intuitionistic set theory") ;; (find-gnomesinthefogpage (+ 21 67) "2.6.2 Further development of intuitionistic mathematics") ;; (find-gnomesinthefogpage (+ 21 75) "2.7 The Brouwer lectures.") ;; (find-gnomesinthefogpage (+ 21 75) "2.7.1 Berlin") ;; (find-gnomesinthefogpage (+ 21 77) "2.7.2 Amsterdam") ;; (find-gnomesinthefogpage (+ 21 79) "2.7.3 Vienna.....") ;; (find-gnomesinthefogpage (+ 21 81) "2.8 The Mathematische Annalen and afterwards.") ;; (find-gnomesinthefogpage (+ 21 86) "2.9 Brouwer's personality") ;; (find-gnomesinthefogpage (+ 21 89) "2.10 Conclusion") ;; (find-gnomesinthefogpage (+ 21 91) "3 Overview of the foundational debate") ;; (find-gnomesinthefogpage (+ 21 91) "3.1 Introduction.......") ;; (find-gnomesinthefogpage (+ 21 93) "3.2 Quantitative inquiry") ;; (find-gnomesinthefogpage (+ 21 93) "3.2.1 The Fortschritte") ;; (find-gnomesinthefogpage (+ 21 95) "3.2.2 'All' public reactions to intuitionism") ;; (find-gnomesinthefogpage (+ 21 97) "3.3 Qualitative inquiry") ;; (find-gnomesinthefogpage (+ 21 97) "3.3.1 Themes") ;; (find-gnomesinthefogpage (+ 21 99) "3.3.2 Tone") ;; (find-gnomesinthefogpage (+ 21 104) "3.3.3 Currents and schools.") ;; (find-gnomesinthefogpage (+ 21 111) "3.3.4 People.........") ;; (find-gnomesinthefogpage (+ 21 113) "3.3.5 Languages and media") ;; (find-gnomesinthefogpage (+ 21 115) "3.4 Conclusion") ;; (find-gnomesinthefogpage (+ 21 117) "4 Reactions: existence and constructivity") ;; (find-gnomesinthefogpage (+ 21 117) "4.1 Introduction................") ;; (find-gnomesinthefogpage (+ 21 117) "4.1.1 Mathematical existence") ;; (find-gnomesinthefogpage (+ 21 120) "4.1.2 A short history of constructivism") ;; (find-gnomesinthefogpage (+ 21 124) "4.2 The beginning of the debate") ;; (find-gnomesinthefogpage (+ 21 125) "4.2.1 Weyl's Grundlagenkrise") ;; (find-gnomesinthefogpage (+ 21 133) "4.2.2 Hilbert's first reactions.") ;; (find-gnomesinthefogpage (+ 21 145) "4.2.3 Becker's phenomenology") ;; (find-gnomesinthefogpage (+ 21 149) "4.2.4 Fraenkel's early commentaries.") ;; (find-gnomesinthefogpage (+ 21 152) "4.2.5 Baldus' rector's address") ;; (find-gnomesinthefogpage (+ 21 154) "4.3 The debate widened") ;; (find-gnomesinthefogpage (+ 21 158) "4.3.1 Existence in a central position") ;; (find-gnomesinthefogpage (+ 21 175) "4.3.2 Existence as a minor subject") ;; (find-gnomesinthefogpage (+ 21 183) "4.4 Later reactions") ;; (find-gnomesinthefogpage (+ 21 183) "4.4.1 The Konigsberg conference") ;; (find-gnomesinthefogpage (+ 21 190) "4.4.2 Wittgenstein") ;; (find-gnomesinthefogpage (+ 21 198) "4.4.3 Others") ;; (find-gnomesinthefogpage (+ 21 212) "4.5 Conclusion") ;; (find-gnomesinthefogpage (+ 20 217) "5 Reactions: logic and the excluded middle") ;; (find-gnomesinthefogpage (+ 20 217) "5.1 Introduction") ;; (find-gnomesinthefogpage (+ 20 218) "5.1.1 A short history of classical logic") ;; (find-gnomesinthefogpage (+ 20 220) "5.2 The beginning of the debate") ;; (find-gnomesinthefogpage (+ 20 222) "5.2.1 Weyl's Grundlagenkrise") ;; (find-gnomesinthefogpage (+ 20 225) "5.2.2 Hilbert's first reactions") ;; (find-gnomesinthefogpage (+ 20 229) "5.2.3 Addresses: Wolff, Finsler and Baldus") ;; (find-gnomesinthefogpage (+ 20 231) "5.2.4 Fraenkel's early commentaries.") ;; (find-gnomesinthefogpage (+ 20 231) "5.3 The debate widened") ;; (find-gnomesinthefogpage (+ 20 236) "5.3.1 The excluded middle in a central position") ;; (find-gnomesinthefogpage (+ 20 268) "5.3.2 The excluded middle as a minor subject") ;; (find-gnomesinthefogpage (+ 20 271) "5.4 Later reactions") ;; (find-gnomesinthefogpage (+ 20 271) "5.4.1 Glivenko, Heyting and Kolmogorov") ;; (find-gnomesinthefogpage (+ 20 281) "5.4.2 Godel") ;; (find-gnomesinthefogpage (+ 20 289) "5.4.3 Barzin and Errera") ;; (find-gnomesinthefogpage (+ 20 296) "5.5 Conclusion") ;; (find-gnomesinthefogpage (+ 19 301) "6 The foundational crisis in its context") ;; (find-gnomesinthefogpage (+ 19 301) "6.1 Introduction") ;; (find-gnomesinthefogpage (+ 19 302) "6.2 Metaphors") ;; (find-gnomesinthefogpage (+ 19 302) "6.2.1 Crisis and revolution") ;; (find-gnomesinthefogpage (+ 19 311) "6.3 Philosophy") ;; (find-gnomesinthefogpage (+ 19 312) "6.3.1 Lebensphilosophie") ;; (find-gnomesinthefogpage (+ 19 316) "6.3.2 Mathematical and philosophical intuitionism: a comparison") ;; (find-gnomesinthefogpage (+ 19 320) "6.3.3 Contemporaries' remarks") ;; (find-gnomesinthefogpage (+ 19 322) "6.3.4 Gottingen and Hilbert") ;; (find-gnomesinthefogpage (+ 19 323) "6.3.5 Spengler") ;; (find-gnomesinthefogpage (+ 19 325) "6.3.6 Summary") ;; (find-gnomesinthefogpage (+ 19 326) "6.4 Physics") ;; (find-gnomesinthefogpage (+ 19 327) "6.4.1 Theory of relativity") ;; (find-gnomesinthefogpage (+ 19 329) "6.4.2 Quantum mechanics") ;; (find-gnomesinthefogpage (+ 19 333) "6.5 Art") ;; (find-gnomesinthefogpage (+ 19 334) "6.5.1 Constructivism...") ;; (find-gnomesinthefogpage (+ 19 335) "6.6 Politics") ;; (find-gnomesinthefogpage (+ 19 335) "6.6.1 Mathematics and the rise of the Third Reich") ;; (find-gnomesinthefogpage (+ 19 338) "6.6.2 Bieberbach's racial interpretation of the foundational debate") ;; (find-gnomesinthefogpage (+ 19 340) "6.7 Modeme and Gegenmodeme.") ;; (find-gnomesinthefogpage (+ 19 342) "6.8 Conclusion") ;; (find-gnomesinthefogpage (+ 19 345) "Conclusion") ;; (find-gnomesinthefogpage (+ 19 355) "A Chronology of the debate") ;; (find-gnomesinthefogpage (+ 18 363) "B Public reactions to Brouwer's intuitionism") ;; (find-gnomesinthefogpage (+ 17 371) "C Logical notations") ;; (find-gnomesinthefogpage (+ 16 373) "Glossary") ;; (find-gnomesinthefogpage (+ 16 377) "Bibliography") ;; (find-gnomesinthefogtext (+ 16 377) "Bibliography") ;; (find-gnomesinthefogpage (+ 16 431) "Index") ;; (find-gnomesinthefogpage (+ 15 445) "Acknowledgements") ;; (find-gnomesinthefogtext "") ;; «heyting» (to ".heyting") ;; (find-books "__logic/__logic.el" "heyting") (code-pdf-page "heytingii" "~/books/__logic/heyting__intuitionism_an_introduction.pdf") (code-pdf-text "heytingii" "~/books/__logic/heyting__intuitionism_an_introduction.pdf" 12) ;; (find-heytingiipage) ;; (find-heytingiipage 7 "Contents") ;; (find-heytingiitext 7 "Contents") ;; (find-heytingiipage (+ 12 1) "Index") ;; (find-heytingiipage (+ 11 143) "Index") ;; (find-heytingiitext "") ;; «hindley» (to ".hindley") ;; (find-books "__logic/__logic.el" "hindley") ;; http://www.users.waitrose.com/~hindley/ (code-pdf "hindleyseldin2" "~/books/__logic/hindley_seldin__lambda-calculus_and_combinators_2nd_ed.pdf") (code-pdftotext "hindleyseldin2" "~/books/__logic/hindley_seldin__lambda-calculus_and_combinators_2nd_ed.pdf" 14) ;; (find-hindleyseldin2page) ;; (find-hindleyseldin2page 8 "Contents") ;; (find-hindleyseldin2page (+ 14 107) "10 Simple typing, Church-style") ;; (find-hindleyseldin2page (+ 14 147) "11J Propositions-as-types and normalization") ;; (find-hindleyseldin2page (+ 14 334) "List of symbols") ;; (find-hindleyseldin2page (+ 14 337) "Index") ;; (find-hindleyseldin2text "") (code-pdf-page "hindleybstt" "~/books/__logic/hindley__basic_simple_type_theory.pdf") (code-pdf-text "hindleybstt" "~/books/__logic/hindley__basic_simple_type_theory.pdf" 13) ;; (find-hindleybsttpage) ;; (find-hindleybsttpage 8 "Contents") ;; (find-hindleybsttpage (+ 13 1) "1 The type-free A-calculus") ;; (find-hindleybsttpage (+ 13 4) "1B /3-reduction and #-normal forms") ;; (find-hindleybsttpage (+ 13 7) "1C ri- and fn-reductions") ;; (find-hindleybsttpage (+ 13 10) "1D Restricted 2-terms") ;; (find-hindleybsttpage (+ 13 12) "2 Assigning types to terms") ;; (find-hindleybsttpage (+ 13 12) "2A The system TAA") ;; (find-hindleybsttpage (+ 13 20) "2B The subject-construction theorem") ;; (find-hindleybsttpage (+ 13 24) "2C Subject reduction and expansion") ;; (find-hindleybsttpage (+ 13 27) "2D The typable terms") ;; (find-hindleybsttpage (+ 13 30) "3 The principal-type algorithm") ;; (find-hindleybsttpage (+ 13 31) "3A Principal types and their history") ;; (find-hindleybsttpage (+ 13 34) "3B Type-substitutions") ;; (find-hindleybsttpage (+ 13 38) "3C Motivating the PT algorithm") ;; (find-hindleybsttpage (+ 13 40) "3D Unification") ;; (find-hindleybsttpage (+ 13 44) "3E The PT algorithm") ;; (find-hindleybsttpage (+ 13 52) "4 Type assignment with equality") ;; (find-hindleybsttpage (+ 13 52) "4A The equality rule") ;; (find-hindleybsttpage (+ 13 57) "4B Semantics and completeness") ;; (find-hindleybsttpage (+ 13 63) "5 A version using typed terms") ;; (find-hindleybsttpage (+ 13 63) "5A Typed terms") ;; (find-hindleybsttpage (+ 13 67) "5B Reducing typed terms") ;; (find-hindleybsttpage (+ 13 71) "5C Normalization theorems") ;; (find-hindleybsttpage (+ 13 74) "6 The correspondence with implication") ;; (find-hindleybsttpage (+ 13 74) "6A Intuitionist implicational logic") ;; (find-hindleybsttpage (+ 13 79) "6B The Curry-Howard isomorphism") ;; (find-hindleybsttpage (+ 13 85) "6C Some weaker logics") ;; (find-hindleybsttpage (+ 13 88) "6D Axiom-based versions") ;; (find-hindleybsttpage (+ 13 93) "7 The converse principal-type algorithm") ;; (find-hindleybsttpage (+ 13 93) "7A The converse PT theorems") ;; (find-hindleybsttpage (+ 13 95) "7B Identifications") ;; (find-hindleybsttpage (+ 13 96) "7C The converse PT proof") ;; (find-hindleybsttpage (+ 13 102) "7D Condensed detachment") ;; (find-hindleybsttpage (+ 13 108) "8 Counting a type's inhabitants") ;; (find-hindleybsttpage (+ 13 108) "8A Inhabitants") ;; (find-hindleybsttpage (+ 13 114) "8B Examples of the search strategy") ;; (find-hindleybsttpage (+ 13 118) "8C The search algorithm") ;; (find-hindleybsttpage (+ 13 124) "8D The Counting algorithm") ;; (find-hindleybsttpage (+ 13 127) "8E The structure of a nf-scheme") ;; (find-hindleybsttpage (+ 13 132) "8F Stretching, shrinking and completeness") ;; (find-hindleybsttpage (+ 13 140) "9 Technical details") ;; (find-hindleybsttpage (+ 13 140) "9A The structure of a term") ;; (find-hindleybsttpage (+ 13 144) "9B Residuals") ;; (find-hindleybsttpage (+ 13 148) "9C The structure of a TA2-deduction") ;; (find-hindleybsttpage (+ 13 151) "9D The structure of a type") ;; (find-hindleybsttpage (+ 13 153) "9E The condensed structure of a type") ;; (find-hindleybsttpage (+ 13 157) "9F Imitating combinatory logic in A-calculus") ;; (find-hindleybsttpage (+ 13 161) "Answers to starred exercises") ;; (find-hindleybsttpage (+ 13 169) "Bibliography") ;; (find-hindleybsttpage (+ 13 177) "Table of principal types") ;; (find-hindleybsttpage (+ 13 179) "Index") ;; (find-hindleybstttext "") ;; «hindley-seldin2» (to ".hindley-seldin2") ;; (find-books "__logic/__logic.el" "hindley-seldin2") (code-pdf-page "hindleyseldin2" "~/books/__logic/hindley_seldin__lambda-calculus_and_combinators_an_introduction.pdf") (code-pdf-text "hindleyseldin2" "~/books/__logic/hindley_seldin__lambda-calculus_and_combinators_an_introduction.pdf" 14) ;; (find-hindleyseldin2page) ;; (find-hindleyseldin2page 8 "Contents") ;; (find-hindleyseldin2page 11 "Preface") ;; (find-hindleyseldin2page (+ 1 189) "Index") ;; (find-hindleyseldin2text "") ;; (find-hindleyseldin2page (+ 14 1) "1 The -calculus") ;; (find-hindleyseldin2page (+ 14 1) "1A Introduction") ;; (find-hindleyseldin2page (+ 14 3) "will be called pure") ;; (find-hindleyseldin2page (+ 14 5) "1B Term-structure and substitution") ;; (find-hindleyseldin2page (+ 14 11) "1C -reduction") ;; (find-hindleyseldin2page (+ 14 16) "1D -equality") ;; (find-hindleyseldin2page (+ 14 21) "2 Combinatory logic") ;; (find-hindleyseldin2page (+ 14 21) "without using bound variables") ;; (find-hindleyseldin2page (+ 14 21) "2A Introduction to CL") ;; (find-hindleyseldin2page (+ 14 24) "2B Weak reduction") ;; (find-hindleyseldin2page (+ 14 26) "2C Abstraction in CL") ;; (find-hindleyseldin2page (+ 14 29) "2D Weak equality") ;; (find-hindleyseldin2page (+ 14 33) "3 The power of and combinators") ;; (find-hindleyseldin2page (+ 14 33) "3A Introduction") ;; (find-hindleyseldin2page (+ 14 34) "3B The fixed-point theorem") ;; (find-hindleyseldin2page (+ 14 36) "3C B¨ohm's theorem") ;; (find-hindleyseldin2page (+ 14 40) "3D The quasi-leftmost-reduction theorem") ;; (find-hindleyseldin2page (+ 14 43) "3E History and interpretation") ;; (find-hindleyseldin2page (+ 14 47) "4 Representing the computable functions") ;; (find-hindleyseldin2page (+ 14 47) "4A Introduction") ;; (find-hindleyseldin2page (+ 14 48) "Definition 4.2 (The Church numerals)") ;; (find-hindleyseldin2text (+ 14 48) "Definition 4.2 (The Church numerals)") ;; (find-hindleyseldin2page (+ 14 50) "4B Primitive recursive functions") ;; (find-hindleyseldin2page (+ 14 56) "4C Recursive functions") ;; (find-hindleyseldin2page (+ 14 61) "4D Abstract numerals and Z") ;; (find-hindleyseldin2page (+ 14 63) "5 The undecidability theorem") ;; (find-hindleyseldin2page (+ 14 69) "6 The formal theories and CLw") ;; (find-hindleyseldin2page (+ 14 69) "6A The definitions of the theories") ;; (find-hindleyseldin2page (+ 14 72) "6B First-order theories") ;; (find-hindleyseldin2page (+ 14 73) "6C Equivalence of theories") ;; (find-hindleyseldin2page (+ 14 76) "7 Extensionality in -calculus") ;; (find-hindleyseldin2page (+ 14 76) "7A Extensional equality") ;; (find-hindleyseldin2page (+ 14 79) "7B -reduction in -calculus") ;; (find-hindleyseldin2page (+ 14 82) "8 Extensionality in combinatory logic") ;; (find-hindleyseldin2page (+ 14 82) "8A Extensional equality") ;; (find-hindleyseldin2page (+ 14 85) "8B Axioms for extensionality in CL") ;; (find-hindleyseldin2page (+ 14 89) "8C Strong reduction") ;; (find-hindleyseldin2page (+ 14 92) "9 Correspondence between and CL") ;; (find-hindleyseldin2page (+ 14 92) "9A Introduction") ;; (find-hindleyseldin2page (+ 14 95) "9B The extensional equalities") ;; (find-hindleyseldin2page (+ 14 100) "9C New abstraction algorithms in CL") ;; (find-hindleyseldin2page (+ 14 102) "9D Combinatory -equality") ;; (find-hindleyseldin2page (+ 14 107) "10 Simple typing, Church-style") ;; (find-hindleyseldin2page (+ 14 107) "10A Simple types") ;; (find-hindleyseldin2page (+ 14 109) "10B Typed -calculus") ;; (find-hindleyseldin2page (+ 14 115) "10C Typed CL") ;; (find-hindleyseldin2page (+ 14 119) "11 Simple typing, Curry-style in CL") ;; (find-hindleyseldin2page (+ 14 119) "11A Introduction") ;; (find-hindleyseldin2page (+ 14 122) "11B The system TA C") ;; (find-hindleyseldin2page (+ 14 126) "11C Subject-construction") ;; (find-hindleyseldin2page (+ 14 127) "11D Abstraction") ;; (find-hindleyseldin2page (+ 14 130) "11E Subject-reduction") ;; (find-hindleyseldin2page (+ 14 134) "11F Typable CL-terms") ;; (find-hindleyseldin2page (+ 14 137) "11G Link with Church's approach") ;; (find-hindleyseldin2page (+ 14 138) "11H Principal types") ;; (find-hindleyseldin2page (+ 14 143) "11I Adding new axioms") ;; (find-hindleyseldin2page (+ 14 147) "11J Propositions-as-types and normalization") ;; (find-hindleyseldin2page (+ 14 155) "11K The equality-rule Eq") ;; (find-hindleyseldin2page (+ 14 159) "12 Simple typing, Curry-style in") ;; (find-hindleyseldin2page (+ 14 159) "12A The system TA") ;; (find-hindleyseldin2page (+ 14 165) "12B Basic properties of TA") ;; (find-hindleyseldin2page (+ 14 170) "12C Typable -terms") ;; (find-hindleyseldin2page (+ 14 173) "12D Propositions-as-types and normalization") ;; (find-hindleyseldin2page (+ 14 176) "12E The equality-rule Eq") ;; (find-hindleyseldin2page (+ 14 180) "13 Generalizations of typing") ;; (find-hindleyseldin2page (+ 14 180) "13A Introduction") ;; (find-hindleyseldin2page (+ 14 181) "13B Dependent function types, introduction") ;; (find-hindleyseldin2page (+ 14 183) "13C Basic generalized typing, Curry-style in") ;; (find-hindleyseldin2page (+ 14 187) "13D Deductive rules to define types") ;; (find-hindleyseldin2page (+ 14 191) "13E Church-style typing in") ;; (find-hindleyseldin2page (+ 14 192) "Definition 13.23 (-cube)") ;; (find-hindleyseldin2text (+ 14 192) "Definition 13.23 (-cube)") ;; (find-hindleyseldin2page (+ 14 202) "13F Normalization in PTSs") ;; (find-hindleyseldin2page (+ 14 209) "13G Propositions-as-types") ;; (find-hindleyseldin2page (+ 14 210) "pairing and projection operators") ;; (find-hindleyseldin2text (+ 14 210) "pairing and projection operators") ;; (find-hindleyseldin2page (+ 14 217) "13H PTSs with equality") ;; (find-hindleyseldin2page (+ 14 220) "14 Models of CL") ;; (find-hindleyseldin2page (+ 14 220) "14A Applicative structures") ;; (find-hindleyseldin2page (+ 14 223) "14B Combinatory algebras") ;; (find-hindleyseldin2page (+ 14 229) "15 Models of -calculus") ;; (find-hindleyseldin2page (+ 14 229) "15A The definition of -model") ;; (find-hindleyseldin2page (+ 14 236) "15B Syntax-free definitions") ;; (find-hindleyseldin2page (+ 14 242) "15C General properties of -models") ;; (find-hindleyseldin2page (+ 14 247) "16 Scott's D and other models") ;; (find-hindleyseldin2page (+ 14 247) "16A Introduction: complete partial orders") ;; (find-hindleyseldin2page (+ 14 252) "16B Continuous functions") ;; (find-hindleyseldin2page (+ 14 256) "16C The construction of D") ;; (find-hindleyseldin2page (+ 14 261) "16D Basic properties of D") ;; (find-hindleyseldin2page (+ 14 267) "16E D is a -model") ;; (find-hindleyseldin2page (+ 14 271) "16F Some other models") ;; (find-hindleyseldin2page (+ 14 276) "Appendix A1 Bound variables and -conversion") ;; (find-hindleyseldin2page (+ 14 282) "Appendix A2 Confluence proofs") ;; (find-hindleyseldin2page (+ 14 293) "Appendix A3 Strong normalization proofs") ;; (find-hindleyseldin2page (+ 14 305) "Appendix A4 Care of your pet combinator") ;; (find-hindleyseldin2page (+ 14 307) "Appendix A5 Answers to starred exercises") ;; (find-hindleyseldin2page (+ 14 323) "References") ;; (find-hindleyseldin2page (+ 14 334) "List of symbols") ;; (find-hindleyseldin2page (+ 14 337) "Index") ;; (find-hindleyseldin2page (+ 14 339) "deduction") ;; (find-hindleyseldin2text ) ;; «hintikka» (to ".hintikka") ;; http://gigapedia.com/items/35756/the-philosophy-of-mathematics--oxford-readings-in-philosophy- (code-djvu "hintikkaphilmat" "~/books/__logic/hintikka_ed__the_philosophy_of_mathematics.djvu") ;; (find-hintikkaphilmatpage 176 "Contents") ;; (find-hintikkaphilmatpage (+ 176 1) "Introduction") ;; (find-hintikkaphilmatpage (+ 176 9) "I. Semantic entailment and formal derivability" "E.W. Beth") ;; (find-hintikkaphilmatpage (+ -12 14) "I. 3. Heuristic considerations") ;; (find-hintikkaphilmatpage (+ -12 42) "II. The completeness of the first-order functional calculus" "Leon Henkin") ;; (find-hintikkaphilmatpage (+ -12 95) "VI. Systems of predicative analysis" "Solomon Feferman") ;; «hofstadter» (to ".hofstadter") (code-xpdf "geb" "~/books/__logic/hofstadter__godel_escher_bach_an_eternal_golden_braid.pdf") (code-pdftotext "geb" "~/books/__logic/hofstadter__godel_escher_bach_an_eternal_golden_braid.pdf" 0) ;; (ee-page-parameters "geb" 0) ;; (find-gebpage 1 "Contents") ;; (find-gebpage 193 "The Converse of the Fantasy Rule") ;; (find-gebtext 193 "The Converse of the Fantasy Rule") ;; (find-gebpage (+ 9 761) "Index") ;; (find-gebtext "") ;; «howard» (to ".howard") ;; (find-books "__logic/__logic.el" "howard") ;; (find-LATEX "catsem-u.bib" "bib-Howard") ;; https://www.cs.cmu.edu/~crary/819-f09/Howard80.pdf ;; (find-fline "$S/https/www.cs.cmu.edu/~crary/819-f09/") (code-pdf-page "howard80" "$S/https/www.cs.cmu.edu/~crary/819-f09/Howard80.pdf") (code-pdf-text "howard80" "$S/https/www.cs.cmu.edu/~crary/819-f09/Howard80.pdf" -478) ;; (find-howard80page) ;; (find-howard80text) ;; (find-howard80page (+ -478 479)) ;; (find-howard80page (+ -478 479) "I. Intuitionistic propositional calculus") ;; (find-howard80page (+ -478 480) "1. Formulation of the sequent calculus") ;; (find-howard80page (+ -478 480) "2. Type symbols, terms and constructions") ;; (find-howard80page (+ -478 481) "3. Correspondence between derivations and terms") ;; (find-howard80page (+ -478 481) "4. Interpretation of terms") ;; (find-howard80page (+ -478 482) "Lauchli") ;; (find-howard80page (+ -478 482) "5. Normalization of terms and cut elimination") ;; (find-howard80page (+ -478 483) "6. Addition of not, and, and or to P(->)") ;; (find-howard80page (+ -478 484) "II. Heyting Arithmetic") ;; (find-howard80page (+ -478 485) "7. Constructions") ;; (find-howard80page (+ -478 485) "8. Special terms") ;; (find-howard80page (+ -478 486) "9. Constructions and derivations in H(imp, and, Fa)") ;; (find-howard80page (+ -478 486) "10. Interpretation of terms of H(imp, and, Fa)") ;; (find-howard80page (+ -478 487) "11. Normalization of terms") ;; (find-howard80page (+ -478 488) "12. Introduction of Ex") ;; (find-howard80page (+ -478 489) "13. Infinite constructions") ;; (find-howard80page (+ -478 490) "References") ;; «hott» (to ".hott") ;; (find-books "__logic/__logic.el" "hott") ;; (find-LATEX "catsem-u.bib" "bib-HOTT") ;; https://homotopytypetheory.org/book/ ;; https://hott.github.io/book/ ;; https://hott.github.io/book/nightly/hott-online-1204-g7415493.pdf ;; http://saunders.phil.cmu.edu/book/hott-online.pdf (code-pdf-page "hott" "$S/https/hott.github.io/book/nightly/hott-online-1204-g7415493.pdf") (code-pdf-text "hott" "$S/https/hott.github.io/book/nightly/hott-online-1204-g7415493.pdf" 12) (code-pdf-page "hott" "$S/http/saunders.phil.cmu.edu/book/hott-online.pdf") (code-pdf-text "hott" "$S/http/saunders.phil.cmu.edu/book/hott-online.pdf" 12) ;; (find-hottpage) ;; (find-hotttext) ;; (find-hottpage 7 "Contents") ;; (find-hotttext 7 "Contents") ;; (find-hottpage (+ 12 1) "Introduction") ;; (find-hottpage (+ 12 6) "small object argument") ;; (find-hotttext (+ 12 6) "small object argument") ;; (find-hottpage (+ 12 15) "I Foundations") ;; (find-hottpage (+ 12 17) "1 Type theory") ;; (find-hottpage (+ 12 17) "1.1 Type theory versus set theory") ;; (find-hottpage (+ 12 18) "a witness to the provability of A") ;; (find-hotttext (+ 12 18) "a witness to the provability of A") ;; (find-hottpage (+ 12 21) "1.2 Function types") ;; (find-hottpage (+ 12 23) "this means that y gets captured") ;; (find-hotttext (+ 12 23) "this means that y gets captured") ;; (find-hottpage (+ 12 24) "1.3 Universes and families") ;; (find-hottpage (+ 12 25) "1.4 Dependent function types (-types)") ;; (find-hottpage (+ 12 26) "1.5 Product types") ;; (find-hottpage (+ 12 30) "1.6 Dependent pair types (-types)") ;; (find-hottpage (+ 12 33) "1.7 Coproduct types") ;; (find-hottpage (+ 12 35) "1.8 The type of booleans") ;; (find-hottpage (+ 12 36) "1.9 The natural numbers") ;; (find-hottpage (+ 12 40) "1.10 Pattern matching and recursion") ;; (find-hottpage (+ 12 41) "1.11 Propositions as types") ;; (find-hottpage (+ 12 47) "1.12 Identity types") ;; (find-hottpage (+ 12 54) "Notes") ;; (find-hottpage (+ 12 56) "Exercises") ;; (find-hottpage (+ 12 59) "2 Homotopy type theory") ;; (find-hottpage (+ 12 62) "2.1 Types are higher groupoids") ;; (find-hottpage (+ 12 71) "2.2 Functions are functors") ;; (find-hottpage (+ 12 72) "2.3 Type families are fibrations") ;; (find-hottpage (+ 12 76) "2.4 Homotopies and equivalences") ;; (find-hottpage (+ 12 79) "2.5 The higher groupoid structure of type formers") ;; (find-hottpage (+ 12 81) "2.6 Cartesian product types") ;; (find-hottpage (+ 12 83) "2.7 -types") ;; (find-hottpage (+ 12 86) "2.8 The unit type") ;; (find-hottpage (+ 12 86) "2.9 -types and the function extensionality axiom") ;; (find-hottpage (+ 12 89) "2.10 Universes and the univalence axiom") ;; (find-hottpage (+ 12 91) "2.11 Identity type") ;; (find-hottpage (+ 12 93) "2.12 Coproducts") ;; (find-hottpage (+ 12 95) "2.13 Natural numbers") ;; (find-hottpage (+ 12 97) "2.14 Example: equality of structures") ;; (find-hottpage (+ 12 100) "2.15 Universal properties") ;; (find-hottpage (+ 12 102) "Notes") ;; (find-hottpage (+ 12 104) "Exercises") ;; (find-hottpage (+ 12 107) "3 Sets and logic") ;; (find-hottpage (+ 12 107) "3.1 Sets and n-types") ;; (find-hottpage (+ 12 109) "3.2 Propositions as types?") ;; (find-hotttext (+ 12 109) "Propositions as types?") ;; (find-hottpage (+ 12 111) "3.3 Mere propositions") ;; (find-hottpage (+ 12 113) "3.4 Classical vs. intuitionistic logic") ;; (find-hottpage (+ 12 114) "3.5 Subsets and propositional resizing") ;; (find-hottpage (+ 12 116) "3.6 The logic of mere propositions") ;; (find-hottpage (+ 12 117) "3.7 Propositional truncation") ;; (find-hottpage (+ 12 118) "3.8 The axiom of choice") ;; (find-hottpage (+ 12 120) "3.9 The principle of unique choice") ;; (find-hottpage (+ 12 121) "3.10 When are propositions truncated?") ;; (find-hottpage (+ 12 123) "3.11 Contractibility") ;; (find-hottpage (+ 12 126) "Notes") ;; (find-hottpage (+ 12 127) "Exercises") ;; (find-hottpage (+ 12 129) "4 Equivalences") ;; (find-hottpage (+ 12 130) "4.1 Quasi-inverses") ;; (find-hottpage (+ 12 132) "4.2 Half adjoint equivalences") ;; (find-hottpage (+ 12 136) "4.3 Bi-invertible maps") ;; (find-hottpage (+ 12 136) "4.4 Contractible fibers") ;; (find-hottpage (+ 12 138) "4.5 On the definition of equivalences") ;; (find-hottpage (+ 12 138) "4.6 Surjections and embeddings") ;; (find-hottpage (+ 12 139) "4.7 Closure properties of equivalences") ;; (find-hottpage (+ 12 142) "4.8 The object classifier") ;; (find-hottpage (+ 12 144) "4.9 Univalence implies function extensionality") ;; (find-hottpage (+ 12 146) "Notes") ;; (find-hottpage (+ 12 146) "Exercises") ;; (find-hottpage (+ 12 149) "5 Induction") ;; (find-hottpage (+ 12 149) "5.1 Introduction to inductive types") ;; (find-hottpage (+ 12 152) "5.2 Uniqueness of inductive types") ;; (find-hottpage (+ 12 154) "5.3 W-types") ;; (find-hottpage (+ 12 157) "5.4 Inductive types are initial algebras") ;; (find-hottpage (+ 12 160) "5.5 Homotopy-inductive types") ;; (find-hottpage (+ 12 164) "5.6 The general syntax of inductive definitions") ;; (find-hottpage (+ 12 168) "5.7 Generalizations of inductive types") ;; (find-hottpage (+ 12 170) "5.8 Identity types and identity systems") ;; (find-hottpage (+ 12 174) "Notes") ;; (find-hottpage (+ 12 175) "Exercises") ;; (find-hottpage (+ 12 179) "6 Higher inductive types") ;; (find-hottpage (+ 12 179) "6.1 Introduction") ;; (find-hottpage (+ 12 181) "6.2 Induction principles and dependent paths") ;; (find-hottpage (+ 12 186) "6.3 The interval") ;; (find-hottpage (+ 12 187) "6.4 Circles and spheres") ;; (find-hottpage (+ 12 189) "6.5 Suspensions") ;; (find-hottpage (+ 12 192) "6.6 Cell complexes") ;; (find-hottpage (+ 12 194) "6.7 Hubs and spokes") ;; (find-hottpage (+ 12 195) "6.8 Pushouts") ;; (find-hottpage (+ 12 198) "6.9 Truncations") ;; (find-hottpage (+ 12 201) "6.10 Quotients") ;; (find-hottpage (+ 12 206) "6.11 Algebra") ;; (find-hottpage (+ 12 211) "6.12 The flattening lemma") ;; (find-hottpage (+ 12 216) "6.13 The general syntax of higher inductive definitions") ;; (find-hottpage (+ 12 218) "Notes") ;; (find-hottpage (+ 12 219) "Exercises") ;; (find-hottpage (+ 12 221) "7 Homotopy n-types") ;; (find-hottpage (+ 12 221) "7.1 Definition of n-types") ;; (find-hottpage (+ 12 225) "7.2 Uniqueness of identity proofs and Hedberg's theorem") ;; (find-hottpage (+ 12 228) "7.3 Truncations") ;; (find-hottpage (+ 12 234) "7.4 Colimits of n-types") ;; (find-hottpage (+ 12 238) "7.5 Connectedness") ;; (find-hottpage (+ 12 243) "7.6 Orthogonal factorization") ;; (find-hottpage (+ 12 248) "7.7 Modalities") ;; (find-hottpage (+ 12 252) "Notes") ;; (find-hottpage (+ 12 253) "Exercises") ;; (find-hottpage (+ 12 257) "II Mathematics") ;; (find-hottpage (+ 12 259) "8 Homotopy theory") ;; (find-hottpage (+ 12 263) "8.1 1 (S1 )") ;; (find-hottpage (+ 12 271) "8.2 Connectedness of suspensions") ;; (find-hottpage (+ 12 272) "8.3 kn of an n-connected space and k