semantics:completeness
INTRODUCTION TO
THE SECOND PART
Yoshihiro Maruyama
co-taught with Pascal Bercher
on the legacy of John Slaney
2
➤ We have learned the basics of logic (natural deduction calculus, truth table semantics, etc.).
➤ What is logic all about? What is it doing? And why?
➤ We applied formal rules so many times, but why? Why do we apply rules and prove theorems?
What is the meaning or significance of doing so?
➤ Why do we need a proof system in the first place? Why do we have to play such a mechanical
rule-following game?
➤ Logic is not a fancy symbol manipulation game. We are doing something more meaningful.
WHAT IS IT ALL ABOUT?
Ghi
WHAT IS IT ALL ABOUT THEN?
3GhiLogicomix (2008, 2009)
NB. Wittgenstein is
one of the discoverers
of truth table semantics
Logic is about finitary
means to characterise
(generate) infinitary
truths.
Logic is about characterising the infinite truths in finitary terms; there are infinitely many
semantically valid formulae, but they can be finitely generated by a finitary proof system.
LOGICOMIX (2008, 2009)
4Ghi
Highly enjoyable,
but not always precise
5
➤ It is not obvious whether there is any finitary means to characterise (generate) all truths.
➤ Completeness theorems tell that is possible. It is possible to characterise the infinite set of all
logical truths by finitary means, namely by a proof system. Natural deduction allows us to
derive all logical truths by finitary proof procedures.
➤ Incompleteness theorems tell it is impossible; e.g., it is impossible to characterise the infinite
set of all arithmetical truths by any finitary means, i.e., by any (computable) proof system.
➤ There is a mechanical procedure (program) to generate all logical truths, but no such procedure
(program) to generate all arithmetical truths, let alone all mathematical truths. A small number
of rules allow us to generate all truths, which is a highly non-trivial mathematical phenomenon.
WHAT IS IT ALL ABOUT THEN?
Ghi
GÖDEL ANNOUNCES INCOMPLETENESS THEOREMS
6Ghi
7
➤ “Very few logical concepts and axioms” allow us to generate all truths, which is amazing. Note:
the human being is a finitary entity, and only comprehends finitary things.
➤ Gödel (1944): “It was only [Russell’s] Principia Mathematica that full use was made […] for
actually deriving large parts of mathematics from a very few logical concepts and axioms.”
➤ Kleene (1952): “Leibniz (1666) first conceived of logic as a science containing the ideas and
principles underlying all other sciences.” Can we generate all scientific truths via logic?
➤ (It’s open, but we can generate physical (e.g., quantum-physical) truths via logic (there is even
an automated reasoning system, called Quantomatic, based on category-theoretical logic).)
QUOTES FROM GREAT LOGICIANS
Ghi
https://en.wikipedia.org/wiki/Logicism
“Large parts” do not mean “all”!
JUST SEVEN AXIOMS ALLOW YOU TO DERIVE ALMOST EVERYTHING
8Ghi
https://www.chegg.com/homework-help/questions-and-answers/relation-u-greater-equal-v-natural-numbers-n-defined-formula-ez-u-z-v–give-formal-proof-u-q64888301
=: binary relation symbol
0: constant symbol
s: “+1” function symbol
+: “add” function symb.
・:“multiply” fun. sym.
PA7: induction axiom
PA1,…,PA7 ⊢ almost all truths!
(NB. Just to give a broader perspective on logic; you don’t have to understand this.)
9
➤ Semantics of first-order logic; soundness and completeness of first-order logic
➤ Another (arguably easier) proof system: sequent calculus (a method to prove the consistency of
mathematical theories, which is an origin of modern logic. Is the logic we learned consistent?
Why are we not able to derive contradictions? We can already prove it semantically.)
➤ Additional ingredients of first-order logic: identity (equality) and restricted quantifiers
➤ Introduction to non-classical logic and analyses of paradoxes: modern formal logic allows us to
give different mathematical solutions to philosophical paradoxes; simplistically speaking,
formal logic allows us to resolve philosophers’ long-standing worries since Greek philosophy.
OVERVIEW OF THE SECOND PART
Ghi
10
➤ May not have sufficient time to answer questions (esp. complex ones) in lectures, so if your
questions are not answered in lectures, please ask them at drop-ins, Wattle forum, or tutorials.
➤ Topics become more advanced, but I will try to make them as easy to understand as possible
(since I understand that some of you may be finding this course a bit difficult; should it be
rather too easy for you, try to learn more advanced materials, such as a completeness proof.)
REMARKS
Ghi
11Ghi
Appendix (Just for Fun)
PRINCIPIA MATHEMATICA (1910-1913) AND KLEENE’S ARITHMETICAL HIERARCHY
12Ghi
Just to give a broader perspective on logic.
You do not have to understand this at all!
https://www.researchgate.net/figure/The-arithmetical-hierarchy_fig1_220520596
Russell and Whitehead prove that 1+1=2！
Incompleteness is about
complexity of truths:
RUSSELL (1903) AND RUSSELL (1959)
13Ghi
https://www.abebooks.com/servlet/BookDetailsPL?bi=30812221982&cm_sp=SEARCHREC-_-WIDGET-L-_-BDP-F&searchurl=an%3Dbertrand%2Brussell%26fe%3Don%26sortby%3D17%26tn%3Dmy%2Bphilosophical%2Bdevelopment
https://www.biblio.com/book/principles-mathematics-russell-bertrand/d/1287662772
It is said Russell did not understand the
differences between ∅ and {∅}, between
syntax and semantics. Logic was difficult
even for him. Still he understood what
logic is (and enjoyed it).
Even if you are currently struggling with
formals proofs and/or L4F, you can still
become Russell, one of the greatest
logicians (and enjoy logic).
14
➤ An interesting story about Bertrand Russell, one of the founders of (modern) symbolic logic and
analytic philosophy (~ philosophy based on logical analysis).
➤ When Bertrand Russell died, Valerie Eliot contributed the following message to The Times: “My
husband, T.S. Eliot, loved to recount how late one evening he stopped a taxi. As he got in, the
driver said: ‘You’re T.S. Eliot’. When asked how he knew, he replied: ‘Ah, I’ve got an eye for
celebrity. Only the other evening I picked up Bertrand Russell, and I said to him: ‘Well, Lord
Russell, what’s it all about’, and do you know, he couldn’t tell me.’”
➤ Russell still knew what logic is about, as he says (Principles of Mathematics, 1903): “The present
work has two main objects. One of these, the proof that all pure mathematics deals exclusively
with concepts definable in terms of a very small number of fundamental logical concepts, and that
all its propositions are deducible from a very small number of fundamental logical principles”
RUSSELL AND ELIOT
Ghi
SEMANTICS OF
FIRST ORDER
LOGIC
GOAL, INFORMALLY
16
“Pascal looks more formal than John”
>LF
The Syntactic World (Language)
The Semantic World (Reality; does not have to be true in this world)
Mapping from Language to Reality
“Gödel is taller than Tarski”
>height
https://www.facebook.com/alfredtarski/
Interpretation
Alfred Tarski (1933):
“Setting out a mathematical
definition of truth
for formal languages”
We aim to understand the correspondence between language and reality (can be counterfactual):
What is Language? A finitary
system of symbols (proof theory).
What is Reality? A (infinitary)
system of entities (e.g., sets) and their truths (model theory)
GOAL, FORMALLY
17
Formal Symbols in First-Order Logic
(Syntax)
Interpretation/Denotations/Referents
(Semantics; Model Theory)
Names (aka. constants): a, b, . . . Domain (non-empty set): D I(a), I(b) . . . ∈ D
Function symbols: f(x1, . . . , xn) Functions on the domain: I( f ) : D
n → D
Predicate symbols: R(x1, . . . , xn) Relations: I(R) : D
n → {1,0} or I(R) ⊆ Dn
Formulae: A(x1, . . . , xn) Truth value functions: I(A) : D
n → {1,0}
Formulae with all variables quantified: A Truth values: or I(A) = 1 0
GhiNotation: means are free variables(x1, . . . , xn) x1, . . . , xn
SEMANTICS AND COMPOSITIONALITY
➤ Symbols in proof systems have no meaning (denotations); they just follow syntactic
rules (cf. formalism). Semantics or interpretation gives meaning (denotations) to
them.
➤ An interpretation of propositional logic is an assignment of truth values (0 or 1) to
atoms (atomic propositions; propositional variables) .
Once we assign truth values to atoms, all formulae are assigned with truth values, which is
called compositionality, i.e., the denotation of a complex expression is determined on the
basis of the denotations of its simpler parts (and the way they are connected).
Remark: Compositional semantics of programming languages is essential for formal
verification of programs, especially for safety-critical systems such as self-driving cars.
p, q, r…
18Tony HoareFrege
SEMANTICS AND COMPOSITIONALITY (CONT’D)
➤ In general, an interpretation of a logical system is an assignment of denotations
(aka. referents) to symbols, especially non-logical ones.
It is fixed how to interpret logical symbols (including logical connectives).
➤ In first-order logic, the non-logical symbols are names, function symbols, and
predicate symbols.
➤ Once we fix denotations (interpretations) of these symbols, we are able to determine
the truth values of all formulae in first-order logic, from simple to complex ones.
The same kind of compositionality as in the semantics of propositional logic.
Remark: Semantics in natural language processing in AI is not necessarily compositional.
19
PRESUPPOSITIONS IN SYNTAX AND SEMANTICS
➤ In semantics (model theory), we rely on the language of set theory (sets, functions,
relations, etc.); in syntax (or proof theory), we construct everything from scratch.
➤ Recall: (i.e., x is an element of D) and (i.e., A is a subset of B).
Product (aka. cartesian product) and functions are very important too:
x ∈ D A ⊂ B
20
https://slideplayer.com/slide/4158335/https://hyperskill.org/learn/step/8653
f : X → Y f(x) ∈ Y
See also Pascal’s set theory slides on Wattle
RELATION AS SUBSET AND FUNCTION
➤ A binary relation on a set is a subset of , i.e., . An -ary relation
is a subset of , i.e., .
➤ Equivalently, a binary relation is ; likewise, an -ary relation is
.
➤ Given a subset , we have defined by: iff
(and it’s otherwise).
➤ Given a function , we have defined by: iff
. So they are equivalent.
➤ Note: relations are set-theoretical entities; relation symbols are syntactic symbols.
R X X × X R ⊂ X × X n
R Xn R ⊂ Xn
R : X × X → {0,1} n
R : Xn → {0,1}
R ⊂ X × X S : X × X → {0,1} S(x1, x2) = 1
(x1, x2) ∈ R 0
S : X × X → {0,1} R ⊂ X × X (x1, x2) ∈ R
S(x1, x2) = 1
21
EXAMPLES OF RELATIONS
➤ The equality relation is , or equivalently,
such that if , and otherwise.
➤ The inequality relation on (set of natural numbers) is , or
such that if and otherwise.
{(x, x) | x ∈ X} ⊂ X × X
R= : X × X → {0,1} R=(x, y) = 1 x = y R=(x, y) = 0
ℕ {(n, m) | n < m} R< : ℕ × ℕ → {0,1} R<(n, m) = 1 n < m R<(n, m) = 0 22 DOMAIN AND INTERPRETATION ➤ An interpretation of first-order language consists of and such that: ➤ (i) is a non-empty set, called a domain (of discourse). ➤ Examples of domains: the set of natural numbers, a set of animals, etc. ➤ (ii) gives denotations (interpretations) of symbols in the following manner. D I D I 23 INTERPRETATION OF NAMES AND RELATIONS ➤ Names (aka. constants) are interpreted as elements of the domain : For a name , assigns an element to . ➤ Predicate symbols are interpreted as relations, i.e., for an -ary predicate symbol , is defined as: A subset ; Equivalently, a function . D m I I(m) ∈ D m n R I(R) I(R) ⊆ Dn I(R) : Dn → {1,0} 24 F D b k l a EXAMPLES 25 In this example, the domain is the set . The names “ ” and “ ” are interpreted as the two elements k and l in D, which are their denotations. The unary (i.e., one-variable) predicate symbol is interpreted as the relation indicated by the orange subset. Equivalently, the interpretation of can be represented as a function: where in particular, and . D a b F F I(F) : D → {1,0} I(F)(k) = 1 I(F)(l) = 0 EXAMPLES (CONT’D) 26 D 2 3 13 is the domain. The binary predicate symbol “ ” is interpreted as the binary relation “<”: i.e., ; or equivalently, such that , , , and gives in all the other cases. D = {2,3,13} F I(F) = {(2,3), (3,13), (2,13)} ⊂ D × D I(F) : D × D → {1,0} I(F)(2,3) = 1 I(F)(3,13) = 1 I(F)(2,13) = 1 0 F (2, 3) (3, 13) (2, 13) INTERPRETATION OF FUNCTION SYMBOLS ➤ Function symbols are interpreted as follows: for an n-ary function symbol , its interpretation is a function . Suppose the interpretations of names are elements in , respectively. The term behaves like a name. So its interpretation is defined as an element in . More formally, if then is defined as . ➤ Note that the above interpretation combines or composes the interpretations of names with the interpretation of a function. A general term (a name or of form where each is a term) is interpreted in a similar, compositional manner. f I( f ) : Dn → D t1, . . . , tn a1, . . . , an D f(t1, . . . , tn) I( f(t1, . . . , tn)) I( f )(a1, . . . , an) D I(t1) = a1, . . . , I(tn) = an I( f(t1, . . . , tn)) I( f )(I(t1), . . . , I(tn)), i.e., I( f )(a1, . . . , an) f(t1, . . . , tn) ti 27 EXAMPLES 28 In this example, the domain is the set of all natural numbers. Let be the names for the numbers , respectively. Let the binary function symbol be interpreted as the function on the natural numbers such that: Then we have: D a, b 2,3 f h : D2 → D 0,1,2,3,4,5,... D h(x, y) = x2 + y2 I( f(a, b)) = I( f )(I(a), I(b)) = I( f )(2,3) = h(2,3) = 13 INTERPRETATION OF PROPOSITIONAL CONNECTIVES We assign truth values to formulae with propositional connectives as follows: iff and . (It’s otherwise.) A formula is called open if there is a free variable in it; called closed if not. In general, it’s an open formula: if the free variables of are , iff and . iff . The rest omitted (the same as in propositional logic). Compositionality: the value of is determined on the basis of values of and . I(A ∧ B) = 1 I(A) = 1 I(B) = 1 0 A ∧ B x1, . . . , xn I(A ∧ B)(c1, . . . , cn) = 1 I(A)(c1, . . . , cn) = 1 I(B)(c1, . . . , cn) = 1 I(¬A) = 1 I(A) = 0 A ∧ B A B 29Ghi EXAMPLES (CONT’D) Consider the following formula with two variables and : Suppose: the set of natural numbers is the domain; is interpreted as inequality relation ; is interpreted as ; and are interpreted as numbers resp. Then the interpretation is a function where, e.g., is true and is false. In general, it is interpreted as . A(x, y) x y F < f h(x) = x2 a, b 5,10 I(A) I(A) : D2 → {1,0} I(A)(3,13) I(A)(2,13) 5 < x2 ∧ 10 < y 30 F(a, f(x)) ∧ F(b, y) INTERPRETATION OF QUANTIFIERS We assign truth values to quantified formulae in the following way: iff for any element in the domain . iff is true for some element in the domain . In general, there may be additional free variables. For example, consider the formula . iff for any in . I(∀xA(x)) = 1 I(A)(a) = 1 a D I(∃xA(x)) = 1 I(A)(a) = 1 a D ∀x(Fx → Gx) I(∀x(Fx → Gx)) = 1 I(Fx → Gx)(a) = 1 a D 31Ghi 32 Consider the formula in the following interpretation: the domain is the set of natural numbers 0, 1, 2, …, and is the binary relation “ ”. The interpretation of the formula is as follows. (true) iff: evaluates to (true) for all natural numbers, i.e., for any natural number , , which means: Given any natural number , there is a natural number such that . The formula says that for any natural number there is a bigger natural number. What if the domain is the natural numbers plus bigger than any numbers? It’s false then. ∀x∃y Rxy D I(R) < ∀x∃y Rxy I(∀x∃y Rxy) = 1 I(∃y Rxy) : D → {1,0} 1 a I(∃y Rxy)(a) = 1 a b I(Rxy)(a, b) = 1 ∞ EXAMPLE Ghi SUMMARY 33 Formal Symbols in First-Order Logic (Syntax) Interpretation/Denotations/Referents (Semantics; Model Theory) Names (aka. constants): a, b, . . . Elements of the domain: I(a), I(b) . . . ∈ D Function symbols: f(x1, . . . , xn) Functions on the domain: I( f ) : D n → D Predicate symbols: R(x1, . . . , xn) Relations: I(R) : D n → {1,0} or I(R) ⊆ Dn Open formulae: A(x1, . . . , xn) Truth value functions: I(A) : D n → {1,0} Closed formulae (all variables quantified): A Truth values: or I(A) = 1 I(A) = 0 Ghi NB. A formula is called open if there is a free variable in it; called closed if not. INTERPRETATION OF SEQUENTS Finally we define (semantic) validity: Closed formula case: is valid iff implies . Here note that is defined as: for any Open formula case with free variables: is valid iff implies , for any . We write if is (semantically) valid. It’s called semantic entailment relation. X ⊢ A I(X) = 1 I(A) = 1 I(X) = 1 I(B) = 1 B ∈ X . n X ⊢ A I(X)(c1, . . . cn) = 1 I(A)(c1, . . . , cn) = 1 c1, . . . , cn ∈ D X ⊨ A X ⊢ A 34Ghi 35 An interpretation is a model of a set of (closed) formulae iff any formula in is true in that interpretation. For example, consider the formula “ ”. If the domain is the set of logicians, is the is-taller-than relation in the real world, and and are Gödel and Tarski, resp., then it is a model of , assuming Gödel is taller than Tarski. You can also think of a counterfactual world in which Tarski is taller than Gödel, and then it is not a model of , assuming the interpretation of remains the same. X X Rtaller(g, t) I(Rtaller) I(g) I(t) Rtaller(g, t) Rtaller(g, t) Rtaller MODELS Ghi 36 ➤ An interpretation may be any possible interpretation, however strange it is, but a model (of ) must be an interpretation making formulae concerned (i.e. ) true. ➤ What are the possible models for the formula: ? (where and are formulae with no free variables.) For to be true in an interpretation , there are exactly three possibilities: In , 1. is true, is false; 2. is false, is true; 3. is true, is true. X X A ∨ B A B A ∨ B I I A B A B A B MODELS (CONT’D) Ghi SOUNDNESS AND COMPLETENESS SOUNDNESS AND COMPLETENESS ➤ Two ways of doing first-order logic. ➤ 1. Syntactically with a proof system. ➤ 2. Semantically with interpretations (models). ➤ Then: ➤ 1. The proof system defines provability. ➤ 2. The interpretations (models) define validity (truth). ➤ Question: do they coincide with each other? 38Ghi DEFINITIONS ➤ Soundness of a proof system means that every provable sequent is semantically valid. We cannot prove anything that is false; if we prove something, it is true. ➤ Completeness of a proof system means that every valid sequent is provable. We can prove everything that is true; there is no true, unprovable sequent. 39Ghi SOUNDNESS AND COMPLETENESS, PICTORIALLY 40 Completeness Syntactically Provable Semantically Valid Soundness Semantically Valid Syntactically Provable+ Syntactically Provable Semantically Valid (True)= GhiNB. Completeness (theorems) sometimes mean both soundness and completeness in the above sense 41 ➤ Symbols in a proof system have no meaning; you just mechanically apply rules without semantically interpreting them. ➤ Leo Corry “Axiomatics between Hilbert and the New Math” (2007): “It is well known that Hilbert once explained his newly introduced approach by saying that in his system one might write “chairs,” “tables” and “beer mugs,” instead of “points,” “lines” and “planes,” and this would not affect the structure and the validity of the theory presented.” ➤ In a proof system, one may write “chairs,” “tables” and “beer-mugs”, instead of “ ”, “ ”, and “ ”. It does not matter whey they are as long as they follow the rules specified; they have no meaning other than following the rules. ∧ ¬ → THE NATURE OF PROOF SYSTEM Ghi 42 Syntax (Proof Theory) ➤ A proof system with symbols and deductive rules, such as and I, etc. ➤ The symbols have no intrinsic meaning and they only mechanically follow certain derivation rules to form proofs. ➤ Syntactic (or proof-theoretic) entailment is represented by the symbol . means is provable from via the deductive rules (of natural deduction or sequent calculus which we learn soon). Semantics (Model Theory) ➤ Gives meaning to the syntactic symbols. ➤ Semantic (or model theoretic) entailment is represented by the symbol . means that formula is true in all models of . ➤ Soundness: if then . It suffices to show that all rules preserve validity. ➤ Completeness: if then . Shown by assuming and constructing a model to show . The model consists of syntactic symbols (cf. symbolic construction of reality). R, ∀, a, ∧ ⊢ X ⊢ A A X ⊨ X ⊨ A A X X ⊢ A X ⊨ A X ⊨ A X ⊢ A X ⊬ A X ⊭ A SYNTAX VS SEMANTICS 43 ➤ Consider the conjunction elimination rule: ➤ The soundness of the rule means that: if then , i.e., the rule preserves semantic validity. ➤ The soundness of this rule holds because: if any interpretation that makes true also makes true, then any interpretation that makes true also makes true. ➤ Proving the soundness of the entire system amounts to proving that all the deductive rules of natural deduction preserve semantic validity. X ⊨ A ∧ B X ⊨ A X A ∧ B X A SOUNDNESS OF CONJUNCTION ELIMINATION RULE Ghi X ⊢ A ∧ B X ⊢ A SOUNDNESS OF DISJUNCTION ELIMINATION How about the disjunction elimination E? We suppose the three input sequents are valid: We want to show that the output of the rule is valid: ∨ 44 Z, B ⊢ CX ⊢ A ∨ B X, Y, Z ⊢ C ∨ E Y, A ⊢ C Z, B ⊨ CX ⊨ A ∨ B Y, A ⊨ C X, Y, Z ⊨ C Ghi SOUNDNESS OF DISJUNCTION ELIMINATION To prove a semantic entailment, we have to show that the conclusion is true in any interpretation that makes the assumptions true. Consider an interpretation that makes the assumptions true. Since we assumed the validity of the following sequents: we know that is true in . Then either is true or is true in . Either case makes true in (due to the above assumptions), and thus we have got: X, Y, Z A ∨ B I Y, A Z, B I C I 45 Z, B ⊨ CX ⊨ A ∨ B Y, A ⊨ C X, Y, Z ⊨ C Ghi SOUNDNESS EXAMPLES: ∀I Now consider the I rule: Assume , which means implies , for any ; for simplicity we assume there is only one free variable (if not just add ). By the side condition of the rule, actually does not include any free variable . Then: “ implies ” actually means “ implies ”, which implies “ implies ” since is any element in . Thus we have: . The side condition is essential in this proof. Soundness proofs for the other rules are similar or simpler. ∀ X ⊨ A I(X)(c) = 1 I(A)(c) = 1 c ∈ D x c1, . . . , cn X x I(X)(c) = 1 I(A)(c) = 1 I(X) = 1 I(A)(c) = 1 I(X) = 1 I(∀xA) = 1 c D X ⊨ ∀xA 46 X ⊢ A X ⊢ ∀xA ∀I Ghi SOUNDNESS ➤ All rules of natural deduction preserve semantic validity. ➤ Thus: any sequent provable via natural deduction is semantically valid. ➤ In other words: we cannot prove anything invalid using natural deduction. ➤ Formally: implies .X ⊢ A X ⊨ A 47Ghi COMPLETENESS PROOF To prove implies , we prove the contrapositive: if then , which is shown by constructing a syntactic model of that invalidates (called Henkin model). See the logic notes, which give some ideas and references for a completeness proof. [NB. It is known that there is no finitary proof of completeness (it is known, for example, in Reverse Mathematics that Gödel's completeness theorem for countable languages is equivalent to Weak König's Lemma, an infinitary principle of proof; for general languages, a stronger principle is required, e.g. the existence of ultrafilters or Zorn’s Lemma).] You only need to understand the concept of completeness in this course (not its proof). X ⊨ A X ⊢ A X ⊬ A X ⊭ A X A 48Ghi DUALITY ➤ Thanks to soundness and completeness, we can use either of a proof system and semantics to verify or refute sequents. ➤ Proof theory (proof system) is basically useful for verifying a sequent . ➤ Model theory (semantics) is basically useful for refuting a sequent (i.e. verifying ). ➤ Remark: In general, it is not easy to prove using proof-theoretic methods only, but doing so has both mathematical and philosophical merits. X ⊢ A X ⊢ A X ⊬ A X ⊬ A 49Ghi 50Ghi Appendix (Just for Fun) ADVANCED ISSUES ➤ There are several philosophical/mathematical issues I would like to mention but you don’t have to fully understand: ➤ 1. Presuppositions in proof theory and model theory. ➤ 2. Denotationalism vs. inferentialism in the theory of meaning. Do you really need the Tarskian model-theoretic semantics (the one you just learned) in order to confer meaning on logical symbols? ➤ 3. Broader significance of completeness (just to mention). 51Ghi PRESUPPOSITIONS IN PROOF AND MODEL THEORIES ➤ Proof theory (syntax) is finitary and independent of set theory, but model theory (semantics) is dependent upon set theory and in general infinitary. ➤ Proof theory was originally conceived for proving the consistency of mathematics; formalise mathematics and prove its consistency, i.e., prove formal unprovability of a contradiction . ➤ To do this, proof theory must be finitary; otherwise, it only proves the consistency of infinitary math on the basis of infinitary math, which does not make much sense (if not no sense). It has to prove the consistency of infinitary math upon a finitary basis. ➤ How to prove for the logic you learned? You can prove it semantically. How to prove it in a purely syntactic, finitary manner? It’s an origin of sequent calculus. ⊢ A ∧ ¬A ⊬ A ∧ ¬A 52 PRESUPPOSITIONS (CONT’D) ➤ Related remarks on presupossitions: what do you presuppose when you use or define a proof system (or semantics)? ➤ Is logic defining logical connectives from scratch? No. We cannot define anything without presupposing anything at all. ➤ The conj. intro. rule: if you have and , then you may derive . We are using conjunction and implication in our meta-language to talk about ND. ➤ Object-level language: natural deduction. Meta-language: natural language. But we do not need the full power of natural language to do natural deduction. ➤ What exactly do we need? It’s a subtle question of both math. and phil. significance. X ⊢ A X ⊢ B X ⊢ A ∧ B 53 DENOTATIONALISM AND INFERENTIALISM ➤ Some logicians actually argue that proof systems are sufficient for conferring meaning on syntactic symbols. Called inferentialism or proof-theoretic semantics. ➤ Simplistically, saying, they argue deductive rules themselves give meaning. The meaning of logical symbols is how to use them in inferences (cf. Wittgenstein below). ➤ What we learned is denotational semantics: an expression denotes something, which is meaning. In inferential semantics, they argue inferential rules governing the expression give meaning (cf. operational semantics in programming language theory). ➤ Wittgenstein (in his later philosophy): “Meaning is use”; “The words are not a translation of something else that was there before they were.” Autonomy of language. (If you are interested in inferentialism, read Dummett, Brandom, etc.) 54 55 ➤ Logic is about characterising the infinite set of (logical/mathematical/scientific) truths by a finitary proof system. ➤ Turing machine is about characterising the infinite set of certain functions (recursive functions) by finitary mechanical procedures. ➤ Deep learning is about characterising the infinite set of certain functions (e.g., Bochner- Lebesgue p-integrable functions) by (functions generated from) finitary neural networks. ➤ Algebraic geometry is about characterising infinitely many geometric objects (and their geometric properties) by finitary algebraic equations (and their algebraic properties). COMPLETENESS THEOREMS ARE ALMOST EVERYWHERE (JUST TO MENTION)