# Creative Commons Attribution-Share Alike 3.0 Unported (http://creativecommons.org/licenses/by-sa/3.0/) # {{header # | title = First-order logic # | subtitle = # | left = # | right = # | shortcut = # | notes = This interface collects important theorems from first-order logic, which builds on [[Interface:Classical propositional calculus|propositional logic]] by adding quantifiers ("for all" and "there exists") and equality. It is meant as a user-friendly reservoir for those interfaces and proof modules which merely use first-order logic, without proving anything new within it. It does not include results which rely on the [[Interface:Axiom of quantifiability]]; many modules may wish to import [[Interface:First-order logic with quantifiability]] instead of this interface. # # Statements can be added if necessary, but then the exporting modules have to be updated accordingly. # }} # {{modules # | parameters = [[Interface:Classical propositional calculus]] # | importedby = [[First-order logic with quantifiability]] # | exportedby = [[First-order logic]] # }} # == Formulas, objects, and quantification == # We build on [[Interface:Classical propositional calculus]]: param (CLASSICAL Classical_propositional_calculus.ghi () "") # # By convention we use φ, ψ, χ, and θ to represent formulas: tvar (formula φ ψ χ θ) # # We also define some variables which suggest which variables are likely to occur in a formula. For example, `φx` is likely to include the variable `x` (of course, it is the distinct variable constraints which really specify what variables are allowed). This is similar in intent to the notation `φ(x)` which is sometimes used in treatments of predicate logic. tvar (formula φx φy ψy) # # We use the term ''object'' to refer to something which is subject to quantification or equality. From an axiomatic point of view, what is a valid object is defined implicitly, by axioms such as those of [[w:Zermelo-Fraenkel set theory|ZFC set theory]] or [[w:Peano axioms|Peano arithmetic]]. # kind (object) tvar (object s t u s0 s1 t0 t1) # # A ''variable'' is something we can quantify over. # var (object x y z x0 x1 y0 y1) # # We extend the available formulas with [[w:Universal quantification|universal quantification]] and [[w:Existential quantification|existential quantification]]: term (formula (∀ x φ)) term (formula (∃ x φ)) # # === Order of operations === # In informal discussion, we omit some parentheses, building on the [[w:Order of operations|precedence]] from [[Interface:Classical propositional calculus]]. The precedence, from tightest to loosest, is: # # * = # * ∀, ∃ # * ¬ # * ∧ # * ∨ # * →, ↔ # # For example, `∀ z x = y ∨ ¬ x = y` means `(∀ z (x = y)) ∨ (¬ (x = y))`. We do not supply a precedence for `value` because we simply omit it in informal discussion. # # == Relationship between universal and existential quantification == # stmt (NotForAll () () (↔ (¬ (∀ x φ)) (∃ x (¬ φ)))) stmt (NotThereExists () () (↔ (¬ (∃ x φ)) (∀ x (¬ φ)))) # # == Builders for quantifiers == # As with propositional calculus, we need to build up formulas explicitly, and these rules let us do it. We provide them for both quantifiers, for implication and the biconditional. stmt (addForAll () ((→ φ ψ)) (→ (∀ x φ) (∀ x ψ))) stmt (addThereExists () ((→ φ ψ)) (→ (∃ x φ) (∃ x ψ))) stmt (buildForAll () ((↔ φ ψ)) (↔ (∀ x φ) (∀ x ψ))) stmt (buildThereExists () ((↔ φ ψ)) (↔ (∃ x φ) (∃ x ψ))) # # === Additional builders === # Some of these builders rely on theorems we haven't presented yet, but they are similar to the simple ones above in terms of general intent. stmt (buildThereExistsInConsequent ((φ x)) ((→ φ (↔ ψ χ))) (→ φ (↔ (∃ x ψ) (∃ x χ)))) stmt (buildForAllInConsequent ((φ x)) ((→ φ (↔ ψ χ))) (→ φ (↔ (∀ x ψ) (∀ x χ)))) # # == Order == # The order of adjacent quantifiers of the same type can be exchanged: stmt (ForAllCommutation () () (↔ (∀ x (∀ y φ)) (∀ y (∀ x φ)))) stmt (ThereExistsCommutation () () (↔ (∃ x (∃ y φ)) (∃ y (∃ x φ)))) # # ∃ followed by ∀ can be switched, stmt (ThereExistsForAllCommutation () () (→ (∃ x (∀ y φ)) (∀ y (∃ x φ)))) # # but the converse does not in general hold. # # == Combining quantified statements == # Quantifiers of the same variable can sometimes be combined or split: stmt (ForAllConjunction () () (↔ (∀ x (∧ φ ψ)) (∧ (∀ x φ) (∀ x ψ)))) stmt (ThereExistsDisjunction () () (↔ (∃ x (∨ φ ψ)) (∨ (∃ x φ) (∃ x ψ)))) stmt (ThereExistsImplication () () (↔ (∃ x (→ φ ψ)) (→ (∀ x φ) (∃ x ψ)))) stmt (ForAllImplication () () (→ (∀ x (→ φ ψ)) (→ (∀ x φ) (∀ x ψ)))) stmt (ThereExistsConjunction () () (→ (∃ x (∧ φ ψ)) (∧ (∃ x φ) (∃ x ψ)))) # # === Biconditional === stmt (ForAllBiconditional () () (→ (∀ x (↔ φ ψ)) (↔ (∀ x φ) (∀ x ψ)))) # # === Other kinds of splits and combinations === stmt (ForAllImplicationThereExists () () (→ (∀ x (→ φ ψ)) (→ (∃ x φ) (∃ x ψ)))) stmt (ForAllBiconditionalThereExists () () (→ (∀ x (↔ φ ψ)) (↔ (∃ x φ) (∃ x ψ)))) stmt (ThereExistsConjunctionCombining () () (→ (∧ (∀ x φ) (∃ x ψ)) (∃ x (∧ φ ψ)))) stmt (ThereExistsConjunctionRightCombining () () (→ (∧ (∃ x φ) (∀ x ψ)) (∃ x (∧ φ ψ)))) stmt (combineThereExistsForAll () ((∃ x φ) (∀ x ψ)) (∃ x (∧ φ ψ))) # # == Generalization and specialization == # We can remove a universal quantifier: stmt (Specialization () () (→ (∀ x φ) φ)) stmt (specialize () ((∀ x φ)) φ) # # The converse is sometimes possible, but only with some restrictions. Either the variable does not occur in the formula, or the formula is unconditionally true: stmt (Generalization ((φ x)) () (→ φ (∀ x φ))) stmt (generalize () (φ) (∀ x φ)) # # An existential quantifier can be added unconditionally, stmt (ThereExistsIntroduction () () (→ φ (∃ x φ))) # # and can be removed if the variable does not occur in the formula. stmt (NullThereExists ((φ x)) () (↔ (∃ x φ) φ)) stmt (removeThereExists ((φ x)) ((∃ x φ)) φ) tvar (formula antecedent) stmt (removeThereExistsInConsequent ((φ x)) ((→ antecedent (∃ x φ))) (→ antecedent φ)) # # == Equality == # At least for now, we just define equality between terms here (rather than trying to separate equality between terms and equality between variables). # # Equality is reflexive, symmetry, and transitive. term (formula (= s t)) stmt (EqualityReflexivity () () (= s s)) stmt (EqualitySymmetry () () (↔ (= s t) (= t s))) stmt (swapEquality () ((= s t)) (= t s)) stmt (EqualityTransitivity () () (→ (∧ (= s t) (= t u)) (= s u))) stmt (applyEqualityTransitivity () ((= s t) (= t u)) (= s u)) # # To say that two terms are not equal, we simply use `(¬ (= s t))`. Ghilbert then typesets that as `s ≠ t`. # # == Free variables == # Metamath has `φ → ∀ x φ` as a way to say that a variable is not free in a formula, but we rely instead on the free variable features built in to ghilbert. # === Adding or removing quantifiers === # If a variable is not free in a formula, it is legitimate to add or remove quantifiers from that formula: stmt (ForAllAddRemove ((φ x)) () (↔ (∀ x φ) φ)) stmt (ThereExistsAddRemove ((φ x)) () (↔ (∃ x φ) φ)) # # === Moving formulas in and out of quantification === # The results in this section all have to do with being able to move around formulas relative to quantifiers, given that the quantified variable is not free in the formula being moved. # stmt (ForAllImplicationConsequentMovement ((ψ x)) () (↔ (∀ x (→ φ ψ)) (→ (∃ x φ) ψ))) stmt (ThereExistsConjunctionMovement ((φ x)) () (↔ (∃ x (∧ φ ψ)) (∧ φ (∃ x ψ)))) stmt (ThereExistsConjunctionRightMovement ((ψ x)) () (↔ (∃ x (∧ φ ψ)) (∧ (∃ x φ) ψ))) stmt (ThereExistsDisjunctionMovement ((φ x)) () (↔ (∃ x (∨ φ ψ)) (∨ φ (∃ x ψ)))) stmt (ThereExistsDisjunctionRightMovement ((ψ x)) () (↔ (∃ x (∨ φ ψ)) (∨ (∃ x φ) ψ)) ) stmt (ThereExistsAntecedentMovement ((φ x)) () (↔ (∃ x (→ φ ψ)) (→ φ (∃ x ψ)))) # # Here are a few rules based on these: stmt (moveLeftConjunctIntoThereExistsInConsequent ((φ x)) ((→ antecedent (∧ φ (∃ x ψ)))) (→ antecedent (∃ x (∧ φ ψ)))) stmt (moveRightConjunctIntoThereExistsInConsequent ((ψ x)) ((→ antecedent (∧ (∃ x φ) ψ))) (→ antecedent (∃ x (∧ φ ψ)))) stmt (repeatAntecedentThereExists ((antecedent x)) ((→ antecedent (∃ x ψ))) (→ antecedent (∃ x (∧ antecedent ψ)))) # # ==== Scattering and gathering ==== # If we have two formulas joined by a conjunction, one quantified over one variable and the other quantified over another, we can express the quantifiers either at the beginning or with the formulas they apply to.[http://us.metamath.org/mpeuni/eeanv.html eeanv], metamath's set.mm, accessed August 8, 2010 We refer to this process as gathering (that is, gathering the quantifiers together at the start of the formula) or scattering (the opposite). stmt (ThereExistsScattering ((φx y) (ψy x)) () (↔ (∃ x (∃ y (∧ φx ψy))) (∧ (∃ x φx) (∃ y ψy)))) stmt (gatherThereExistsInConsequent ((φx y) (ψy x)) ((→ antecedent (∧ (∃ x φx) (∃ y ψy)))) (→ antecedent (∃ x (∃ y (∧ φx ψy))))) # # ==== Adding quantifiers to theorems which are implications ==== # # These variants on moving formulas turn out to be used particularly often: stmt (addThereExistsToAntecedent ((ψ x)) ((→ φ ψ)) (→ (∃ x φ) ψ)) stmt (addForAllToConsequent ((φ x)) ((→ φ ψ)) (→ φ (∀ x ψ))) # # === Changing the quantified variable === # We can transform a quantified formula by substituting each of the occurences of the variable we are quantifying over to another variable, and changing the variable in the quantifier accordingly. Here is a version with implicit substitution. stmt (ChangeVariableThereExists ((φx y) (φy x) ) ((→ (= x y) (↔ φx φy))) (↔ (∃ x φx) (∃ y φy))) stmt (ChangeVariableForAll ((φx y) (φy x) ) ((→ (= x y) (↔ φx φy))) (↔ (∀ x φx) (∀ y φy))) # # === Other theorems related to substitution === stmt (equs3 () () (↔ (∃ x (∧ (= x s) φ)) (¬ (∀ x (→ (= x s) (¬ φ)))))) stmt (VariableSubstitution () () (→ (= x y) (→ φ (∀ x (→ (= x y) φ)))) ) # # == References == # # # [[Category:Classical first-order logic|{{PAGENAME}}]]