Glossary

Last updated

Mar 8, 2024
Save as PDF
- Index
- Appendix A: Proofs

$\newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} }$

$\newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}}$

$\newcommand{\id}{\mathrm{id}}$ $\newcommand{\Span}{\mathrm{span}}$

( \newcommand{\kernel}{\mathrm{null}\,}\) $\newcommand{\range}{\mathrm{range}\,}$

$\newcommand{\RealPart}{\mathrm{Re}}$ $\newcommand{\ImaginaryPart}{\mathrm{Im}}$

$\newcommand{\Argument}{\mathrm{Arg}}$ $\newcommand{\norm}[1]{\| #1 \|}$

$\newcommand{\inner}[2]{\langle #1, #2 \rangle}$

$\newcommand{\Span}{\mathrm{span}}$

$\newcommand{\id}{\mathrm{id}}$

$\newcommand{\Span}{\mathrm{span}}$

$\newcommand{\kernel}{\mathrm{null}\,}$

$\newcommand{\range}{\mathrm{range}\,}$

$\newcommand{\RealPart}{\mathrm{Re}}$

$\newcommand{\ImaginaryPart}{\mathrm{Im}}$

$\newcommand{\Argument}{\mathrm{Arg}}$

$\newcommand{\norm}[1]{\| #1 \|}$

$\newcommand{\inner}[2]{\langle #1, #2 \rangle}$

$\newcommand{\Span}{\mathrm{span}}$ $\newcommand{\AA}{\unicode[.8,0]{x212B}}$

$\newcommand{\vectorA}[1]{\vec{#1}} % arrow$

$\newcommand{\vectorAt}[1]{\vec{\text{#1}}} % arrow$

$\newcommand{\vectorB}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} }$

$\newcommand{\vectorC}[1]{\textbf{#1}}$

$\newcommand{\vectorD}[1]{\overrightarrow{#1}}$

$\newcommand{\vectorDt}[1]{\overrightarrow{\text{#1}}}$

$\newcommand{\vectE}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash{\mathbf {#1}}}}$

$\newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} }$

$\newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}}$

$\newcommand{\avec}{\mathbf a}$

$\newcommand{\bvec}{\mathbf b}$

$\newcommand{\cvec}{\mathbf c}$

$\newcommand{\dvec}{\mathbf d}$

$\newcommand{\dtil}{\widetilde{\mathbf d}}$

$\newcommand{\evec}{\mathbf e}$

$\newcommand{\fvec}{\mathbf f}$

$\newcommand{\nvec}{\mathbf n}$

$\newcommand{\pvec}{\mathbf p}$

$\newcommand{\qvec}{\mathbf q}$

$\newcommand{\svec}{\mathbf s}$

$\newcommand{\tvec}{\mathbf t}$

$\newcommand{\uvec}{\mathbf u}$

$\newcommand{\vvec}{\mathbf v}$

$\newcommand{\wvec}{\mathbf w}$

$\newcommand{\xvec}{\mathbf x}$

$\newcommand{\yvec}{\mathbf y}$

$\newcommand{\zvec}{\mathbf z}$

$\newcommand{\rvec}{\mathbf r}$

$\newcommand{\mvec}{\mathbf m}$

$\newcommand{\zerovec}{\mathbf 0}$

$\newcommand{\onevec}{\mathbf 1}$

$\newcommand{\real}{\mathbb R}$

$\newcommand{\twovec}[2]{\left[\begin{array}{r}#1 \\ #2 \end{array}\right]}$

$\newcommand{\ctwovec}[2]{\left[\begin{array}{c}#1 \\ #2 \end{array}\right]}$

$\newcommand{\threevec}[3]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \end{array}\right]}$

$\newcommand{\cthreevec}[3]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \end{array}\right]}$

$\newcommand{\fourvec}[4]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \\ #4 \end{array}\right]}$

$\newcommand{\cfourvec}[4]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \\ #4 \end{array}\right]}$

$\newcommand{\fivevec}[5]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \\ #4 \\ #5 \\ \end{array}\right]}$

$\newcommand{\cfivevec}[5]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \\ #4 \\ #5 \\ \end{array}\right]}$

$\newcommand{\mattwo}[4]{\left[\begin{array}{rr}#1 \amp #2 \\ #3 \amp #4 \\ \end{array}\right]}$

$\newcommand{\laspan}[1]{\text{Span}\{#1\}}$

$\newcommand{\bcal}{\cal B}$

$\newcommand{\ccal}{\cal C}$

$\newcommand{\scal}{\cal S}$

$\newcommand{\wcal}{\cal W}$

$\newcommand{\ecal}{\cal E}$

$\newcommand{\coords}[2]{\left\{#1\right\}_{#2}}$

$\newcommand{\gray}[1]{\color{gray}{#1}}$

$\newcommand{\lgray}[1]{\color{lightgray}{#1}}$

$\newcommand{\rank}{\operatorname{rank}}$

$\newcommand{\row}{\text{Row}}$

$\newcommand{\col}{\text{Col}}$

$\renewcommand{\row}{\text{Row}}$

$\newcommand{\nul}{\text{Nul}}$

$\newcommand{\var}{\text{Var}}$

$\newcommand{\corr}{\text{corr}}$

$\newcommand{\len}[1]{\left|#1\right|}$

$\newcommand{\bbar}{\overline{\bvec}}$

$\newcommand{\bhat}{\widehat{\bvec}}$

$\newcommand{\bperp}{\bvec^\perp}$

$\newcommand{\xhat}{\widehat{\xvec}}$

$\newcommand{\vhat}{\widehat{\vvec}}$

$\newcommand{\uhat}{\widehat{\uvec}}$

$\newcommand{\what}{\widehat{\wvec}}$

$\newcommand{\Sighat}{\widehat{\Sigma}}$

$\newcommand{\lt}{<}$

$\newcommand{\gt}{>}$

$\newcommand{\amp}{&}$

$\definecolor{fillinmathshade}{gray}{0.9}$

$\def\Assign#1#2{ { #1^{\Struct{#2}} } }$

$\def\Atom#1#2{ { \mathord{#1}(#2) } }$

$\def\Bin{ {\mathbb{B}} }$

$\def\cardeq#1#2{ { #1 \approx #2 } }$

$\def\cardle#1#2{ { #1 \preceq #2 } }$

$\def\cardless#1#2{ { #1 \prec #2 } }$

$\def\cardneq#1#2{ { #1 \not\approx #2 } }$

$\def\comp#1#2{ { #2 \circ #1 } }$

$\def\concat{ { \;\frown\; } }$

$\def\Cut{ { \text{Cut} } }$

$\def\Discharge#1#2{ { [#1]^#2 } }$

$\def\DischargeRule#1#2{ { \RightLabel{#1}\LeftLabel{\scriptsize{#2} } } }$

$\def\dom#1{ {\operatorname{dom}(#1)} }$

$\def\Domain#1{ {\left| \Struct{#1} \right|} }$

$\def\Elim#1{ { {#1}\mathrm{Elim} } }$

$\newcommand{\Entails}{\vDash}$

$\newcommand{\EntailsN}{\nvDash}$

$\def\eq[#1][#2]{ { #1 = #2 } }$

$\def\eqN[#1][#2]{ { #1 \neq #2 } }$

$\def\equivclass#1#2{ { #1/_{#2} } }$

$\def\equivrep#1#2{ { [#1]_{#2} } }$

$\def\Exchange{ { \text{X} } }$

$\def\False{ { \mathbb{F} } }$

$\def\FalseCl{ { \lfalse_C } }$

$\def\FalseInt{ { \lfalse_I } }$

$\def\fCenter{ { \,\Sequent\, } }$

$\def\fdefined{ { \;\downarrow } }$

$\def\fn#1{ { \operatorname{#1} } }$

$\def\Frm[#1]{ {\operatorname{Frm}(\Lang #1)} }$

$\def\fundefined{ { \;\uparrow } }$

$\def\funimage#1#2{ { #1[#2] } }$

$\def\funrestrictionto#1#2{ { #1 \restriction_{#2} } }$

$\newcommand{\ident}{\equiv}$

$\newcommand{\indcase}[2]{#1 \ident #2\text{:}}$

$\newcommand{\indcaseA}[2]{#1 \text{ is atomic:}}$

$\def\indfrm{ { A } }$

$\def\indfrmp{ { A } }$

$\def\joinrel{\mathrel{\mkern-3mu}}$

$\def\lambd[#1][#2]{\lambda #1 . #2}$

$\def\Lang#1{ { \mathcal{#1} } }$

$\def\LeftR#1{ { {#1}\mathrm{L} } }$

$\def\len#1{ {\operatorname{len}(#1)} }$

$\def\lexists#1#2{ { \exists #1\, #2 } }$

$\def\lfalse{ {\bot} }$

$\def\lforall#1#2{ { \forall#1\, #2 } }$

$\newcommand{\lif}{\rightarrow}$

$\newcommand{\liff}{\leftrightarrow}$

$\def\Log#1{ { \mathbf{#1} } }$

$\def\ltrue{ {\top} }$

$\def\Id#1{ {\operatorname{Id}_#1} }$

$\def\Int{ {\mathbb{Z}} }$

$\def\Intro#1{ { {#1}\mathrm{Intro} } }$

$\def\mModel#1{ { \mathfrak{#1} } }$

$\newcommand{\mSat}[3][{}]{\mModel{#2}{#1}\Vdash{#3}}$

$\newcommand{\mSatN}[3][{}]{\mModel{#2}{#1}\nVdash{#3}}$

$\def\Nat{ {\mathbb{N}} }$

$\def\nicefrac#1#2{ {{}^#1/_#2} }$

$\def\num#1{ { \overline{#1} } }$

$\def\ran#1{ {\operatorname{ran}(#1)} }$

$\newcommand{\Obj}[1]{\mathsf{#1}}$

$\def\Rat{ {\mathbb{Q}} }$

$\def\Real{ {\mathbb{R}} }$

$\def\RightR#1{ { {#1}\mathrm{R} } }$

$\def\Part#1#2{ { \Atom{\Obj P}{#1, #2} } }$

$\def\pto{ { \hspace{0.1 cm}\to\hspace{-0.44 cm}\vcenter{\tiny{\hbox{|}}}\hspace{0.35 cm} } }$

$\def\PosInt{ {\mathbb{Z}^+} }$

$\def\Pow#1{ {\wp(#1)} }$

$\newcommand{\Proves}{\vdash}$

$\newcommand{\ProvesN}{\nvdash}$

$\def\Relbar{\mathrel{=}}$

$\newcommand{\Sat}[3][{}]{\Struct{#2}{#1}\vDash{#3}}$

$\newcommand{\SatN}[3][{}]{\Struct{#2}{#1}\nvDash{#3}}$

$\newcommand{\Sequent}{\Rightarrow}$

$\def\Setabs#1#2{ { \{#1:#2\} } }$

$\newcommand{\sFmla}[2]{#1\,#2}$

$\def\Struct#1{ {#1} }$

$\def\subst#1#2{ { #1/#2 } }$

$\def\Subst#1#2#3{ { #1[\subst{#2}{#3}] } }$

$\def\TMblank{ { 0 } }$

$\newcommand{\TMendtape}{\triangleright}$

$\def\TMleft{ { L } }$

$\def\TMright{ { R } }$

$\def\TMstay{ { N } }$

$\def\TMstroke{ { 1 } }$

$\def\TMtrans#1#2#3{ { #1,#2,#3 } }$

$\def\Trm[#1]{ {\operatorname{Trm}(\Lang #1)} }$

$\def\True{ { \mathbb{T} } }$

$\newcommand{\TRule}[2]{#2#1}$

$\def\tuple#1{ {\langle #1 \rangle} }$

$\newcommand{\Value}[3][\,]{\mathrm{Val}_{#1}^{#3}(#2)}$

$\def\Var{ { \mathrm{Var} } }$

$\newcommand{\varAssign}[3]{#1 \sim_{#3} #2}$

$\def\Weakening{ { \text{W} } }$

Example and Directions
Words (or words that have the same definition)	The definition is case sensitive	(Optional) Image to display with the definition [Not displayed in Glossary, only in pop-up on pages]	(Optional) Caption for Image	(Optional) External or Internal Link	(Optional) Source for Definition
(Eg. "Genetic, Hereditary, DNA ...")	(Eg. "Relating to genes or heredity")		The infamous double helix	https://bio.libretexts.org/	CC-BY-SA; Delmar Larsen

Glossary Entries
Word(s)	Definition	Link
extensionality (of sets), extensionality of sets	Sets A and B are identical, A = B, iff every element of A is also an element of B, and vice versa	https://eng.libretexts.org/Under_Con...Extensionality
set	A collection of objects, considered independently of the way it is specified, of the order of the objects in the set, and of their multiplicity	https://eng.libretexts.org/Under_Con...Extensionality
subset, ⊆, \subseteq, $\subseteq$	(A ⊆ B) A set every element of which is an element of a given set B	https://eng.libretexts.org/Under_Con...and_Power_Sets
sequence (finite)	(A*) A finite string of elements of A; an element of Aⁿ for some n	https://eng.libretexts.org/Under_Con...Important_Sets
Cartesian product	(A × B) Set of all pairs of elements of A and B; A × B = {⟨x,y⟩ : x ∈ A and y ∈ B}	https://eng.libretexts.org/Under_Con...esian_Products
binary relation	A subset of A²; we write Rxy (or xRy) for ⟨x, y⟩ ∈ R	https://eng.libretexts.org/Under_Con...ations_as_Sets
symmetric	R is symmetric iff, whenever Rxy then also Ryx	https://eng.libretexts.org/Under_Con...s_of_Relations
equivalence relation	A reflexive, symmetric, and transitive relation	https://eng.libretexts.org/Under_Con...ence_Relations
linear order, total order	A connected partial order	https://eng.libretexts.org/Under_Con...2.05%3A_Orders
partial order	A reflexive, anti-symmetric, transitive relation	https://eng.libretexts.org/Under_Con...2.05%3A_Orders
preorder	A reflexive and transitive relation	https://eng.libretexts.org/Under_Con...2.05%3A_Orders
strict linear order	A connected strict order	https://eng.libretexts.org/Under_Con...2.05%3A_Orders
strict order	An irreflexive, asymmetric, and transitive relation	https://eng.libretexts.org/Under_Con...2.05%3A_Orders
inverse relation	(R^-1) The relation R “turned around”; R^-1 = {⟨y, x⟩ : ⟨x, y⟩ ∈ R}	https://eng.libretexts.org/Under_Con...s_on_Relations
transitive closure	(R⁺) The smallest transitive relation containing R	https://eng.libretexts.org/Under_Con...s_on_Relations
domain (of a function)	(dom(f)) The set of objects for which a (partial) function is defined	https://eng.libretexts.org/Under_Con...3.01%3A_Basics
function	(f : A → B) A mapping of each element of a domain (of a function) A to an element of the codomain B	https://eng.libretexts.org/Under_Con...3.01%3A_Basics
range	(ran(f)) the subset of the codomain that is actually output by f; ran(f) = {y ∈ B : f(x) = y for some x ∈ A}	https://eng.libretexts.org/Under_Con...3.01%3A_Basics
graph (of a function), graph	The relation R_f ⊆ A × B defined by R_f = {⟨x,y⟩ : f(x) = y}, if f : A ⇸ B	https://eng.libretexts.org/Under_Con...s_as_Relations
inverse function	If f : A → B is a bijection, f^-1 : B → A is the function with f^-¹(y) = whatever unique x ∈ A is such that f(x) = y	https://eng.libretexts.org/Under_Con...s_of_Functions
composition	(g ∘ f) The function resulting from “chaining together” f and g; (g ∘ f)(x) = g(f(x))	https://eng.libretexts.org/Under_Con...n_of_Functions
partial function	(f : A ⇸ B) A partial function is a mapping which assigns to every element of A at most one element of B. If f assigns an element of B to x ∈ A, f(x) is defined, and otherwise undefined	https://eng.libretexts.org/Under_Con...tial_Functions
enumeration	A possibly infinite list of all elements of a set A; formally a surjective function f : ℕ → A	https://eng.libretexts.org/Under_Con...numerable_Sets
injective	f : A → B is injective iff for each y ∈ B there is at most one x ∈ A such that f(x) = y; equivalently if whenever x ≠ x' then f(x) ≠ f(x')	https://eng.libretexts.org/Under_Con...s_of_Functions
surjective	f : A → B is surjective iff the range of f is all of B, i.e., for every y ∈ B there is at least one x ∈ A such that f(x) = y	https://eng.libretexts.org/Under_Con...s_of_Functions
bijection	A function that is both surjective and injective	https://eng.libretexts.org/Under_Con...s_of_Functions
intersection	(A ∩ B) The set of all things which are elements of both A and B: A ∩ B = {x : x ∈ A ∧ x ∈ B}	https://eng.libretexts.org/Under_Con...g:intersection
union	(A ∪ B) The set of all elements of A and B together: A ∪ B = {x : x ∈ A ∨ x ∈ B}	https://eng.libretexts.org/Under_Con..._Intersections
difference	(A \ B) the set of all elements of A which are not also elements of B: A \ B = {x : x ∈ A and x ∉ B}	https://eng.libretexts.org/Under_Con...ons#difference
equinumerous	A and B are equinumerous iff there is a total bijection from A to B	https://eng.libretexts.org/Under_Con...Equinumerosity
reflexive	R is reflexive iff, for every x ∈ A, Rxx	https://eng.libretexts.org/Under_Con...s_of_Relations
anti-symmetric	R is anti-symmetric iff, whenever both Rxy and Ryx, then x = y; in other words: if x ≠ y then not Rxy or not Ryx	https://eng.libretexts.org/Under_Con...s_of_Relations
transitive	R is transitive iff, whenever Rxy and Ryz, then also Rxz	https://eng.libretexts.org/Under_Con...s_of_Relations
connected	R is connected if for all x,y ∈ A with x ≠ y, then either Rxy or Ryx	https://eng.libretexts.org/Under_Con...s_of_Relations
irreflexive	R is irreflexive if, for no x ∈ A, Rxx	https://eng.libretexts.org/Under_Con...s_of_Relations
asymmetric	R is asymmetric if for no pair x,y ∈ A we have Rxy and Ryx	https://eng.libretexts.org/Under_Con...s_of_Relations
sentence	A formula with no free variable	https://eng.libretexts.org/Under_Con..._and_Sentences
free	An occurrence of a variable that is not bound	https://eng.libretexts.org/Under_Con..._and_Sentences
bound	Occurrence of a variable within the scope of a quantifier that uses the same variable	https://eng.libretexts.org/Under_Con..._and_Sentences
subformula	Part of a formula which is itself a formula	https://eng.libretexts.org/Under_Con...3A_Subformulas
formula	Expressions of a first-order language ℒ which express relations or properties, or are true or false	https://eng.libretexts.org/Under_Con...s_and_Formulas
power set	(℘(A)) The set consisting of all subsets of a set A, ℘(A) = {x : x ⊆ A}	https://eng.libretexts.org/Under_Con...and_Power_Sets
sequence (infinite)	(A^ω) A gapless, unending sequence of elements of A; formally, a function s : ℤ⁺ → A	https://eng.libretexts.org/Under_Con...Important_Sets
disjoint	Two sets with no elements in common	https://eng.libretexts.org/Under_Con..._Intersections
free for	A term t is free for x in A if none of the free occurrences of x in A occur in the scope of a quantifier that binds a variable in t	https://eng.libretexts.org/Under_Con...A_Substitution
covered	A structure in which every element of the domain is the value of some closed term	https://eng.libretexts.org/Under_Con...rder_Languages
domain (of a structure)	(\|M\|) Non-empty set from which a structure takes assignments and values of variables	https://eng.libretexts.org/Under_Con...rder_Languages
structure	(M) An interpretation of a first-order language, consisting of a domain (of a structure) and assignments of the constant, predicate and function symbols of the language	https://eng.libretexts.org/Under_Con...rder_Languages
variable assignment	A function which maps each variable to an element of \|M\|	https://eng.libretexts.org/Under_Con...in_a_Structure
x-variant, x-variant, $x$ -variant	Two variable assignments are x-variants, s ~_x s', if they differ at most in what they assign to x	https://eng.libretexts.org/Under_Con...in_a_Structure
entailment, entails	(Γ ⊨ A) A set of sentences Γ entails a sentence A iff for every structure M with M ⊨ Γ, M ⊨ A	https://eng.libretexts.org/Under_Con...mantic_Notions
satisfiable, satisfiability	A set of sentences Γ is satisfiable if M ⊨ Γ for some structure M, otherwise it is unsatisfiable	https://eng.libretexts.org/Under_Con...mantic_Notions
valid, validity	(⊨ A) A sentence A is valid iff M ⊨ A for every structure M	https://eng.libretexts.org/Under_Con...mantic_Notions
deduction theorem	Relates entailment and provability of a sentence from an assumption with that of a corresponding conditional. In the semantic form (Theorem 5.14.1), it states that Γ ∪ {A} ⊨ B iff Γ ⊨ A → B. In the proof-theoretic form, it states that Γ ∪ {A} ⊢ B iff Γ ⊢ A → B.
closed	A set of sentences Γ is closed iff, whenever Γ ⊨ A then A ∈ Γ. The set {A : Γ ⊨ A} is the closure of Γ	https://eng.libretexts.org/Under_Con...A_Introduction
model	A structure in which every sentence in Γ is true is a model of Γ	https://eng.libretexts.org/Under_Con..._of_Structures
derivation	In the sequent calculus, a tree of sequents in which every sequent is either an initial sequent or follows from the sequents immediately above it by a rule of inference. In natural deduction, a tree of formulas in which every formula is either an assumption or follows from the formulas immediately above it by a rule of inference.
sequent	An expression of the form Γ ⇒ Δ where Γ and Δ are finite sequences of sentences	https://eng.libretexts.org/Under_Con...nd_Derivations
eigenvariable	In the sequent calculus, a special constant symbol in a premise of a ∃L or ∀R inference which may not appear in the conclusion. In natural deduction, a special constant symbol in a premise of a ∃Elim or ∀Intro inference which may not appear in the conclusion or any undischarged assumption.
consistent, inconsistent	In the sequent calculus, a set of sentences Γ is consistent iff there is no derivation of a sequent Γ₀ ⇒ with Γ₀ ⊆ Γ. In natural deduction, Γ is consistent iff Γ ⊬ ⊥. If Γ is not consistent, it is inconsistent.
derivability, derivable	(Γ ⊢ A) In the sequent calculus, A is derivable from Γ if there is a derivation of a sequent Γ₀ ⇒ A where Γ₀ ⊆ Γ is a finite sequence of sentences in Γ. In natural deduction, A is derivable from Γ if there is a derivation with end-formula A and in which every assumption is either discharged or is in Γ.
theorem	(⊢ A) In the sequent calculus, a formula A is a theorem (of logic) if there is a derivation of the sequent ⇒ A. In natural deduction, a formula A is a theorem if there is a derivation of A with all assumptions discharged. We also say that A is a theorem of a theory Γ if Γ ⊢ A.
soundness, sound	Property of a proof system: it is sound if whenever Γ ⊢ A then Γ ⊨ A (see section 8.12 and section 9.11)
assumption	A formula that stands topmost in a derivation, also called an initial formula. It may be discharged or undischarged.	https://eng.libretexts.org/Under_Con...nd_Derivations
discharged, undischarged	An assumption in a derivation may be discharged by an inference rule below it (the rule and the assumption are then assigned a matching label, e.g., [A]²). If it is not discharged, it is called undischarged.	https://eng.libretexts.org/Under_Con...nd_Derivations
completeness, complete	Property of a proof system; it is complete if, whenever Γ entails A, then there is also a derivation that establishes Γ ⊢ A; equivalently, iff every consistent set of sentences is satisfiable	https://eng.libretexts.org/Under_Con...A_Introduction
completeness theorem	States that first-order logic is complete: every consistent set of sentences is satisfiable
complete consistent set	A set of sentences is complete and consistent iff it is consistent, and for every sentence A either A or ¬A is in the set	https://eng.libretexts.org/Under_Con...s_of_Sentences
compactness theorem	States that every finitely satisfiable set of sentences is satisfiable	https://eng.libretexts.org/Under_Con...ctness_Theorem
finitely satisfiable	Γ is finitely satisfiable iff every finite Γ₀ ⊆ Γ is satisfiable	https://eng.libretexts.org/Under_Con...ctness_Theorem
Löwenheim-Skolem Theorem	States that every satisfiable set of sentences has a countable model	https://eng.libretexts.org/Under_Con...Skolem_Theorem
Church-Turing Thesis	States that anything computable via an effective procedure is Turing computable	https://eng.libretexts.org/Under_Con...-Turing_Thesis
halting problem	The problem of determining (for any e, n) whether the Turing machine M_e halts for an input of n strokes	https://eng.libretexts.org/Under_Con...alting_Problem
decision problem	Problem of deciding if a given sentence of first-order logic is valid or not (see Church-Turing Theorem)
Church-Turing Theorem	States that there is no Turing machine which decides if a given sentence of first-order logic is valid or not	https://eng.libretexts.org/Under_Con..._is_Unsolvable
extensionality (of satisfaction)	Whether or not a formula A is satisfied depends only on the assignments to the non-logical symbols and free variables that actually occur in A

anti-symmetric | R is anti-symmetric iff, whenever both Rxy and Ryx, then x = y; in other words: if x ≠ y then not Rxy or not Ryx

assumption | A formula that stands topmost in a derivation, also called an initial formula. It may be discharged or undischarged.

asymmetric | R is asymmetric if for no pair x,y ∈ A we have Rxy and Ryx

bijection | A function that is both surjective and injective

binary relation | A subset of A²; we write Rxy (or xRy) for ⟨x, y⟩ ∈ R

bound | Occurrence of a variable within the scope of a quantifier that uses the same variable

Cartesian product | (A × B) Set of all pairs of elements of A and B; A × B = {⟨x,y⟩ : x ∈ A and y ∈ B}

Church-Turing Theorem | States that there is no Turing machine which decides if a given sentence of first-order logic is valid or not

Church-Turing Thesis | States that anything computable via an effective procedure is Turing computable

closed | A set of sentences Γ is closed iff, whenever Γ ⊨ A then A ∈ Γ. The set {A : Γ ⊨ A} is the closure of Γ

compactness theorem | States that every finitely satisfiable set of sentences is satisfiable

complete consistent set | A set of sentences is complete and consistent iff it is consistent, and for every sentence A either A or ¬A is in the set

completeness | Property of a proof system; it is complete if, whenever Γ entails A, then there is also a derivation that establishes Γ ⊢ A; equivalently, iff every consistent set of sentences is satisfiable

completeness theorem | States that first-order logic is complete: every consistent set of sentences is satisfiable

composition | (g ∘ f) The function resulting from “chaining together” f and g; (g ∘ f)(x) = g(f(x))

connected | R is connected if for all x,y ∈ A with x ≠ y, then either Rxy or Ryx

consistent | In the sequent calculus, a set of sentences Γ is consistent iff there is no derivation of a sequent Γ₀ ⇒ with Γ₀ ⊆ Γ. In natural deduction, Γ is consistent iff Γ ⊬ ⊥. If Γ is not consistent, it is inconsistent.

covered | A structure in which every element of the domain is the value of some closed term

decision problem | Problem of deciding if a given sentence of first-order logic is valid or not (see Church-Turing Theorem)

deduction theorem | Relates entailment and provability of a sentence from an assumption with that of a corresponding conditional. In the semantic form (Theorem 5.14.1), it states that Γ ∪ {A} ⊨ B iff Γ ⊨ A → B. In the proof-theoretic form, it states that Γ ∪ {A} ⊢ B iff Γ ⊢ A → B.

derivability | (Γ ⊢ A) In the sequent calculus, A is derivable from Γ if there is a derivation of a sequent Γ₀ ⇒ A where Γ₀ ⊆ Γ is a finite sequence of sentences in Γ. In natural deduction, A is derivable from Γ if there is a derivation with end-formula A and in which every assumption is either discharged or is in Γ.

derivation | In the sequent calculus, a tree of sequents in which every sequent is either an initial sequent or follows from the sequents immediately above it by a rule of inference. In natural deduction, a tree of formulas in which every formula is either an assumption or follows from the formulas immediately above it by a rule of inference.

difference | (A \ B) the set of all elements of A which are not also elements of B: A \ B = {x : x ∈ A and x ∉ B}

discharged | An assumption in a derivation may be discharged by an inference rule below it (the rule and the assumption are then assigned a matching label, e.g., [A]²). If it is not discharged, it is called undischarged.

disjoint | Two sets with no elements in common

domain (of a function) | (dom(f)) The set of objects for which a (partial) function is defined

domain (of a structure) | (|M|) Non-empty set from which a structure takes assignments and values of variables

eigenvariable | In the sequent calculus, a special constant symbol in a premise of a ∃L or ∀R inference which may not appear in the conclusion. In natural deduction, a special constant symbol in a premise of a ∃Elim or ∀Intro inference which may not appear in the conclusion or any undischarged assumption.

entailment | (Γ ⊨ A) A set of sentences Γ entails a sentence A iff for every structure M with M ⊨ Γ, M ⊨ A

enumeration | A possibly infinite list of all elements of a set A; formally a surjective function f : ℕ → A

equinumerous | A and B are equinumerous iff there is a total bijection from A to B

equivalence relation | A reflexive, symmetric, and transitive relation

extensionality (of satisfaction) | Whether or not a formula A is satisfied depends only on the assignments to the non-logical symbols and free variables that actually occur in A

extensionality (of sets) | Sets A and B are identical, A = B, iff every element of A is also an element of B, and vice versa

finitely satisfiable | Γ is finitely satisfiable iff every finite Γ₀ ⊆ Γ is satisfiable

formula | Expressions of a first-order language ℒ which express relations or properties, or are true or false

free | An occurrence of a variable that is not bound

free for | A term t is free for x in A if none of the free occurrences of x in A occur in the scope of a quantifier that binds a variable in t