Documentation

Bookshelf.Enderton.Logic.Chapter_1

Enderton.Logic.Chapter_1 #

Sentential Logic

source
inductive Enderton.Logic.Chapter_1.Wff :
Type

An abstract representation of a well-formed formula as defined by Enderton.

Instances For
    source
    def Enderton.Logic.Chapter_1.Wff.length :
    Enderton.Logic.Chapter_1.Wff → ℕ

    Returns the length of the expression, i.e. a count of all symbols..

    Equations
    Instances For
      source
      theorem Enderton.Logic.Chapter_1.Wff.length_gt_zero (φ : Enderton.Logic.Chapter_1.Wff) :
      Enderton.Logic.Chapter_1.Wff.length φ > 0

      Every Wff has a positive length.

      source
      def Enderton.Logic.Chapter_1.Wff.sentenceSymbolCount :
      Enderton.Logic.Chapter_1.Wff → ℕ

      The number of sentence symbols found in the provided Wff.

      Equations
      Instances For
        source
        def Enderton.Logic.Chapter_1.Wff.sententialSymbolCount :
        Enderton.Logic.Chapter_1.Wff → ℕ

        The number of sentential connective symbols found in the provided Wff.

        Equations
        Instances For
          source
          def Enderton.Logic.Chapter_1.Wff.binarySymbolCount :
          Enderton.Logic.Chapter_1.Wff → ℕ

          The number of binary connective symbols found in the provided Wff.

          Equations
          Instances For
            source
            def Enderton.Logic.Chapter_1.Wff.parenCount :
            Enderton.Logic.Chapter_1.Wff → ℕ

            The number of parentheses found in the provided Wff.

            Equations
            Instances For
              source
              def Enderton.Logic.Chapter_1.Wff.hasNotSymbol :
              Enderton.Logic.Chapter_1.Wff → Prop

              Whether or not the Wff contains a ¬.

              Equations
              Instances For
                source
                theorem Enderton.Logic.Chapter_1.Wff.no_neg_sentential_count_eq_binary_count {φ : Enderton.Logic.Chapter_1.Wff} (h : ¬Enderton.Logic.Chapter_1.Wff.hasNotSymbol φ) :
                Enderton.Logic.Chapter_1.Wff.sententialSymbolCount φ = Enderton.Logic.Chapter_1.Wff.binarySymbolCount φ

                If a Wff does not contain the ¬ symbol, it has the same number of sentential connective symbols as it does binary connective symbols. In other words, the negation symbol is the only non-binary sentential connective.

                source
                theorem Enderton.Logic.Chapter_1.Wff.paren_count_double_sentential_count (φ : Enderton.Logic.Chapter_1.Wff) :
                Enderton.Logic.Chapter_1.Wff.parenCount φ = 2 * Enderton.Logic.Chapter_1.Wff.sententialSymbolCount φ

                Parentheses Count #

                Let φ be a well-formed formula and c be the number of places at which a sentential connective symbol exists. Then there is 2c parentheses in φ.

                source
                theorem Enderton.Logic.Chapter_1.Wff.length_eq_sum_symbol_count (φ : Enderton.Logic.Chapter_1.Wff) :
                Enderton.Logic.Chapter_1.Wff.length φ = Enderton.Logic.Chapter_1.Wff.sentenceSymbolCount φ + Enderton.Logic.Chapter_1.Wff.sententialSymbolCount φ + Enderton.Logic.Chapter_1.Wff.parenCount φ

                The length of a Wff corresponds to the summation of sentence symbols, sentential connective symbols, and parentheses.

                Exercise 1.1.2 #

                Show that there are no wffs of length 2, 3, or 6, but that any other positive length is possible.

                source
                theorem Enderton.Logic.Chapter_1.exercise_1_1_2_i (φ : Enderton.Logic.Chapter_1.Wff) :
                Enderton.Logic.Chapter_1.Wff.length φ ≠ 2 ∧ Enderton.Logic.Chapter_1.Wff.length φ ≠ 3 ∧ Enderton.Logic.Chapter_1.Wff.length φ ≠ 6
                source
                theorem Enderton.Logic.Chapter_1.exercise_1_1_2_ii (n : ℕ) (hn : n ≠ 2 ∧ n ≠ 3 ∧ n ≠ 6) :
                ∃ (φ : Enderton.Logic.Chapter_1.Wff), Enderton.Logic.Chapter_1.Wff.length φ = n
                source
                theorem Enderton.Logic.Chapter_1.exercise_1_1_3 (φ : Enderton.Logic.Chapter_1.Wff) :
                Enderton.Logic.Chapter_1.Wff.sentenceSymbolCount φ = Enderton.Logic.Chapter_1.Wff.binarySymbolCount φ + 1

                Exercise 1.1.3 #

                Let α be a wff; let c be the number of places at which binary connective symbols (∧, ∨, →, ↔) occur in α; let s be the number of places at which sentence symbols occur in α. (For example, if α is (A → (¬ A)) then c = 1 and s = 2.) Show by using the induction principle that s = c + 1.

                source
                theorem Enderton.Logic.Chapter_1.exercise_1_1_5a (α : Enderton.Logic.Chapter_1.Wff) (hα : ¬Enderton.Logic.Chapter_1.Wff.hasNotSymbol α) :
                Odd (Enderton.Logic.Chapter_1.Wff.length α)

                Exercise 1.1.5 (a) #

                Suppose that α is a wff not containing the negation symbol ¬. Show that the length of α (i.e., the number of symbols in the string) is odd.

                Suggestion: Apply induction to show that the length is of the form 4k + 1.

                source
                theorem Enderton.Logic.Chapter_1.exercise_1_1_5b (α : Enderton.Logic.Chapter_1.Wff) (hα : ¬Enderton.Logic.Chapter_1.Wff.hasNotSymbol α) :
                ↑(Enderton.Logic.Chapter_1.Wff.sentenceSymbolCount α) > ↑(Enderton.Logic.Chapter_1.Wff.length α) / 4

                Exercise 1.1.5 (b) #

                Suppose that α is a wff not containing the negation symbol ¬. Show that more than a quarter of the symbols are sentence symbols.

                Suggestion: Apply induction to show that the number of sentence symbols is k + 1.

                Exercise 1.2.1 #

                Show that neither of the following two formulas tautologically implies the other:

                (A ↔ (B ↔ C))
((A ∧ (B ∧ C)) ∨ ((¬ A) ∧ ((¬ B) ∧ (¬ C)))).

                Suggestion: Only two truth assignments are needed, not eight.

                source
                theorem Enderton.Logic.Chapter_1.exercise_1_2_1_i :
                Enderton.Logic.Chapter_1.f₁ True False False ≠ Enderton.Logic.Chapter_1.f₂ True False False
                source
                theorem Enderton.Logic.Chapter_1.exercise_1_2_1_ii :
                Enderton.Logic.Chapter_1.f₁ False False False ≠ Enderton.Logic.Chapter_1.f₂ False False False
                source
                theorem Enderton.Logic.Chapter_1.exercise_1_2_2a (P : Prop) (Q : Prop) :
                ((P → Q) → P) → P

                Exercise 1.2.2 (a) #

                Is (((P → Q) → P) → P) a tautology?

                Exercise 1.2.2 (b) #

                Define σₖ recursively as follows: σ₀ = (P → Q) and σₖ₊₁ = (σₖ → P). For which values of k is σₖ a tautology? (Part (a) corresponds to k = 2.)

                source
                theorem Enderton.Logic.Chapter_1.exercise_1_2_2b_i (P : Prop) (Q : Prop) {k : ℕ} (h : k > 0) :
                Enderton.Logic.Chapter_1.σ P Q (2 * k)
                source
                theorem Enderton.Logic.Chapter_1.exercise_1_2_2b_ii :
                ¬Enderton.Logic.Chapter_1.σ True False 0
                source
                theorem Enderton.Logic.Chapter_1.exercise_1_2_2b_iii {Q : Prop} {k : ℕ} (h : Odd k) :
                ¬Enderton.Logic.Chapter_1.σ False Q k
                source
                theorem Enderton.Logic.Chapter_1.exercise_1_2_3a (P : Prop) (Q : Prop) :
                (P → Q) ∨ (Q → P)

                Exercise 1.2.3 (a) #

                Determine whether or not ((P → Q)) ∨ (Q → P) is a tautology.

                source
                theorem Enderton.Logic.Chapter_1.exercise_1_2_3b (P : Prop) (Q : Prop) (R : Prop) :
                P ∧ Q → R ↔ (P → R) ∨ (Q → R)

                Exercise 1.2.3 (b) #

                Determine whether or not ((P ∧ Q) → R)) tautologically implies ((P → R) ∨ (Q → R)).

                Exercise 1.2.5 #

                Prove or refute each of the following assertions:

                (a) If either Σ ⊨ α or Σ ⊨ β, then Σ ⊨ (α ∨ β). (b) If Σ ⊨ (α ∨ β), then either Σ ⊨ α or Σ ⊨ β.

                source
                theorem Enderton.Logic.Chapter_1.exercise_1_2_5a (P : Prop) (α : Prop) (β : Prop) :
                (P → α) ∨ (P → β) → P → α ∨ β
                source
                theorem Enderton.Logic.Chapter_1.exercise_1_2_6b :
                (False ∨ True) ∧ ¬False

                Exercise 1.2.15 #

                Of the following three formulas, which tautologically implies which? (a) (A ↔ B) (b) (¬((A → B) →(¬(B → A)))) (c) (((¬ A) ∨ B) ∧ (A ∨ (¬ B)))

                source
                theorem Enderton.Logic.Chapter_1.exercise_1_2_15_i (A : Prop) (B : Prop) :
                (A ↔ B) ↔ ¬((A → B) → ¬(B → A))
                source
                theorem Enderton.Logic.Chapter_1.exercise_1_2_15_ii (A : Prop) (B : Prop) :
                (A ↔ B) ↔ (¬A ∨ B) ∧ (A ∨ ¬B)