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\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} } }\)
\(\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} } }\)
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 |
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 : 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 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 | (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 Γ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 Γ0 ⇒ A 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 |