THE OPEN LOGIC TEXT

2y ago
20 Views
2 Downloads
3.83 MB
944 Pages
Last View : 19d ago
Last Download : 2m ago
Upload by : Sasha Niles
Transcription

THE OPEN LOGIC TEXTComplete BuildOpen Logic ProjectRevision: b92204b (master)2021-04-17The Open Logic Text bythe Open Logic Projectis licensed under a Creative Commons Attribution 4.0 International License.

About the Open Logic ProjectThe Open Logic Text is an open-source, collaborative textbook of formal metalogic and formal methods, starting at an intermediate level (i.e., after an introductory formal logic course). Though aimed at a non-mathematical audience(in particular, students of philosophy and computer science), it is rigorous.Coverage of some topics currently included may not yet be complete, andmany sections still require substantial revision. We plan to expand the text tocover more topics in the future. We also plan to add features to the text, suchas a glossary, a list of further reading, historical notes, pictures, better explanations, sections explaining the relevance of results to philosophy, computerscience, and mathematics, and more problems and examples. If you find anerror, or have a suggestion, please let the project team know.The project operates in the spirit of open source. Not only is the text freelyavailable, we provide the LaTeX source under the Creative Commons Attribution license, which gives anyone the right to download, use, modify, rearrange, convert, and re-distribute our work, as long as they give appropriatecredit. Please see the Open Logic Project website at openlogicproject.org foradditional information.1

ContentsAbout the Open Logic ProjectI1231Naı̈ve Set Theory22Sets1.1 Extensionality . . . . . . . . . . .1.2 Subsets and Power Sets . . . . . .1.3 Some Important Sets . . . . . . . .1.4 Unions and Intersections . . . . .1.5 Pairs, Tuples, Cartesian Products .1.6 Russell’s Paradox . . . . . . . . .Problems . . . . . . . . . . . . . . . . . .2424252627303233Relations2.1 Relations as Sets . . . . . . . .2.2 Philosophical Reflections . . .2.3 Special Properties of Relations2.4 Equivalence Relations . . . . .2.5 Orders . . . . . . . . . . . . . .2.6 Graphs . . . . . . . . . . . . . .2.7 Operations on Relations . . . .Problems . . . . . . . . . . . . . . . .343436373839414242Functions3.1 Basics . . . . . . . . . . .3.2 Kinds of Functions . . . .3.3 Functions as Relations . .3.4 Inverses of Functions . .3.5 Composition of Functions3.6 Partial Functions . . . . .Problems . . . . . . . . . . . . .4444464849505152.2.

CONTENTS456II7The Size of Sets4.1 Introduction . . . . . . . . . . . . . . . . . . .4.2 Enumerations and Enumerable Sets . . . . . .4.3 Cantor’s Zig-Zag Method . . . . . . . . . . . .4.4 Pairing Functions and Codes . . . . . . . . . .4.5 An Alternative Pairing Function . . . . . . . .4.6 Non-enumerable Sets . . . . . . . . . . . . . .4.7 Reduction . . . . . . . . . . . . . . . . . . . . .4.8 Equinumerosity . . . . . . . . . . . . . . . . .4.9 Sets of Different Sizes, and Cantor’s Theorem4.10 The Notion of Size, and Schröder-Bernstein .4.11 Enumerations and Enumerable Sets . . . . . .4.12 Non-enumerable Sets . . . . . . . . . . . . . .4.13 Reduction . . . . . . . . . . . . . . . . . . . . .Problems . . . . . . . . . . . . . . . . . . . . . . . . .Arithmetization5.1 From N to Z . . . . . . . . . . .5.2 From Z to Q . . . . . . . . . . .5.3 The Real Line . . . . . . . . . . .5.4 From Q to R . . . . . . . . . . .5.5 Some Philosophical Reflections .5.6 Ordered Rings and Fields . . . .5.7 The Reals as Cauchy SequencesProblems . . . . . . . . . . . . . . . . .Infinite Sets6.1 Hilbert’s Hotel . . . . . . . . .6.2 Dedekind Algebras . . . . . .6.3 Arithmetical Induction . . . .6.4 Dedekind’s “Proof” . . . . . .6.5 A Proof of 3.777779808183848791.929293959698Propositional LogicSyntax and Semantics7.1 Introduction . . . . . . . .7.2 Propositional Formulas . .7.3 Preliminaries . . . . . . . .7.4 Valuations and Satisfaction7.5 Semantic Notions . . . . .Problems . . . . . . . . . . . . . .Release : b92204b (2021-04-17)100.1021021031051061071083

CONTENTS8.109109111111113114The Sequent Calculus9.1 Rules and Derivations . . . . . . . . . . . . . . .9.2 Propositional Rules . . . . . . . . . . . . . . . .9.3 Structural Rules . . . . . . . . . . . . . . . . . .9.4 Derivations . . . . . . . . . . . . . . . . . . . . .9.5 Examples of Derivations . . . . . . . . . . . . .9.6 Proof-Theoretic Notions . . . . . . . . . . . . . .9.7 Derivability and Consistency . . . . . . . . . . .9.8 Derivability and the Propositional Connectives9.9 Soundness . . . . . . . . . . . . . . . . . . . . . .Problems . . . . . . . . . . . . . . . . . . . . . . . . . .11611611711811912012412612712813210 Natural Deduction10.1 Rules and Derivations . . . . . . . . . . . . . . .10.2 Propositional Rules . . . . . . . . . . . . . . . .10.3 Derivations . . . . . . . . . . . . . . . . . . . . .10.4 Examples of Derivations . . . . . . . . . . . . .10.5 Proof-Theoretic Notions . . . . . . . . . . . . . .10.6 Derivability and Consistency . . . . . . . . . . .10.7 Derivability and the Propositional Connectives10.8 Soundness . . . . . . . . . . . . . . . . . . . . . .Problems . . . . . . . . . . . . . . . . . . . . . . . . . .13313313413513614014114314414811 Tableaux11.1 Rules and Tableaux . . . . . . . . . . . . . . . .11.2 Propositional Rules . . . . . . . . . . . . . . . .11.3 Tableaux . . . . . . . . . . . . . . . . . . . . . . .11.4 Examples of Tableaux . . . . . . . . . . . . . . .11.5 Proof-Theoretic Notions . . . . . . . . . . . . . .11.6 Derivability and Consistency . . . . . . . . . . .11.7 Derivability and the Propositional Connectives11.8 Soundness . . . . . . . . . . . . . . . . . . . . . .Problems . . . . . . . . . . . . . . . . . . . . . . . . . .1491491501511521561581601621659Derivation Systems8.1 Introduction . . . . .8.2 The Sequent Calculus8.3 Natural Deduction . .8.4 Tableaux . . . . . . . .8.5 Axiomatic Derivations.12 Axiomatic Derivations16612.1 Rules and Derivations . . . . . . . . . . . . . . . . . . . . . . . . 16612.2 Axiom and Rules for the Propositional Connectives . . . . . . . 1674Release : b92204b (2021-04-17)

CONTENTS12.3 Examples of Derivations . . . . . . . . . . . . .12.4 Proof-Theoretic Notions . . . . . . . . . . . . . .12.5 The Deduction Theorem . . . . . . . . . . . . . .12.6 Derivability and Consistency . . . . . . . . . . .12.7 Derivability and the Propositional Connectives12.8 Soundness . . . . . . . . . . . . . . . . . . . . . .Problems . . . . . . . . . . . . . . . . . . . . . . . . . .13 The Completeness Theorem13.1 Introduction . . . . . . . . . . . . . . . . . .13.2 Outline of the Proof . . . . . . . . . . . . . .13.3 Complete Consistent Sets of Sentences . . .13.4 Lindenbaum’s Lemma . . . . . . . . . . . . .13.5 Construction of a Model . . . . . . . . . . . .13.6 The Completeness Theorem . . . . . . . . .13.7 The Compactness Theorem . . . . . . . . . .13.8 A Direct Proof of the Compactness TheoremProblems . . . . . . . . . . . . . . . . . . . . . . . 1182183First-order Logic18414 Syntax and Semantics14.1 Introduction . . . . . . . . . . . . . . . . . . .14.2 First-Order Languages . . . . . . . . . . . . . .14.3 Terms and Formulas . . . . . . . . . . . . . . .14.4 Unique Readability . . . . . . . . . . . . . . .14.5 Main operator of a Formula . . . . . . . . . . .14.6 Subformulas . . . . . . . . . . . . . . . . . . .14.7 Free Variables and Sentences . . . . . . . . . .14.8 Substitution . . . . . . . . . . . . . . . . . . . .14.9 Structures for First-order Languages . . . . .14.10 Covered Structures for First-order Languages14.11 Satisfaction of a Formula in a Structure . . . .14.12 Variable Assignments . . . . . . . . . . . . . .14.13 Extensionality . . . . . . . . . . . . . . . . . .14.14 Semantic Notions . . . . . . . . . . . . . . . .Problems . . . . . . . . . . . . . . . . . . . . . . . . 5 Theories and Their Models15.1 Introduction . . . . . . . . . . . . .15.2 Expressing Properties of Structures15.3 Examples of First-Order Theories .15.4 Expressing Relations in a Structure.212212214214217Release : b92204b (2021-04-17).5

CONTENTS15.5 The Theory of Sets . . . . . . . . . . . . . . . . . . . . . . . . . . 21815.6 Expressing the Size of Structures . . . . . . . . . . . . . . . . . . 220Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22116 Derivation Systems16.1 Introduction . . . . .16.2 The Sequent Calculus16.3 Natural Deduction . .16.4 Tableaux . . . . . . . .16.5 Axiomatic Derivations.22322322522522722817 The Sequent Calculus17.1 Rules and Derivations . . . . . . . . . . . . . . .17.2 Propositional Rules . . . . . . . . . . . . . . . .17.3 Quantifier Rules . . . . . . . . . . . . . . . . . .17.4 Structural Rules . . . . . . . . . . . . . . . . . .17.5 Derivations . . . . . . . . . . . . . . . . . . . . .17.6 Examples of Derivations . . . . . . . . . . . . .17.7 Derivations with Quantifiers . . . . . . . . . . .17.8 Proof-Theoretic Notions . . . . . . . . . . . . . .17.9 Derivability and Consistency . . . . . . . . . . .17.10 Derivability and the Propositional Connectives17.11 Derivability and the Quantifiers . . . . . . . . .17.12 Soundness . . . . . . . . . . . . . . . . . . . . . .17.13 Derivations with Identity predicate . . . . . . .17.14 Soundness with Identity predicate . . . . . . . .Problems . . . . . . . . . . . . . . . . . . . . . . . . . 8 Natural Deduction18.1 Rules and Derivations . . . . . . . . . . . . . . .18.2 Propositional Rules . . . . . . . . . . . . . . . .18.3 Quantifier Rules . . . . . . . . . . . . . . . . . .18.4 Derivations . . . . . . . . . . . . . . . . . . . . .18.5 Examples of Derivations . . . . . . . . . . . . .18.6 Derivations with Quantifiers . . . . . . . . . . .18.7 Proof-Theoretic Notions . . . . . . . . . . . . . .18.8 Derivability and Consistency . . . . . . . . . . .18.9 Derivability and the Propositional Connectives18.10 Derivability and the Quantifiers . . . . . . . . .18.11 Soundness . . . . . . . . . . . . . . . . . . . . . .18.12 Derivations with Identity predicate . . . . . . .18.13 Soundness with Identity predicate . . . . . . . .Problems . . . . . . . . . . . . . . . . . . . . . . . . . lease : b92204b (2021-04-17)

CONTENTS19 Tableaux19.1 Rules and Tableaux . . . . . . . . . . . . . . . .19.2 Propositional Rules . . . . . . . . . . . . . . . .19.3 Quantifier Rules . . . . . . . . . . . . . . . . . .19.4 Tableaux . . . . . . . . . . . . . . . . . . . . . . .19.5 Examples of Tableaux . . . . . . . . . . . . . . .19.6 Tableaux with Quantifiers . . . . . . . . . . . . .19.7 Proof-Theoretic Notions . . . . . . . . . . . . . .19.8 Derivability and Consistency . . . . . . . . . . .19.9 Derivability and the Propositional Connectives19.10 Derivability and the Quantifiers . . . . . . . . .19.11 Soundness . . . . . . . . . . . . . . . . . . . . . .19.12 Tableaux with Identity predicate . . . . . . . . .19.13 Soundness with Identity predicate . . . . . . . .Problems . . . . . . . . . . . . . . . . . . . . . . . . . .27727727827928028128528929129229529629829930020 Axiomatic Derivations20.1 Rules and Derivations . . . . . . . . . . . . . . . . .20.2 Axiom and Rules for the Propositional Connectives20.3 Axioms and Rules for Quantifiers . . . . . . . . . .20.4 Examples of Derivations . . . . . . . . . . . . . . .20.5 Derivations with Quantifiers . . . . . . . . . . . . .20.6 Proof-Theoretic Notions . . . . . . . . . . . . . . . .20.7 The Deduction Theorem . . . . . . . . . . . . . . . .20.8 The Deduction Theorem with Quantifiers . . . . .20.9 Derivability and Consistency . . . . . . . . . . . . .20.10 Derivability and the Propositional Connectives . .20.11 Derivability and the Quantifiers . . . . . . . . . . .20.12 Soundness . . . . . . . . . . . . . . . . . . . . . . . .20.13 Derivations with Identity predicate . . . . . . . . .Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . .30130130230330430530630730931031131131231331421 The Completeness Theorem21.1 Introduction . . . . . . . . . . . . . . . . . .21.2 Outline of the Proof . . . . . . . . . . . . . .21.3 Complete Consistent Sets of Sentences . . .21.4 Henkin Expansion . . . . . . . . . . . . . . .21.5 Lindenbaum’s Lemma . . . . . . . . . . . . .21.6 Construction of a Model . . . . . . . . . . . .21.7 Identity . . . . . . . . . . . . . . . . . . . . .21.8 The Completeness Theorem . . . . . . . . .21.9 The Compactness Theorem . . . . . . . . . .21.10 A Direct Proof of the Compactness Theorem21.11 The Löwenheim-Skolem Theorem . . . . . .315315316318319321322324326327329330Release : b92204b (2021-04-17).7

CONTENTSProblems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33022 Beyond First-order Logic22.1 Overview . . . . . .22.2 Many-Sorted Logic .22.3 Second-Order logic .22.4 Higher-Order logic .22.5 Intuitionistic Logic .22.6 Modal Logics . . . .22.7 Other Logics . . . .IV.Model Theory23 Basics of Model Theory23.1 Reducts and Expansions23.2 Substructures . . . . . . .23.3 Overspill . . . . . . . . .23.4 Isomorphic Structures . .23.5 The Theory of a Structure23.6 Partial Isomorphisms . .23.7 Dense Linear Orders . . .Problems . . . . . . . . . . . . 35635724 Models of Arithmetic24.1 Introduction . . . . . . . . . . . .24.2 Standard Models of Arithmetic . .24.3 Non-Standard Models . . . . . . .24.4 Models of Q . . . . . . . . . . . . .24.5 Models of PA . . . . . . . . . . . .24.6 Computable Models of ArithmeticProblems . . . . . . . . . . . . . . . . . .35835835936136236436836925 The Interpolation Theorem25.1 Introduction . . . . . . . . . .25.2 Separation of Sentences . . . .25.3 Craig’s Interpolation Theorem25.4 The Definability Theorem . . .37137137137337526 Lindström’s Theorem26.1 Introduction . . . . . . . . . . . . . . . . . . . . .26.2 Abstract Logics . . . . . . . . . . . . . . . . . . . .26.3 Compactness and Löwenheim-Skolem Properties26.4 Lindström’s Theorem . . . . . . . . . . . . . . . .3783783783803818.Release : b92204b (2021-04-17)

CONTENTSVComputability27 Recursive Functions27.1 Introduction . . . . . . . . . . . . . . . . . . . .27.2 Primitive Recursion . . . . . . . . . . . . . . . .27.3 Composition . . . . . . . . . . . . . . . . . . . .27.4 Primitive Recursion Functions . . . . . . . . . .27.5 Primitive Recursion Notations . . . . . . . . . .27.6 Primitive Recursive Functions are Computable27.7 Examples of Primitive Recursive Functions . . .27.8 Primitive Recursive Relations . . . . . . . . . .27.9 Bounded Minimization . . . . . . . . . . . . . .27.10 Primes . . . . . . . . . . . . . . . . . . . . . . . .27.11 Sequences . . . . . . . . . . . . . . . . . . . . . .27.12 Trees . . . . . . . . . . . . . . . . . . . . . . . . .27.13 Other Recursions . . . . . . . . . . . . . . . . . .27.14 Non-Primitive Recursive Functions . . . . . . .27.15 Partial Recursive Functions . . . . . . . . . . . .27.16 The Normal Form Theorem . . . . . . . . . . . .27.17 The Halting Problem . . . . . . . . . . . . . . . .27.18 General Recursive Functions . . . . . . . . . . .Problems . . . . . . . . . . . . . . . . . . . . . . . . . 40740940941141128 Computability Theory28.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . .28.2 Coding Computations . . . . . . . . . . . . . . . . . . . . . . .28.3 The Normal Form Theorem . . . . . . . . . . . . . . . . . . . .28.4 The s-m-n Theorem . . . . . . . . . . . . . . . . . . . . . . . .28.5 The Universal Partial Computable Function . . . . . . . . . .28.6 No Universal Computable Function . . . . . . . . . . . . . . .28.7 The Halting Problem . . . . . . . . . . . . . . . . . . . . . . . .28.8 Comparison with Russell’s Paradox . . . . . . . . . . . . . . .28.9 Computable Sets . . . . . . . . . . . . . . . . . . . . . . . . . .28.10 Computably Enumerable Sets . . . . . . . . . . . . . . . . . .28.11 Definitions of C. E. Sets . . . . . . . . . . . . . . . . . . . . . .28.12 Union and Intersection of C.E. Sets . . . . . . . . . . . . . . .28.13 Computably Enumerable Sets not Closed under Complement28.14 Reducibility . . . . . . . . . . . . . . . . . . . . . . . . . . . . .28.15 Properties of Reducibility . . . . . . . . . . . . . . . . . . . . .28.16 Complete Computably Enumerable Sets . . . . . . . . . . . .28.17 An Example of Reducibility . . . . . . . . . . . . . . . . . . . .28.18 Totality is Undecidable . . . . . . . . . . . . . . . . . . . . . .28.19 Rice’s Theorem . . . . . . . . . . . . . . . . . . . . . . . . . . .28.20 The Fixed-Point Theorem . . . . . . . . . . . . . . . . . . . . 27428429430432Release : b92204b (2021-04-17).

About the Open Logic Project The Open Logic Text is an open-source, collaborative textbook of formal meta-logic and formal methods, starting at an intermediate level (i.e., after an intro-ductory formal logic course). Though aimed at a non-mathematical audience (in particular, stud

Related Documents:

Text text text Text text text Text text text Text text text Text text text Text text text Text text text Text text text Text text text Text text text Text text text

May 02, 2018 · D. Program Evaluation ͟The organization has provided a description of the framework for how each program will be evaluated. The framework should include all the elements below: ͟The evaluation methods are cost-effective for the organization ͟Quantitative and qualitative data is being collected (at Basics tier, data collection must have begun)

Silat is a combative art of self-defense and survival rooted from Matay archipelago. It was traced at thé early of Langkasuka Kingdom (2nd century CE) till thé reign of Melaka (Malaysia) Sultanate era (13th century). Silat has now evolved to become part of social culture and tradition with thé appearance of a fine physical and spiritual .

On an exceptional basis, Member States may request UNESCO to provide thé candidates with access to thé platform so they can complète thé form by themselves. Thèse requests must be addressed to esd rize unesco. or by 15 A ril 2021 UNESCO will provide thé nomineewith accessto thé platform via their émail address.

̶The leading indicator of employee engagement is based on the quality of the relationship between employee and supervisor Empower your managers! ̶Help them understand the impact on the organization ̶Share important changes, plan options, tasks, and deadlines ̶Provide key messages and talking points ̶Prepare them to answer employee questions

Dr. Sunita Bharatwal** Dr. Pawan Garga*** Abstract Customer satisfaction is derived from thè functionalities and values, a product or Service can provide. The current study aims to segregate thè dimensions of ordine Service quality and gather insights on its impact on web shopping. The trends of purchases have

Chính Văn.- Còn đức Thế tôn thì tuệ giác cực kỳ trong sạch 8: hiện hành bất nhị 9, đạt đến vô tướng 10, đứng vào chỗ đứng của các đức Thế tôn 11, thể hiện tính bình đẳng của các Ngài, đến chỗ không còn chướng ngại 12, giáo pháp không thể khuynh đảo, tâm thức không bị cản trở, cái được

Dynamic Logic Dynamic Circuits will be introduced and their performance in terms of power, area, delay, energy and AT2 will be reviewed. We will review the following logic families: Domino logic P-E logic NORA logic 2-phase logic Multiple O/P domino logic Cascode logic