Cover -- Contents -- Preface -- Chapter 1 Syntax of First-Order Languages -- 1.1 Symbols of first-order languages -- 1.2 Terms -- 1.3 Logical formulas -- 1.4 Free variables and substitutions -- 1.5 G246;del terms of formulas -- 1.6 Proof by structural induction -- Chapter 2 Models of First-Order Languages -- 2.1 Domains and interpretations -- 2.2 Assignments and models -- 2.3 Semantics of terms -- 2.4 Semantics of logical connective symbols -- 2.5 Semantics of formulas -- 2.6 Satisfiability and validity -- 2.7 Valid formulas with -- 2.8 Hintikka set -- 2.9 Herbrand model -- 2.10 Herbrand model with variables -- 2.11 Substitution lemma -- 2.12 Theorem of isomorphism -- Chapter 3 Formal Inference Systems -- 3.1 G inference system -- 3.2 Inference trees, proof trees and provable sequents -- 3.3 Soundness of the G inference system -- 3.4 Compactness and consistency -- 3.5 Completeness of the G inference system -- 3.6 Some commonly used inference rules -- 3.7 Proof theory and model theory -- Chapter 4 Computability & Representability -- 4.1 Formal theory -- 4.2 Elementary arithmetic theory -- 4.3 P-kernel on N -- 4.4 Church-Turing thesis -- 4.5 Problem of representability -- 4.6 States of P-kernel -- 4.7 Operational calculus of P-kernel -- 4.8 Representations of statements -- 4.9 Representability theorem -- Chapter 5 G246;del Theorems -- 5.1 Self-referential proposition -- 5.2 Decidable sets -- 5.3 Fixed point equation in 928; -- 5.4 G246;del8217;s incompleteness theorem -- 5.5 G246;del8217;s consistency theorem -- 5.6 Halting problem -- Chapter 6 Sequences of Formal Theories -- 6.1 Two examples -- 6.2 Sequences of formal theories -- 6.3 Proschemes -- 6.4 Resolvent sequences -- 6.5 Default expansion sequences -- 6.6 Forcing sequences -- 6.7 Discussions on proschemes -- Chapter 7 Revision Calculus -- 7.1 Necessary antecedents of formal consequences -- 7.2 New conjectures and new axioms -- 7.3 Refutation by facts and maximal contraction -- 7.4 R-calculus -- 7.5 Some examples -- 7.6 Special theory of relativity -- 7.7 Darwin8217;s theory of evolution -- 7.8 Reachability of R-calculus -- 7.9 Soundness and completeness of R-calculus -- 7.10 Basic theorem of testing -- Chapter 8 Version Sequences -- 8.1 Versions and version sequences -- 8.2 The Proscheme OPEN -- 8.3 Convergence of the proscheme -- 8.4 Commutativity of the proscheme -- 8.5 Independence of the proscheme -- 8.6 Reliable proschemes -- Chapter 9 Inductive Inference -- 9.1 Ground terms, basic sentences, and basic instances -- 9.2 Inductive inference system A -- 9.3 Inductive versions and inductive process -- 9.4 The Proscheme GUINA -- 9.5 Convergence of the proscheme GUINA -- 9.6 Commutativity of the proscheme GUINA -- 9.7 Independence of the proscheme GUINA -- Chapter 10 Workflows for Scientific Discovery -- 10.1 Three language environments -- 10.2 Basic principles of the meta-language environment -- 10.3 Axiomatization -- 10.4 Formal methods -- 10.5 Workflow of scientific research -- Appendix 1 Sets and Maps -- Appendix 2 Substitution Lemma and Its Proof -- Appendix 3 Proof of the Representability Theorem -- A3.1 Representation of the while statement in 928; -- A3.2 Representability of the P-procedure body.