Mathematical Logic: A Study Guide (Peter Smith)
(link)
31 flashcards · Mathematics · by lakesare
What does FOL stand for?
First-Order Logic
[First-Order Logic] What's a real-world correspondence to: semantics syntax
semantics - truth table syntax - rules of the deductive system
[First-Order Logic] Deductive system's soundness and completeness is about the relationship between ______________?
Between: what can be derived from the deductive system VS what can be confirmed by the truth table. Relationship between syntax VS semantics! Soundness: Г ⊢ A → Г ⊨ ACompleteness: Г ⊨ A → Г ⊢ ANote that the names "sound" and "complete" are from the point of view of the syntactic system.
[First-Order Logic] What's a "Google as deductive system" analogy for: soundness completeness
We can ask Google to be: be more sound - don't overshoot Stop returning stupid results!be more complete - don't undershoot Stop hiding positive results!
[First-Order Logic] In "false positive" - what do these describe: false positive
false - our mark Our mark of the system response!positive - what system actually returned
[First-Order Logic] What do we need to get rid of to make google perfect?
Get rid of: false positives false negatives
[First-Order Logic] What a model for Γ = { sentence, sentence, ~}?
Model = any interpretation that makes all sentences in Г true at the same time. There can be many models for one Г.
[First-Order Logic] When the deductive system is compact? Γ = { sentence, sentence, ~}
Г has a model ≡ each finite subset of Г has a model. In mathematical logic, the compactness theorem states that a set of first-order sentences has a model if and only if every finite subset of it has a model. This implies that if a formula is a logical consequence of an infinite set of first-order axioms, then it is a logical consequence of some finite number of those axioms. This theorem was proved first by Kurt Gödel as a consequence of the completeness theorem.
[First-Order Logic: deductive systems] Name 3 deductive systems for First-Order Logic.
Axiomatic systems Natural deduction Semantic tableaux Aka "Truth trees"Sequent calculi Resolution calculi
[First-Order Logic: deductive systems] Visually imagine these FOL deductive systems: standard axiomatic system natural deduction Deductive systems for FOL.
standard axiomatic system natural deduction In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning.A natural-deduction system of logic aims to formalize patterns of reasoning now including those where we can argue by making and then later discharging temporary assumptions. Hence, for example as well as the simple modus ponens (MP) rule for the conditional ‘→’, there wil…
[First-Order Logic: deductive systems] Visually imagine Natural Deduction inferences: in Fitch-style in Gentzen-style Deductive systems for FOL.
Fitch-style A multi-column layout was popularized by Frederick Fitch in his classic 1952 logic text, Symbolic Logic: an Introduction.Gentzen-style The layout for natural deductions favoured for proof-theoretic work was first introduced Gerhard Gentzen in his doctoral thesis of 1933. He sets out the proofs as trees, with premises or temporary assumptions at the top of branches and the conclusion at the root of the tree – and he uses a system for explicitly tagging temporary assumptions and the i…
What does SOL stand for?
Second-Order Logic
[First-Order Logic: Many-Sorted Logic variant] Visually imagine this claim written in: normal FOL many-sorted FOL
normal FOL many-sorted FOL Ordinary first-order interpretations have a single domain of discourse over which all quantifiers range. Many-sorted first-order logic allows variables to have different sorts, which have different domains.
[Second-Order Logic] What's the difference between: First-Order Logic and Second-Order Logic
Second-Order Logic = FOL + can quantify over predicates! Quantification over predicates – second-order quantification – is not available in standard first-order languages of the kind that you now know and love.
[Second-Order Logic] Why do we not use Second-Order Logic in maths? There are quite a few familiar mathematical claims like the arithmetical induction principle, and familiar mathematical constructions like forming the ancestral or forming the closure of a relation, which are naturally regimented using quantifications over properties (and/or relations and/or functions). Quantification over predicates (aka functions).
Because there can be no "sound and complete deductive system" for SOL! And it isn't obvious either what exactly the significance of this failure of completeness might be. In fact, the whole question of the status of second-order logic leads to some tangled debates.
[Decidability and Computability] Decidable VS effectively decidable?
Same, reflects the difference between logic vs theoretical CS communities. "Decidable" and "effectively decidable" mean the same thing. I realize that's a bit confusing; but it reflects a difference in terminology between two communities (logic vs theoretical computer science).
[Church-Turing Thesis] What's the Church thesis?
All computable functions == λ-computable functions. It's proved that three formally defined classes of computable functions coincide: a function is λ-computable if and only if it is Turing computable, and if and only if it is general recursive.
[Church-Turing Thesis] What's the Turing thesis?
All computable functions == Turing computable functions. It's proved that three formally defined classes of computable functions coincide: a function is λ-computable if and only if it is Turing computable, and if and only if it is general recursive.
[Church-Turing Thesis] What question does the Church-Turing Thesis answer?
Clarifies the vague term "computable"! And so it goes: every other attempt to give an exact characterization of the class of effectively computable functions turns out to locate just the same class of functions. That’s remarkable, and this is a key theme you will want to explore in a first encounter with the theory of computable functions.
[Church-Turing Thesis] Why do we accept Church-Turing Thesis as true?
Empirically. Why? For a start, there are quasi-empirical reasons: no one has found a function which is incontrovertibly computable by a finite-step deterministic algorithmic procedure but which isn’t recursive. If there were a device which could answer questions beyond those that a Turing machine can answer, then it would be called an oracle.
[Church-Turing Thesis] Visually imagine: primitive recursive functions VS general recursive functions. Primitive recursive functions form a strict subset of those general recursive functions that are also total functions.
primitive recursive functions - for loop Primitive recursive functions is roughly speaking a function that can be computed by a computer program whose loops are all "for" loops (that is, an upper bound of the number of iterations of every loop can be determined before entering the loop)general recursive functions - while loop General recursive functions: the smallest class of functions (with arbitrarily many arguments) that is closed under composition, recursion, and minimization, and includes…
What does PA stand for?
Peano Arithmetic Giuseppe Peano (1858 – 1932), Italy
[Peano Arithmetic] Name 2 ways to define induction in Peano Arithmetic.
induction as an axiom induction as an inference rule
[Godel's Incompleteness Theorems] What's a Godel number?
Natural number for expression/sequence of expressions.
[Godel's Incompleteness Theorems] What's a Godel sentence?
Sentence in the language of PA that has the property: "G is true iff g (godel number for G) cannot be proved"
[Computer Science] What's meant by "effective" method? "Decidable" and "effectively decidable" mean the same thing. I realize that's a bit confusing; but it reflects a difference in terminology between two communities (logic vs theoretical computer science).
A mechanical procedure (in finite steps, no Gods). An effective method is sometimes also called a mechanical method or procedure.
[Decidability and Computability] Definition of decidability: Theory is decidable when VS Decision problem is decidable when?
It's all about the existence of an effective method. Theory - effective method for deciding whether ANY formula is a theorem. A theory (set of sentences closed under logical consequence) in a fixed logical system is decidable if there is an effective method for determining whether arbitrary formulas are included in the theory.Note that a theorem might be defined via ⊨ or ⊢ in format systems. So, an "algorithm" or an "effective method"Decision problem - effective method for deciding if the answe…
[Decidability and Computability] What's the difference between: decidability VS computability?
These are the same, but applied to different objects: decidability - of a mathematical property P Or of a "decision problem"computability - of a function
What does Cosovo stand for?
Complete Sound We can ask Google to be: be more sound - don't overshoot Stop returning stupid results!be more complete - don't undershoot Stop hiding positive results!
What does Deco stand for?
Decidable Computable These are the same, but applied to different objects: decidability - of a mathematical property P Or of a "decision problem"computability - of a function
Which of these classes of languages relate to Turing Machines?
Turing recognizable Turing decidable