COMP 230 Midterm Terms

Proof (basic)

sequence of statements connected by inferences

Theorem (basic)

last line in a proof

Lemma

theorem used within another proof

Conditional statement

If A then B

Biconditional statement

A iff B

Deductive reasoning

the truth of the conclusion necessarily follows the truth of the premises

Inductive reasoning

the conclusion is made more likely by the premises

Recursive definition

defines a term of a function based on other term/s in the function

Parts of a recursive definition

Base clause, induction clause, final clause

Parts of mathematical induction

Base case, induction step/s (via induction hypothesis), conclusion

Set

unordered collection of objects (elements that have certain properties)

Extensional presentation

{the set, written out}

Intensional presentation

{x ∈ A | P(x)}

Russell’s paradox

S = {x | x is not an element of x}. Is S ∈ S?

A ∩ B

intersection (only elements in both)

A ∪ B

union (all of the elements)

Ā

complement (all elements not in A)

𝒫(A)

powerset (set of all subsets INCLUDING the empty set)

Ordered pair

collection of elements where the order matters

A × B

cross product (set of all ordered pairs consisting of elements from the two sets) (n*m)

R (relation)

subset of a cross product (so it's a set of ordered pairs) (2^(n*m))

Function

*single-valued* binary relation on A and B where every element of the domain is mapped to some element

Injective

one-one; for every element in the range, there is only one x

Surjective

onto; range = codomain (every element of B is used)

Bijective

one-to-one correspondence; both injective and surjective

Countably infinite

equinumerous to ℕ (= ℵo)

Diagonalization

method to prove uncountable infinity of a set

Cantor's Theorem

|𝒫(A)| > |A|; prove by contradiction

Continuum Hypothesis

there is no set with cardinality greater than |ℕ| but less than |ℝ| (ℵ1)

Parts of a formal system

alphabet (well-formed strings), axioms, inference rules

Metavariable

belongs to the metalanguage, stands for an element of the object language

Derivation (formal systems)

non-empty sequence of strings where each string is either an axiom or obtained from an earlier string using an inference rule

Theorem (formal systems)

last string in a derivation

M-Mode

mechanical mode; inside a system; object-language (reasoning within the formal system)

I-Mode

intelligent mode; outside a system; meta-language (reasoning about the formal system)

Decision procedure

guarantees a yes/no after a finite amount of time

Decidable

if a question has a decision procedure

Axiom schema

a metalanguage formula that generates axioms of a formal system

Model

interpretation where all axioms and all theorems are true

Interpretation

mapping theorems to true statements; mapping from alphabet to give meaning to well-formed strings

Soundness

every theorem is a true statement (syntax to semantics)

Completeness

every true statement (of a particular form) is a theorem (semantics to syntax)

Recursively enumerable

a set whose members can be generated as theorems of a formal system

Recursive

both the theorems and non-theorems can be generated by a formal system (decidable)

Explicit definition

definition by the expression of old terms already in the system (

Implicit definition

definition by context of usage

Syntactic equivalence

whatever you can prove from a set of assumptions and P, you can also prove with the same set of assumptions and Q

Playfair's postulate

equivalent to Euclid's fifth postulate

Independence

both P and ~P cannot be proved from a set of assumptions

Truth preservation

if the premises are true, then the conclusion must also be true

Elliptic geometry

no-parallel non-Euclidean geometry

Hyperbolic geometry

many-parallel non-Euclidean geometry

Atomic formula tree

any propositional variable alone

Tautology

a well-formed formula of propositional logic that is always true (decision procedure = truth table)

Logically equivalent

when two formulas yield exactly the same column in a truth table

Semantic consequence

entailment; determined via truth tables

Entailment

when a well-formed formula follows from a set of well-formed formulas

Modus ponens

B follows from A ⊃ B and A

Premises (natural deduction calc)

formulas at the top of a derivation tree

Conclusion (natural deduction calc)

formula at the bottom of a derivation tree

Axiomatic calculus

proof system that has only a single inference rule (modus ponens) and a rule for substitutions

Proof (axiomatic calc)

similar to derivation; sequence of formulas where all are either axioms or obtained by applying inference rules to axioms

Syntactic consequence

provability; determined via logical calculi

Extralogical symbols of ℒ

meaning is determined by an interpretation; function and predicate symbols

Terms (FOA)

variable/s and function symbol (names)

Formulas (FOA)

variable/s and predicate symbol; can be joined by logical connectives; can be the scope of quantifiers (statements)

σ

maps formulas to truth values and terms to elements of the domain (interpretation and/or valuation)

Valuation

interpretation that also assigns elements from the domain to the variables

σ satisfies A

A^σ is TRUE

σ satisfies Γ

σ satisfies every member (every A) in Γ

Logically true

⊨A; every valuation satisfies A (tautology)

Logical consequence

Γ⊨A; every valuation that makes every formula in Γ true also makes A true

Bound

when a variable falls inside the scope of a quantifier

Free variables

unbound variables

Closed term

the term contains no variables

Sentence

formula without free variables

theory

A set of sentences that are closed under deduction (s is an element of T iff T proves s)

axiomatic theory

Every element of the theory can be deduced from a DECIDABLE set of axioms

consistent theory

The theory does not contain/prove an inconsistent pair of formulas

complete theory

If, for any sentence A, the theory proves either A or ~A

showing consistency of a theory

Give a model that makes all formulas true

Hilbert's Program

“Finitary arithmetic”; consistency of the theory of natural numbers

Dedekind-Peano axioms

About the natural numbers, in the language of FOA

Gödel numbers

An interpretation (coding) of the wffs of a formal system as natural numbers

dual nature

Gödel numbers; can be treated either typographically (symbols/numerals) or arithmetically (numbers); syntax or semantics

arithmetization

Formal system --\> arithmetic (Gödel numbering)

producible numbers

r.e. (because theorems of a formal system are r.e.)

formalization

Arithmetic --\> FOA

the power of Gödel numbering

Allows formal systems (FOA, TNT) to speak (make statements) about themselves

Church-Turing thesis

Any real-world computation can be translated into a Turing Machine; any non-TM-computable function is not computable at all

parts of a TM

Tape

Head

State

Instructions (qi, S, Op, qf)

TM computable

If there is a TM that calculates a function

the Halting Problem

Can we decide whether a TM halts/loops on a given input? Can we use another TM to decide this?

purpose of primitive recursive functions

Determine computability by building more and more complex functions

primitive recursive function base cases

0

Successor

Projection

total function

A function that always yields a result

characteristic function

Functions that represent relations or predicates (T/F)

bounded minimization

f yields the minimal value of y (up to the bound n) for which h holds

BlooP programs

Predictably terminable computations

least search operator (miu-operator)

Returns the smallest value for z which makes f(x-\>, z) = 0 and for which all smaller values the function is defined