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 Gö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 Gödel Theorems
5.1 Self-referential proposition
5.2 Decidable sets
5.3 Fixed point equation in Pi;
5.4 Gödel's incompleteness theorem
5.5 Gödel'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 Darwin'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 Pi;
A3.2 Representability of the P-procedure body.