Skip to main content
Humanities LibreTexts

2.6: Summary of first order logic

  • Page ID
    16878
  • \( \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}\)

    16. Summary of first order logic

    16.1 Elements of the language

    • Symbolic terms are either names, indefinite names, variables, or arbitrary terms.
      • Names: a, b, c, d, e….
      • Indefinite names: p, q, r….
      • Variables: x, y, z….
      • Arbitrary terms: x, y, z….
    • Each predicate has an arity, which is the number of symbolic terms required by that predicate to form a well-formed formula. The predicates of our language are: F, G, H, I….
    • Each function has an arity, which is the number of symbolic terms required by the function in order for it to form a symbolic term. The functions of our language are: f, g, h, i….
    • There are two quantifiers.
      • , the universal quantifier.
      • , the existential quantifier.
    • The connectives are the same as those of the propositional logic.

    16.2 Syntax of the language

    • An arity n function combined with n symbolic terms is a symbolic term.
    • An arity n predicate combined with n symbolic terms is a well-formed formula.
    • If Φ and Ψ are well-formed formulas, then the following are also well-formed formulas. (And if Φ and Ψ are sentences, then the following are also sentences.)
      • ¬Φ
      • (Φ Ψ)
      • (Φ ^ Ψ)
      • (Φ v Ψ)
      • (Φ Ψ)
    • We write Φ(α) to mean Φ is a well-formed formula in which the symbolic term α appears.
    • If there are no quantifiers in Φ(x) then x is a free variable in Φ. (Names are never described as being free.) If for that formula Φ we write xΦ(x) or ∃xΦ(x), we say that x is now bound in Φ. A variable that is bound is not free.
    • A well-formed formula with no free variables is a sentence.

    16.3 Semantics of the language

    • The semantics of names, predicates, and the quantifiers will remain intuitive for us. Advanced logic (with set theory) is required to make these more precise. We say:
      • The domain of discourse is the collection of objects that our language is about.
      • A name refers to exactly one object from our domain of discourse.
      • A predicate of arity n describes a property or relation of n objects.
      • xΦ(x) means that any object in our domain of discourse has property Φ.
      • xΦ(x) means that at least one object in our domain of discourse has property Φ.
    • If Φ and Ψ are sentences, then the meanings of the connectives are fully given by their truth tables. These semantics-defining truth tables are:
    Φ ¬Φ
    T F
    F T
    Φ Ψ (Φ → Ψ)
    T T T
    T F F
    F T T
    F F T
    Φ Ψ (Φ ^ Ψ)
    T T T
    T F F
    F T F
    F F F
    Φ Ψ (Φ v Ψ)
    T T T
    T F T
    F T T
    F F F
    Φ Ψ (Φ ↔ Ψ)
    T T T
    T F F
    F T F
    F F T
    • Each sentence must be true or false, never both, never neither.
    • A sentence that must be true is logically true. (Sentences of our logic that have the same form as tautologies of the propositional logic we can still call “tautologies”. However, there are some sentences of the first order logic that must be true but that do not have the form of tautologies of the propositional logic. Examples would include x(Fx Fx) and x(Fx v ¬Fx).)
    • A sentence that must be false is a contradictory sentence.
    • A sentence that could be true or could be false is a contingent sentence.
    • Two sentences Φ and Ψ are “equivalent” or “logically equivalent” when (ΦΨ) is a theorem.

    16.4 Reasoning with the Language

    • An argument is an ordered list of sentences, one sentence of which we call the “conclusion” and the others of which we call the “premises”.
    • A valid argument is an argument in which: necessarily, if the premises are true, then the conclusion is true.
    • A sound argument is a valid argument with true premises.
    • Inference rules allow us to write down a sentence that must be true, assuming that certain other sentences must be true. We say that the sentence is derived from those other sentences using the inference rule.
    • Schematically, we can write out the inference rules in the following way (think of these as saying, if you have written down the sentence(s) above the line, then you can write down the sentence below the line; also, the order of the sentences above the line, if there are several, does not matter):
    Modus ponens Modus tollens Double negation Double negation
    (Φ → Ψ)

    Φ

    _____

    Ψ

    (Φ → Ψ)

    ¬Ψ

    _____

    ¬Φ

    Φ

    _____

    ¬¬Φ

    ¬¬Φ

    _____

    Φ

    Addition Addition Modus tollendo ponens Modus tollendo ponens
    Φ

    _____

    (Φ v Ψ)

    Ψ

    _____

    (Φ v Ψ)

    (Φ v Ψ)

    ¬Φ

    _____

    Ψ

    (Φ v Ψ)

    ¬Ψ

    _____

    Φ

    Adjunction Simplification Simplification Bicondition
    Φ

    Ψ

    _____

    (Φ ^ Ψ)

    (Φ ^ Ψ)

    _____

    Φ

    (Φ ^ Ψ)

    _____

    Ψ

    (Φ → Ψ)

    (Ψ → Φ)

    _____

    (Φ ↔ Ψ)

    Equivalence Equivalence Equivalence Equivalence
    (Φ ↔ Ψ)

    Φ

    _____

    Ψ

    (Φ ↔ Ψ)

    Ψ

    _____

    Φ

    (Φ ↔ Ψ)

    ¬Φ

    _____

    ¬Ψ

    (Φ ↔ Ψ)¬Ψ

    _____

    ¬Φ

    Repeat Universal instantiation Existential generalization Existential instantiation
    Φ

    _____

    Φ

    αΦ(α)

    _____

    Φ(β)

    Φ(β)

    _____

    ∃αΦ(α)

    ∃αΦ(α)

    _____

    Φ(χ)

      where β is any symbolic term where β is any symbolic term where χ is an indefinite name that does not appear above in any open proof
    • A proof (or derivation) is a syntactic method for showing an argument is valid. Our system has four kinds of proof (or derivation): direct, conditional, indirect, and universal.
    • A direct proof (or direct derivation) is an ordered list of sentences in which every sentence is either a premise or is derived from earlier lines using an inference rule. The last line of the proof is the conclusion.
    • A conditional proof (or conditional derivation) is an ordered list of sentences in which every sentence is either a premise, is the special assumption for conditional derivation, or is derived from earlier lines using an inference rule. If the assumption for conditional derivation is Φ, and we derive as some step in the proof Ψ, then we can write after this Ψ) as our conclusion.
    • An indirect proof (or indirect derivation, and also known as a reductio ad absurdum) is: an ordered list of sentences in which every sentence is either 1) a premise, 2) the special assumption for indirect derivation (also sometimes called the “assumption for reductio”), or 3) derived from earlier lines using an inference rule. If our assumption for indirect derivation is ¬Φ, and we derive as some step in the proof Ψ and also as some step of our proof ¬Ψ, then we conclude that Φ.
    • A universal proof (or universal derivation) is an ordered list of sentences in which every sentence is either a premise or is derived from earlier lines (not within a completed subproof) using an inference rule. If we are able to prove Φ(x) where x′ does not appear free in any line above the universal derivation, then we conclude that xΦ(x).
    • The schematic form of the direct, conditional, and indirect proof methods remain the same as they were for the propositional logic. We can use Fitch bars to write out this fourth proof schema in the following way:

    \[ \fitchctx{ \boxedsubproof []{\alpha '}{}{ \ellipsesline \\ \pline{\phi (\alpha ')} } \pline{\lall \alpha \phi (\alpha)} } \]

    • A sentence that we can prove without premises is a theorem.

    16.5 Some advice on translations using quantifiers

    Most phrases in English that we want to translate into our first order logic are of the following forms.

    Everything is Φ

    xΦ(x)

    Something is Φ

    xΦ(x)

    Nothing is Φ

    ¬∃xΦ(x)

    Something is not Φ

    x¬Φ(x)

    All Φ are Ψ

    x(Φ(x) Ψ(x))

    Some Φ are Ψ

    x(Φ(x) ^ Ψ(x))

    No Φ are Ψ

    ¬∃x(Φ(x) ^ Ψ(x))

    Some Φ are not Ψ

    x(Φ(x) ^ ¬Ψ(x))

    Only Φ are Ψ

    x(Ψ(x) → Φ(x))

    All and only Φ are Ψ

    x(Φ(x) ↔ Ψ(x))


    This page titled 2.6: Summary of first order logic is shared under a CC BY-NC-SA 4.0 license and was authored, remixed, and/or curated by Craig DeLancey (OpenSUNY) via source content that was edited to the style and standards of the LibreTexts platform.