Skip to main content
Humanities LibreTexts

Glossary

  • Page ID
    121614
  • \( \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

    Image Caption Link Source
    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 An 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 A2; 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 : AB) A mapping of each element of a domain (of a function) A to an element of the codomain B function.png   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 Rf A × B defined by Rf = {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-1(y) = whatever unique x A is such that f(x) = y     https://eng.libretexts.org/Under_Con...s_of_Functions  
    composition (gf) The function resulting from “chaining together” f and g; (g f)(x) = g(f(x)) composition.png   https://eng.libretexts.org/Under_Con...n_of_Functions  
    partial function (f : AB) 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') injective.png   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 surjective.png   https://eng.libretexts.org/Under_Con...s_of_Functions  
    bijection A function that is both surjective and injective bijective.png   https://eng.libretexts.org/Under_Con...s_of_Functions  
    intersection (AB) The set of all things which are elements of both A and B: A B = {x : x A x B} intersection.png   https://eng.libretexts.org/Under_Con...g:intersection  
    union (AB) The set of all elements of A and B together: A B = {x : x A x B} union.png   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} difference.png   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 Γ0 ⇒   with Γ0Γ. 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 Γ0A where Γ0Γ 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]2). 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 Γ0 Γ 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 Me 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        
    • Was this article helpful?